---

Step * of Lemma list_accum-mapfilter

∀[T,U,A:Type]. ∀[f:A ⟶ U ⟶ A]. ∀[L:T List]. ∀[p:{a:T| (a ∈ L)}  ⟶ 𝔹]. ∀[g:{a:T| (a ∈ L) ∧ (↑(p a))}  ⟶ U]. ∀[x:A].
  (accumulate (with value a and list item x):
    f[a;x]
   over list:
     mapfilter(g;p;L)
   with starting value:
    x) ~ accumulate (with value a and list item x):
          if p x then f[a;g x] else a fi 
         over list:
           L
         with starting value:
          x))
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN ListInd (-1)
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN RepUR ``mapfilter`` 0
   THEN Try (Complete (Auto))
   THEN Repeat ((AutoSplit THENA Try (Complete (Auto))))
   THEN Try (Fold `mapfilter` 0)
   THEN OnMaybeHyp 8 (\h. (BHyp h⋅ THEN DoSubsume THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T,U,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  U  {}\mrightarrow{}  A].  \mforall{}[L:T  List].  \mforall{}[p:\{a:T|  (a  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[g:\{a:T| 
                                                                                                                                                          (a  \mmember{}  L)  \mwedge{}  (\muparrow{}(p  a))\} 
                                                                                                                                                        {}\mrightarrow{}  U].  \mforall{}[x:A].
    (accumulate  (with  value  a  and  list  item  x):
        f[a;x]
      over  list:
          mapfilter(g;p;L)
      with  starting  value:
        x)  \msim{}  accumulate  (with  value  a  and  list  item  x):
                    if  p  x  then  f[a;g  x]  else  a  fi 
                  over  list:
                      L
                  with  starting  value:
                    x))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  RepUR  ``mapfilter``  0
  THEN  Try  (Complete  (Auto))
  THEN  Repeat  ((AutoSplit  THENA  Try  (Complete  (Auto))))
  THEN  Try  (Fold  `mapfilter`  0)
  THEN  OnMaybeHyp  8  (\mbackslash{}h.  (BHyp  h\mcdot{}  THEN  DoSubsume  THEN  Auto)))

---

Home Index