---

Step * 1 of Lemma bag-filter-as-accum


1. A : Type
2. p : A ⟶ 𝔹
3. u : A
4. v : A List
5. [x∈v|p[x]] = bag-accum(b,x.if p[x] then x.b else b fi ;{};v) ∈ bag({x:A| ↑p[x]} )
⊢ [x∈[u / v]|p[x]] = bag-accum(b,x.if p[x] then x.b else b fi ;{};[u / v]) ∈ bag({x:A| ↑p[x]} )
BY
{ (RepUR ``bag-filter`` 0
   THEN Try (Fold `bag-filter` 0)
   THEN Try (Fold `cons-bag` 0)
   THEN OldAutoSplit
   THEN (RWO "-2" 0
         THENA (Auto
                THEN Repeat OldAutoSplit
                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 Thin (-2)
   THEN (RWO "cons-bag-as-append" 0 THENA Auto)
   THEN (InstLemma `bag-append-comm` [⌜A⌝;⌜{u}⌝;⌜v⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0
         THENA (Auto
                THEN Repeat OldAutoSplit
                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 Thin (-1)
   THEN RepUR ``bag-accum bag-append`` 0
   THEN (RWO "list_accum_append" 0 THENA (Auto THEN Unfold `single-bag` 0 THEN Auto))
   THEN Try (Folds ``bag-accum bag-append`` 0)
   THEN (RWO "bag-accum-single" 0 THENA Auto)
   THEN OldAutoSplit⋅) }

1
1. A : Type
2. p : A ⟶ 𝔹
3. u : A
4. v : A List
5. ↑p[u]
6. ↑p[u]
⊢ ({u} + bag-accum(b,x.if p[x] then x.b else b fi ;{};v))
= ({u} + bag-accum(b,x.if p[x] then {x} + b else b fi ;{};v))
∈ bag({x:A| ↑p[x]} )

---

Latex:

---

Latex:

1.  A  :  Type
2.  p  :  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  [x\mmember{}v|p[x]]  =  bag-accum(b,x.if  p[x]  then  x.b  else  b  fi  ;\{\};v)
\mvdash{}  [x\mmember{}[u  /  v]|p[x]]  =  bag-accum(b,x.if  p[x]  then  x.b  else  b  fi  ;\{\};[u  /  v])


By

---

Latex:
(RepUR  ``bag-filter``  0
  THEN  Try  (Fold  `bag-filter`  0)
  THEN  Try  (Fold  `cons-bag`  0)
  THEN  OldAutoSplit
  THEN  (RWO  "-2"  0
              THENA  (Auto
                            THEN  Repeat  OldAutoSplit
                            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  Thin  (-2)
  THEN  (RWO  "cons-bag-as-append"  0  THENA  Auto)
  THEN  (InstLemma  `bag-append-comm`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\{u\}\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0
              THENA  (Auto
                            THEN  Repeat  OldAutoSplit
                            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  Thin  (-1)
  THEN  RepUR  ``bag-accum  bag-append``  0
  THEN  (RWO  "list\_accum\_append"  0  THENA  (Auto  THEN  Unfold  `single-bag`  0  THEN  Auto))
  THEN  Try  (Folds  ``bag-accum  bag-append``  0)
  THEN  (RWO  "bag-accum-single"  0  THENA  Auto)
  THEN  OldAutoSplit\mcdot{})

---

Home Index