Step * 1 1 of Lemma bag-extensionality1

.....antecedent..... 
1. Type
2. eq T ⟶ T ⟶ 𝔹
3. ∀[x,y:T].  (↑(eq y) ⇐⇒ y ∈ T)
4. List ∈ Type
5. ∀a1,b1:T List.  (permutation(T;a1;b1) ∈ Type)
6. ∀a1:T List. permutation(T;a1;a1)
7. Base
8. Base
9. b ∈ pertype(λas,bs. ((as ∈ List) ∧ (bs ∈ List) ∧ permutation(T;as;bs)))
10. a ∈ List
11. b ∈ List
12. permutation(T;a;b)
13. List ∈ Type
14. ∀as,b1:T List.  (permutation(T;as;b1) ∈ Type)
15. ∀as:T List. permutation(T;as;as)
16. a1 Base
17. b1 Base
18. c1 a1 b1 ∈ pertype(λas,bs. ((as ∈ List) ∧ (bs ∈ List) ∧ permutation(T;as;bs)))
19. a1 ∈ List
20. b1 ∈ List
21. permutation(T;a1;b1)
22. ∀x:T. (#([y∈a|eq y]) #([y∈a1|eq y]) ∈ ℤ)
⊢ permutation(T;a;a1)
BY
((InstLemma `permutation-iff-count1` [⌜T⌝;⌜eq⌝]⋅ THENA Auto) THEN BHyp -1  THEN Auto THEN Thin (-2))⋅ }

1
1. Type
2. eq T ⟶ T ⟶ 𝔹
3. ∀[x,y:T].  (↑(eq y) ⇐⇒ y ∈ T)
4. List ∈ Type
5. ∀a1,b1:T List.  (permutation(T;a1;b1) ∈ Type)
6. ∀a1:T List. permutation(T;a1;a1)
7. Base
8. Base
9. b ∈ pertype(λas,bs. ((as ∈ List) ∧ (bs ∈ List) ∧ permutation(T;as;bs)))
10. a ∈ List
11. b ∈ List
12. permutation(T;a;b)
13. List ∈ Type
14. ∀as,b1:T List.  (permutation(T;as;b1) ∈ Type)
15. ∀as:T List. permutation(T;as;as)
16. a1 Base
17. b1 Base
18. c1 a1 b1 ∈ pertype(λas,bs. ((as ∈ List) ∧ (bs ∈ List) ∧ permutation(T;as;bs)))
19. a1 ∈ List
20. b1 ∈ List
21. permutation(T;a1;b1)
22. ∀x:T. (#([y∈a|eq y]) #([y∈a1|eq y]) ∈ ℤ)
23. T
⊢ ||filter(eq x;a)|| ||filter(eq x;a1)|| ∈ ℤ


Latex:


Latex:
.....antecedent..... 
1.  T  :  Type
2.  eq  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
3.  \mforall{}[x,y:T].    (\muparrow{}(eq  x  y)  \mLeftarrow{}{}\mRightarrow{}  x  =  y)
4.  T  List  \mmember{}  Type
5.  \mforall{}a1,b1:T  List.    (permutation(T;a1;b1)  \mmember{}  Type)
6.  \mforall{}a1:T  List.  permutation(T;a1;a1)
7.  a  :  Base
8.  b  :  Base
9.  c  :  a  =  b
10.  a  \mmember{}  T  List
11.  b  \mmember{}  T  List
12.  permutation(T;a;b)
13.  T  List  \mmember{}  Type
14.  \mforall{}as,b1:T  List.    (permutation(T;as;b1)  \mmember{}  Type)
15.  \mforall{}as:T  List.  permutation(T;as;as)
16.  a1  :  Base
17.  b1  :  Base
18.  c1  :  a1  =  b1
19.  a1  \mmember{}  T  List
20.  b1  \mmember{}  T  List
21.  permutation(T;a1;b1)
22.  \mforall{}x:T.  (\#([y\mmember{}a|eq  x  y])  =  \#([y\mmember{}a1|eq  x  y]))
\mvdash{}  permutation(T;a;a1)


By


Latex:
((InstLemma  `permutation-iff-count1`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto  THEN  Thin  (-2))
\mcdot{}




Home Index