---

Step * 2 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
⊢ [u / filter(λx.(¬b(eq x u));remove-repeats(eq;v @ L2))] ~ [u / 
                                                             (filter(λx.(¬b(eq x u));remove-repeats(eq;v))
                                                             @ filter(λx.(¬b((eq u x) ∨bx ∈b v));
                                                                      remove-repeats(eq;L2)))]
BY
{ (EqCD THEN Try (Trivial)) }

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 @ 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{}  [u  /  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;v  @  L2))]  \msim{}  [u  / 
                                                                                                                          (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:
(EqCD  THEN  Try  (Trivial))

---

Home Index