Step
*
4
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. n ≤ (||v|| + 1)
14. left ∈ polyform(n - 1)
15. l1 ∈ polyform(n - 1)
16. p2 ∈ polyform(n)
17. q2 ∈ polyform(n)
⊢ eval aa = mul-polynom(left;l1) in
eval ab = mul-polynom(tree_node(left;polyconst(0));q2) in
eval ba = mul-polynom(p2;tree_node(l1;polyconst(0))) in
eval bb = mul-polynom(p2;q2) in
eval mid = add-polynom(ab;ba) in
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
{ (((InstHyp [⌜k - 1⌝;⌜n - 1⌝;⌜left⌝;⌜l1⌝;⌜v⌝] 2⋅ THENA Auto)
THEN MoveToConcl (-1)
THEN (GenConcl ⌜mul-polynom(left;l1) = aa ∈ polyform(n - 1)⌝⋅ THENA Auto))
THEN ((Assert tree_node(left;polyconst(0)) ∈ polyform(n) BY
((GenConcl ⌜polyconst(0) = z ∈ polyform(n)⌝⋅ THENA (Auto THEN SubsumeC ⌜polynom(n)⌝⋅ THEN Auto))
THEN Auto
))
THEN (Assert tree_size(tree_node(left;polyconst(0))) = (1 + tree_size(left)) ∈ ℤ BY
(RW (AddrC [2] RecUnfoldTopAbC) 0
THEN Reduce 0
THEN Subst' tree_size(polyconst(0)) ~ 0 0
THEN Auto))
)
THEN (Assert tree_node(l1;polyconst(0)) ∈ polyform(n) BY
((GenConcl ⌜polyconst(0) = z ∈ polyform(n)⌝⋅ THENA (Auto THEN SubsumeC ⌜polynom(n)⌝⋅ THEN Auto))
THEN Auto
))
THEN (Assert tree_size(tree_node(l1;polyconst(0))) = (1 + tree_size(l1)) ∈ ℤ BY
(RW (AddrC [2] RecUnfoldTopAbC) 0 THEN Reduce 0 THEN Subst' tree_size(polyconst(0)) ~ 0 0 THEN 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. n ≤ (||v|| + 1)
14. left ∈ polyform(n - 1)
15. l1 ∈ polyform(n - 1)
16. p2 ∈ polyform(n)
17. q2 ∈ polyform(n)
18. aa : polyform(n - 1)
19. mul-polynom(left;l1) = aa ∈ polyform(n - 1)
20. tree_node(left;polyconst(0)) ∈ polyform(n)
21. tree_size(tree_node(left;polyconst(0))) = (1 + tree_size(left)) ∈ ℤ
22. tree_node(l1;polyconst(0)) ∈ polyform(n)
23. tree_size(tree_node(l1;polyconst(0))) = (1 + tree_size(l1)) ∈ ℤ
⊢ (aa@v = (left@v * l1@v) ∈ ℤ)
⇒ (eval aa = aa in
eval ab = mul-polynom(tree_node(left;polyconst(0));q2) in
eval ba = mul-polynom(p2;tree_node(l1;polyconst(0))) in
eval bb = mul-polynom(p2;q2) in
eval mid = add-polynom(ab;ba) in
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])
∈ ℤ)
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. n \mleq{} (||v|| + 1)
14. left \mmember{} polyform(n - 1)
15. l1 \mmember{} polyform(n - 1)
16. p2 \mmember{} polyform(n)
17. q2 \mmember{} polyform(n)
\mvdash{} eval aa = mul-polynom(left;l1) in
eval ab = mul-polynom(tree\_node(left;polyconst(0));q2) in
eval ba = mul-polynom(p2;tree\_node(l1;polyconst(0))) in
eval bb = mul-polynom(p2;q2) in
eval mid = add-polynom(ab;ba) in
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:
(((InstHyp [\mkleeneopen{}k - 1\mkleeneclose{};\mkleeneopen{}n - 1\mkleeneclose{};\mkleeneopen{}left\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}] 2\mcdot{} THENA Auto)
THEN MoveToConcl (-1)
THEN (GenConcl \mkleeneopen{}mul-polynom(left;l1) = aa\mkleeneclose{}\mcdot{} THENA Auto))
THEN ((Assert tree\_node(left;polyconst(0)) \mmember{} polyform(n) BY
((GenConcl \mkleeneopen{}polyconst(0) = z\mkleeneclose{}\mcdot{} THENA (Auto THEN SubsumeC \mkleeneopen{}polynom(n)\mkleeneclose{}\mcdot{} THEN Auto))
THEN Auto
))
THEN (Assert tree\_size(tree\_node(left;polyconst(0))) = (1 + tree\_size(left)) BY
(RW (AddrC [2] RecUnfoldTopAbC) 0
THEN Reduce 0
THEN Subst' tree\_size(polyconst(0)) \msim{} 0 0
THEN Auto))
)
THEN (Assert tree\_node(l1;polyconst(0)) \mmember{} polyform(n) BY
((GenConcl \mkleeneopen{}polyconst(0) = z\mkleeneclose{}\mcdot{} THENA (Auto THEN SubsumeC \mkleeneopen{}polynom(n)\mkleeneclose{}\mcdot{} THEN Auto))
THEN Auto
))
THEN (Assert tree\_size(tree\_node(l1;polyconst(0))) = (1 + tree\_size(l1)) BY
(RW (AddrC [2] RecUnfoldTopAbC) 0
THEN Reduce 0
THEN Subst' tree\_size(polyconst(0)) \msim{} 0 0
THEN Auto)))
Home
Index