---

Step * of Lemma ipolynomial-term-cons-value

∀[m:iMonomial()]. ∀[p:iMonomial() List].
  ∀f:ℤ ⟶ ℤ
    (int_term_value(f;ipolynomial-term([m / p]))
    = (int_term_value(f;imonomial-term(m)) + int_term_value(f;ipolynomial-term(p)))
    ∈ ℤ)
BY
{ (InstLemma `ipolynomial-term-cons` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN (D 3 With ⌜f⌝  THENA Auto)
   THEN HypSubst' (-1) 0
   THEN (Unfold `int_term_value` 0 THEN Reduce 0)
   THEN Fold `int_term_value` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[m:iMonomial()].  \mforall{}[p:iMonomial()  List].
    \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
        (int\_term\_value(f;ipolynomial-term([m  /  p]))
        =  (int\_term\_value(f;imonomial-term(m))  +  int\_term\_value(f;ipolynomial-term(p))))


By

---

Latex:
(InstLemma  `ipolynomial-term-cons`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  (D  3  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  (Unfold  `int\_term\_value`  0  THEN  Reduce  0)
  THEN  Fold  `int\_term\_value`  0
  THEN  Auto)

---

Home Index