---

Step * 2 of Lemma natrec_wf_intseg


1. k : ℤ
2. T : {k...} ⟶ Type
3. g : n:{k...} ⟶ (m:{k..n-} ⟶ T[m]) ⟶ T[n]
4. ∀n:ℕ. (letrec f(n)=g[n;f] in f  ∈ m:{k..k + n-} ⟶ T[m])
⊢ letrec f(n)=g[n;f] in
   f  ∈ n:{k...} ⟶ T[n]
BY
{ (Unfold `genrec` 0 THEN (RW (SweepUpC UnrollRecursionC) 0 THENA Auto) THEN Fold `genrec` 0 THEN Reduce 0 THEN Auto)⋅ }

1
1. k : ℤ
2. T : {k...} ⟶ Type
3. g : n:{k...} ⟶ (m:{k..n-} ⟶ T[m]) ⟶ T[n]
4. ∀n:ℕ. (letrec f(n)=g[n;f] in f  ∈ m:{k..k + n-} ⟶ T[m])
5. n : {k...}@i
⊢ letrec f(n)=g[n;f] in
   f  ∈ m:{k..n-} ⟶ T[m]

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  T  :  \{k...\}  {}\mrightarrow{}  Type
3.  g  :  n:\{k...\}  {}\mrightarrow{}  (m:\{k..n\msupminus{}\}  {}\mrightarrow{}  T[m])  {}\mrightarrow{}  T[n]
4.  \mforall{}n:\mBbbN{}.  (letrec  f(n)=g[n;f]  in  f    \mmember{}  m:\{k..k  +  n\msupminus{}\}  {}\mrightarrow{}  T[m])
\mvdash{}  letrec  f(n)=g[n;f]  in
      f    \mmember{}  n:\{k...\}  {}\mrightarrow{}  T[n]


By

---

Latex:
(Unfold  `genrec`  0
  THEN  (RW  (SweepUpC  UnrollRecursionC)  0  THENA  Auto)
  THEN  Fold  `genrec`  0
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index