---

Step * 2 2 of Lemma add-poly-lemma1


1. u : iMonomial()
2. v : iMonomial() List
3. ∀q:iMonomial() List. ∀m:iMonomial().
     ((∀i:ℕ||v||. ∀j:ℕi.  imonomial-less(v[j];v[i]))
     ⇒ (∀i:ℕ||q||. ∀j:ℕi.  imonomial-less(q[j];q[i]))
     ⇒ (0 < ||v|| ⇒ imonomial-less(m;v[0]))
     ⇒ (0 < ||q|| ⇒ imonomial-less(m;q[0]))
     ⇒ 0 < ||add-ipoly(v;q)||
     ⇒ imonomial-less(m;add-ipoly(v;q)[0]))
4. u1 : iMonomial()
5. v1 : iMonomial() List
6. ∀m:iMonomial()
     ((∀i:ℕ||[u / v]||. ∀j:ℕi.  imonomial-less([u / v][j];[u / v][i]))
     ⇒ (∀i:ℕ||v1||. ∀j:ℕi.  imonomial-less(v1[j];v1[i]))
     ⇒ (0 < ||[u / v]|| ⇒ imonomial-less(m;[u / v][0]))
     ⇒ (0 < ||v1|| ⇒ imonomial-less(m;v1[0]))
     ⇒ 0 < ||add-ipoly([u / v];v1)||
     ⇒ imonomial-less(m;add-ipoly([u / v];v1)[0]))
⊢ ∀m:iMonomial()
    ((∀i:ℕ||[u / v]||. ∀j:ℕi.  imonomial-less([u / v][j];[u / v][i]))
    ⇒ (∀i:ℕ||[u1 / v1]||. ∀j:ℕi.  imonomial-less([u1 / v1][j];[u1 / v1][i]))
    ⇒ (0 < ||[u / v]|| ⇒ imonomial-less(m;[u / v][0]))
    ⇒ (0 < ||[u1 / v1]|| ⇒ imonomial-less(m;[u1 / v1][0]))
    ⇒ 0 < ||add-ipoly([u / v];[u1 / v1])||
    ⇒ imonomial-less(m;add-ipoly([u / v];[u1 / v1])[0]))
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN (RecUnfold `add-ipoly` 0 THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto)))
   THEN Reduce 0) }

1
1. u : iMonomial()
2. v : iMonomial() List
3. ∀q:iMonomial() List. ∀m:iMonomial().
     ((∀i:ℕ||v||. ∀j:ℕi.  imonomial-less(v[j];v[i]))
     ⇒ (∀i:ℕ||q||. ∀j:ℕi.  imonomial-less(q[j];q[i]))
     ⇒ (0 < ||v|| ⇒ imonomial-less(m;v[0]))
     ⇒ (0 < ||q|| ⇒ imonomial-less(m;q[0]))
     ⇒ 0 < ||add-ipoly(v;q)||
     ⇒ imonomial-less(m;add-ipoly(v;q)[0]))
4. u1 : iMonomial()
5. v1 : iMonomial() List
6. ∀m:iMonomial()
     ((∀i:ℕ||[u / v]||. ∀j:ℕi.  imonomial-less([u / v][j];[u / v][i]))
     ⇒ (∀i:ℕ||v1||. ∀j:ℕi.  imonomial-less(v1[j];v1[i]))
     ⇒ (0 < ||[u / v]|| ⇒ imonomial-less(m;[u / v][0]))
     ⇒ (0 < ||v1|| ⇒ imonomial-less(m;v1[0]))
     ⇒ 0 < ||add-ipoly([u / v];v1)||
     ⇒ imonomial-less(m;add-ipoly([u / v];v1)[0]))
