---

Step * 1 1 1 1 1 2 2 1 of Lemma bag-member-splits


1. T : Type
2. ∀b:T List. (bag-splits(b) ∈ (bag(T) × bag(T)) List)
3. u : T
4. v : T List
5. ∀as,bs:bag(T).  ((<as, bs> ∈ bag-splits(v)) ⇒ ((as + bs) = v ∈ bag(T)))
6. bag-splits(v) ∈ (bag(T) × bag(T)) List
7. as : bag(T)
8. bs : bag(T)
9. (<as, bs> ∈ bag-map(λp.<{u} + (fst(p)), snd(p)>;bag-splits(v)) + bag-map(λp.<fst(p), {u} + (snd(p))>;bag-splits(v)))
⊢ (as + bs) = ({u} + v) ∈ bag(T)
BY
{ (RepUR ``bag-append bag-map`` (-1)
   THEN (RWO "member_append" (-1) THENA (Try (Fold `bag-append` 0) THEN Auto))
   THEN (D -1
         THEN Fold `bag-append` (-1)
         THEN (RWO "member_map" (-1) THENA Auto)
         THEN Reduce (-1)
         THEN ExRepD
         THEN (SplitPair (-1) THENA Auto)
         THEN D (-4)
         THEN FHyp 5 [-3]
         THEN Auto
         THEN All Reduce
         THEN (ElimVar `as' THENA Auto)
         THEN (ElimVar `bs' THENA Auto)
         THEN RevHypSubst (-1) 0
         THEN Auto
         THEN RWW "bag-append-assoc" 0
         THEN Auto
         THEN (RWO "bag-append-assoc<" 0 THEN Auto THEN EqCD⋅ THEN Auto THEN BLemma `bag-append-comm` THEN Auto)⋅)⋅)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  \mforall{}b:T  List.  (bag-splits(b)  \mmember{}  (bag(T)  \mtimes{}  bag(T))  List)
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}as,bs:bag(T).    ((<as,  bs>  \mmember{}  bag-splits(v))  {}\mRightarrow{}  ((as  +  bs)  =  v))
6.  bag-splits(v)  \mmember{}  (bag(T)  \mtimes{}  bag(T))  List
7.  as  :  bag(T)
8.  bs  :  bag(T)
9.  (<as,  bs>  \mmember{}  bag-map(\mlambda{}p.<\{u\}  +  (fst(p)),  snd(p)>bag-splits(v))
        +  bag-map(\mlambda{}p.<fst(p),  \{u\}  +  (snd(p))>bag-splits(v)))
\mvdash{}  (as  +  bs)  =  (\{u\}  +  v)


By

---

Latex:
(RepUR  ``bag-append  bag-map``  (-1)
  THEN  (RWO  "member\_append"  (-1)  THENA  (Try  (Fold  `bag-append`  0)  THEN  Auto))
  THEN  (D  -1
              THEN  Fold  `bag-append`  (-1)
              THEN  (RWO  "member\_map"  (-1)  THENA  Auto)
              THEN  Reduce  (-1)
              THEN  ExRepD
              THEN  (SplitPair  (-1)  THENA  Auto)
              THEN  D  (-4)
              THEN  FHyp  5  [-3]
              THEN  Auto
              THEN  All  Reduce
              THEN  (ElimVar  `as'  THENA  Auto)
              THEN  (ElimVar  `bs'  THENA  Auto)
              THEN  RevHypSubst  (-1)  0
              THEN  Auto
              THEN  RWW  "bag-append-assoc"  0
              THEN  Auto
              THEN  (RWO  "bag-append-assoc<"  0
                          THEN  Auto
                          THEN  EqCD\mcdot{}
                          THEN  Auto
                          THEN  BLemma  `bag-append-comm`
                          THEN  Auto)\mcdot{})\mcdot{})\mcdot{}

---

Home Index