---

Step * of Lemma natrec_wf_intseg

∀[k:ℤ]. ∀[T:{k...} ⟶ Type]. ∀[g:n:{k...} ⟶ (m:{k..n-} ⟶ T[m]) ⟶ T[n]].  (letrec f(n)=g[n;f] in f ∈ n:{k...} ⟶ T[n])
BY
{ (Unfold `natrec` 0 THEN Auto THEN Assert ⌜∀n:ℕ. (letrec f(n)=g[n;f] in f  ∈ m:{k..k + n-} ⟶ T[m])⌝⋅) }

1
.....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])

2
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]

---

Latex:

---

Latex:
\mforall{}[k:\mBbbZ{}].  \mforall{}[T:\{k...\}  {}\mrightarrow{}  Type].  \mforall{}[g:n:\{k...\}  {}\mrightarrow{}  (m:\{k..n\msupminus{}\}  {}\mrightarrow{}  T[m])  {}\mrightarrow{}  T[n]].
    (letrec  f(n)=g[n;f]  in
        f  \mmember{}  n:\{k...\}  {}\mrightarrow{}  T[n])


By

---

Latex:
(Unfold  `natrec`  0
  THEN  Auto
  THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  (letrec  f(n)=g[n;f]  in  f    \mmember{}  m:\{k..k  +  n\msupminus{}\}  {}\mrightarrow{}  T[m])\mkleeneclose{}\mcdot{})

---

Home Index