---

Step * of Lemma polyconst_wf

∀[n:ℕ]. ∀[k:ℤ].  (polyconst(n;k) ∈ polyform(n))
BY
{ (InductionOnNat
   THEN RecUnfold `polyconst` 0
   THEN RecUnfold `polyform` 0
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN Try (Trivial)
   THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))) }

1
.....subterm..... T:t
4:n
1. n : ℤ
2. 0 < n
3. ∀[k:ℤ]. (polyconst(n - 1;k) ∈ polyform(n - 1))
4. k : ℤ
5. ¬(n = 0 ∈ ℤ)
6. ¬(k = 0 ∈ ℤ)
⊢ eval m = n - 1 in
  eval c = polyconst(m;k) in
    [c] ∈ if (n =z 0) then ℤ else polyform(n - 1) List fi 

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[k:\mBbbZ{}].    (polyconst(n;k)  \mmember{}  polyform(n))


By

---

Latex:
(InductionOnNat
  THEN  RecUnfold  `polyconst`  0
  THEN  RecUnfold  `polyform`  0
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto)))))

---

Home Index