---

Step * 1 of Lemma add-poly-lemma1


∀q:iMonomial() List. ∀m:iMonomial().
  ((∀i:ℕ||[]||. ∀j:ℕi.  imonomial-less([][j];[][i]))
  ⇒ (∀i:ℕ||q||. ∀j:ℕi.  imonomial-less(q[j];q[i]))
  ⇒ (0 < ||[]|| ⇒ imonomial-less(m;[][0]))
  ⇒ (0 < ||q|| ⇒ imonomial-less(m;q[0]))
  ⇒ 0 < ||add-ipoly([];q)||
  ⇒ imonomial-less(m;add-ipoly([];q)[0]))
BY
{ ((D 0 THENA Auto)
   THEN (RecUnfold `add-ipoly` 0 THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto)))
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

\mforall{}q:iMonomial()  List.  \mforall{}m:iMonomial().
    ((\mforall{}i:\mBbbN{}||[]||.  \mforall{}j:\mBbbN{}i.    imonomial-less([][j];[][i]))
    {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||q||.  \mforall{}j:\mBbbN{}i.    imonomial-less(q[j];q[i]))
    {}\mRightarrow{}  (0  <  ||[]||  {}\mRightarrow{}  imonomial-less(m;[][0]))
    {}\mRightarrow{}  (0  <  ||q||  {}\mRightarrow{}  imonomial-less(m;q[0]))
    {}\mRightarrow{}  0  <  ||add-ipoly([];q)||
    {}\mRightarrow{}  imonomial-less(m;add-ipoly([];q)[0]))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (RecUnfold  `add-ipoly`  0  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index