---

Step * 2 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||. (¬f[i] < ||as||)
⊢ False
BY
{ Assert ⌜∀[n,m,p,q:ℕ]. ∀[f:ℕp + q ⟶ ℕn + m].
            (False) supposing 
               ((∀i:ℕp. (n ≤ f[i])) and 
               q < p and 
               m < n and 
               ((p + q) = (n + m) ∈ ℤ) and 
               Inj(ℕp + q;ℕn + m;f))⌝⋅ }

1
.....assertion..... 
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||)
⊢ ∀[n,m,p,q:ℕ]. ∀[f:ℕp + q ⟶ ℕn + m].
    (False) supposing ((∀i:ℕp. (n ≤ f[i])) and q < p and m < n and ((p + q) = (n + m) ∈ ℤ) and Inj(ℕp + q;ℕn + m;f))

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||)
17. ∀[n,m,p,q:ℕ]. ∀[f:ℕp + q ⟶ ℕn + m].
      (False) supposing ((∀i:ℕp. (n ≤ f[i])) and q < p and m < n and ((p + q) = (n + m) ∈ ℤ) and Inj(ℕp + q;ℕn + m;f))
⊢ False

---

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.  \mforall{}i:\mBbbN{}||bs||.  (\mneg{}f[i]  <  ||as||)
\mvdash{}  False


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}[n,m,p,q:\mBbbN{}].  \mforall{}[f:\mBbbN{}p  +  q  {}\mrightarrow{}  \mBbbN{}n  +  m].
                    (False)  supposing 
                          ((\mforall{}i:\mBbbN{}p.  (n  \mleq{}  f[i]))  and 
                          q  <  p  and 
                          m  <  n  and 
                          ((p  +  q)  =  (n  +  m))  and 
                          Inj(\mBbbN{}p  +  q;\mBbbN{}n  +  m;f))\mkleeneclose{}\mcdot{}

---

Home Index