---

Step * of Lemma real_polynomial_null

∀t:int_term(). t ≡ "0" supposing inl Ax ≤ null(int_term_to_ipoly(t))
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. inl Ax ≤ tt
⊢ t ≡ "0"

2
1. t : int_term()
2. u : iMonomial()
3. v : iMonomial() List
4. ipolynomial-term([u / v]) ≡ t
5. inl Ax ≤ ff
⊢ t ≡ "0"

---

Latex:

---

Latex:
\mforall{}t:int\_term().  t  \mequiv{}  "0"  supposing  inl  Ax  \mleq{}  null(int\_term\_to\_ipoly(t))


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