---

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


1. T : Type
2. u : T
3. v : T List
4. ∀as,bs:T List.  (permutation(T;v;as @ bs) ⇒ (<as, bs> ∈ bag-splits(v)))
5. as : T List
6. bs : T List
7. permutation(T;[u / v];as @ bs)
⊢ (<as, bs> ∈ bag-map(λp.<{u} + (fst(p)), snd(p)>;bag-splits(v)) + bag-map(λp.<fst(p), {u} + (snd(p))>;bag-splits(v)))
BY
{ (((RWO "permutation-cons" (-1)⋅ THENA Auto)
    THEN ExRepD
    THEN (Assert bag-splits(v) ∈ (bag(T) × bag(T)) List BY
                (BLemma `bag-splits_wf_list` THEN Auto)))
   THEN (Unfolds ``bag-append bag-map`` 0
         THEN (RWO "member_append" 0⋅ THENA (Try (Fold `bag-append` 0) THEN Auto THEN Auto))
         THEN Fold `bag-append` 0
         THEN (RWO "member_map" 0 THENA Auto))⋅
   ) }

1
1. T : Type
2. u : T
3. v : T List
4. ∀as,bs:T List.  (permutation(T;v;as @ bs) ⇒ (<as, bs> ∈ bag-splits(v)))
5. as : T List
6. bs : T List
7. a1 : T List
8. b1 : T List
9. (as @ bs) = (a1 @ [u / b1]) ∈ (T List)
10. permutation(T;v;a1 @ b1)
11. bag-splits(v) ∈ (bag(T) × bag(T)) List
⊢ (∃y:bag(T) × bag(T). ((y ∈ bag-splits(v)) ∧ (<as, bs> = ((λp.<{u} + (fst(p)), snd(p)>) y) ∈ (bag(T) × bag(T)))))
∨ (∃y:bag(T) × bag(T). ((y ∈ bag-splits(v)) ∧ (<as, bs> = ((λp.<fst(p), {u} + (snd(p))>) y) ∈ (bag(T) × bag(T)))))

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}as,bs:T  List.    (permutation(T;v;as  @  bs)  {}\mRightarrow{}  (<as,  bs>  \mmember{}  bag-splits(v)))
5.  as  :  T  List
6.  bs  :  T  List
7.  permutation(T;[u  /  v];as  @  bs)
\mvdash{}  (<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)))


By

---

Latex:
(((RWO  "permutation-cons"  (-1)\mcdot{}  THENA  Auto)
    THEN  ExRepD
    THEN  (Assert  bag-splits(v)  \mmember{}  (bag(T)  \mtimes{}  bag(T))  List  BY
                            (BLemma  `bag-splits\_wf\_list`  THEN  Auto)))
  THEN  (Unfolds  ``bag-append  bag-map``  0
              THEN  (RWO  "member\_append"  0\mcdot{}  THENA  (Try  (Fold  `bag-append`  0)  THEN  Auto  THEN  Auto))
              THEN  Fold  `bag-append`  0
              THEN  (RWO  "member\_map"  0  THENA  Auto))\mcdot{}
  )

---

Home Index