---

Step * of Lemma filter-as-accum-aux

∀[A:Type]. ∀[p:A ⟶ 𝔹]. ∀[L:A List]. ∀[X:Top List].
  (filter(p;rev(L)) @ X ~ accumulate (with value a and list item x):
                           if p[x] then [x / a] else a fi 
                          over list:
                            L
                          with starting value:
                           X))
BY
{ xxx(InductionOnList
      THEN Reduce 0
      THEN Auto
      THEN (RWO "filter_append" 0 THENA Auto)
      THEN Reduce 0
      THEN RepeatFor 2 (AutoSplit)
      THEN Auto
      THEN Try ((RWO "append-nil" 0 THEN Auto))
      THEN (RWO "append_assoc_sq" 0 THENA Auto)
      THEN RWO "-4" 0
      THEN Reduce 0
      THEN Auto)xxx }

---

Latex:

---

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


By

---

Latex:
xxx(InductionOnList
        THEN  Reduce  0
        THEN  Auto
        THEN  (RWO  "filter\_append"  0  THENA  Auto)
        THEN  Reduce  0
        THEN  RepeatFor  2  (AutoSplit)
        THEN  Auto
        THEN  Try  ((RWO  "append-nil"  0  THEN  Auto))
        THEN  (RWO  "append\_assoc\_sq"  0  THENA  Auto)
        THEN  RWO  "-4"  0
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index