7. m : iMonomial()
8. ∀i:ℕ||[u / v]||. ∀j:ℕi.  imonomial-less([u / v][j];[u / v][i])
9. ∀i:ℕ||[u1 / v1]||. ∀j:ℕi.  imonomial-less([u1 / v1][j];[u1 / v1][i])
10. 0 < ||[u / v]|| ⇒ imonomial-less(m;[u / v][0])
11. 0 < ||[u1 / v1]|| ⇒ imonomial-less(m;[u1 / v1][0])
⊢ 0 < ||if imonomial-le(u;u1)
then if imonomial-le(u1;u)
     then eval x = add-ipoly(v;v1) in
          let cp,vs = u 
          in eval c = cp + (fst(u1)) in
             if c=0  then x  else [<c, vs> / x]
     else eval x = add-ipoly(v;[u1 / v1]) in
          [u / x]
     fi 
else eval x = add-ipoly([u / v];v1) in
     [u1 / x]
fi ||
⇒ imonomial-less(m;if imonomial-le(u;u1)
   then if imonomial-le(u1;u)
        then eval x = add-ipoly(v;v1) in
             let cp,vs = u 
             in eval c = cp + (fst(u1)) in
                if c=0  then x  else [<c, vs> / x]
        else eval x = add-ipoly(v;[u1 / v1]) in
             [u / x]
        fi 
   else eval x = add-ipoly([u / v];v1) in
        [u1 / x]
   fi [0])

---

Latex:

---

Latex:

1.  u  :  iMonomial()
2.  v  :  iMonomial()  List
3.  \mforall{}q:iMonomial()  List.  \mforall{}m:iMonomial().
          ((\mforall{}i:\mBbbN{}||v||.  \mforall{}j:\mBbbN{}i.    imonomial-less(v[j];v[i]))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||q||.  \mforall{}j:\mBbbN{}i.    imonomial-less(q[j];q[i]))
          {}\mRightarrow{}  (0  <  ||v||  {}\mRightarrow{}  imonomial-less(m;v[0]))
          {}\mRightarrow{}  (0  <  ||q||  {}\mRightarrow{}  imonomial-less(m;q[0]))
          {}\mRightarrow{}  0  <  ||add-ipoly(v;q)||
          {}\mRightarrow{}  imonomial-less(m;add-ipoly(v;q)[0]))
4.  u1  :  iMonomial()
5.  v1  :  iMonomial()  List
6.  \mforall{}m:iMonomial()
          ((\mforall{}i:\mBbbN{}||[u  /  v]||.  \mforall{}j:\mBbbN{}i.    imonomial-less([u  /  v][j];[u  /  v][i]))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||v1||.  \mforall{}j:\mBbbN{}i.    imonomial-less(v1[j];v1[i]))
          {}\mRightarrow{}  (0  <  ||[u  /  v]||  {}\mRightarrow{}  imonomial-less(m;[u  /  v][0]))
          {}\mRightarrow{}  (0  <  ||v1||  {}\mRightarrow{}  imonomial-less(m;v1[0]))
          {}\mRightarrow{}  0  <  ||add-ipoly([u  /  v];v1)||
          {}\mRightarrow{}  imonomial-less(m;add-ipoly([u  /  v];v1)[0]))
\mvdash{}  \mforall{}m:iMonomial()
        ((\mforall{}i:\mBbbN{}||[u  /  v]||.  \mforall{}j:\mBbbN{}i.    imonomial-less([u  /  v][j];[u  /  v][i]))
        {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||[u1  /  v1]||.  \mforall{}j:\mBbbN{}i.    imonomial-less([u1  /  v1][j];[u1  /  v1][i]))
        {}\mRightarrow{}  (0  <  ||[u  /  v]||  {}\mRightarrow{}  imonomial-less(m;[u  /  v][0]))
        {}\mRightarrow{}  (0  <  ||[u1  /  v1]||  {}\mRightarrow{}  imonomial-less(m;[u1  /  v1][0]))
        {}\mRightarrow{}  0  <  ||add-ipoly([u  /  v];[u1  /  v1])||
        {}\mRightarrow{}  imonomial-less(m;add-ipoly([u  /  v];[u1  /  v1])[0]))


By

---

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

---

Home Index