---

Step * 1 1 1 3 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;L1))|| = 1 ∈ ℤ supposing 1 ≤ ||filter(eq x;list-to-set(eq;L1))||
12. 1 ≤ ||filter(eq x;list-to-set(eq;L1))|| supposing ||filter(eq x;list-to-set(eq;L1))|| = 1 ∈ ℤ
13. ||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ supposing 1 ≤ ||filter(eq x;list-to-set(eq;L2))||
14. 1 ≤ ||filter(eq x;list-to-set(eq;L2))|| supposing ||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ
15. (x ∈ list-to-set(eq;L2)) ⇒ (x ∈ L2)
16. (x ∈ list-to-set(eq;L2)) ⇐ (x ∈ L2)
17. (x ∈ list-to-set(eq;L1)) ⇒ (x ∈ L1)
18. (x ∈ list-to-set(eq;L1)) ⇐ (x ∈ L1)
19. ∀a:T. ((a ∈ L1) ⇐⇒ (a ∈ L2))
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
{ Auto' }

---

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;L1))||  =  1  supposing  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L1))||
12.  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L1))||  supposing  ||filter(eq  x;list-to-set(eq;L1))||  =  1
13.  ||filter(eq  x;list-to-set(eq;L2))||  =  1  supposing  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L2))||
14.  1  \mleq{}  ||filter(eq  x;list-to-set(eq;L2))||  supposing  ||filter(eq  x;list-to-set(eq;L2))||  =  1
15.  (x  \mmember{}  list-to-set(eq;L2))  {}\mRightarrow{}  (x  \mmember{}  L2)
16.  (x  \mmember{}  list-to-set(eq;L2))  \mLeftarrow{}{}  (x  \mmember{}  L2)
17.  (x  \mmember{}  list-to-set(eq;L1))  {}\mRightarrow{}  (x  \mmember{}  L1)
18.  (x  \mmember{}  list-to-set(eq;L1))  \mLeftarrow{}{}  (x  \mmember{}  L1)
19.  \mforall{}a:T.  ((a  \mmember{}  L1)  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  L2))
20.  \mneg{}(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:
Auto'

---

Home Index