---

Step * 1 2 1 2 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)
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 o f4;LL) @ map(f1 o f3;LL);map(f1 o f3;LL) @ map(f4 o f2;LL))
BY
{ (Subst ⌜map(f2 o f4;LL) = map(f4 o f2;LL) ∈ ((bag(T) × bag(T)) List)⌝ 0⋅ THEN Auto)⋅ }

1
.....equality..... 
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)))
⊢ map(f2 o f4;LL) = map(f4 o f2;LL) ∈ ((bag(T) × bag(T)) List)

---

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
7.  f1  :  (bag(T)  \mtimes{}  bag(T))  {}\mrightarrow{}  (bag(T)  \mtimes{}  bag(T))
8.  (\mlambda{}p.<\{b\}  +  (fst(p)),  snd(p)>)  =  f1
9.  f2  :  (bag(T)  \mtimes{}  bag(T))  {}\mrightarrow{}  (bag(T)  \mtimes{}  bag(T))
10.  (\mlambda{}p.<\{a\}  +  (fst(p)),  snd(p)>)  =  f2
11.  f3  :  (bag(T)  \mtimes{}  bag(T))  {}\mrightarrow{}  (bag(T)  \mtimes{}  bag(T))
12.  (\mlambda{}p.<fst(p),  \{a\}  +  (snd(p))>)  =  f3
13.  f4  :  (bag(T)  \mtimes{}  bag(T))  {}\mrightarrow{}  (bag(T)  \mtimes{}  bag(T))
14.  (\mlambda{}p.<fst(p),  \{b\}  +  (snd(p))>)  =  f4
\mvdash{}  permutation(bag(T)  \mtimes{}  bag(T);map(f2  o  f4;LL)  @  map(f1  o  f3;LL);map(f1  o  f3;LL)  @  map(f4  o  f2;LL))


By

---

Latex:
(Subst  \mkleeneopen{}map(f2  o  f4;LL)  =  map(f4  o  f2;LL)\mkleeneclose{}  0\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index