---

Step * 1 of Lemma remove-repeats_property


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)))
BY
{ (RWW "member_filter" 0 THEN Reduce 0 THEN Auto THEN RW assert_pushdownC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  no\_repeats(T;remove-repeats(eq;v))
6.  \mforall{}a:T.  ((a  \mmember{}  remove-repeats(eq;v))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  v))
7.  no\_repeats(T;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;v)))
\mvdash{}  \mneg{}(u  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;v)))


By

---

Latex:
(RWW  "member\_filter"  0  THEN  Reduce  0  THEN  Auto  THEN  RW  assert\_pushdownC  0  THEN  Auto)

---

Home Index