---

Step * of Lemma l_sum_as_accum

∀[T:Type]. ∀[f:T ⟶ ℤ]. ∀[L:T List]. ∀[x:ℤ].
  (accumulate (with value s and list item a):
    s + f[a]
   over list:
     L
   with starting value:
    x) ~ l_sum(map(λx.f[x];L)) + x)
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN RWO "-2" 0 THEN Auto THEN RepUR ``so_apply`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[L:T  List].  \mforall{}[x:\mBbbZ{}].
    (accumulate  (with  value  s  and  list  item  a):
        s  +  f[a]
      over  list:
          L
      with  starting  value:
        x)  \msim{}  l\_sum(map(\mlambda{}x.f[x];L))  +  x)


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "-2"  0
  THEN  Auto
  THEN  RepUR  ``so\_apply``  0
  THEN  Auto)

---

Home Index