---

Step * 4 1 1 of Lemma select_concat


1. [T] : Type
2. u : T List
3. v : T List List
4. ∀n:ℕ||concat(v)||
     ∃m:ℕ||v||
      ((||concat(firstn(m;v))|| ≤ n)
      c∧ n - ||concat(firstn(m;v))|| < ||v[m]||
      c∧ (concat(v)[n] = v[m][n - ||concat(firstn(m;v))||] ∈ T))
5. n : ℕ||concat([u / v])||
6. n < ||u||
⊢ ∃m:ℕ||v|| + 1
   ((||concat(firstn(m;[u / v]))|| ≤ n)
   c∧ n - ||concat(firstn(m;[u / v]))|| < ||[u / v][m]||
   c∧ (u @ concat(v)[n] = [u / v][m][n - ||concat(firstn(m;[u / v]))||] ∈ T))
BY
{ InstConcl [⌜0⌝] ⋅ }

1
.....wf..... 
1. T : Type
2. u : T List
3. v : T List List
4. ∀n:ℕ||concat(v)||
     ∃m:ℕ||v||
      ((||concat(firstn(m;v))|| ≤ n)
      c∧ n - ||concat(firstn(m;v))|| < ||v[m]||
      c∧ (concat(v)[n] = v[m][n - ||concat(firstn(m;v))||] ∈ T))
5. n : ℕ||concat([u / v])||
6. n < ||u||
⊢ 0 ∈ ℕ||v|| + 1

2
1. [T] : Type
2. u : T List
3. v : T List List
4. ∀n:ℕ||concat(v)||
     ∃m:ℕ||v||
      ((||concat(firstn(m;v))|| ≤ n)
      c∧ n - ||concat(firstn(m;v))|| < ||v[m]||
      c∧ (concat(v)[n] = v[m][n - ||concat(firstn(m;v))||] ∈ T))
5. n : ℕ||concat([u / v])||
6. n < ||u||
⊢ (||concat(firstn(0;[u / v]))|| ≤ n)
c∧ n - ||concat(firstn(0;[u / v]))|| < ||[u / v][0]||
c∧ (u @ concat(v)[n] = [u / v][0][n - ||concat(firstn(0;[u / v]))||] ∈ T)

3
.....wf..... 
1. T : Type
2. u : T List
3. v : T List List
4. ∀n:ℕ||concat(v)||
     ∃m:ℕ||v||
      ((||concat(firstn(m;v))|| ≤ n)
      c∧ n - ||concat(firstn(m;v))|| < ||v[m]||
      c∧ (concat(v)[n] = v[m][n - ||concat(firstn(m;v))||] ∈ T))
5. n : ℕ||concat([u / v])||
6. n < ||u||
7. m : ℕ||v|| + 1
⊢ (||concat(firstn(m;[u / v]))|| ≤ n)
  c∧ n - ||concat(firstn(m;[u / v]))|| < ||[u / v][m]||
  c∧ (u @ concat(v)[n] = [u / v][m][n - ||concat(firstn(m;[u / v]))||] ∈ T) ∈ ℙ

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  u  :  T  List
3.  v  :  T  List  List
4.  \mforall{}n:\mBbbN{}||concat(v)||
          \mexists{}m:\mBbbN{}||v||
            ((||concat(firstn(m;v))||  \mleq{}  n)
            c\mwedge{}  n  -  ||concat(firstn(m;v))||  <  ||v[m]||
            c\mwedge{}  (concat(v)[n]  =  v[m][n  -  ||concat(firstn(m;v))||]))
5.  n  :  \mBbbN{}||concat([u  /  v])||
6.  n  <  ||u||
\mvdash{}  \mexists{}m:\mBbbN{}||v||  +  1
      ((||concat(firstn(m;[u  /  v]))||  \mleq{}  n)
      c\mwedge{}  n  -  ||concat(firstn(m;[u  /  v]))||  <  ||[u  /  v][m]||
      c\mwedge{}  (u  @  concat(v)[n]  =  [u  /  v][m][n  -  ||concat(firstn(m;[u  /  v]))||]))


By

---

Latex:
InstConcl  [\mkleeneopen{}0\mkleeneclose{}]  \mcdot{}

---

Home Index