---

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


1. T : Type
2. as : T List
3. bs : T List
4. cs : T List
5. permutation(T;as @ bs;cs)
⊢ (<as, bs> ∈ bag-splits(cs))
BY
{ ((FLemma `permutation_inversion` [-1] THENA Auto)
   THEN Thin (-2)
   THEN Auto
   THEN MoveToConcl (-3)
   THEN MoveToConcl (-2)
   THEN ListInd (-1)
   THEN RepUR ``bag-splits`` 0⋅
   THEN Try (Fold `bag-splits` 0)
   THEN Auto) }

1
1. T : Type
2. as : T List
3. bs : T List
4. permutation(T;[];as @ bs)
⊢ (<as, bs> ∈ {<{}, {}>})

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  bs  :  T  List
4.  cs  :  T  List
5.  permutation(T;as  @  bs;cs)
\mvdash{}  (<as,  bs>  \mmember{}  bag-splits(cs))


By

---

Latex:
((FLemma  `permutation\_inversion`  [-1]  THENA  Auto)
  THEN  Thin  (-2)
  THEN  Auto
  THEN  MoveToConcl  (-3)
  THEN  MoveToConcl  (-2)
  THEN  ListInd  (-1)
  THEN  RepUR  ``bag-splits``  0\mcdot{}
  THEN  Try  (Fold  `bag-splits`  0)
  THEN  Auto)

---

Home Index