---

Step * 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. ∀a:T. ((a ∈ list-to-set(eq;L1)) ⇐⇒ (a ∈ L1))
9. no_repeats(T;list-to-set(eq;L2))
10. ∀a:T. ((a ∈ list-to-set(eq;L2)) ⇐⇒ (a ∈ L2))
11. ∀[x:T]. uiff(1 ≤ ||filter(eq x;list-to-set(eq;L2))||;||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ)
12. ∀[x:T]. uiff(1 ≤ ||filter(eq x;list-to-set(eq;L1))||;||filter(eq x;list-to-set(eq;L1))|| = 1 ∈ ℤ)
13. no_repeats(T;list-to-set(eq;L2))
14. no_repeats(T;list-to-set(eq;L1))
⊢ ||filter(eq x;list-to-set(eq;L1))|| = ||filter(eq x;list-to-set(eq;L2))|| ∈ ℤ
BY
{ ((InstHyp [⌜x⌝] 12⋅ THENA Complete (Auto))
   THEN (InstHyp [⌜x⌝] 11⋅ THENA Complete (Auto))
   THEN (InstHyp [⌜x⌝] 10⋅ THENA Complete (Auto))
   THEN (InstHyp [⌜x⌝] 8⋅ THENA Complete (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. ∀a:T. ((a ∈ list-to-set(eq;L1)) ⇐⇒ (a ∈ L1))
9. no_repeats(T;list-to-set(eq;L2))
10. ∀a:T. ((a ∈ list-to-set(eq;L2)) ⇐⇒ (a ∈ L2))
11. ∀[x:T]. uiff(1 ≤ ||filter(eq x;list-to-set(eq;L2))||;||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ)
12. ∀[x:T]. uiff(1 ≤ ||filter(eq x;list-to-set(eq;L1))||;||filter(eq x;list-to-set(eq;L1))|| = 1 ∈ ℤ)
13. no_repeats(T;list-to-set(eq;L2))
14. no_repeats(T;list-to-set(eq;L1))
15. uiff(1 ≤ ||filter(eq x;list-to-set(eq;L1))||;||filter(eq x;list-to-set(eq;L1))|| = 1 ∈ ℤ)
16. uiff(1 ≤ ||filter(eq x;list-to-set(eq;L2))||;||filter(eq x;list-to-set(eq;L2))|| = 1 ∈ ℤ)
17. (x ∈ list-to-set(eq;L2)) ⇐⇒ (x ∈ L2)
18. (x ∈ list-to-set(eq;L1)) ⇐⇒ (x ∈ L1)
⊢ ||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.  \mforall{}a:T.  ((a  \mmember{}  list-to-set(eq;L1))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  L1))
9.  no\_repeats(T;list-to-set(eq;L2))
10.  \mforall{}a:T.  ((a  \mmember{}  list-to-set(eq;L2))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  L2))
11.  \mforall{}[x:T].  uiff(1  \mleq{}  ||filter(eq  x;list-to-set(eq;L2))||;||filter(eq  x;list-to-set(eq;L2))||  =  1)
12.  \mforall{}[x:T].  uiff(1  \mleq{}  ||filter(eq  x;list-to-set(eq;L1))||;||filter(eq  x;list-to-set(eq;L1))||  =  1)
13.  no\_repeats(T;list-to-set(eq;L2))
14.  no\_repeats(T;list-to-set(eq;L1))
\mvdash{}  ||filter(eq  x;list-to-set(eq;L1))||  =  ||filter(eq  x;list-to-set(eq;L2))||


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  12\mcdot{}  THENA  Complete  (Auto))
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  11\mcdot{}  THENA  Complete  (Auto))
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  10\mcdot{}  THENA  Complete  (Auto))
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  8\mcdot{}  THENA  Complete  (Auto)))

---

Home Index