Step
*
1
1
1
2
of Lemma
respects-equality-bag
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
7. as ∈ B List
8. f : ℕ||bs|| ⟶ ℕ||bs||
9. Inj(ℕ||bs||;ℕ||bs||;f)
10. as = (bs o f) ∈ (A List)
11. as = (bs o f) ∈ (B List)
12. permutation(B;bs;as)
⊢ ∀i:ℕ||bs||. (bs[i] ∈ B)
BY
{ ((D 0 THENA Auto) THEN D -2 THEN ExRepD) }
1
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
7. as ∈ B List
8. f : ℕ||bs|| ⟶ ℕ||bs||
9. Inj(ℕ||bs||;ℕ||bs||;f)
10. as = (bs o f) ∈ (A List)
11. as = (bs o f) ∈ (B List)
12. f1 : ℕ||bs|| ⟶ ℕ||bs||
13. Inj(ℕ||bs||;ℕ||bs||;f1)
14. as = (bs o f1) ∈ (B List)
15. i : ℕ||bs||
⊢ bs[i] ∈ B
Latex:
Latex:
1.  A  :  Type
2.  B  :  Type
3.  respects-equality(A;B)
4.  as  :  A  List
5.  bs  :  A  List
6.  permutation(A;as;bs)
7.  as  \mmember{}  B  List
8.  f  :  \mBbbN{}||bs||  {}\mrightarrow{}  \mBbbN{}||bs||
9.  Inj(\mBbbN{}||bs||;\mBbbN{}||bs||;f)
10.  as  =  (bs  o  f)
11.  as  =  (bs  o  f)
12.  permutation(B;bs;as)
\mvdash{}  \mforall{}i:\mBbbN{}||bs||.  (bs[i]  \mmember{}  B)
By
Latex:
((D  0  THENA  Auto)  THEN  D  -2  THEN  ExRepD)
Home
Index