---

Step * 5 of Lemma select_concat


1. [T] : Type
2. ∀L:T List List. ∀n:ℕ||concat(L)||.
     ∃m:ℕ||L||
      ((||concat(firstn(m;L))|| ≤ n)
      c∧ n - ||concat(firstn(m;L))|| < ||L[m]||
      c∧ (concat(L)[n] = L[m][n - ||concat(firstn(m;L))||] ∈ T))
⊢ ∀ll:T List List. ∀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))
BY
{ Auto }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}L:T  List  List.  \mforall{}n:\mBbbN{}||concat(L)||.
          \mexists{}m:\mBbbN{}||L||
            ((||concat(firstn(m;L))||  \mleq{}  n)
            c\mwedge{}  n  -  ||concat(firstn(m;L))||  <  ||L[m]||
            c\mwedge{}  (concat(L)[n]  =  L[m][n  -  ||concat(firstn(m;L))||]))
\mvdash{}  \mforall{}ll:T  List  List.  \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))||]))


By

---

Latex:
Auto

---

Home Index