---

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)
   THENL [(RecUnfold `polynom` 0 THEN Reduce 0 THEN Auto)
         ; ((Decide ⌜n = 0 ∈ ℤ⌝⋅ THENA Auto) THEN Reduce 0 THEN Auto THEN Thin (-1) THEN Thin (-2))]
) }

1
1. n : ℤ
2. 0 < n
3. ∀[p,q:polynom(n - 1)].  (mul-polynom(n - 1;p;q) ∈ polynom(n - 1))
4. ¬(n = 0 ∈ ℤ)
5. p : polynom(n)
6. q : polynom(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) ∈ 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)
  THENL  [(RecUnfold  `polynom`  0  THEN  Reduce  0  THEN  Auto)
              ;  ((Decide  \mkleeneopen{}n  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Reduce  0  THEN  Auto  THEN  Thin  (-1)  THEN  Thin  (-2))]
)

---

Home Index