---

Step * 1 1 2 of Lemma primtailrec-unroll


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))
BY
{ ((Subst' (m - 1) + 1 ~ m -2 THENA Auto) THEN (D 0 THENA Auto)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((Subst'  (m  -  1)  +  1  \msim{}  m  -2  THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index