---

Step * 1 2 of Lemma real_term_polynomial


1. const : ℤ
2. ¬(const = 0 ∈ ℤ)
⊢ ipolynomial-term([<const, []>]) ≡ "const"
BY
{ (RepUR ``ipolynomial-term imonomial-term`` 0 THEN ((D 0 THEN Auto) THEN RepUR ``int_term_value`` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  const  :  \mBbbZ{}
2.  \mneg{}(const  =  0)
\mvdash{}  ipolynomial-term([<const,  []>])  \mequiv{}  "const"


By

---

Latex:
(RepUR  ``ipolynomial-term  imonomial-term``  0
  THEN  ((D  0  THEN  Auto)  THEN  RepUR  ``int\_term\_value``  0)
  THEN  Auto)

---

Home Index