---

Step * 4 1 of Lemma select_concat


1. [T] : Type
2. aaaa : T List
3. LLLL : T List List
4. ∀n:ℕ||concat(LLLL)||
     ∃m:ℕ||LLLL||
      ((||concat(firstn(m;LLLL))|| ≤ n)
      c∧ n - ||concat(firstn(m;LLLL))|| < ||LLLL[m]||
      c∧ (concat(LLLL)[n] = LLLL[m][n - ||concat(firstn(m;LLLL))||] ∈ T))
5. n : ℕ||concat([aaaa / LLLL])||
⊢ ∃m:ℕ||LLLL|| + 1
   ((||concat(firstn(m;[aaaa / LLLL]))|| ≤ n)
   c∧ n - ||concat(firstn(m;[aaaa / LLLL]))|| < ||[aaaa / LLLL][m]||
   c∧ (concat([aaaa / LLLL])[n] = [aaaa / LLLL][m][n - ||concat(firstn(m;[aaaa / LLLL]))||] ∈ T))
BY
{ (RenameVar `u' 2
   THEN RenameVar `v' 3
   THEN Unfold `concat` 0
   THEN Reduce 0
   THEN Try (Fold `concat` 0)
   THEN (Decide ⌜n < ||u||⌝⋅ THENA Auto)) }

1
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))

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||
⊢ ∃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.  aaaa  :  T  List
3.  LLLL  :  T  List  List
4.  \mforall{}n:\mBbbN{}||concat(LLLL)||
          \mexists{}m:\mBbbN{}||LLLL||
            ((||concat(firstn(m;LLLL))||  \mleq{}  n)
            c\mwedge{}  n  -  ||concat(firstn(m;LLLL))||  <  ||LLLL[m]||
            c\mwedge{}  (concat(LLLL)[n]  =  LLLL[m][n  -  ||concat(firstn(m;LLLL))||]))
5.  n  :  \mBbbN{}||concat([aaaa  /  LLLL])||
\mvdash{}  \mexists{}m:\mBbbN{}||LLLL||  +  1
      ((||concat(firstn(m;[aaaa  /  LLLL]))||  \mleq{}  n)
      c\mwedge{}  n  -  ||concat(firstn(m;[aaaa  /  LLLL]))||  <  ||[aaaa  /  LLLL][m]||
      c\mwedge{}  (concat([aaaa  /  LLLL])[n]  =  [aaaa  /  LLLL][m][n  -  ||concat(firstn(m;[aaaa  /  LLLL]))||]))


By

---

Latex:
(RenameVar  `u'  2
  THEN  RenameVar  `v'  3
  THEN  Unfold  `concat`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `concat`  0)
  THEN  (Decide  \mkleeneopen{}n  <  ||u||\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index