---

Step * 1 1 2 1 1 1 of Lemma primtailrec-unroll


1. n : ℤ
2. b : Top
3. c : Top
4. 1 ≤ n
5. m : ℤ
6. ¬m + 1 < 1
7. 0 < m
8. ∀i:ℤ. ∀u:Top.  (primtailrec(m;i;u;c) ~ c ((m - 1) + i) primtailrec(m - 1;i;u;c))
9. i : ℤ
10. u : Top
11. primtailrec(m;i + 1;c i u;c) ~ c ((m - 1) + i + 1) primtailrec(m - 1;i + 1;c i u;c)
⊢ primtailrec(m;i + 1;c i u;c) ~ c (m + i) primtailrec(m;i;u;c)
BY
{ (HypSubst  (-1) 0 THEN EqCD) }

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

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

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  b  :  Top
3.  c  :  Top
4.  1  \mleq{}  n
5.  m  :  \mBbbZ{}
6.  \mneg{}m  +  1  <  1
7.  0  <  m
8.  \mforall{}i:\mBbbZ{}.  \mforall{}u:Top.    (primtailrec(m;i;u;c)  \msim{}  c  ((m  -  1)  +  i)  primtailrec(m  -  1;i;u;c))
9.  i  :  \mBbbZ{}
10.  u  :  Top
11.  primtailrec(m;i  +  1;c  i  u;c)  \msim{}  c  ((m  -  1)  +  i  +  1)  primtailrec(m  -  1;i  +  1;c  i  u;c)
\mvdash{}  primtailrec(m;i  +  1;c  i  u;c)  \msim{}  c  (m  +  i)  primtailrec(m;i;u;c)


By

---

Latex:
(HypSubst    (-1)  0  THEN  EqCD)

---

Home Index