---

Step * 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]||
⊢ j < ||concat(ll)|| - Σ(||ll[k]|| | k < i)
BY
{ (RWO "length_concat" 0
   THEN Auto
   THEN (InstLemma `sum_split` [⌜||ll||⌝;⌜λi.||ll[i]||⌝;⌜i⌝]⋅ THENA Auto)
   THEN RepUR ``so_apply`` (-1)) }

1
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[i]|| | i < ||ll||) - Σ(||ll[k]|| | k < i)

---

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]||
\mvdash{}  j  <  ||concat(ll)||  -  \mSigma{}(||ll[k]||  |  k  <  i)


By

---

Latex:
(RWO  "length\_concat"  0
  THEN  Auto
  THEN  (InstLemma  `sum\_split`  [\mkleeneopen{}||ll||\mkleeneclose{};\mkleeneopen{}\mlambda{}i.||ll[i]||\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``so\_apply``  (-1))

---

Home Index