Proof of Nuprl Lemma : mul-polynom-val

Step * 4 1 1 2 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)
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)) ∈ ℤ
24. ∀p:polyform(n - 1). (tree_node(p;polyconst(0))@[u / v] = p@v ∈ ℤ)
⊢ (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])
   ∈ ℤ)
BY
{ (PromoteHyp (-1) 13

   THEN (InstHyp [⌜k - 1⌝;⌜n⌝;⌜tree_node(left;polyconst(0))⌝;⌜q2⌝;⌜[u / v]⌝] 2⋅ THENA Auto)

   THEN (RWO "13" (-1) THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜mul-polynom(tree_node(left;polyconst(0));q2) = ab ∈ polyform(n)⌝⋅ THENA Auto)

   THEN (InstHyp [⌜k - 1⌝;⌜n⌝;⌜p2⌝;⌜tree_node(l1;polyconst(0))⌝;⌜[u / v]⌝] 2⋅ THENA Auto)

   THEN (RWO "13" (-1) THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜mul-polynom(p2;tree_node(l1;polyconst(0))) = ba ∈ polyform(n)⌝⋅ THENA Auto)
   THEN (InstHyp [⌜k - 1⌝;⌜n⌝;⌜p2⌝;⌜q2⌝;⌜[u / v]⌝] 2⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜mul-polynom(p2;q2) = bb ∈ polyform(n)⌝⋅ THENA Auto)
   THEN RepeatFor 4 ((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)
⊢ (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 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) 18. aa : polyform(n - 1) 19. mul-polynom(left;l1) = aa 20. tree\_node(left;polyconst(0)) \mmember{} polyform(n) 21. tree\_size(tree\_node(left;polyconst(0))) = (1 + tree\_size(left)) 22. tree\_node(l1;polyconst(0)) \mmember{} polyform(n) 23. tree\_size(tree\_node(l1;polyconst(0))) = (1 + tree\_size(l1)) 24. \mforall{}p:polyform(n - 1). (tree\_node(p;polyconst(0))@[u / v] = p@v) \mvdash{} (aa@v = (left@v * l1@v)) {}\mRightarrow{} (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])) By Latex: (PromoteHyp (-1) 13 THEN (InstHyp [\mkleeneopen{}k - 1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}tree\_node(left;polyconst(0))\mkleeneclose{};\mkleeneopen{}q2\mkleeneclose{};\mkleeneopen{}[u / v]\mkleeneclose{}] 2\mcdot{} THENA Auto) THEN (RWO "13" (-1) THENA Auto) THEN MoveToConcl (-1) THEN (GenConcl \mkleeneopen{}mul-polynom(tree\_node(left;polyconst(0));q2) = ab\mkleeneclose{}\mcdot{} THENA Auto) THEN (InstHyp [\mkleeneopen{}k - 1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{};\mkleeneopen{}tree\_node(l1;polyconst(0))\mkleeneclose{};\mkleeneopen{}[u / v]\mkleeneclose{}] 2\mcdot{} THENA Auto) THEN (RWO "13" (-1) THENA Auto) THEN MoveToConcl (-1) THEN (GenConcl \mkleeneopen{}mul-polynom(p2;tree\_node(l1;polyconst(0))) = ba\mkleeneclose{}\mcdot{} THENA Auto) THEN (InstHyp [\mkleeneopen{}k - 1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{};\mkleeneopen{}q2\mkleeneclose{};\mkleeneopen{}[u / v]\mkleeneclose{}] 2\mcdot{} THENA Auto) THEN MoveToConcl (-1) THEN (GenConcl \mkleeneopen{}mul-polynom(p2;q2) = bb\mkleeneclose{}\mcdot{} THENA Auto) THEN RepeatFor 4 ((CallByValueReduce 0 THENA Auto))) Home Index