---

Step * 1 2 1 1 2 of Lemma listify_wf


1. T : Type
2. n : ℤ
3. m : {...n}
4. f : {m..n-} ⟶ T
5. ∀k:ℕ. ∀n:ℤ. ∀m:{...n}.  (n - m < k ⇒ (∀f:{m..n-} ⟶ T. (listify(f;m;n) ∈ T List)))
⊢ listify(f;m;n) ∈ T List
BY
{ (InstHyp [⌜(n - m) + 1⌝;⌜n⌝;⌜m⌝;⌜f⌝] (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  m  :  \{...n\}
4.  f  :  \{m..n\msupminus{}\}  {}\mrightarrow{}  T
5.  \mforall{}k:\mBbbN{}.  \mforall{}n:\mBbbZ{}.  \mforall{}m:\{...n\}.    (n  -  m  <  k  {}\mRightarrow{}  (\mforall{}f:\{m..n\msupminus{}\}  {}\mrightarrow{}  T.  (listify(f;m;n)  \mmember{}  T  List)))
\mvdash{}  listify(f;m;n)  \mmember{}  T  List


By

---

Latex:
(InstHyp  [\mkleeneopen{}(n  -  m)  +  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index