---

Step * of Lemma real_polynomial_null_orig

∀t:int_term(). t ≡ "0" supposing null(int_term_to_ipoly(t)) = tt
BY
{ (InstLemma `real_term_polynomial` []
   THEN ParallelLast'
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜int_term_to_ipoly(t)⌝⋅ THENA Auto)
   THEN RepeatFor 2 ((Thin (-1) THEN D -1))
   THEN Reduce 0
   THEN Auto) }

1
1. t : int_term()
2. ipolynomial-term([]) ≡ t
3. tt = tt
⊢ t ≡ "0"

---

Latex:

---

Latex:
\mforall{}t:int\_term().  t  \mequiv{}  "0"  supposing  null(int\_term\_to\_ipoly(t))  =  tt


By

---

Latex:
(InstLemma  `real\_term\_polynomial`  []
  THEN  ParallelLast'
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}int\_term\_to\_ipoly(t)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((Thin  (-1)  THEN  D  -1))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index