---

Step * of Lemma primrec-wf-nsub

∀[b:ℕ+]. ∀[P:ℕb ⟶ ℙ]. ∀[init:P[0]]. ∀[s:∀n:ℕb - 1. (P[n] ⇒ P[n + 1])]. ∀[n:ℕb].  (primrec(n;init;s) ∈ P[n])
BY
{ (Auto THEN InstLemma `primrec-wf-int_seg` [⌜0⌝;⌜b⌝;⌜P⌝;⌜init⌝;⌜s⌝;⌜n⌝]⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  InstLemma  `primrec-wf-int\_seg`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}init\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index