---

Step * 1 1 1 1 1 2 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. 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)))
⊢ (as + bs) = [u / v] ∈ bag(T)
BY
{ Subst' [u / v] ~ {u} + v 0 }

1
.....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

2
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)))
⊢ (as + bs) = ({u} + v) ∈ bag(T)

---

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.  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{}  (as  +  bs)  =  [u  /  v]


By

---

Latex:
Subst'  [u  /  v]  \msim{}  \{u\}  +  v  0

---

Home Index