---

Step * of Lemma primrec-unroll+1

∀[n:{n:ℤ| 0 < n} ]. ∀[b,c:Top].  (primrec(n + 1;b;c) ~ c n primrec(n;b;c))
BY
{ (Auto THEN RW (AddrC [1] (LemmaC `primrec-unroll-1`)) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\{n:\mBbbZ{}|  0  <  n\}  ].  \mforall{}[b,c:Top].    (primrec(n  +  1;b;c)  \msim{}  c  n  primrec(n;b;c))


By

---

Latex:
(Auto  THEN  RW  (AddrC  [1]  (LemmaC  `primrec-unroll-1`))  0  THEN  Auto)

---

Home Index