---

Step * of Lemma primrec-wf-upper

∀[k:ℤ]. ∀[P:{k...} ⟶ ℙ]. ∀[b:P[k]]. ∀[s:∀n:{k...}. (P[n] ⇒ P[n + 1])]. ∀[n:{k...}].
  (primrec(n - k;b;λi,x. (s (i + k) x)) ∈ P[n])
BY
{ RepeatFor 5 ((D 0 THENA Auto)) }

1
1. k : ℤ
2. P : {k...} ⟶ ℙ
3. b : P[k]
4. s : ∀n:{k...}. (P[n] ⇒ P[n + 1])
5. n : {k...}
⊢ primrec(n - k;b;λi,x. (s (i + k) x)) ∈ P[n]

---

Latex:

---

Latex:
\mforall{}[k:\mBbbZ{}].  \mforall{}[P:\{k...\}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[b:P[k]].  \mforall{}[s:\mforall{}n:\{k...\}.  (P[n]  {}\mRightarrow{}  P[n  +  1])].  \mforall{}[n:\{k...\}].
    (primrec(n  -  k;b;\mlambda{}i,x.  (s  (i  +  k)  x))  \mmember{}  P[n])


By

---

Latex:
RepeatFor  5  ((D  0  THENA  Auto))

---

Home Index