---

Step * of Lemma primrec-wf-nat-plus

∀[P:ℕ+ ⟶ ℙ]. ∀[b:P[1]]. ∀[s:∀n:ℕ+. (P[n] ⇒ P[n + 1])]. ∀[n:ℕ+].  (primrec(n - 1;b;λi,x. (s (i + 1) x)) ∈ P[n])
BY
{ ((InstLemma `primrec-wf-upper` [⌜1⌝]⋅ THENA Auto) THEN RepeatFor 4 (ParallelLast)) }

---

Latex:

---

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


By

---

Latex:
((InstLemma  `primrec-wf-upper`  [\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RepeatFor  4  (ParallelLast))

---

Home Index