---

Step * of Lemma bag-splits-permutation1

∀T:Type. ∀L:T List. ∀a,b:T.  permutation(bag(T) × bag(T);bag-splits([a; [b / L]]);bag-splits([b; [a / L]]))
BY
{ (Auto
   THEN RepUR ``bag-splits`` 0
   THEN Fold `bag-splits` 0
   THEN (GenConcl ⌜bag-splits(L) = LL ∈ ((bag(T) × bag(T)) List)⌝⋅ THENA (Auto THEN BLemma `bag-splits-wf` THEN Auto))
   THEN RepUR ``bag-map bag-append`` 0
   THEN ((RWO "map_append_sq" 0 THENA Auto) THEN (RWO "append_assoc_sq" 0⋅ THENA Auto))
   THEN skip{((RWO "append_assoc_sq" 0 THENM BLemma `append_functionality_wrt_permutation`)
              THENA ((Try ((Fold `bag-append` 0 THEN Complete (Auto))) THEN Try (Complete (Auto)))
                     THEN RepeatFor 2 ((MemCD THEN Try ((Try (Fold `bag-append` 0) THEN Complete (Auto)))))⋅
                     )
              )}) }

1
1. T : Type
2. L : T List
3. a : T
4. b : T
5. LL : (bag(T) × bag(T)) List
6. bag-splits(L) = LL ∈ ((bag(T) × bag(T)) List)
⊢ permutation(bag(T) × bag(T);map(λp.<{a} @ (fst(p)), snd(p)>;map(λp.<{b} @ (fst(p)), snd(p)>;LL))
              @ map(λp.<{a} @ (fst(p)), snd(p)>;map(λp.<fst(p), {b} @ (snd(p))>;LL))
              @ map(λp.<fst(p), {a} @ (snd(p))>;map(λp.<{b} @ (fst(p)), snd(p)>;LL))
              @ map(λp.<fst(p), {a} @ (snd(p))>;map(λp.<fst(p), {b} @ (snd(p))>;LL));
              map(λp.<{b} @ (fst(p)), snd(p)>;map(λp.<{a} @ (fst(p)), snd(p)>;LL))
              @ map(λp.<{b} @ (fst(p)), snd(p)>;map(λp.<fst(p), {a} @ (snd(p))>;LL))
              @ map(λp.<fst(p), {b} @ (snd(p))>;map(λp.<{a} @ (fst(p)), snd(p)>;LL))
              @ map(λp.<fst(p), {b} @ (snd(p))>;map(λp.<fst(p), {a} @ (snd(p))>;LL)))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}L:T  List.  \mforall{}a,b:T.
    permutation(bag(T)  \mtimes{}  bag(T);bag-splits([a;  [b  /  L]]);bag-splits([b;  [a  /  L]]))


By

---

Latex:
(Auto
  THEN  RepUR  ``bag-splits``  0
  THEN  Fold  `bag-splits`  0
  THEN  (GenConcl  \mkleeneopen{}bag-splits(L)  =  LL\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  BLemma  `bag-splits-wf`  THEN  Auto))
  THEN  RepUR  ``bag-map  bag-append``  0
  THEN  ((RWO  "map\_append\_sq"  0  THENA  Auto)  THEN  (RWO  "append\_assoc\_sq"  0\mcdot{}  THENA  Auto))
  THEN  skip\{((RWO  "append\_assoc\_sq"  0  THENM  BLemma  `append\_functionality\_wrt\_permutation`)
                        THENA  ((Try  ((Fold  `bag-append`  0  THEN  Complete  (Auto)))  THEN  Try  (Complete  (Auto)))
                                      THEN  RepeatFor  2  ((MemCD
                                                                            THEN  Try  ((Try  (Fold  `bag-append`  0)  THEN  Complete  (Auto)))
                                                                            ))\mcdot{}
                                      )
                        )\})

---

Home Index