---

Step * 1 of Lemma real-term-nonneg


1. t : int_term()
2. ↑nonneg-poly(int_term_to_ipoly(t))
3. f : ℤ ⟶ ℝ
4. r0 ≤ real_term_value(f;ipolynomial-term(int_term_to_ipoly(t)))
⊢ r0 ≤ real_term_value(f;t)
BY
{ ((InstLemma `real_term_polynomial` [⌜t⌝]⋅ THENA Auto) THEN D -1 With ⌜f⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  t  :  int\_term()
2.  \muparrow{}nonneg-poly(int\_term\_to\_ipoly(t))
3.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
4.  r0  \mleq{}  real\_term\_value(f;ipolynomial-term(int\_term\_to\_ipoly(t)))
\mvdash{}  r0  \mleq{}  real\_term\_value(f;t)


By

---

Latex:
((InstLemma  `real\_term\_polynomial`  [\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1  With  \mkleeneopen{}f\mkleeneclose{}    THEN  Auto)

---

Home Index