---

Step * of Lemma list-to-set_functionality_wrt_permutation

∀[T:Type]
  ∀eq:EqDecider(T). ∀L1,L2:T List.  (permutation(T;L1;L2) ⇒ permutation(T;list-to-set(eq;L1);list-to-set(eq;L2)))
BY
{ (Auto
   THEN (InstLemma `permutation-iff-count1` [⌜T⌝;⌜eq⌝]⋅ THENA (Auto THEN RW assert_pushdownC (-1) THEN Auto))
   THEN BHyp (-1)
   THEN Auto
   THEN Thin (-2)
   THEN (InstLemma `list-to-set-property` [⌜T⌝;⌜eq⌝;⌜L1⌝]⋅ THENA Auto)
   THEN (InstLemma `list-to-set-property` [⌜T⌝;⌜eq⌝;⌜L2⌝]⋅ THENA Auto)
   THEN (InstLemma `no-repeats-iff-count` [⌜T⌝;⌜eq⌝;⌜list-to-set(eq;L1)⌝]⋅ THENA Auto)
   THEN (InstLemma `no-repeats-iff-count` [⌜T⌝;⌜eq⌝;⌜list-to-set(eq;L2)⌝]⋅ THENA Auto)
   THEN Auto
   THEN ThinTrivial) }

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))
⊢ ||filter(eq x;list-to-set(eq;L1))|| = ||filter(eq x;list-to-set(eq;L2))|| ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}L1,L2:T  List.
        (permutation(T;L1;L2)  {}\mRightarrow{}  permutation(T;list-to-set(eq;L1);list-to-set(eq;L2)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `permutation-iff-count1`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RW  assert\_pushdownC  (-1)  THEN  Auto)
              )
  THEN  BHyp  (-1)
  THEN  Auto
  THEN  Thin  (-2)
  THEN  (InstLemma  `list-to-set-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `list-to-set-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `no-repeats-iff-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}list-to-set(eq;L1)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `no-repeats-iff-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}list-to-set(eq;L2)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Auto
  THEN  ThinTrivial)

---

Home Index