---

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

.....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))
BY
{ ((Assert ||as @ bs|| = ||a1 @ [u / b1]|| ∈ ℤ BY
          (EqCD THEN Auto))
   THEN (RWO "length_append" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN (Assert (as @ bs) = (a1 @ [u / b1]) ∈ {L:T List| ||L|| = ||a1 @ [u / b1]|| ∈ ℤ}  BY
               Auto)
   THEN (ApFunToHypEquands `Z' ⌜snd(remove-nth(||a1||;Z))⌝ ⌜T List⌝ (-1)⋅
         THENA (Auto THEN D (-1) THEN RWO "length-append" (-1) THEN Auto')
         )
   THEN (RepUR ``remove-nth`` (-1) THEN (RWW "firstn-append append_assoc_sq nth_tl-append" (-1) THENA Auto))⋅) }

1
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) ∈ ℤ
13. (as @ bs) = (a1 @ [u / b1]) ∈ {L:T List| ||L|| = ||a1 @ [u / b1]|| ∈ ℤ} 
14. (if ||a1|| ≤z ||as|| then firstn(||a1||;as) else as @ firstn(||a1|| - ||as||;bs) fi 
@ if ||a1|| + 1 <z ||as|| then nth_tl(||a1|| + 1;as) @ bs else nth_tl((||a1|| + 1) - ||as||;bs) fi )
= (if ||a1|| ≤z ||a1|| then firstn(||a1||;a1) else a1 @ firstn(||a1|| - ||a1||;[u / b1]) fi 
  @ if ||a1|| + 1 <z ||a1|| then nth_tl(||a1|| + 1;a1) @ [u / b1] else nth_tl((||a1|| + 1) - ||a1||;[u / b1]) fi )
∈ (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))

---

Latex:

---

Latex:
.....assertion..... 
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{}  ((||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)


By

---

Latex:
((Assert  ||as  @  bs||  =  ||a1  @  [u  /  b1]||  BY
                (EqCD  THEN  Auto))
  THEN  (RWO  "length\_append"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  (Assert  (as  @  bs)  =  (a1  @  [u  /  b1])  BY
                          Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}snd(remove-nth(||a1||;Z))\mkleeneclose{}  \mkleeneopen{}T  List\mkleeneclose{}  (-1)\mcdot{}
              THENA  (Auto  THEN  D  (-1)  THEN  RWO  "length-append"  (-1)  THEN  Auto')
              )
  THEN  (RepUR  ``remove-nth``  (-1)
              THEN  (RWW  "firstn-append  append\_assoc\_sq  nth\_tl-append"  (-1)  THENA  Auto)
              )\mcdot{})

---

Home Index