---

Step * of Lemma bag-intersection

∀[A:Type]. ∀[as,as',bs,bs':bag(A)].
  (↓∃x:A. (x ↓∈ as ∧ x ↓∈ bs)) supposing (#(as') < #(as) and #(bs') < #(bs) and ((as + as') = (bs + bs') ∈ bag(A)))
BY
{ (Auto
   THEN ∀i:hyp. (BagToList i THENA Auto) 
   THEN All (RepUR ``bag-append bag-size``)
   THEN (EqTypeHD (-3) THENA Auto)
   THEN Duplicate (-3)
   THEN RepUR ``permutation`` (-1)
   THEN ExRepD
   THEN (FLemma `permutation-length` [-6] THENA Auto')
   THEN ( Decide ⌜∃i:ℕ||bs||. f[i] < ||as||⌝⋅ THENA Auto)) }

1
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||. f[i] < ||as||
⊢ ↓∃x:A. (x ↓∈ as ∧ x ↓∈ bs)

2
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||. f[i] < ||as||)
⊢ ↓∃x:A. (x ↓∈ as ∧ x ↓∈ bs)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[as,as',bs,bs':bag(A)].
    (\mdownarrow{}\mexists{}x:A.  (x  \mdownarrow{}\mmember{}  as  \mwedge{}  x  \mdownarrow{}\mmember{}  bs))  supposing 
          (\#(as')  <  \#(as)  and 
          \#(bs')  <  \#(bs)  and 
          ((as  +  as')  =  (bs  +  bs')))


By

---

Latex:
(Auto
  THEN  \mforall{}i:hyp.  (BagToList  i  THENA  Auto) 
  THEN  All  (RepUR  ``bag-append  bag-size``)
  THEN  (EqTypeHD  (-3)  THENA  Auto)
  THEN  Duplicate  (-3)
  THEN  RepUR  ``permutation``  (-1)
  THEN  ExRepD
  THEN  (FLemma  `permutation-length`  [-6]  THENA  Auto')
  THEN  (  Decide  \mkleeneopen{}\mexists{}i:\mBbbN{}||bs||.  f[i]  <  ||as||\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index