---

Step * of Lemma mul-polynom_wf

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

1
1. n : ℤ
2. 0 < n
3. ∀[p,q:polyform(n - 1)].  (mul-polynom(n - 1;p;q) ∈ polyform(n - 1))
4. p : polyform(n)
5. q : polyform(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 map(λx.mul-polynom(n - 1;a;x);q)
  fi );polyconst(n;0);p) ∈ polyform(n)

---

Latex:

---

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


By

---

Latex:
(InductionOnNat
  THEN  RecUnfold  `mul-polynom`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  Thin  (-1)
  THEN  Thin  (-2)
  THEN  Thin  2)

---

Home Index