---

Step * of Lemma nonzero-mul-polynom

∀[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)
BY
{ (CompleteInductionOnNat
   THEN (UnivCD THENA Auto)
   THEN RecUnfold `mul-polynom` 0⋅
   THEN RepeatFor 4 ((CallByValueReduce 0 THENA Auto))
   THEN (CaseNat 0 `n' THENL [Reduce 0; (InstHyp [⌜n - 1⌝] 2⋅ 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. p : polynom(n)
4. q : polynom(n)
5. poly-zero(n;p) = ff
6. poly-zero(n;q) = ff
7. n = 0 ∈ ℤ
⊢ poly-zero(0;if poly-zero(0;p) then p if poly-zero(0;q) then q else p * q fi ) = ff

2
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. p : polynom(n)
4. q : polynom(n)
5. poly-zero(n;p) = ff
6. poly-zero(n;q) = ff
7. ¬(n = 0 ∈ ℤ)
8. ∀[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)
⊢ poly-zero(n;if poly-zero(n;p) then p
  if poly-zero(n;q) then q
  else if n=0
       then p * q
       else 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 map(λx.mul-polynom(n - 1;a;x);q)
            fi );polyconst(n;0);p)
  fi ) 
= ff

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \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)


By

---

Latex:
(CompleteInductionOnNat
  THEN  (UnivCD  THENA  Auto)
  THEN  RecUnfold  `mul-polynom`  0\mcdot{}
  THEN  RepeatFor  4  ((CallByValueReduce  0  THENA  Auto))
  THEN  (CaseNat  0  `n'  THENL  [Reduce  0;  (InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  2\mcdot{}  THENA  Auto)]))

---

Home Index