---

Step * 1 3 1 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. Σ(||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
BY
{ ((Assert ⌜(m = i ∈ ℤ) ∨ m < i ∨ (m > i)⌝⋅ THENA Auto) THEN D (-1)) }

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]||
8. m = i ∈ ℤ
⊢ ll[i][j] = ll[m][(Σ(||ll[k]|| | k < i) + j) - ||concat(firstn(m;ll))||] ∈ T

2
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]||
8. m < i ∨ (m > i)
⊢ 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.  \mSigma{}(||ll[i]||  |  i  <  m)  \mleq{}  (\mSigma{}(||ll[k]||  |  k  <  i)  +  j)
7.  (\mSigma{}(||ll[k]||  |  k  <  i)  +  j)  -  \mSigma{}(||ll[i]||  |  i  <  m)  <  ||ll[m]||
\mvdash{}  ll[i][j]  =  ll[m][(\mSigma{}(||ll[k]||  |  k  <  i)  +  j)  -  ||concat(firstn(m;ll))||]


By

---

Latex:
((Assert  \mkleeneopen{}(m  =  i)  \mvee{}  m  <  i  \mvee{}  (m  >  i)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  (-1))

---

Home Index