---

Step * of Lemma minus-polynom_wf2

∀[n:ℕ]. ∀[p:polynom(n)].  (minus-polynom(n;p) ∈ polynom(n))
BY
{ (InductionOnNat
   THEN Auto
   THEN RecUnfold `polynom` 0
   THEN Reduce 0
   THEN RecUnfold `minus-polynom` 0
   THEN ((SplitOnConclITE THEN Auto) ORELSE (Reduce 0 THEN Auto))
   THEN (RecUnfold `polynom` (-3) THEN SplitOnHypITE -3  THEN Auto)
   THEN DSetVars
   THEN MemTypeCD
   THEN Auto
   THEN Try ((RecUnfold `polyform` 0 THEN SplitOnConclITE THEN Auto))) }

1
.....set predicate..... 
1. n : ℤ
2. 0 < n
3. ∀[p:polynom(n - 1)]. (minus-polynom(n - 1;p) ∈ polynom(n - 1))
4. p : polynom(n - 1) List
5. polyform-lead-nonzero(n;p)
6. ¬(n = 0 ∈ ℤ)
7. ¬(n = 0 ∈ ℤ)
8. ¬(n = 0 ∈ ℤ)
⊢ polyform-lead-nonzero(n;map(λq.minus-polynom(n - 1;q);p))

---

Latex:

---

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


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  RecUnfold  `polynom`  0
  THEN  Reduce  0
  THEN  RecUnfold  `minus-polynom`  0
  THEN  ((SplitOnConclITE  THEN  Auto)  ORELSE  (Reduce  0  THEN  Auto))
  THEN  (RecUnfold  `polynom`  (-3)  THEN  SplitOnHypITE  -3    THEN  Auto)
  THEN  DSetVars
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  ((RecUnfold  `polyform`  0  THEN  SplitOnConclITE  THEN  Auto)))

---

Home Index