---

Step * of Lemma primrec-wf2

∀[P:ℕ ⟶ ℙ]. ∀[b:P[0]]. ∀[s:∀n:{n:ℤ| 0 < n} . (P[n - 1] ⇒ P[n])]. ∀[n:ℕ].  (primrec(n;b;λi,x. (s (i + 1) x)) ∈ 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:\{n:\mBbbZ{}|  0  <  n\}  .  (P[n  -  1]  {}\mRightarrow{}  P[n])].  \mforall{}[n:\mBbbN{}].
    (primrec(n;b;\mlambda{}i,x.  (s  (i  +  1)  x))  \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