---

Step * 1 of Lemma bag-splits-permutation1


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)))
BY
{ (Fold `bag-append` 0
   THEN (GenConcl ⌜(λp.<{b} + (fst(p)), snd(p)>) = f1 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(λp.<{a} + (fst(p)), snd(p)>) = f2 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(λp.<fst(p), {a} + (snd(p))>) = f3 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(λp.<fst(p), {b} + (snd(p))>) = f4 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))⌝⋅ THENA Auto)
   THEN Unfold `bag-append` 0
   THEN (BLemma `append_functionality_wrt_permutation` THENA 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)
7. f1 : (bag(T) × bag(T)) ⟶ (bag(T) × bag(T))
8. (λp.<{b} + (fst(p)), snd(p)>) = f1 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))
9. f2 : (bag(T) × bag(T)) ⟶ (bag(T) × bag(T))
10. (λp.<{a} + (fst(p)), snd(p)>) = f2 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))
11. f3 : (bag(T) × bag(T)) ⟶ (bag(T) × bag(T))
12. (λp.<fst(p), {a} + (snd(p))>) = f3 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))
13. f4 : (bag(T) × bag(T)) ⟶ (bag(T) × bag(T))
14. (λp.<fst(p), {b} + (snd(p))>) = f4 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))
⊢ permutation(bag(T) × bag(T);map(f2;map(f1;LL));map(f1;map(f2;LL)))

2
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)
7. f1 : (bag(T) × bag(T)) ⟶ (bag(T) × bag(T))
8. (λp.<{b} + (fst(p)), snd(p)>) = f1 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))
9. f2 : (bag(T) × bag(T)) ⟶ (bag(T) × bag(T))
10. (λp.<{a} + (fst(p)), snd(p)>) = f2 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))
11. f3 : (bag(T) × bag(T)) ⟶ (bag(T) × bag(T))
12. (λp.<fst(p), {a} + (snd(p))>) = f3 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))
13. f4 : (bag(T) × bag(T)) ⟶ (bag(T) × bag(T))
14. (λp.<fst(p), {b} + (snd(p))>) = f4 ∈ ((bag(T) × bag(T)) ⟶ (bag(T) × bag(T)))
⊢ permutation(bag(T) × bag(T);map(f2;map(f4;LL)) @ map(f3;map(f1;LL)) @ map(f3;map(f4;LL));map(f1;map(f3;LL))
              @ map(f4;map(f2;LL))
              @ map(f4;map(f3;LL)))

---

Latex:

---

Latex:

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


By

---

Latex:
(Fold  `bag-append`  0
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}p.<\{b\}  +  (fst(p)),  snd(p)>)  =  f1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}p.<\{a\}  +  (fst(p)),  snd(p)>)  =  f2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}p.<fst(p),  \{a\}  +  (snd(p))>)  =  f3\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}p.<fst(p),  \{b\}  +  (snd(p))>)  =  f4\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Unfold  `bag-append`  0
  THEN  (BLemma  `append\_functionality\_wrt\_permutation`  THENA  Auto))

---

Home Index