---

Step * of Lemma rm-zeros_wf

∀[n:ℕ+]. ∀[p:polynom(n - 1) List].  (rm-zeros(n - 1;p) ∈ polynom(n))
BY
{ ((Intros THEN RecUnfold `polynom` 0⋅ THEN (Unhide THENA Auto))
   THEN SplitOnConclITE
   THEN Auto
   THEN ListInd 2
   THEN RepUR ``rm-zeros`` 0
   THEN Try (Fold `rm-zeros` 0)) }

1
1. n : ℕ+
2. ¬(n = 0 ∈ ℤ)
⊢ [] ∈ {p:polynom(n - 1) List| polyform-lead-nonzero(n;p)} 

2
1. n : ℕ+
2. ¬(n = 0 ∈ ℤ)
3. u : polynom(n - 1)
4. v : polynom(n - 1) List
5. rm-zeros(n - 1;v) ∈ {p:polynom(n - 1) List| polyform-lead-nonzero(n;p)} 
⊢ if poly-zero(n - 1;u) then rm-zeros(n - 1;v) else [u / v] fi  ∈ {p:polynom(n - 1) List| polyform-lead-nonzero(n;p)} 

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[p:polynom(n  -  1)  List].    (rm-zeros(n  -  1;p)  \mmember{}  polynom(n))


By

---

Latex:
((Intros  THEN  RecUnfold  `polynom`  0\mcdot{}  THEN  (Unhide  THENA  Auto))
  THEN  SplitOnConclITE
  THEN  Auto
  THEN  ListInd  2
  THEN  RepUR  ``rm-zeros``  0
  THEN  Try  (Fold  `rm-zeros`  0))

---

Home Index