---

Step * of Lemma select_concat

∀[T:Type]
  ∀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
{ ((D 0 THENA Auto)
   THEN InstLemma `list_induction` [⌜T List⌝;⌜λ2ll.∀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))⌝]⋅
   ) }

1
.....wf..... 
1. T : Type
⊢ T List ∈ Type

2
.....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) ⟶ ℙ

3
.....antecedent..... 
1. [T] : Type
⊢ ∀n:ℕ||concat([])||
    ∃m:ℕ||[]||
     ((||concat(firstn(m;[]))|| ≤ n)
     c∧ n - ||concat(firstn(m;[]))|| < ||[][m]||
     c∧ (concat([])[n] = [][m][n - ||concat(firstn(m;[]))||] ∈ T))

4
.....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))))

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

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \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:
((D  0  THENA  Auto)
  THEN  InstLemma  `list\_induction`  [\mkleeneopen{}T  List\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}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))||]))\mkleeneclose{}]\mcdot{}
  )

---

Home Index