---

Step * of Lemma bag-separate-merge

∀[as,bs:Top List].  (bag-separate(bag-merge(as;bs)) ~ <as, bs>)
BY
{ (Auto
   THEN RepUR ``bag-separate bag-mapfilter bag-merge`` 0
   THEN RepUR ``bag-filter bag-map bag-append`` 0
   THEN (RWO "filter_append_sq" 0 THENA Auto)
   THEN (RWO "map_append_sq" 0
         THENA (Try (Complete (Auto)) THEN SubsumeC ⌜(Top + Top) List⌝⋅ THEN Auto THEN SubtypeReasoning THEN Auto)
         )⋅
   THEN EqCD) }

1
1. as : Top List
2. bs : Top List
⊢ map(λt.outl(t);filter(λx.isl(x);map(λx.(inl x);as))) @ map(λt.outl(t);filter(λx.isl(x);map(λx.(inr x );bs))) ~ as

2
1. as : Top List
2. bs : Top List
⊢ map(λt.outr(t);filter(λx.(¬bisl(x));map(λx.(inl x);as))) @ map(λt.outr(t);filter(λx.(¬bisl(x));map(λx.(inr x );bs))) 
~ bs

---

Latex:

---

Latex:
\mforall{}[as,bs:Top  List].    (bag-separate(bag-merge(as;bs))  \msim{}  <as,  bs>)


By

---

Latex:
(Auto
  THEN  RepUR  ``bag-separate  bag-mapfilter  bag-merge``  0
  THEN  RepUR  ``bag-filter  bag-map  bag-append``  0
  THEN  (RWO  "filter\_append\_sq"  0  THENA  Auto)
  THEN  (RWO  "map\_append\_sq"  0
              THENA  (Try  (Complete  (Auto))
                            THEN  SubsumeC  \mkleeneopen{}(Top  +  Top)  List\mkleeneclose{}\mcdot{}
                            THEN  Auto
                            THEN  SubtypeReasoning
                            THEN  Auto)
              )\mcdot{}
  THEN  EqCD)

---

Home Index