Step
*
2
1
1
1
1
1
1
2
1
of Lemma
nonzero-mul-polynom
1. n : ℕ
2. ∀n:ℕn
∀[p,q:polynom(n)]. (poly-zero(n;mul-polynom(n;p;q)) = ff) supposing (poly-zero(n;q) = ff and poly-zero(n;p) = ff)
3. u : polynom(n - 1)
4. ¬↑poly-zero(n - 1;u)
5. v : polynom(n - 1) List
6. polyform-lead-nonzero(n;[u / v])
7. u1 : polynom(n - 1)
8. v1 : polynom(n - 1) List
9. polyform-lead-nonzero(n;[u1 / v1])
10. poly-zero(n;[u / v]) = ff
11. poly-zero(n;[u1 / v1]) = ff
12. ¬(n = 0 ∈ ℤ)
13. ∀[p,q:polynom(n - 1)].
(poly-zero(n - 1;mul-polynom(n - 1;p;q)) = ff) supposing (poly-zero(n - 1;q) = ff and poly-zero(n - 1;p) = ff)
14. ¬False
15. ¬False
16. ¬↑poly-zero(n - 1;u1)
17. ¬False
18. [mul-polynom(n - 1;u;u1) / map(λx.mul-polynom(n - 1;u;x);v1)] ∈ polyform(n - 1) List
⊢ poly-zero(n;eager-accum(z,a.add-polynom(n;tt;if null(z)
then []
else z @ [polyconst(n - 1;0)]
fi ;if poly-zero(n - 1;a)
then []
else [mul-polynom(n - 1;a;u1) / map(λx.mul-polynom(n - 1;a;x);v1)]
fi );[mul-polynom(n - 1;u;u1) / map(λx.mul-polynom(n - 1;u;x);v1)];v))
= ff
BY
{ (RW (AddrC [2] UnfoldTopAbC) 0
THEN (SplitOnConclITE THEN Try (Complete (Auto)))
THEN (InstHyp [⌜u⌝;⌜u1⌝] (-7)⋅ THENA Auto)
THEN (MoveToConcl (-1) THEN (GenConcl ⌜mul-polynom(n - 1;u;u1) = X ∈ polyform(n - 1)⌝⋅ THENA Auto))
THEN (GenConcl ⌜map(λx.mul-polynom(n - 1;u;x);v1) = q ∈ {q:polyform(n - 1) List| ||v1|| ≤ ||q||} ⌝⋅ THENA Auto)) }
1
1. n : ℕ
2. ∀n:ℕn
∀[p,q:polynom(n)]. (poly-zero(n;mul-polynom(n;p;q)) = ff) supposing (poly-zero(n;q) = ff and poly-zero(n;p) = ff)
3. u : polynom(n - 1)
4. ¬↑poly-zero(n - 1;u)
5. v : polynom(n - 1) List
6. polyform-lead-nonzero(n;[u / v])
7. u1 : polynom(n - 1)
8. v1 : polynom(n - 1) List
9. polyform-lead-nonzero(n;[u1 / v1])
10. poly-zero(n;[u / v]) = ff
11. poly-zero(n;[u1 / v1]) = ff
12. ¬(n = 0 ∈ ℤ)
13. ∀[p,q:polynom(n - 1)].
(poly-zero(n - 1;mul-polynom(n - 1;p;q)) = ff) supposing (poly-zero(n - 1;q) = ff and poly-zero(n - 1;p) = ff)
14. ¬False
15. ¬False
16. ¬↑poly-zero(n - 1;u1)
17. ¬False
18. [mul-polynom(n - 1;u;u1) / map(λx.mul-polynom(n - 1;u;x);v1)] ∈ polyform(n - 1) List
19. ¬(n = 0 ∈ ℤ)
20. X : polyform(n - 1)
21. mul-polynom(n - 1;u;u1) = X ∈ polyform(n - 1)
22. q : {q:polyform(n - 1) List| ||v1|| ≤ ||q||}
23. map(λx.mul-polynom(n - 1;u;x);v1) = q ∈ {q:polyform(n - 1) List| ||v1|| ≤ ||q||}
⊢ poly-zero(n - 1;X) = ff
⇒ null(eager-accum(z,a.add-polynom(n;tt;if null(z) then [] else z @ [polyconst(n - 1;0)] fi ;if poly-zero(n - 1;a)
then []
else [mul-polynom(n - 1;a;u1) / map(λx.mul-polynom(n - 1;a;x);v1)]
fi );[X / q];v))
= ff
Latex:
Latex:
1. n : \mBbbN{}
2. \mforall{}n:\mBbbN{}n
\mforall{}[p,q:polynom(n)].
(poly-zero(n;mul-polynom(n;p;q)) = ff) supposing
(poly-zero(n;q) = ff and
poly-zero(n;p) = ff)
3. u : polynom(n - 1)
4. \mneg{}\muparrow{}poly-zero(n - 1;u)
5. v : polynom(n - 1) List
6. polyform-lead-nonzero(n;[u / v])
7. u1 : polynom(n - 1)
8. v1 : polynom(n - 1) List
9. polyform-lead-nonzero(n;[u1 / v1])
10. poly-zero(n;[u / v]) = ff
11. poly-zero(n;[u1 / v1]) = ff
12. \mneg{}(n = 0)
13. \mforall{}[p,q:polynom(n - 1)].
(poly-zero(n - 1;mul-polynom(n - 1;p;q)) = ff) supposing
(poly-zero(n - 1;q) = ff and
poly-zero(n - 1;p) = ff)
14. \mneg{}False
15. \mneg{}False
16. \mneg{}\muparrow{}poly-zero(n - 1;u1)
17. \mneg{}False
18. [mul-polynom(n - 1;u;u1) / map(\mlambda{}x.mul-polynom(n - 1;u;x);v1)] \mmember{} polyform(n - 1) List
\mvdash{} poly-zero(n;eager-accum(z,a.add-polynom(n;tt;if null(z)
then []
else z @ [polyconst(n - 1;0)]
fi ;if poly-zero(n - 1;a)
then []
else [mul-polynom(n - 1;a;u1) / map(\mlambda{}x.mul-polynom(n - 1;a;x);v1)]
fi );[mul-polynom(n - 1;u;u1) / map(\mlambda{}x.mul-polynom(n - 1;u;x);v1)];v))
= ff
By
Latex:
(RW (AddrC [2] UnfoldTopAbC) 0
THEN (SplitOnConclITE THEN Try (Complete (Auto)))
THEN (InstHyp [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}u1\mkleeneclose{}] (-7)\mcdot{} THENA Auto)
THEN (MoveToConcl (-1) THEN (GenConcl \mkleeneopen{}mul-polynom(n - 1;u;u1) = X\mkleeneclose{}\mcdot{} THENA Auto))
THEN (GenConcl \mkleeneopen{}map(\mlambda{}x.mul-polynom(n - 1;u;x);v1) = q\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index