---

Step * of Lemma imonomial-cons-req

∀v:ℤ List. ∀u,a:ℤ. ∀f:ℤ ⟶ ℝ.  (real_term_value(f;imonomial-term(<a, [u / v]>)) = ((f u) * real_term_value(f;imonomial-t\000Cerm(<a, v>))))
BY
{ ((Auto THEN (RWO "imonomial-term-linear-req" 0 THENA Auto))
   THEN (Assert  ⌜real_term_value(f;imonomial-term(<1, [u / v]>)) = ((f u) * real_term_value(f;imonomial-term(<1, v>)))⌝\000C⋅ THENM (RWO "-1" 0 THEN Auto))
   ) }

1
.....assertion..... 
1. v : ℤ List
2. u : ℤ
3. a : ℤ
4. f : ℤ ⟶ ℝ
⊢ real_term_value(f;imonomial-term(<1, [u / v]>)) = ((f u) * real_term_value(f;imonomial-term(<1, v>)))

---

Latex:

---

Latex:
\mforall{}v:\mBbbZ{}  List.  \mforall{}u,a:\mBbbZ{}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}.    (real\_term\_value(f;imonomial-term(<a,  [u  /  v]>))  =  ((f  u)  *  real\_term\000C\_value(f;imonomial-term(<a,  v>))))


By

---

Latex:
((Auto  THEN  (RWO  "imonomial-term-linear-req"  0  THENA  Auto))
  THEN  (Assert    \mkleeneopen{}real\_term\_value(f;imonomial-term(ə,  [u  /  v]>))  =  ((f  u)  *  real\_term\_value(f;imonomi\000Cal-term(ə,  v>)))\mkleeneclose{}\mcdot{}  THENM  (RWO  "-1"  0  THEN  Auto))
  )

---

Home Index