---

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


1. f : ℤ ⟶ ℝ
2. u : ℤ
3. v : ℤ List
4. ∀as:ℤ List. (real_term_value(f;imonomial-term(<1, merge-int(as;v)>)) = (real_term_value(f;imonomial-term(<1, as>)) * \000Creal_term_value(f;imonomial-term(<1, v>))))
⊢ ∀as:ℤ List. (real_term_value(f;imonomial-term(<1, merge-int(as;[u / v])>)) = (real_term_value(f;imonomial-term(<1, as>\000C)) * real_term_value(f;imonomial-term(<1, [u / v]>))))
BY
{ (Unfold `merge-int` 0
   THEN Reduce 0
   THEN Fold `merge-int` 0
   THEN (ParallelLast THENA Auto)
   THEN (RWO "imonomial-term-linear-req" 0 THENA Auto)) }

1
1. f : ℤ ⟶ ℝ
2. u : ℤ
3. v : ℤ List
4. ∀as:ℤ List. (real_term_value(f;imonomial-term(<1, merge-int(as;v)>)) = (real_term_value(f;imonomial-term(<1, as>)) * \000Creal_term_value(f;imonomial-term(<1, v>))))
5. as : ℤ List
6. real_term_value(f;imonomial-term(<1, merge-int(as;v)>)) = (real_term_value(f;imonomial-term(<1, as>)) * real_term_val\000Cue(f;imonomial-term(<1, v>)))
⊢ (r1 * real_term_value(f;imonomial-term(<1, insert-int(u;merge-int(as;v))>))) = ((r1 * real_term_value(f;imonomial-term\000C(<1, as>))) * r1 * real_term_value(f;imonomial-term(<1, [u / v]>)))

---

Latex:

---

Latex:

1.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
2.  u  :  \mBbbZ{}
3.  v  :  \mBbbZ{}  List
4.  \mforall{}as:\mBbbZ{}  List.  (real\_term\_value(f;imonomial-term(ə,  merge-int(as;v)>))  =  (real\_term\_value(f;imonomi\000Cal-term(ə,  as>))  *  real\_term\_value(f;imonomial-term(ə,  v>))))
\mvdash{}  \mforall{}as:\mBbbZ{}  List.  (real\_term\_value(f;imonomial-term(ə,  merge-int(as;[u  /  v])>))  =  (real\_term\_value(f;im\000Conomial-term(ə,  as>))  *  real\_term\_value(f;imonomial-term(ə,  [u  /  v]>))))


By

---

Latex:
(Unfold  `merge-int`  0
  THEN  Reduce  0
  THEN  Fold  `merge-int`  0
  THEN  (ParallelLast  THENA  Auto)
  THEN  (RWO  "imonomial-term-linear-req"  0  THENA  Auto))

---

Home Index