---

Step * 1 2 1 2 of Lemma select_concat_sum


1. T : Type
2. ll : T List List
3. i : ℕ||ll||
4. j : ℤ
5. 0 ≤ j
6. j < ||ll[i]||
7. Σ(||ll[x]|| | x < ||ll||) = (Σ(||ll[x]|| | x < i) + Σ(||ll[x + i]|| | x < ||ll|| - i)) ∈ ℤ
8. j < Σ(||ll[x + i]|| | x < ||ll|| - i)
⊢ j < (Σ(||ll[x]|| | x < i) + Σ(||ll[x + i]|| | x < ||ll|| - i)) - Σ(||ll[k]|| | k < i)
BY
{ Auto' }

---

Latex:

---

Latex:

1.  T  :  Type
2.  ll  :  T  List  List
3.  i  :  \mBbbN{}||ll||
4.  j  :  \mBbbZ{}
5.  0  \mleq{}  j
6.  j  <  ||ll[i]||
7.  \mSigma{}(||ll[x]||  |  x  <  ||ll||)  =  (\mSigma{}(||ll[x]||  |  x  <  i)  +  \mSigma{}(||ll[x  +  i]||  |  x  <  ||ll||  -  i))
8.  j  <  \mSigma{}(||ll[x  +  i]||  |  x  <  ||ll||  -  i)
\mvdash{}  j  <  (\mSigma{}(||ll[x]||  |  x  <  i)  +  \mSigma{}(||ll[x  +  i]||  |  x  <  ||ll||  -  i))  -  \mSigma{}(||ll[k]||  |  k  <  i)


By

---

Latex:
Auto'

---

Home Index