---

Step * of Lemma primrec-unroll-1

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

---

Latex:

---

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


By

---

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

---

Home Index