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