---

Step * 2 1 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])
5. n : {k...}@i
⊢ letrec f(n)=g[n;f] in
   f  ∈ m:{k..n-} ⟶ T[m]
BY
{ (InstHyp [⌜n - k⌝] (-2)⋅ THEN Auto' THEN GenConclAtAddr [2] THEN Auto)⋅ }

---

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])
5.  n  :  \{k...\}@i
\mvdash{}  letrec  f(n)=g[n;f]  in
      f    \mmember{}  m:\{k..n\msupminus{}\}  {}\mrightarrow{}  T[m]


By

---

Latex:
(InstHyp  [\mkleeneopen{}n  -  k\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto'  THEN  GenConclAtAddr  [2]  THEN  Auto)\mcdot{}

---

Home Index