---

Step * 1 3 of Lemma select_concat_sum


1. T : Type
2. ll : T List List
3. i : ℕ||ll||
4. j : ℕ||ll[i]||
5. ∃m:ℕ||ll||
    ((||concat(firstn(m;ll))|| ≤ (Σ(||ll[k]|| | k < i) + j))
    c∧ (Σ(||ll[k]|| | k < i) + j) - ||concat(firstn(m;ll))|| < ||ll[m]||
    c∧ (concat(ll)[Σ(||ll[k]|| | k < i) + j] = ll[m][(Σ(||ll[k]|| | k < i) + j) - ||concat(firstn(m;ll))||] ∈ T))
⊢ ll[i][j] = concat(ll)[Σ(||ll[k]|| | k < i) + j] ∈ T
BY
{ (ExRepD THEN (HypSubst' (-1) 0 THENA Auto) THEN Thin (-1)) }

1
1. T : Type
2. ll : T List List
3. i : ℕ||ll||
4. j : ℕ||ll[i]||
5. m : ℕ||ll||
6. ||concat(firstn(m;ll))|| ≤ (Σ(||ll[k]|| | k < i) + j)
7. (Σ(||ll[k]|| | k < i) + j) - ||concat(firstn(m;ll))|| < ||ll[m]||
⊢ ll[i][j] = ll[m][(Σ(||ll[k]|| | k < i) + j) - ||concat(firstn(m;ll))||] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  ll  :  T  List  List
3.  i  :  \mBbbN{}||ll||
4.  j  :  \mBbbN{}||ll[i]||
5.  \mexists{}m:\mBbbN{}||ll||
        ((||concat(firstn(m;ll))||  \mleq{}  (\mSigma{}(||ll[k]||  |  k  <  i)  +  j))
        c\mwedge{}  (\mSigma{}(||ll[k]||  |  k  <  i)  +  j)  -  ||concat(firstn(m;ll))||  <  ||ll[m]||
        c\mwedge{}  (concat(ll)[\mSigma{}(||ll[k]||  |  k  <  i)  +  j]
              =  ll[m][(\mSigma{}(||ll[k]||  |  k  <  i)  +  j)  -  ||concat(firstn(m;ll))||]))
\mvdash{}  ll[i][j]  =  concat(ll)[\mSigma{}(||ll[k]||  |  k  <  i)  +  j]


By

---

Latex:
(ExRepD  THEN  (HypSubst'  (-1)  0  THENA  Auto)  THEN  Thin  (-1))

---

Home Index