---

Step * 2 1 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(λ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))
BY
{ (GenConclAtAddr [1;2] THEN Thin (-1) THEN ListInd (-1) THEN Reduce 0 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
7. u1 : T
8. v2 : T List
9. filter(λt.((¬bt ∈b v) ∧b (¬b(eq t u)));v2) ~ filter(λx.(¬b((eq u x) ∨bx ∈b v));v2)
⊢ if (¬bu1 ∈b v) ∧b (¬b(eq u1 u))
then [u1 / filter(λt.((¬bt ∈b v) ∧b (¬b(eq t u)));v2)]
else filter(λt.((¬bt ∈b v) ∧b (¬b(eq t u)));v2)
fi  ~ if ¬b((eq u u1) ∨bu1 ∈b v)
then [u1 / filter(λx.(¬b((eq u x) ∨bx ∈b v));v2)]
else filter(λx.(¬b((eq u x) ∨bx ∈b v));v2)
fi 

---

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{}t.((\mneg{}\msubb{}t  \mmember{}\msubb{}  v)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(eq  t  u)));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:
(GenConclAtAddr  [1;2]  THEN  Thin  (-1)  THEN  ListInd  (-1)  THEN  Reduce  0  THEN  Try  (Trivial))

---

Home Index