Step
*
2
2
1
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]))
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])
BY
{ (BoolCase ⌜imonomial-le(u;u1)⌝⋅ THENA Auto) }
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])
12. ↑imonomial-le(u;u1)
⊢ 0 < ||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 ||
⇒ imonomial-less(m;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 [0])
2
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. ¬↑imonomial-le(u;u1)
6. v1 : iMonomial() List
7. ∀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]))
8. m : iMonomial()
9. ∀i:ℕ||[u / v]||. ∀j:ℕi. imonomial-less([u / v][j];[u / v][i])
10. ∀i:ℕ||[u1 / v1]||. ∀j:ℕi. imonomial-less([u1 / v1][j];[u1 / v1][i])
11. 0 < ||[u / v]|| ⇒ imonomial-less(m;[u / v][0])
12. 0 < ||[u1 / v1]|| ⇒ imonomial-less(m;[u1 / v1][0])
⊢ 0 < ||eval x = add-ipoly([u / v];v1) in [u1 / x]|| ⇒ imonomial-less(m;eval x = add-ipoly([u / v];v1) in [u1 / x][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]))
7. m : iMonomial()
8. \mforall{}i:\mBbbN{}||[u / v]||. \mforall{}j:\mBbbN{}i. imonomial-less([u / v][j];[u / v][i])
9. \mforall{}i:\mBbbN{}||[u1 / v1]||. \mforall{}j:\mBbbN{}i. imonomial-less([u1 / v1][j];[u1 / v1][i])
10. 0 < ||[u / v]|| {}\mRightarrow{} imonomial-less(m;[u / v][0])
11. 0 < ||[u1 / v1]|| {}\mRightarrow{} imonomial-less(m;[u1 / v1][0])
\mvdash{} 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 ||
{}\mRightarrow{} 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])
By
Latex:
(BoolCase \mkleeneopen{}imonomial-le(u;u1)\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index