---

Step * of Lemma primrec-wf

∀[P:ℕ ⟶ ℙ]. ∀[b:P[0]]. ∀[s:∀n:ℕ. (P[n] ⇒ P[n + 1])]. ∀[n:ℕ].  (primrec(n;b;s) ∈ P[n])
BY
{ (RepeatFor 4 ((D 0 THENA Auto)) THEN WeakNatInd (-1) THEN (RWO  "primrec-unroll" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

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


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  WeakNatInd  (-1)
  THEN  (RWO    "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index