---

Step * 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. uiff(1 ≤ ||filter(eq x;list-to-set(eq;L1))||;||filter(eq x;list-to-set(eq;L1))|| = 1 ∈ ℤ)
12. uiff(1 ≤ ||filter(eq x;list-to-set(eq;L2))||;||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ)
13. (x ∈ list-to-set(eq;L2)) ⇐⇒ (x ∈ L2)
14. (x ∈ list-to-set(eq;L1)) ⇐⇒ (x ∈ L1)
⊢ ||filter(eq x;list-to-set(eq;L1))|| = ||filter(eq x;list-to-set(eq;L2))|| ∈ ℤ
BY
{ ((FLemma `member-permutation` [5] THEN Auto)
   THEN (Decide ⌜1 ≤ ||filter(eq x;list-to-set(eq;L1))||⌝⋅ THEN Auto)
   THEN Decide ⌜1 ≤ ||filter(eq x;list-to-set(eq;L2))||⌝⋅
   THEN Auto) }

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. ||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))|| ∈ ℤ

2
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. (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))||
20. ||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ
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))|| ∈ ℤ

3
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))|| ∈ ℤ

---

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.  uiff(1  \mleq{}  ||filter(eq  x;list-to-set(eq;L1))||;||filter(eq  x;list-to-set(eq;L1))||  =  1)
12.  uiff(1  \mleq{}  ||filter(eq  x;list-to-set(eq;L2))||;||filter(eq  x;list-to-set(eq;L2))||  =  1)
13.  (x  \mmember{}  list-to-set(eq;L2))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L2)
14.  (x  \mmember{}  list-to-set(eq;L1))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L1)
\mvdash{}  ||filter(eq  x;list-to-set(eq;L1))||  =  ||filter(eq  x;list-to-set(eq;L2))||


By

---

Latex:
((FLemma  `member-permutation`  [5]  THEN  Auto)
  THEN  (Decide  \mkleeneopen{}1  \mleq{}  ||filter(eq  x;list-to-set(eq;L1))||\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  Decide  \mkleeneopen{}1  \mleq{}  ||filter(eq  x;list-to-set(eq;L2))||\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index