---

Step * 1 1 1 1 1 2 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
{ ((InstHyp [⌜v⌝] 2⋅ THENA Auto) THEN PromoteHyp (-1) 6) }

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

---

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:
((InstHyp  [\mkleeneopen{}v\mkleeneclose{}]  2\mcdot{}  THENA  Auto)  THEN  PromoteHyp  (-1)  6)

---

Home Index