---

Step * 1 of Lemma natrec_wf_intseg

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

---

Latex:

---

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


By

---

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

---

Home Index