---

Step * 1 of Lemma add-ipoly_wf


∀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])))))
BY
{ TACTIC:((Assert ⌜∀n:ℕ. ∀p,q:iMonomial() List.
                     (||p|| + ||q|| < n
                     ⇒ (∀i:ℕ||p||. ∀j:ℕi.  imonomial-less(p[j];p[i]))
                     ⇒ (∀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])))⌝⋅
          THENM (Auto THEN (InstHyp [⌜(||p|| + ||q||) + 1⌝] 1⋅ THENM BHyp -1) THEN Auto)
          )
          THEN InductionOnNat
          THEN Auto) }

1
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])

2
1. n : ℤ
2. 0 < n
3. ∀p,q:iMonomial() List.
     (||p|| + ||q|| < n - 1
     ⇒ (∀i:ℕ||p||. ∀j:ℕi.  imonomial-less(p[j];p[i]))
     ⇒ (∀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])))
4. p : iMonomial() List@i
5. q : iMonomial() List@i
6. ||p|| + ||q|| < n
7. ∀i:ℕ||p||. ∀j:ℕi.  imonomial-less(p[j];p[i])
8. ∀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:iMonomial()  List
    ((\mforall{}i:\mBbbN{}||p||.  \mforall{}j:\mBbbN{}i.    imonomial-less(p[j];p[i]))
    {}\mRightarrow{}  (\mforall{}q:iMonomial()  List
                ((\mforall{}i:\mBbbN{}||q||.  \mforall{}j:\mBbbN{}i.    imonomial-less(q[j];q[i]))
                {}\mRightarrow{}  (\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:((Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}p,q:iMonomial()  List.
                                      (||p||  +  ||q||  <  n
                                      {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||p||.  \mforall{}j:\mBbbN{}i.    imonomial-less(p[j];p[i]))
                                      {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||q||.  \mforall{}j:\mBbbN{}i.    imonomial-less(q[j];q[i]))
                                      {}\mRightarrow{}  (\mdownarrow{}\mforall{}i:\mBbbN{}||add-ipoly(p;q)||.  \mforall{}j:\mBbbN{}i.
                                                    imonomial-less(add-ipoly(p;q)[j];add-ipoly(p;q)[i])))\mkleeneclose{}\mcdot{}
                THENM  (Auto  THEN  (InstHyp  [\mkleeneopen{}(||p||  +  ||q||)  +  1\mkleeneclose{}]  1\mcdot{}  THENM  BHyp  -1)  THEN  Auto)
                )
                THEN  InductionOnNat
                THEN  Auto)

---

Home Index