---

Step * 4 of Lemma select_concat

.....antecedent..... 
1. [T] : Type
⊢ ∀aaaa:T List. ∀LLLL:T List List.
    ((∀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)))
    ⇒ (∀n:ℕ||concat([aaaa / LLLL])||
          ∃m:ℕ||[aaaa / LLLL]||
           ((||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
{ (Reduce 0 THEN Auto) }

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

---

Latex:

---

Latex:
.....antecedent..... 
1.  [T]  :  Type
\mvdash{}  \mforall{}aaaa:T  List.  \mforall{}LLLL:T  List  List.
        ((\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))||])))
        {}\mRightarrow{}  (\mforall{}n:\mBbbN{}||concat([aaaa  /  LLLL])||
                    \mexists{}m:\mBbbN{}||[aaaa  /  LLLL]||
                      ((||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:
(Reduce  0  THEN  Auto)

---

Home Index