---

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


1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. istype(T List)
5. ∀a1,b1:T List.  istype(permutation(T;a1;b1))
6. ∀a1:T List. permutation(T;a1;a1)
7. a : Base
8. a ∈ T List
9. cs : T List
10. <as, bs> ↓∈ bag-splits(cs)
⊢ (as + bs) = cs ∈ bag(T)
BY
{ (D (-1)
   THEN ExRepD
   THEN (Assert bag-splits(cs) ∈ (bag(T) × bag(T)) List BY
               Auto)
   THEN Unfold `bag` -3
   THEN EqTypeHD (-3)
   THEN All (Fold `bag`)
   THEN Auto
   THEN (FLemma `member-permutation` [-3] THENA Auto)
   THEN (FHyp (-1) [-3] THENA Auto)
   THEN (Lemmaize [-1] THEN Auto)
   THEN InstLemma `bag-splits_wf_list` [⌜T⌝]⋅
   THEN Auto
   THEN PromoteHyp (-1) 2)⋅ }

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. cs : T List
6. (<as, bs> ∈ bag-splits(cs))
⊢ (as + bs) = cs ∈ bag(T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  bag(T)
3.  bs  :  bag(T)
4.  istype(T  List)
5.  \mforall{}a1,b1:T  List.    istype(permutation(T;a1;b1))
6.  \mforall{}a1:T  List.  permutation(T;a1;a1)
7.  a  :  Base
8.  a  \mmember{}  T  List
9.  cs  :  T  List
10.  <as,  bs>  \mdownarrow{}\mmember{}  bag-splits(cs)
\mvdash{}  (as  +  bs)  =  cs


By

---

Latex:
(D  (-1)
  THEN  ExRepD
  THEN  (Assert  bag-splits(cs)  \mmember{}  (bag(T)  \mtimes{}  bag(T))  List  BY
                          Auto)
  THEN  Unfold  `bag`  -3
  THEN  EqTypeHD  (-3)
  THEN  All  (Fold  `bag`)
  THEN  Auto
  THEN  (FLemma  `member-permutation`  [-3]  THENA  Auto)
  THEN  (FHyp  (-1)  [-3]  THENA  Auto)
  THEN  (Lemmaize  [-1]  THEN  Auto)
  THEN  InstLemma  `bag-splits\_wf\_list`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  PromoteHyp  (-1)  2)\mcdot{}

---

Home Index