---

Step * of Lemma l_sum_filter0

∀[L:ℤ List]. (l_sum(L) = l_sum(filter(λx.(¬b(x =z 0));L)) ∈ ℤ)
BY
{ (Unfold `l_sum` 0 THEN InductionOnList THEN Reduce 0 THEN Auto THEN AutoSplit THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  (l\_sum(L)  =  l\_sum(filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  0));L)))


By

---

Latex:
(Unfold  `l\_sum`  0  THEN  InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  AutoSplit  THEN  Auto')

---

Home Index