---

Step * of Lemma mul-polynom_wf2

∀[n:ℕ]. ∀[p,q:polynom(n)].  (mul-polynom(n;p;q) ∈ polynom(n))
BY
{ (InductionOnNat THEN RecUnfold `mul-polynom` 0 THEN Reduce 0) }

1
1. n : ℤ
⊢ ∀[p,q:polynom(0)].  (p * q ∈ polynom(0))

2
1. n : ℤ
2. 0 < n
3. ∀[p,q:polynom(n - 1)].  (mul-polynom(n - 1;p;q) ∈ polynom(n - 1))
⊢ ∀[p,q:polynom(n)].
    (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) ∈ polynom(n))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p,q:polynom(n)].    (mul-polynom(n;p;q)  \mmember{}  polynom(n))


By

---

Latex:
(InductionOnNat  THEN  RecUnfold  `mul-polynom`  0  THEN  Reduce  0)

---

Home Index