---

Step * 1 1 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 : ℤ ⟶ ℝ
⊢ 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>)))
BY
{ ((RWO "imonomial-term-linear-req" 0 THENA Auto)
   THEN Assert ⌜real_term_value(f;imonomial-term(<1, merge-int(m6;m4)>)) = (real_term_value(f;imonomial-term(<1, m6>)) *\000C real_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 : ℤ ⟶ ℝ
⊢ real_term_value(f;imonomial-term(<1, merge-int(m6;m4)>)) = (real_term_value(f;imonomial-term(<1, m6>)) * real_term_val\000Cue(f;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. 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>)))

---

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{}
\mvdash{}  real\_term\_value(f;imonomial-term(<m5  *  m3,  merge-int-accum(m6;m4)>))  =  (real\_term\_value(f;imonomia\000Cl-term(<m5,  m6>))  *  real\_term\_value(f;imonomial-term(<m3,  m4>)))


By

---

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

---

Home Index