---

Step * 2 1 1 1 1 1 2 1 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. 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)))))
BY
{ Assert ⌜((||as|| + ||bs||) = (||a1|| + ||b1|| + 1) ∈ ℤ)
          ∧ (if ||a1|| ≤z ||as|| then firstn(||a1||;as) else as @ firstn(||a1|| - ||as||;bs) fi  = a1 ∈ (T List))
          ∧ (if ||a1|| + 1 <z ||as|| then nth_tl(||a1|| + 1;as) @ bs else nth_tl((||a1|| + 1) - ||as||;bs) fi 
            = b1
            ∈ (T List))⌝⋅ }

1
.....assertion..... 
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
⊢ ((||as|| + ||bs||) = (||a1|| + ||b1|| + 1) ∈ ℤ)
∧ (if ||a1|| ≤z ||as|| then firstn(||a1||;as) else as @ firstn(||a1|| - ||as||;bs) fi  = a1 ∈ (T List))
∧ (if ||a1|| + 1 <z ||as|| then nth_tl(||a1|| + 1;as) @ bs else nth_tl((||a1|| + 1) - ||as||;bs) fi  = b1 ∈ (T List))

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. 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
12. ((||as|| + ||bs||) = (||a1|| + ||b1|| + 1) ∈ ℤ)
∧ (if ||a1|| ≤z ||as|| then firstn(||a1||;as) else as @ firstn(||a1|| - ||as||;bs) fi  = a1 ∈ (T List))
∧ (if ||a1|| + 1 <z ||as|| then nth_tl(||a1|| + 1;as) @ bs else nth_tl((||a1|| + 1) - ||as||;bs) fi  = b1 ∈ (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.  a1  :  T  List
8.  b1  :  T  List
9.  (as  @  bs)  =  (a1  @  [u  /  b1])
10.  permutation(T;v;a1  @  b1)
11.  bag-splits(v)  \mmember{}  (bag(T)  \mtimes{}  bag(T))  List
\mvdash{}  (\mexists{}y:bag(T)  \mtimes{}  bag(T).  ((y  \mmember{}  bag-splits(v))  \mwedge{}  (<as,  bs>  =  ((\mlambda{}p.<\{u\}  +  (fst(p)),  snd(p)>)  y))))
\mvee{}  (\mexists{}y:bag(T)  \mtimes{}  bag(T).  ((y  \mmember{}  bag-splits(v))  \mwedge{}  (<as,  bs>  =  ((\mlambda{}p.<fst(p),  \{u\}  +  (snd(p))>)  y))))


By

---

Latex:
Assert  \mkleeneopen{}((||as||  +  ||bs||)  =  (||a1||  +  ||b1||  +  1))
                \mwedge{}  (if  ||a1||  \mleq{}z  ||as||  then  firstn(||a1||;as)  else  as  @  firstn(||a1||  -  ||as||;bs)  fi    =  a1)
                \mwedge{}  (if  ||a1||  +  1  <z  ||as||
                    then  nth\_tl(||a1||  +  1;as)  @  bs
                    else  nth\_tl((||a1||  +  1)  -  ||as||;bs)
                    fi 
                    =  b1)\mkleeneclose{}\mcdot{}

---

Home Index