---

Step * 1 1 1 1 1 of Lemma mul-monomials-equiv


1. f : ℤ ⟶ ℤ
⊢ ∀as:ℤ List. (int_term_value(f;imonomial-term(<1, merge-int(as;[])>)) = (int_term_value(f;imonomial-term(<1, as>)) * in\000Ct_term_value(f;imonomial-term(<1, []>))) ∈ ℤ)
BY
{ ((Unfold `merge-int` 0 THEN Reduce  0 THEN Auto) THEN (GenConclTerm ⌜int_term_value(f;imonomial-term(<1, as>))⌝⋅ THENA\000C Auto)) }

1
1. f : ℤ ⟶ ℤ
2. as : ℤ List
3. v : ℤ
4. int_term_value(f;imonomial-term(<1, as>)) = v ∈ ℤ
⊢ v = (v * int_term_value(f;imonomial-term(<1, []>))) ∈ ℤ

---

Latex:

---

Latex:

1.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  \mforall{}as:\mBbbZ{}  List.  (int\_term\_value(f;imonomial-term(ə,  merge-int(as;[])>))  =  (int\_term\_value(f;imonomial\000C-term(ə,  as>))  *  int\_term\_value(f;imonomial-term(ə,  []>))))


By

---

Latex:
((Unfold  `merge-int`  0  THEN  Reduce    0  THEN  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}int\_term\_value(f;imonomial-term(ə,  as>))\mkleeneclose{}\mcdot{}  THENA  Auto)
  )

---

Home Index