---

Step * of Lemma polyvar_wf

∀[n:ℕ]. ∀[v:ℤ].  polyvar(n;v) ∈ polyform(n) supposing 0 < n
BY
{ (InductionOnNat
   THEN Auto
   THEN RecUnfold `polyform` 0
   THEN AutoSplit
   THEN RecUnfold `polyvar` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN RepeatFor 3 (AutoSplit)
   THEN (CallByValueReduce 0 THENA Auto)) }

1
1. n : ℤ
2. n ≠ 0
3. 0 < n
4. ∀[v:ℤ]. polyvar(n - 1;v) ∈ polyform(n - 1) supposing 0 < n - 1
5. v : ℤ
6. v ≠ 0
7. ¬n - 1 < v
8. ¬v < 0
9. 0 < n
⊢ eval a = polyvar(n - 1;v - 1) in
  [a] ∈ polyform(n - 1) List

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[v:\mBbbZ{}].    polyvar(n;v)  \mmember{}  polyform(n)  supposing  0  <  n


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  RecUnfold  `polyform`  0
  THEN  AutoSplit
  THEN  RecUnfold  `polyvar`  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  RepeatFor  3  (AutoSplit)
  THEN  (CallByValueReduce  0  THENA  Auto))

---

Home Index