---

Step * 1 1 of Lemma bag-intersection


1. A : Type
2. as : A List
3. as' : A List
4. bs : A List
5. bs' : A List
6. (as @ as') = (bs @ bs') ∈ pertype(λas,bs. ((as ∈ A List) ∧ (bs ∈ A List) ∧ permutation(A;as;bs)))
7. as @ as' ∈ A List
8. bs @ bs' ∈ A List
9. permutation(A;as @ as';bs @ bs')
10. ||bs'|| < ||bs||
11. ||as'|| < ||as||
12. f : ℕ||as @ as'|| ⟶ ℕ||as @ as'||
13. Inj(ℕ||as @ as'||;ℕ||as @ as'||;f)
14. (bs @ bs') = (as @ as' o f) ∈ (A List)
15. ||as @ as'|| = ||bs @ bs'|| ∈ ℤ
16. i : ℕ||bs||
17. f[i] < ||as||
⊢ (bs[i] ∈ as)
BY
{ ((Assert ⌜i < ||as @ as'||⌝⋅ THENA (HypSubst' (-3) 0 THEN All Thin THEN Auto'))
   THEN (Assert ⌜bs[i] = as[f[i]] ∈ A⌝⋅ THENM (HypSubst' (-1) 0 THEN Auto THEN GenListD 0))
   THEN (Assert ⌜bs @ bs'[i] = as @ as'[f[i]] ∈ A⌝⋅ THENM (RWO "select_append_front" (-1) THEN Auto'))
   THEN HypSubst' (-5) 0
   THEN RWO "permute_list_select" 0
   THEN Auto'
   THEN All (RepUR ``so_apply``)
   THEN Auto') }

---

Latex:

---

Latex:

1.  A  :  Type
2.  as  :  A  List
3.  as'  :  A  List
4.  bs  :  A  List
5.  bs'  :  A  List
6.  (as  @  as')  =  (bs  @  bs')
7.  as  @  as'  \mmember{}  A  List
8.  bs  @  bs'  \mmember{}  A  List
9.  permutation(A;as  @  as';bs  @  bs')
10.  ||bs'||  <  ||bs||
11.  ||as'||  <  ||as||
12.  f  :  \mBbbN{}||as  @  as'||  {}\mrightarrow{}  \mBbbN{}||as  @  as'||
13.  Inj(\mBbbN{}||as  @  as'||;\mBbbN{}||as  @  as'||;f)
14.  (bs  @  bs')  =  (as  @  as'  o  f)
15.  ||as  @  as'||  =  ||bs  @  bs'||
16.  i  :  \mBbbN{}||bs||
17.  f[i]  <  ||as||
\mvdash{}  (bs[i]  \mmember{}  as)


By

---

Latex:
((Assert  \mkleeneopen{}i  <  ||as  @  as'||\mkleeneclose{}\mcdot{}  THENA  (HypSubst'  (-3)  0  THEN  All  Thin  THEN  Auto'))
  THEN  (Assert  \mkleeneopen{}bs[i]  =  as[f[i]]\mkleeneclose{}\mcdot{}  THENM  (HypSubst'  (-1)  0  THEN  Auto  THEN  GenListD  0))
  THEN  (Assert  \mkleeneopen{}bs  @  bs'[i]  =  as  @  as'[f[i]]\mkleeneclose{}\mcdot{}  THENM  (RWO  "select\_append\_front"  (-1)  THEN  Auto'))
  THEN  HypSubst'  (-5)  0
  THEN  RWO  "permute\_list\_select"  0
  THEN  Auto'
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto')

---

Home Index