---

Step * 1 1 2 1 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;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)
BY
{ ((RW (AddrC [1] UnfoldTopAbC) 0 THEN AutoSplit)
   THEN (Subst' (m + 1) - 1 ~ m 0 THENA Auto)
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

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
⊢ primtailrec(m;i + 1;c 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;i;u;c)  \msim{}  c  ((m  -  1)  +  i)  primtailrec(m  -  1;i;u;c))
8.  i  :  \mBbbZ{}
9.  u  :  Top
\mvdash{}  primtailrec(m  +  1;i;u;c)  \msim{}  c  (m  +  i)  primtailrec(m;i;u;c)


By

---

Latex:
((RW  (AddrC  [1]  UnfoldTopAbC)  0  THEN  AutoSplit)
  THEN  (Subst'  (m  +  1)  -  1  \msim{}  m  0  THENA  Auto)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index