---

Step * 1 1 of Lemma mul-monomials-equiv


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>))) ∈ ℤ
BY
{ ((RWO "imonomial-term-linear" 0 THENA Auto)
   THEN Assert ⌜int_term_value(f;imonomial-term(<1, merge-int(m6;m4)>)) = (int_term_value(f;imonomial-term(<1, m6>)) * i\000Cnt_term_value(f;imonomial-term(<1, m4>))) ∈ ℤ⌝⋅
   ) }

1
.....assertion..... 
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(<1, merge-int(m6;m4)>)) = (int_term_value(f;imonomial-term(<1, m6>)) * int_term_value(\000Cf;imonomial-term(<1, m4>))) ∈ ℤ

2
1. m5 : ℤ-o
2. m6 : {vs:ℤ List| sorted(vs)} 
3. m3 : ℤ-o
4. m4 : {vs:ℤ List| sorted(vs)} 
5. f : ℤ ⟶ ℤ
6. int_term_value(f;imonomial-term(<1, merge-int(m6;m4)>)) = (int_term_value(f;imonomial-term(<1, m6>)) * int_term_value\000C(f;imonomial-term(<1, m4>))) ∈ ℤ
⊢ ((m5 * m3) * int_term_value(f;imonomial-term(<1, merge-int(m6;m4)>))) = ((m5 * int_term_value(f;imonomial-term(<1, m6>\000C))) * m3 * int_term_value(f;imonomial-term(<1, 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)\} 
5.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  int\_term\_value(f;imonomial-term(<m5  *  m3,  merge-int(m6;m4)>))  =  (int\_term\_value(f;imonomial-term(<\000Cm5,  m6>))  *  int\_term\_value(f;imonomial-term(<m3,  m4>)))


By

---

Latex:
((RWO  "imonomial-term-linear"  0  THENA  Auto)
  THEN  Assert  \mkleeneopen{}int\_term\_value(f;imonomial-term(ə,  merge-int(m6;m4)>))  =  (int\_term\_value(f;imonomial-\000Cterm(ə,  m6>))  *  int\_term\_value(f;imonomial-term(ə,  m4>)))\mkleeneclose{}\mcdot{}
  )

---

Home Index