Step
*
1
2
2
2
1
1
of Lemma
add-ipoly_wf
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. u : iMonomial()
5. v : iMonomial() List
6. u1 : iMonomial()
7. v1 : iMonomial() List
8. ||[u / v]|| + ||[u1 / v1]|| < n
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. ↑imonomial-le(u;u1)
12. ↑imonomial-le(u1;u)
⊢ ↓∀i:ℕ||let cp,vs = u
in eval c = cp + (fst(u1)) in
if c=0 then add-ipoly(v;v1) else [<c, vs> / add-ipoly(v;v1)]||. ∀j:ℕi.
imonomial-less(let cp,vs = u
in eval c = cp + (fst(u1)) in
if c=0 then add-ipoly(v;v1) else [<c, vs> / add-ipoly(v;v1)][j];let cp,vs = u
in eval c = cp + (fst(u1)) in
if c=0
then add-ipoly(v;v1)
else [<c, vs> /
add-ipoly(v;v1)][i])
BY
{ (DVar `u'
THEN DVar `u1'
THEN Reduce 0
THEN (CallByValueReduce 0 THENA Auto)
THEN AutoSplit
THEN (InstHyp [⌜v⌝;⌜v1⌝] 3⋅
THENA (Auto
THEN ∀h:hyp. ((InstHyp [⌜i + 1⌝;⌜j + 1⌝] h⋅ THENA Auto)
THEN NthHypEq (-1)
THEN EqCD
THEN Complete (Auto))
)
)) }
1
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. u2 : ℤ-o
5. u3 : {vs:ℤ List| sorted(vs)}
6. v : iMonomial() List
7. u4 : ℤ-o
8. u5 : {vs:ℤ List| sorted(vs)}
9. v1 : iMonomial() List
10. ||[<u2, u3> / v]|| + ||[<u4, u5> / v1]|| < n
11. ∀i:ℕ||[<u2, u3> / v]||. ∀j:ℕi. imonomial-less([<u2, u3> / v][j];[<u2, u3> / v][i])
12. ∀i:ℕ||[<u4, u5> / v1]||. ∀j:ℕi. imonomial-less([<u4, u5> / v1][j];[<u4, u5> / v1][i])
13. ↑imonomial-le(<u2, u3>;<u4, u5>)
14. ↑imonomial-le(<u4, u5>;<u2, u3>)
15. (u2 + u4) = 0 ∈ ℤ
16. ↓∀i:ℕ||add-ipoly(v;v1)||. ∀j:ℕi. imonomial-less(add-ipoly(v;v1)[j];add-ipoly(v;v1)[i])
⊢ ↓∀i:ℕ||add-ipoly(v;v1)||. ∀j:ℕi. imonomial-less(add-ipoly(v;v1)[j];add-ipoly(v;v1)[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. u2 : ℤ-o
5. u3 : {vs:ℤ List| sorted(vs)}
6. v : iMonomial() List
7. u4 : ℤ-o
8. u2 + u4 ≠ 0
9. u5 : {vs:ℤ List| sorted(vs)}
10. v1 : iMonomial() List
11. ||[<u2, u3> / v]|| + ||[<u4, u5> / v1]|| < n
12. ∀i:ℕ||[<u2, u3> / v]||. ∀j:ℕi. imonomial-less([<u2, u3> / v][j];[<u2, u3> / v][i])
13. ∀i:ℕ||[<u4, u5> / v1]||. ∀j:ℕi. imonomial-less([<u4, u5> / v1][j];[<u4, u5> / v1][i])
14. ↑imonomial-le(<u2, u3>;<u4, u5>)
15. ↑imonomial-le(<u4, u5>;<u2, u3>)
16. ↓∀i:ℕ||add-ipoly(v;v1)||. ∀j:ℕi. imonomial-less(add-ipoly(v;v1)[j];add-ipoly(v;v1)[i])
⊢ ↓∀i:ℕ||add-ipoly(v;v1)|| + 1. ∀j:ℕi.
imonomial-less([<u2 + u4, u3> / add-ipoly(v;v1)][j];[<u2 + u4, u3> / add-ipoly(v;v1)][i])
Latex:
Latex:
1. n : \mBbbZ{}
2. 0 < n
3. \mforall{}p,q:iMonomial() List.
(||p|| + ||q|| < n - 1
{}\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])))
4. u : iMonomial()
5. v : iMonomial() List
6. u1 : iMonomial()
7. v1 : iMonomial() List
8. ||[u / v]|| + ||[u1 / v1]|| < n
9. \mforall{}i:\mBbbN{}||[u / v]||. \mforall{}j:\mBbbN{}i. imonomial-less([u / v][j];[u / v][i])
10. \mforall{}i:\mBbbN{}||[u1 / v1]||. \mforall{}j:\mBbbN{}i. imonomial-less([u1 / v1][j];[u1 / v1][i])
11. \muparrow{}imonomial-le(u;u1)
12. \muparrow{}imonomial-le(u1;u)
\mvdash{} \mdownarrow{}\mforall{}i:\mBbbN{}||let cp,vs = u
in eval c = cp + (fst(u1)) in
if c=0 then add-ipoly(v;v1) else [<c, vs> / add-ipoly(v;v1)]||. \mforall{}j:\mBbbN{}i.
imonomial-less(let cp,vs = u
in eval c = cp + (fst(u1)) in
if c=0
then add-ipoly(v;v1)
else [<c, vs> / add-ipoly(v;v1)][j];let cp,vs = u
in eval c = cp + (fst(u1)) in
if c=0
then add-ipoly(v;v1)
else [<c, vs> / add-ipoly(v;v1)][i])
By
Latex:
(DVar `u'
THEN DVar `u1'
THEN Reduce 0
THEN (CallByValueReduce 0 THENA Auto)
THEN AutoSplit
THEN (InstHyp [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{}] 3\mcdot{}
THENA (Auto
THEN \mforall{}h:hyp. ((InstHyp [\mkleeneopen{}i + 1\mkleeneclose{};\mkleeneopen{}j + 1\mkleeneclose{}] h\mcdot{} THENA Auto)
THEN NthHypEq (-1)
THEN EqCD
THEN Complete (Auto))
)
))
Home
Index