---

Step * 1 2 1 1 of Lemma select_concat_sum

.....assertion..... 
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)) ∈ ℤ
⊢ j < Σ(||ll[x + i]|| | x < ||ll|| - i)
BY
{ Thin (-1) }

1
1. T : Type
2. ll : T List List
3. i : ℕ||ll||
4. j : ℤ
5. 0 ≤ j
6. j < ||ll[i]||
⊢ j < Σ(||ll[x + i]|| | x < ||ll|| - i)

---

Latex:

---

Latex:
.....assertion..... 
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))
\mvdash{}  j  <  \mSigma{}(||ll[x  +  i]||  |  x  <  ||ll||  -  i)


By

---

Latex:
Thin  (-1)

---

Home Index