---

Step * 1 1 of Lemma add-ipoly_wf


1. n : ℤ
2. p : iMonomial() List@i
3. q : iMonomial() List@i
4. ||p|| + ||q|| < 0
5. ∀i:ℕ||p||. ∀j:ℕi.  imonomial-less(p[j];p[i])
6. ∀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])
BY
{ TACTIC:Auto' }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  p  :  iMonomial()  List@i
3.  q  :  iMonomial()  List@i
4.  ||p||  +  ||q||  <  0
5.  \mforall{}i:\mBbbN{}||p||.  \mforall{}j:\mBbbN{}i.    imonomial-less(p[j];p[i])
6.  \mforall{}i:\mBbbN{}||q||.  \mforall{}j:\mBbbN{}i.    imonomial-less(q[j];q[i])
\mvdash{}  \mdownarrow{}\mforall{}i:\mBbbN{}||add-ipoly(p;q)||.  \mforall{}j:\mBbbN{}i.    imonomial-less(add-ipoly(p;q)[j];add-ipoly(p;q)[i])


By

---

Latex:
TACTIC:Auto'

---

Home Index