---

Step * 2 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));remove-repeats(eq;v @ L2)) ~ filter(λx.(¬b(eq x u));remove-repeats(eq;v))
@ filter(λx.(¬b((eq u x) ∨bx ∈b v));remove-repeats(eq;L2))
BY
{ (RWO "-2" 0 THENA Auto) }

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(λx.(¬b(eq x u));remove-repeats(eq;v) @ filter(λx.(¬bx ∈b v);remove-repeats(eq;L2))) 
~ filter(λx.(¬b(eq x u));remove-repeats(eq;v)) @ 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));remove-repeats(eq;v  @  L2))  \msim{}  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;v))
@  filter(\mlambda{}x.(\mneg{}\msubb{}((eq  u  x)  \mvee{}\msubb{}x  \mmember{}\msubb{}  v));remove-repeats(eq;L2))


By

---

Latex:
(RWO  "-2"  0  THENA  Auto)

---

Home Index