---

Step * of Lemma imonomial-term-add

∀vs:ℤ List. ∀a,b:ℤ-o. ∀f:ℤ ⟶ ℤ.  ((int_term_value(f;imonomial-term(<a, vs>)) + int_term_value(f;imonomial-term(<b, vs>)\000C)) = int_term_value(f;imonomial-term(<a + b, vs>)) ∈ ℤ)
BY
{ (Auto THEN RWO "imonomial-term-linear" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}vs:\mBbbZ{}  List.  \mforall{}a,b:\mBbbZ{}\msupminus{}\msupzero{}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.
    ((int\_term\_value(f;imonomial-term(<a,  vs>))  +  int\_term\_value(f;imonomial-term(<b,  vs>)))  =  int\_ter\000Cm\_value(f;imonomial-term(<a  +  b,  vs>)))


By

---

Latex:
(Auto  THEN  RWO  "imonomial-term-linear"  0  THEN  Auto)

---

Home Index