---

Step * 1 of Lemma mul-monomials-req


1. m5 : ℤ-o
2. m6 : {vs:ℤ List| sorted(vs)} 
3. m3 : ℤ-o
4. m4 : {vs:ℤ List| sorted(vs)} 
⊢ imonomial-term(<m5 * m3, merge-int-accum(m6;m4)>) ≡ imonomial-term(<m5, m6>) (*) imonomial-term(<m3, m4>)
BY
{ ((D 0 THEN Auto) THEN RepUR ``real_term_value`` 0 THEN Fold `real_term_value` 0) }

1
1. m5 : ℤ-o
2. m6 : {vs:ℤ List| sorted(vs)} 
3. m3 : ℤ-o
4. m4 : {vs:ℤ List| sorted(vs)} 
5. f : ℤ ⟶ ℝ
⊢ real_term_value(f;imonomial-term(<m5 * m3, merge-int-accum(m6;m4)>)) = (real_term_value(f;imonomial-term(<m5, m6>)) * \000Creal_term_value(f;imonomial-term(<m3, m4>)))

---

Latex:

---

Latex:

1.  m5  :  \mBbbZ{}\msupminus{}\msupzero{}
2.  m6  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
3.  m3  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  m4  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
\mvdash{}  imonomial-term(<m5  *  m3,  merge-int-accum(m6;m4)>)  \mequiv{}  imonomial-term(<m5,  m6>)  (*)  imonomial-term(<m\000C3,  m4>)


By

---

Latex:
((D  0  THEN  Auto)  THEN  RepUR  ``real\_term\_value``  0  THEN  Fold  `real\_term\_value`  0)

---

Home Index