---

Step * of Lemma l_sum-upper-bound

∀b:ℤ. ∀[L:ℤ List]. ((∀x∈L.x ≤ b) ⇒ (l_sum(L) ≤ (b * ||L||)))
BY
{ (InductionOnList
   THEN Unfold `l_sum` 0
   THEN Reduce 0
   THEN Try (Fold `l_sum` 0)
   THEN Try ((RWO "l_all_cons" 0 THEN Auto THEN ThinTrivial))
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}b:\mBbbZ{}.  \mforall{}[L:\mBbbZ{}  List].  ((\mforall{}x\mmember{}L.x  \mleq{}  b)  {}\mRightarrow{}  (l\_sum(L)  \mleq{}  (b  *  ||L||)))


By

---

Latex:
(InductionOnList
  THEN  Unfold  `l\_sum`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `l\_sum`  0)
  THEN  Try  ((RWO  "l\_all\_cons"  0  THEN  Auto  THEN  ThinTrivial))
  THEN  Auto')

---

Home Index