Step * of Lemma bag-mapfilter-fast-eq

`∀[A,B:Type]. ∀[bs:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]}  ⟶ B].`
`  (bag-mapfilter-fast(f;P;bs) = bag-mapfilter(f;P;bs) ∈ bag(B))`
BY
`{ (Auto`
`   THEN RepUR ``bag-mapfilter`` 0`
`   THEN (InstLemma `bag-map-as-accum` [⌜{x:A| ↑P[x]} ⌝;⌜B⌝;⌜f⌝;⌜[x∈bs|P x]⌝]⋅ THENA Auto)`
`   THEN (RWO "-1" 0 THENA Auto)`
`   THEN (InstLemma `bag-filter-as-accum` [⌜A⌝;⌜P⌝;⌜bs⌝]⋅ THENA Auto)`
`   THEN (RWO "-1" 0`
`         THENA (Auto`
`                THEN Repeat ((RWO "cons-bag-as-append" 0 THENA Auto))`
`                THEN (RWO "bag-append-assoc<" 0 THENA Auto)`
`                THEN (MemCD THEN Auto)`
`                THEN BLemma `bag-append-comm``
`                THEN Auto)`
`         )`
`   THEN RepeatFor 2 (Thin (-1))) }`

1
`1. A : Type`
`2. B : Type`
`3. bs : bag(A)`
`4. P : A ⟶ 𝔹`
`5. f : {x:A| ↑P[x]}  ⟶ B`
`⊢ bag-mapfilter-fast(f;P;bs) = bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};bs)) ∈ bag(B)`

Latex:

Latex:
\mforall{}[A,B:Type].  \mforall{}[bs:bag(A)].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:A|  \muparrow{}P[x]\}    {}\mrightarrow{}  B].
(bag-mapfilter-fast(f;P;bs)  =  bag-mapfilter(f;P;bs))

By

Latex:
(Auto
THEN  RepUR  ``bag-mapfilter``  0
THEN  (InstLemma  `bag-map-as-accum`  [\mkleeneopen{}\{x:A|  \muparrow{}P[x]\}  \mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}[x\mmember{}bs|P  x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
THEN  (RWO  "-1"  0  THENA  Auto)
THEN  (InstLemma  `bag-filter-as-accum`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
THEN  (RWO  "-1"  0
THENA  (Auto
THEN  Repeat  ((RWO  "cons-bag-as-append"  0  THENA  Auto))
THEN  (RWO  "bag-append-assoc<"  0  THENA  Auto)
THEN  (MemCD  THEN  Auto)
THEN  BLemma  `bag-append-comm`
THEN  Auto)
)
THEN  RepeatFor  2  (Thin  (-1)))

Home Index