---

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


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))|| ∈ ℤ
BY
{ ((Decide ⌜1 ≤ ||filter(eq x;list-to-set(eq;L))||⌝⋅ THENA Auto)
   THEN (Decide ⌜1 ≤ ||filter(eq x;remove-repeats(eq;L))||⌝⋅ THENA Auto)
   THEN ThinTrivial
   THEN Auto'
   THEN InstLemma `remove-repeats_property` [⌜T⌝;⌜eq⌝;⌜L⌝]⋅
   THEN Auto
   THEN (((InstHyp [⌜x⌝] (-1)⋅ THENA Auto) THEN (InstHyp [⌜x⌝] 7⋅ THENA Auto))
         THEN (All (RWO "l_member-iff-length-filter" ) THENA Auto)
         THEN Repeat (ThinTrivial)
         THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  \mforall{}a1,b1:T  List.    (\mforall{}x:T.  (||filter(eq  x;a1)||  =  ||filter(eq  x;b1)||)  \mLeftarrow{}{}\mRightarrow{}  permutation(T;a1;b1))
5.  x  :  T
6.  no\_repeats(T;list-to-set(eq;L))
7.  \mforall{}a:T.  ((a  \mmember{}  list-to-set(eq;L))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  L))
8.  uiff(1  \mleq{}  ||filter(eq  x;list-to-set(eq;L))||;||filter(eq  x;list-to-set(eq;L))||  =  1)
9.  uiff(1  \mleq{}  ||filter(eq  x;remove-repeats(eq;L))||;||filter(eq  x;remove-repeats(eq;L))||  =  1)
\mvdash{}  ||filter(eq  x;list-to-set(eq;L))||  =  ||filter(eq  x;remove-repeats(eq;L))||


By

---

Latex:
((Decide  \mkleeneopen{}1  \mleq{}  ||filter(eq  x;list-to-set(eq;L))||\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}1  \mleq{}  ||filter(eq  x;remove-repeats(eq;L))||\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinTrivial
  THEN  Auto'
  THEN  InstLemma  `remove-repeats\_property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  7\mcdot{}  THENA  Auto))
              THEN  (All  (RWO  "l\_member-iff-length-filter"  )  THENA  Auto)
              THEN  Repeat  (ThinTrivial)
              THEN  Auto)\mcdot{})

---

Home Index