---

Step * of Lemma polynom_wf

∀[n:ℕ]. (polynom(n) ∈ Type)
BY
{ ((Assert ⌜∀n:ℕ. ((polynom(n) ∈ Type) ∧ (polynom(n) ⊆r polyform(n)))⌝⋅
   THENM ((D 0 THENA Auto) THEN InstHyp [⌜n⌝] 1⋅ THEN Auto)
   )
   THEN CompleteInductionOnNat
   THEN (RecUnfold `polynom` 0 THEN RecUnfold `polyform` 0)
   THEN (SplitOnConclITE THENA Auto)) }

1
.....truecase..... 
1. n : ℕ
2. ∀n:ℕn. ((polynom(n) ∈ Type) ∧ (polynom(n) ⊆r polyform(n)))
3. n = 0 ∈ ℤ
⊢ (ℤ ∈ Type) ∧ (ℤ ⊆r ℤ)

2
.....falsecase..... 
1. n : ℕ
2. ∀n:ℕn. ((polynom(n) ∈ Type) ∧ (polynom(n) ⊆r polyform(n)))
3. ¬(n = 0 ∈ ℤ)
⊢ ({p:polynom(n - 1) List| polyform-lead-nonzero(n;p)}  ∈ Type)
∧ ({p:polynom(n - 1) List| polyform-lead-nonzero(n;p)}  ⊆r (polyform(n - 1) List))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (polynom(n)  \mmember{}  Type)


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  ((polynom(n)  \mmember{}  Type)  \mwedge{}  (polynom(n)  \msubseteq{}r  polyform(n)))\mkleeneclose{}\mcdot{}
  THENM  ((D  0  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  1\mcdot{}  THEN  Auto)
  )
  THEN  CompleteInductionOnNat
  THEN  (RecUnfold  `polynom`  0  THEN  RecUnfold  `polyform`  0)
  THEN  (SplitOnConclITE  THENA  Auto))

---

Home Index