---

Step * 1 1 1 of Lemma primtailrec-unroll


1. n : ℤ
2. b : Top
3. c : Top
4. 1 ≤ n
5. m : ℤ
6. i : ℤ
⊢ ∀u:Top. (primtailrec(1;i;u;c) ~ c (0 + i) primtailrec(0;i;u;c))
BY
{ (RepeatFor 2 ((Unfold `primtailrec` 0 THEN Reduce 0)) THEN Auto THEN CallByValueReduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  b  :  Top
3.  c  :  Top
4.  1  \mleq{}  n
5.  m  :  \mBbbZ{}
6.  i  :  \mBbbZ{}
\mvdash{}  \mforall{}u:Top.  (primtailrec(1;i;u;c)  \msim{}  c  (0  +  i)  primtailrec(0;i;u;c))


By

---

Latex:
(RepeatFor  2  ((Unfold  `primtailrec`  0  THEN  Reduce  0))  THEN  Auto  THEN  CallByValueReduce  0  THEN  Auto)

---

Home Index