---

Step * of Lemma remove-repeats_property

∀[T:Type]
  ∀eq:EqDecider(T). ∀L:T List.  (no_repeats(T;remove-repeats(eq;L)) ∧ (∀a:T. ((a ∈ remove-repeats(eq;L)) ⇐⇒ (a ∈ L))))
BY
{ (InductionOnList THEN Unfold `remove-repeats` 0 THEN Reduce 0 THEN Try (Fold `remove-repeats` 0) THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. no_repeats(T;remove-repeats(eq;v))
6. ∀a:T. ((a ∈ remove-repeats(eq;v)) ⇐⇒ (a ∈ v))
7. no_repeats(T;filter(λx.(¬b(eq x u));remove-repeats(eq;v)))
⊢ ¬(u ∈ filter(λx.(¬b(eq x u));remove-repeats(eq;v)))

2
1. [T] : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. no_repeats(T;remove-repeats(eq;v))
6. ∀a:T. ((a ∈ remove-repeats(eq;v)) ⇐⇒ (a ∈ v))
7. no_repeats(T;[u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))])
8. a : T
9. (a ∈ [u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))])
⊢ (a ∈ [u / v])

3
1. [T] : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. no_repeats(T;remove-repeats(eq;v))
6. ∀a:T. ((a ∈ remove-repeats(eq;v)) ⇐⇒ (a ∈ v))
7. no_repeats(T;[u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))])
8. a : T
9. (a ∈ [u / v])
⊢ (a ∈ [u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))])

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.
        (no\_repeats(T;remove-repeats(eq;L))  \mwedge{}  (\mforall{}a:T.  ((a  \mmember{}  remove-repeats(eq;L))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  L))))


By

---

Latex:
(InductionOnList
  THEN  Unfold  `remove-repeats`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `remove-repeats`  0)
  THEN  Auto)

---

Home Index