---

Step * of Lemma list-to-set-is-remove-repeats

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

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ∀a1,b1:T List.  (∀x:T. (||filter(eq x;a1)|| = ||filter(eq x;b1)|| ∈ ℤ) ⇐⇒ permutation(T;a1;b1))
5. x : T
6. no_repeats(T;list-to-set(eq;L))
7. ∀a:T. ((a ∈ list-to-set(eq;L)) ⇐⇒ (a ∈ L))
8. uiff(1 ≤ ||filter(eq x;list-to-set(eq;L))||;||filter(eq x;list-to-set(eq;L))|| = 1 ∈ ℤ)
9. uiff(1 ≤ ||filter(eq x;remove-repeats(eq;L))||;||filter(eq x;remove-repeats(eq;L))|| = 1 ∈ ℤ)
⊢ ||filter(eq x;list-to-set(eq;L))|| = ||filter(eq x;remove-repeats(eq;L))|| ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.    permutation(T;list-to-set(eq;L);remove-repeats(eq;L))


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  ((InstLemma  `list-to-set-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  D  -1
              THEN  (InstLemma  `no-repeats-iff-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}list-to-set(eq;L)\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  D  (-1)
              THEN  Thin  (-1)
              THEN  (D  -1  THENA  Auto)
              THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
              THEN  Thin  (-2)
              THEN  ((InstLemma  `no-repeats-iff-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}remove-repeats(eq;L)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                          THEN  D  (-1)
                          THEN  Thin  (-1)
                          THEN  (D  -1  THENA  Auto)
                          THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                          THEN  Thin  (-2))\mcdot{})\mcdot{})

---

Home Index