---

Step * of Lemma ring_polynomial_null

∀r:CRng. ∀t:int_term().  t ≡ "0" supposing inl Ax ≤ null(int_term_to_ipoly(t))
BY
{ xxx(InstLemma `ring_term_polynomial` []
      THEN RepeatFor 2 (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)xxx }

1
1. r : CRng
2. t : int_term()
3. ipolynomial-term([]) ≡ t
4. inl Ax ≤ tt
⊢ t ≡ "0"

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

---

Latex:

---

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


By

---

Latex:
xxx(InstLemma  `ring\_term\_polynomial`  []
        THEN  RepeatFor  2  (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)xxx

---

Home Index