---

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

.....equality..... 
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. as : bag(T)
7. bs : bag(T)
8. (<as, bs> ∈ bag-map(λp.<{u} + (fst(p)), snd(p)>;bag-splits(v)) + bag-map(λp.<fst(p), {u} + (snd(p))>;bag-splits(v)))
⊢ [u / v] ~ {u} + v
BY
{ (RepUR ``bag-append single-bag`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
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.  as  :  bag(T)
7.  bs  :  bag(T)
8.  (<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{}  [u  /  v]  \msim{}  \{u\}  +  v


By

---

Latex:
(RepUR  ``bag-append  single-bag``  0  THEN  Auto)

---

Home Index