---

Step * 1 1 of Lemma primtailrec-unroll

.....assertion..... 
1. n : ℤ
2. b : Top
3. c : Top
4. 1 ≤ n
⊢ ∀m:ℕ. ∀i:ℤ. ∀u:Top.  (primtailrec(m + 1;i;u;c) ~ c (m + i) primtailrec(m;i;u;c))
BY
{ (InductionOnNat THEN Intro THEN Reduce 0) }

1
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))

2
1. n : ℤ
2. b : Top
3. c : Top
4. 1 ≤ n
5. m : ℤ
6. 0 < m
7. ∀i:ℤ. ∀u:Top.  (primtailrec((m - 1) + 1;i;u;c) ~ c ((m - 1) + i) primtailrec(m - 1;i;u;c))
8. i : ℤ
⊢ ∀u:Top. (primtailrec(m + 1;i;u;c) ~ c (m + i) primtailrec(m;i;u;c))

---

Latex:

---

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


By

---

Latex:
(InductionOnNat  THEN  Intro  THEN  Reduce  0)

---

Home Index