---

Step * 1 1 1 1 of Lemma list-to-set_functionality_wrt_permutation


1. T : Type
2. eq : EqDecider(T)
3. L1 : T List
4. L2 : T List
5. permutation(T;L1;L2)
6. x : T
7. no_repeats(T;list-to-set(eq;L1))
8. no_repeats(T;list-to-set(eq;L2))
9. no_repeats(T;list-to-set(eq;L2))
10. no_repeats(T;list-to-set(eq;L1))
11. ||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ supposing 1 ≤ ||filter(eq x;list-to-set(eq;L2))||
12. 1 ≤ ||filter(eq x;list-to-set(eq;L2))|| supposing ||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ
13. (x ∈ list-to-set(eq;L2)) ⇒ (x ∈ L2)
14. (x ∈ list-to-set(eq;L2)) ⇐ (x ∈ L2)
15. (x ∈ list-to-set(eq;L1)) ⇒ (x ∈ L1)
16. (x ∈ list-to-set(eq;L1)) ⇐ (x ∈ L1)
17. ∀a:T. ((a ∈ L1) ⇐⇒ (a ∈ L2))
18. 1 ≤ ||filter(eq x;list-to-set(eq;L1))||
19. ||filter(eq x;list-to-set(eq;L1))|| = 1 ∈ ℤ
20. 1 ≤ ||filter(eq x;list-to-set(eq;L1))||
21. ¬(1 ≤ ||filter(eq x;list-to-set(eq;L2))||)
⊢ ||filter(eq x;list-to-set(eq;L1))|| = ||filter(eq x;list-to-set(eq;L2))|| ∈ ℤ
BY
{ Thin 20 THEN Thin 19 }

1
1. T : Type
2. eq : EqDecider(T)
3. L1 : T List
4. L2 : T List
5. permutation(T;L1;L2)
6. x : T
7. no_repeats(T;list-to-set(eq;L1))
8. no_repeats(T;list-to-set(eq;L2))
9. no_repeats(T;list-to-set(eq;L2))
10. no_repeats(T;list-to-set(eq;L1))
11. ||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ supposing 1 ≤ ||filter(eq x;list-to-set(eq;L2))||
12. 1 ≤ ||filter(eq x;list-to-set(eq;L2))|| supposing ||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ
13. (x ∈ list-to-set(eq;L2)) ⇒ (x ∈ L2)
14. (x ∈ list-to-set(eq;L2)) ⇐ (x ∈ L2)
15. (x ∈ list-to-set(eq;L1)) ⇒ (x ∈ L1)
16. (x ∈ list-to-set(eq;L1)) ⇐ (x ∈ L1)
17. ∀a:T. ((a ∈ L1) ⇐⇒ (a ∈ L2))
18. 1 ≤ ||filter(eq x;list-to-set(eq;L1))||
19. ¬(1 ≤ ||filter(eq x;list-to-set(eq;L2))||)
⊢ ||filter(eq x;list-to-set(eq;L1))|| = ||filter(eq x;list-to-set(eq;L2))|| ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L1  :  T  List
4.  L2  :  T  List
5.  permutation(T;L1;L2)
6.  x  :  T
7.  no\_repeats(T;list-to-set(eq;L1))
8.  no\_repeats(T;list-to-set(eq;L2))
9.  no\_repeats(T;list-to-set(eq;L2))
10.  no\_repeats(T;list-to-set(eq;L1))
11.  ||filter(eq  x;list-to-set(eq;L2))||  =  1  supposing  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L2))||
12.  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L2))||  supposing  ||filter(eq  x;list-to-set(eq;L2))||  =  1
13.  (x  \mmember{}  list-to-set(eq;L2))  {}\mRightarrow{}  (x  \mmember{}  L2)
14.  (x  \mmember{}  list-to-set(eq;L2))  \mLeftarrow{}{}  (x  \mmember{}  L2)
15.  (x  \mmember{}  list-to-set(eq;L1))  {}\mRightarrow{}  (x  \mmember{}  L1)
16.  (x  \mmember{}  list-to-set(eq;L1))  \mLeftarrow{}{}  (x  \mmember{}  L1)
17.  \mforall{}a:T.  ((a  \mmember{}  L1)  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  L2))
18.  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L1))||
19.  ||filter(eq  x;list-to-set(eq;L1))||  =  1
20.  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L1))||
21.  \mneg{}(1  \mleq{}  ||filter(eq  x;list-to-set(eq;L2))||)
\mvdash{}  ||filter(eq  x;list-to-set(eq;L1))||  =  ||filter(eq  x;list-to-set(eq;L2))||


By

---

Latex:
Thin  20  THEN  Thin  19

---

Home Index