---

Step * 2 of Lemma select_concat

.....wf..... 
1. T : Type
⊢ λll.∀n:ℕ||concat(ll)||
        ∃m:ℕ||ll||
         ((||concat(firstn(m;ll))|| ≤ n)
         c∧ n - ||concat(firstn(m;ll))|| < ||ll[m]||
         c∧ (concat(ll)[n] = ll[m][n - ||concat(firstn(m;ll))||] ∈ T)) ∈ (T List List) ⟶ ℙ
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
\mvdash{}  \mlambda{}ll.\mforall{}n:\mBbbN{}||concat(ll)||
                \mexists{}m:\mBbbN{}||ll||
                  ((||concat(firstn(m;ll))||  \mleq{}  n)
                  c\mwedge{}  n  -  ||concat(firstn(m;ll))||  <  ||ll[m]||
                  c\mwedge{}  (concat(ll)[n]  =  ll[m][n  -  ||concat(firstn(m;ll))||]))  \mmember{}  (T  List  List)  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
Auto

---

Home Index