---

Step * 2 1 1 1 1 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. v : polynom(n - 1) List
5. polyform-lead-nonzero(n;[u / v])
6. u1 : polynom(n - 1)
7. v1 : polynom(n - 1) List
8. polyform-lead-nonzero(n;[u1 / v1])
9. poly-zero(n;[u / v]) = ff
10. poly-zero(n;[u1 / v1]) = ff
11. ¬(n = 0 ∈ ℤ)
12. ∀[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)
13. ¬False
14. ¬False
15. ¬↑poly-zero(n - 1;u1)
16. ¬↑poly-zero(n - 1;u)
⊢ poly-zero(n;let z ⟵ add-polynom(n;tt;if null(polyconst(n;0))
              then []
              else polyconst(n;0) @ [polyconst(n - 1;0)]
              fi ;if poly-zero(n - 1;u) then [] else [mul-polynom(n - 1;u;u1) / map(λx.mul-polynom(n - 1;u;x);v1)] fi )
              in 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 );z;v)) 
= ff
BY
{ ((Subst' null(polyconst(n;0)) ~ tt 0 THENA (RecUnfold `polyconst` 0 THEN Reduce 0 THEN Auto))
   THEN Reduce 0
   THEN (BoolCase ⌜poly-zero(n - 1;u)⌝⋅ THENA Auto)
   THEN Try (Trivial)) }

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
⊢ poly-zero(n;let z ⟵ add-polynom(n;tt;[];[mul-polynom(n - 1;u;u1) / map(λx.mul-polynom(n - 1;u;x);v1)])
              in 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 );z;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.  v  :  polynom(n  -  1)  List
5.  polyform-lead-nonzero(n;[u  /  v])
6.  u1  :  polynom(n  -  1)
7.  v1  :  polynom(n  -  1)  List
8.  polyform-lead-nonzero(n;[u1  /  v1])
9.  poly-zero(n;[u  /  v])  =  ff
10.  poly-zero(n;[u1  /  v1])  =  ff
11.  \mneg{}(n  =  0)
12.  \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)
13.  \mneg{}False
14.  \mneg{}False
15.  \mneg{}\muparrow{}poly-zero(n  -  1;u1)
16.  \mneg{}\muparrow{}poly-zero(n  -  1;u)
\mvdash{}  poly-zero(n;let  z  \mleftarrow{}{}  add-polynom(n;tt;if  null(polyconst(n;0))
                            then  []
                            else  polyconst(n;0)  @  [polyconst(n  -  1;0)]
                            fi  ;if  poly-zero(n  -  1;u)
                            then  []
                            else  [mul-polynom(n  -  1;u;u1)  /  map(\mlambda{}x.mul-polynom(n  -  1;u;x);v1)]
                            fi  )
                            in  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  );z;v)) 
=  ff


By

---

Latex:
((Subst'  null(polyconst(n;0))  \msim{}  tt  0  THENA  (RecUnfold  `polyconst`  0  THEN  Reduce  0  THEN  Auto))
  THEN  Reduce  0
  THEN  (BoolCase  \mkleeneopen{}poly-zero(n  -  1;u)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Trivial))

---

Home Index