---

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


1. T : Type
2. ∀b:T List. (bag-splits(b) ∈ (bag(T) × bag(T)) List)
3. as : bag(T)
4. bs : bag(T)
5. cs : T List
6. (<as, bs> ∈ bag-splits(cs))
⊢ (as + bs) = cs ∈ bag(T)
BY
{ (MoveToConcl (-3)
   THEN MoveToConcl (-2)
   THEN ListInd (-1)
   THEN Auto
   THEN (RepUR ``bag-splits`` (-1)⋅ THEN Try (Fold `bag-splits` (-1)) THEN Auto)⋅)⋅ }

1
1. T : Type
2. ∀b:T List. (bag-splits(b) ∈ (bag(T) × bag(T)) List)
3. as : bag(T)
4. bs : bag(T)
5. (<as, bs> ∈ {<{}, {}>})
⊢ (as + bs) = [] ∈ bag(T)

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.  as  :  bag(T)
4.  bs  :  bag(T)
5.  cs  :  T  List
6.  (<as,  bs>  \mmember{}  bag-splits(cs))
\mvdash{}  (as  +  bs)  =  cs


By

---

Latex:
(MoveToConcl  (-3)
  THEN  MoveToConcl  (-2)
  THEN  ListInd  (-1)
  THEN  Auto
  THEN  (RepUR  ``bag-splits``  (-1)\mcdot{}  THEN  Try  (Fold  `bag-splits`  (-1))  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index