---

Step * of Lemma remove-repeats-append-sq

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L1,L2:T List].
  (remove-repeats(eq;L1 @ L2) ~ remove-repeats(eq;L1) @ filter(λx.(¬bx ∈b L1);remove-repeats(eq;L2)))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN Unfold `remove-repeats` 0 THEN Reduce 0 THEN Fold `remove-repeats` 0) }

1
1. T : Type
2. eq : EqDecider(T)
3. L2 : T List
⊢ remove-repeats(eq;L2) ~ filter(λx.tt;remove-repeats(eq;L2))

2
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)))]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L1,L2:T  List].
    (remove-repeats(eq;L1  @  L2)  \msim{}  remove-repeats(eq;L1)
    @  filter(\mlambda{}x.(\mneg{}\msubb{}x  \mmember{}\msubb{}  L1);remove-repeats(eq;L2)))


By

---

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

---

Home Index