---

Step * 1 1 2 of Lemma mul-monomials-req


1. m5 : ℤ-o
2. m6 : {vs:ℤ List| sorted(vs)} 
3. m3 : ℤ-o
4. m4 : {vs:ℤ List| sorted(vs)} 
5. f : ℤ ⟶ ℝ
6. real_term_value(f;imonomial-term(<1, merge-int(m6;m4)>)) = (real_term_value(f;imonomial-term(<1, m6>)) * real_term_va\000Clue(f;imonomial-term(<1, m4>)))
⊢ (r(m5 * m3) * real_term_value(f;imonomial-term(<1, merge-int-accum(m6;m4)>))) = ((r(m5) * real_term_value(f;imonomial-\000Cterm(<1, m6>))) * r(m3) * real_term_value(f;imonomial-term(<1, m4>)))
BY
{ Subst' merge-int-accum(m6;m4) ~ merge-int(m6;m4) 0 }

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

2
1. m5 : ℤ-o
2. m6 : {vs:ℤ List| sorted(vs)} 
3. m3 : ℤ-o
4. m4 : {vs:ℤ List| sorted(vs)} 
5. f : ℤ ⟶ ℝ
6. real_term_value(f;imonomial-term(<1, merge-int(m6;m4)>)) = (real_term_value(f;imonomial-term(<1, m6>)) * real_term_va\000Clue(f;imonomial-term(<1, m4>)))
⊢ (r(m5 * m3) * real_term_value(f;imonomial-term(<1, merge-int(m6;m4)>))) = ((r(m5) * real_term_value(f;imonomial-term(<\000C1, m6>))) * r(m3) * real_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{}  \mBbbR{}
6.  real\_term\_value(f;imonomial-term(ə,  merge-int(m6;m4)>))  =  (real\_term\_value(f;imonomial-term(ə,  \000Cm6>))  *  real\_term\_value(f;imonomial-term(ə,  m4>)))
\mvdash{}  (r(m5  *  m3)  *  real\_term\_value(f;imonomial-term(ə,  merge-int-accum(m6;m4)>)))
=  ((r(m5)  *  real\_term\_value(f;imonomial-term(ə,  m6>)))  *  r(m3)  *  real\_term\_value(f;imonomial-term(<\000C1,  m4>)))


By

---

Latex:
Subst'  merge-int-accum(m6;m4)  \msim{}  merge-int(m6;m4)  0

---

Home Index