---

Step * 1 1 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]||
⊢ (0 - Σ(||ll[k]|| | k < i)) ≤ j
BY
{ (Assert ⌜Σ(||ll[k]|| | k < i) ≥ 0 ⌝⋅
   THEN Auto'
   THEN (InstLemma `sum_lower_bound` [⌜i⌝;⌜0⌝;⌜λk.||ll[k]||⌝]⋅ THENA Auto)
   THEN All (RepUR ``so_apply``)
   THEN 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]||
\mvdash{}  (0  -  \mSigma{}(||ll[k]||  |  k  <  i))  \mleq{}  j


By

---

Latex:
(Assert  \mkleeneopen{}\mSigma{}(||ll[k]||  |  k  <  i)  \mgeq{}  0  \mkleeneclose{}\mcdot{}
  THEN  Auto'
  THEN  (InstLemma  `sum\_lower\_bound`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}\mlambda{}k.||ll[k]||\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto')

---

Home Index