Step
*
4
1
1
2
1
1
of Lemma
mul-polynom-val
1. k : ℕ
2. ∀k:ℕk
∀[n:ℕ]. ∀[p,q:polyform(n)].
(((tree_size(p) + tree_size(q)) ≤ k) ⇒ (∀[l:{l:ℤ List| n ≤ ||l||} ]. (mul-polynom(p;q)@l = (p@l * q@l) ∈ ℤ)))
3. n : ℕ
4. left : tree(ℤ)
5. p2 : tree(ℤ)
6. ((↑(ispolyform(left) (n - 1))) ∧ (↑(ispolyform(p2) n))) ∧ 0 < n
7. l1 : tree(ℤ)
8. q2 : tree(ℤ)
9. ((↑(ispolyform(l1) (n - 1))) ∧ (↑(ispolyform(q2) n))) ∧ 0 < n
10. (((1 + tree_size(left)) + tree_size(p2)) + (1 + tree_size(l1)) + tree_size(q2)) ≤ k
11. u : ℤ
12. v : ℤ List
13. ∀p:polyform(n - 1). (tree_node(p;polyconst(0))@[u / v] = p@v ∈ ℤ)
14. n ≤ (||v|| + 1)
15. left ∈ polyform(n - 1)
16. l1 ∈ polyform(n - 1)
17. p2 ∈ polyform(n)
18. q2 ∈ polyform(n)
19. aa : polyform(n - 1)
20. mul-polynom(left;l1) = aa ∈ polyform(n - 1)
21. tree_node(left;polyconst(0)) ∈ polyform(n)
22. tree_size(tree_node(left;polyconst(0))) = (1 + tree_size(left)) ∈ ℤ
23. tree_node(l1;polyconst(0)) ∈ polyform(n)
24. tree_size(tree_node(l1;polyconst(0))) = (1 + tree_size(l1)) ∈ ℤ
25. ab : polyform(n)
26. mul-polynom(tree_node(left;polyconst(0));q2) = ab ∈ polyform(n)
27. ba : polyform(n)
28. mul-polynom(p2;tree_node(l1;polyconst(0))) = ba ∈ polyform(n)
29. bb : polyform(n)
30. mul-polynom(p2;q2) = bb ∈ polyform(n)
31. mid : polyform(n)
32. add-polynom(ab;ba) = mid ∈ polyform(n)
⊢ (mid@[u / v] = (ab@[u / v] + ba@[u / v]) ∈ ℤ)
⇒ (bb@[u / v] = (p2@[u / v] * q2@[u / v]) ∈ ℤ)
⇒ (ba@[u / v] = (p2@[u / v] * l1@v) ∈ ℤ)
⇒ (ab@[u / v] = (left@v * q2@[u / v]) ∈ ℤ)
⇒ (aa@v = (left@v * l1@v) ∈ ℤ)
⇒ (eval bb' = add-polynom(mid;tree_node(polyconst(0);bb)) in
tree_node(aa;bb')@[u / v]
= (tree_node(left;p2)@[u / v] * tree_node(l1;q2)@[u / v])
∈ ℤ)
BY
{ ((Assert tree_node(polyconst(0);bb)@[u / v] = (u * bb@[u / v]) ∈ ℤ BY
(RepUR ``poly-int-val poly-val-fun`` 0
THEN Fold `poly-val-fun` 0
THEN Fold `poly-int-val` 0
THEN Reduce 0
THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
THEN Decide ⌜bb@[u / v] = 0 ∈ ℤ⌝⋅
THEN Reduce 0
THEN Auto))
THEN MoveToConcl (-1)
THEN (GenConcl ⌜tree_node(polyconst(0);bb) = x ∈ polyform(n)⌝⋅ THENA Auto)
THEN (CallByValueReduce 0 THENA Auto)) }
1
1. k : ℕ
2. ∀k:ℕk
∀[n:ℕ]. ∀[p,q:polyform(n)].
(((tree_size(p) + tree_size(q)) ≤ k) ⇒ (∀[l:{l:ℤ List| n ≤ ||l||} ]. (mul-polynom(p;q)@l = (p@l * q@l) ∈ ℤ)))
3. n : ℕ
4. left : tree(ℤ)
5. p2 : tree(ℤ)
6. ((↑(ispolyform(left) (n - 1))) ∧ (↑(ispolyform(p2) n))) ∧ 0 < n
7. l1 : tree(ℤ)
8. q2 : tree(ℤ)
9. ((↑(ispolyform(l1) (n - 1))) ∧ (↑(ispolyform(q2) n))) ∧ 0 < n
10. (((1 + tree_size(left)) + tree_size(p2)) + (1 + tree_size(l1)) + tree_size(q2)) ≤ k
11. u : ℤ
12. v : ℤ List
13. ∀p:polyform(n - 1). (tree_node(p;polyconst(0))@[u / v] = p@v ∈ ℤ)
14. n ≤ (||v|| + 1)
15. left ∈ polyform(n - 1)
16. l1 ∈ polyform(n - 1)
17. p2 ∈ polyform(n)
18. q2 ∈ polyform(n)
19. aa : polyform(n - 1)
20. mul-polynom(left;l1) = aa ∈ polyform(n - 1)
21. tree_node(left;polyconst(0)) ∈ polyform(n)
22. tree_size(tree_node(left;polyconst(0))) = (1 + tree_size(left)) ∈ ℤ
23. tree_node(l1;polyconst(0)) ∈ polyform(n)
24. tree_size(tree_node(l1;polyconst(0))) = (1 + tree_size(l1)) ∈ ℤ
25. ab : polyform(n)
26. mul-polynom(tree_node(left;polyconst(0));q2) = ab ∈ polyform(n)
27. ba : polyform(n)
28. mul-polynom(p2;tree_node(l1;polyconst(0))) = ba ∈ polyform(n)
29. bb : polyform(n)
30. mul-polynom(p2;q2) = bb ∈ polyform(n)
31. mid : polyform(n)
32. add-polynom(ab;ba) = mid ∈ polyform(n)
33. x : polyform(n)
34. tree_node(polyconst(0);bb) = x ∈ polyform(n)
⊢ (x@[u / v] = (u * bb@[u / v]) ∈ ℤ)
⇒ (mid@[u / v] = (ab@[u / v] + ba@[u / v]) ∈ ℤ)
⇒ (bb@[u / v] = (p2@[u / v] * q2@[u / v]) ∈ ℤ)
⇒ (ba@[u / v] = (p2@[u / v] * l1@v) ∈ ℤ)
⇒ (ab@[u / v] = (left@v * q2@[u / v]) ∈ ℤ)
⇒ (aa@v = (left@v * l1@v) ∈ ℤ)
⇒ (tree_node(aa;add-polynom(mid;x))@[u / v] = (tree_node(left;p2)@[u / v] * tree_node(l1;q2)@[u / v]) ∈ ℤ)
Latex:
Latex:
1. k : \mBbbN{}
2. \mforall{}k:\mBbbN{}k
\mforall{}[n:\mBbbN{}]. \mforall{}[p,q:polyform(n)].
(((tree\_size(p) + tree\_size(q)) \mleq{} k)
{}\mRightarrow{} (\mforall{}[l:\{l:\mBbbZ{} List| n \mleq{} ||l||\} ]. (mul-polynom(p;q)@l = (p@l * q@l))))
3. n : \mBbbN{}
4. left : tree(\mBbbZ{})
5. p2 : tree(\mBbbZ{})
6. ((\muparrow{}(ispolyform(left) (n - 1))) \mwedge{} (\muparrow{}(ispolyform(p2) n))) \mwedge{} 0 < n
7. l1 : tree(\mBbbZ{})
8. q2 : tree(\mBbbZ{})
9. ((\muparrow{}(ispolyform(l1) (n - 1))) \mwedge{} (\muparrow{}(ispolyform(q2) n))) \mwedge{} 0 < n
10. (((1 + tree\_size(left)) + tree\_size(p2)) + (1 + tree\_size(l1)) + tree\_size(q2)) \mleq{} k
11. u : \mBbbZ{}
12. v : \mBbbZ{} List
13. \mforall{}p:polyform(n - 1). (tree\_node(p;polyconst(0))@[u / v] = p@v)
14. n \mleq{} (||v|| + 1)
15. left \mmember{} polyform(n - 1)
16. l1 \mmember{} polyform(n - 1)
17. p2 \mmember{} polyform(n)
18. q2 \mmember{} polyform(n)
19. aa : polyform(n - 1)
20. mul-polynom(left;l1) = aa
21. tree\_node(left;polyconst(0)) \mmember{} polyform(n)
22. tree\_size(tree\_node(left;polyconst(0))) = (1 + tree\_size(left))
23. tree\_node(l1;polyconst(0)) \mmember{} polyform(n)
24. tree\_size(tree\_node(l1;polyconst(0))) = (1 + tree\_size(l1))
25. ab : polyform(n)
26. mul-polynom(tree\_node(left;polyconst(0));q2) = ab
27. ba : polyform(n)
28. mul-polynom(p2;tree\_node(l1;polyconst(0))) = ba
29. bb : polyform(n)
30. mul-polynom(p2;q2) = bb
31. mid : polyform(n)
32. add-polynom(ab;ba) = mid
\mvdash{} (mid@[u / v] = (ab@[u / v] + ba@[u / v]))
{}\mRightarrow{} (bb@[u / v] = (p2@[u / v] * q2@[u / v]))
{}\mRightarrow{} (ba@[u / v] = (p2@[u / v] * l1@v))
{}\mRightarrow{} (ab@[u / v] = (left@v * q2@[u / v]))
{}\mRightarrow{} (aa@v = (left@v * l1@v))
{}\mRightarrow{} (eval bb' = add-polynom(mid;tree\_node(polyconst(0);bb)) in
tree\_node(aa;bb')@[u / v]
= (tree\_node(left;p2)@[u / v] * tree\_node(l1;q2)@[u / v]))
By
Latex:
((Assert tree\_node(polyconst(0);bb)@[u / v] = (u * bb@[u / v]) BY
(RepUR ``poly-int-val poly-val-fun`` 0
THEN Fold `poly-val-fun` 0
THEN Fold `poly-int-val` 0
THEN Reduce 0
THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
THEN Decide \mkleeneopen{}bb@[u / v] = 0\mkleeneclose{}\mcdot{}
THEN Reduce 0
THEN Auto))
THEN MoveToConcl (-1)
THEN (GenConcl \mkleeneopen{}tree\_node(polyconst(0);bb) = x\mkleeneclose{}\mcdot{} THENA Auto)
THEN (CallByValueReduce 0 THENA Auto))
Home
Index