---

Step * 2 1 1 1 1 1 1 2 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
⊢ poly-zero(n;let z ⟵ [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
BY
{ ((Assert [mul-polynom(n - 1;u;u1) / map(λx.mul-polynom(n - 1;u;x);v1)] ∈ polyform(n - 1) List BY
          Auto)
   THEN (CallByValueReduce 0 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
⊢ 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

---

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
\mvdash{}  poly-zero(n;let  z  \mleftarrow{}{}  [mul-polynom(n  -  1;u;u1)  /  map(\mlambda{}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(\mlambda{}x.mul-polynom(n  -  1;a;x);v1)]
                            fi  );z;v)) 
=  ff


By

---

Latex:
((Assert  [mul-polynom(n  -  1;u;u1)  /  map(\mlambda{}x.mul-polynom(n  -  1;u;x);v1)]  \mmember{}  polyform(n  -  1)  List  BY
                Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  )

---

Home Index