---

Step * 1 of Lemma mul-monomials-equiv


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

1
1. m5 : ℤ-o
2. m6 : {vs:ℤ List| sorted(vs)} 
3. m3 : ℤ-o
4. m4 : {vs:ℤ List| sorted(vs)} 
5. f : ℤ ⟶ ℤ
⊢ int_term_value(f;imonomial-term(<m5 * m3, merge-int(m6;m4)>)) = (int_term_value(f;imonomial-term(<m5, m6>)) * int_term\000C_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(m6;m4)>)  \mequiv{}  imonomial-term(<m5,  m6>)  (*)  imonomial-term(<m3,  m4>\000C)


By

---

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

---

Home Index