---

Step * of Lemma primtailrec-unroll

∀[n:ℤ]. ∀[b,c:Top].  (primtailrec(n;0;b;c) ~ if n <z 1 then b else c (n - 1) primtailrec(n - 1;0;b;c) fi )
BY
{ (Auto THEN (AutoSplit THENL [(Unfold `primtailrec` 0 THEN Auto); ((Assert 1 ≤ n BY Auto) THEN Thin 2)])) }

1
1. n : ℤ
2. b : Top
3. c : Top
4. 1 ≤ n
⊢ primtailrec(n;0;b;c) ~ c (n - 1) primtailrec(n - 1;0;b;c)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[b,c:Top].
    (primtailrec(n;0;b;c)  \msim{}  if  n  <z  1  then  b  else  c  (n  -  1)  primtailrec(n  -  1;0;b;c)  fi  )


By

---

Latex:
(Auto
  THEN  (AutoSplit  THENL  [(Unfold  `primtailrec`  0  THEN  Auto);  ((Assert  1  \mleq{}  n  BY  Auto)  THEN  Thin  2)])
  )

---

Home Index