---

Step * of Lemma add-ipoly_wf

∀[p,q:iPolynomial()].  (add-ipoly(p;q) ∈ iPolynomial())
BY
{ TACTIC:(Auto
          THEN D -1
          THEN D 1
          THEN MemTypeCD
          THEN Try (Complete (Auto))
          THEN SquashConcl
          THEN Auto
          THEN RepeatFor 4 (MoveToConcl (-1))) }

1
∀p:iMonomial() List
  ((∀i:ℕ||p||. ∀j:ℕi.  imonomial-less(p[j];p[i]))
  ⇒ (∀q:iMonomial() List
        ((∀i:ℕ||q||. ∀j:ℕi.  imonomial-less(q[j];q[i]))
        ⇒ (↓∀i:ℕ||add-ipoly(p;q)||. ∀j:ℕi.  imonomial-less(add-ipoly(p;q)[j];add-ipoly(p;q)[i])))))

---

Latex:

---

Latex:
\mforall{}[p,q:iPolynomial()].    (add-ipoly(p;q)  \mmember{}  iPolynomial())


By

---

Latex:
TACTIC:(Auto
                THEN  D  -1
                THEN  D  1
                THEN  MemTypeCD
                THEN  Try  (Complete  (Auto))
                THEN  SquashConcl
                THEN  Auto
                THEN  RepeatFor  4  (MoveToConcl  (-1)))

---

Home Index