---

Step * of Lemma mapfilter-as-accum-aux

∀[A:Type]. ∀[p:A ⟶ 𝔹]. ∀[L:A List]. ∀[X:Top List]. ∀[f:Top].
  (X @ mapfilter(f;p;L) ~ accumulate (with value a and list item x):
                           if p[x] then a @ [f[x]] else a fi 
                          over list:
                            L
                          with starting value:
                           X))
BY
{ ((Unfold `mapfilter` 0 THEN Unfold `so_apply` 0)
   THEN InductionOnList
   THEN Reduce 0
   THEN ((UnivCD THENA Auto) THEN RWW "append-nil" 0 THEN Auto)
   THEN AutoSplit
   THEN (xxxRWO "5<" 0xxx THEN (RWW "append_assoc_sq" 0 THEN Reduce 0) THEN Try (Complete (Auto)))⋅) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[p:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].  \mforall{}[X:Top  List].  \mforall{}[f:Top].
    (X  @  mapfilter(f;p;L)  \msim{}  accumulate  (with  value  a  and  list  item  x):
                                                      if  p[x]  then  a  @  [f[x]]  else  a  fi 
                                                    over  list:
                                                        L
                                                    with  starting  value:
                                                      X))


By

---

Latex:
((Unfold  `mapfilter`  0  THEN  Unfold  `so\_apply`  0)
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  ((UnivCD  THENA  Auto)  THEN  RWW  "append-nil"  0  THEN  Auto)
  THEN  AutoSplit
  THEN  (xxxRWO  "5<"  0xxx  THEN  (RWW  "append\_assoc\_sq"  0  THEN  Reduce  0)  THEN  Try  (Complete  (Auto)))\mcdot{})

---

Home Index