---

Step * 1 3 1 of Lemma select_concat_sum


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
BY
{ ((RWO "length_concat" (-2) THENA Auto)
   THEN (RWO "length_concat" (-1) THENA Auto)
   THEN (RWO "length_firstn" (-1) THENA Auto)
   THEN (RWO "length_firstn" (-2) THENA Auto)
   THEN (RWO "select_firstn" (-2) THENA Auto)
   THEN (RWO "select_firstn" (-1) THENA Auto)) }

1
1. T : Type
2. ll : T List List
3. i : ℕ||ll||
4. j : ℕ||ll[i]||
5. m : ℕ||ll||
6. Σ(||ll[i]|| | i < m) ≤ (Σ(||ll[k]|| | k < i) + j)
7. (Σ(||ll[k]|| | k < i) + j) - Σ(||ll[i]|| | i < m) < ||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.  m  :  \mBbbN{}||ll||
6.  ||concat(firstn(m;ll))||  \mleq{}  (\mSigma{}(||ll[k]||  |  k  <  i)  +  j)
7.  (\mSigma{}(||ll[k]||  |  k  <  i)  +  j)  -  ||concat(firstn(m;ll))||  <  ||ll[m]||
\mvdash{}  ll[i][j]  =  ll[m][(\mSigma{}(||ll[k]||  |  k  <  i)  +  j)  -  ||concat(firstn(m;ll))||]


By

---

Latex:
((RWO  "length\_concat"  (-2)  THENA  Auto)
  THEN  (RWO  "length\_concat"  (-1)  THENA  Auto)
  THEN  (RWO  "length\_firstn"  (-1)  THENA  Auto)
  THEN  (RWO  "length\_firstn"  (-2)  THENA  Auto)
  THEN  (RWO  "select\_firstn"  (-2)  THENA  Auto)
  THEN  (RWO  "select\_firstn"  (-1)  THENA  Auto))

---

Home Index