---

Step * 1 of Lemma real_polynomial_null


1. t : int_term()
2. ipolynomial-term([]) ≡ t
3. inl Ax ≤ tt
⊢ t ≡ "0"
BY
{ (RepUR ``ipolynomial-term`` -2 THEN RepeatFor 2 (ParallelOp -2) THEN Auto) }

---

Latex:

---

Latex:

1.  t  :  int\_term()
2.  ipolynomial-term([])  \mequiv{}  t
3.  inl  Ax  \mleq{}  tt
\mvdash{}  t  \mequiv{}  "0"


By

---

Latex:
(RepUR  ``ipolynomial-term``  -2  THEN  RepeatFor  2  (ParallelOp  -2)  THEN  Auto)

---

Home Index