---

Step * of Lemma l_sum_as_reduce_general

∀[T:Type]. ∀[f:T ⟶ ℤ]. ∀[L:T List]. ∀[x:ℤ].  (reduce(λa,s. (s + f[a]);x;L) ~ 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{}].    (reduce(\mlambda{}a,s.  (s  +  f[a]);x;L)  \msim{}  l\_sum(map(\mlambda{}x.f[x];L))  \000C+  x)


By

---

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

---

Home Index