---

Step * of Lemma list_accum_filter

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List]. ∀[f,y:Top].
  (accumulate (with value a and list item b):
    f[a;b]
   over list:
     filter(λb.P[b];l)
   with starting value:
    y) ~ accumulate (with value a and list item b):
          if P[b] then f[a;b] else a fi 
         over list:
           l
         with starting value:
          y))
BY
{ (InductionOnList THEN (UnivCD THENA Auto) THEN Reduce 0 THEN ((AutoSplit THEN BackThruSomeHyp) ORELSE Trivial)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[l:T  List].  \mforall{}[f,y:Top].
    (accumulate  (with  value  a  and  list  item  b):
        f[a;b]
      over  list:
          filter(\mlambda{}b.P[b];l)
      with  starting  value:
        y)  \msim{}  accumulate  (with  value  a  and  list  item  b):
                    if  P[b]  then  f[a;b]  else  a  fi 
                  over  list:
                      l
                  with  starting  value:
                    y))


By

---

Latex:
(InductionOnList
  THEN  (UnivCD  THENA  Auto)
  THEN  Reduce  0
  THEN  ((AutoSplit  THEN  BackThruSomeHyp)  ORELSE  Trivial))

---

Home Index