---

Step * 2 1 1 1 of Lemma remove-repeats-append-sq


1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀[L2:T List]. (remove-repeats(eq;v @ L2) ~ remove-repeats(eq;v) @ filter(λx.(¬bx ∈b v);remove-repeats(eq;L2)))
6. L2 : T List
⊢ filter(λx.(¬b(eq x u));filter(λx.(¬bx ∈b v);remove-repeats(eq;L2))) 
~ filter(λx.(¬b((eq u x) ∨bx ∈b v));remove-repeats(eq;L2))
BY
{ ((RWO "filter-filter" 0 THENA Auto) THEN Reduce 0) }

1
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀[L2:T List]. (remove-repeats(eq;v @ L2) ~ remove-repeats(eq;v) @ filter(λx.(¬bx ∈b v);remove-repeats(eq;L2)))
6. L2 : T List
⊢ filter(λt.((¬bt ∈b v) ∧b (¬b(eq t u)));remove-repeats(eq;L2)) 
~ filter(λx.(¬b((eq u x) ∨bx ∈b v));remove-repeats(eq;L2))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}[L2:T  List]
          (remove-repeats(eq;v  @  L2)  \msim{}  remove-repeats(eq;v)
          @  filter(\mlambda{}x.(\mneg{}\msubb{}x  \mmember{}\msubb{}  v);remove-repeats(eq;L2)))
6.  L2  :  T  List
\mvdash{}  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));filter(\mlambda{}x.(\mneg{}\msubb{}x  \mmember{}\msubb{}  v);remove-repeats(eq;L2))) 
\msim{}  filter(\mlambda{}x.(\mneg{}\msubb{}((eq  u  x)  \mvee{}\msubb{}x  \mmember{}\msubb{}  v));remove-repeats(eq;L2))


By

---

Latex:
((RWO  "filter-filter"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index