---

Step * 2 1 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
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 
BY
{ RepeatFor 3 (AutoSplit) }

---

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
7.  u1  :  T
8.  v2  :  T  List
9.  filter(\mlambda{}t.((\mneg{}\msubb{}t  \mmember{}\msubb{}  v)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(eq  t  u)));v2)  \msim{}  filter(\mlambda{}x.(\mneg{}\msubb{}((eq  u  x)  \mvee{}\msubb{}x  \mmember{}\msubb{}  v));v2)
\mvdash{}  if  (\mneg{}\msubb{}u1  \mmember{}\msubb{}  v)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(eq  u1  u))
then  [u1  /  filter(\mlambda{}t.((\mneg{}\msubb{}t  \mmember{}\msubb{}  v)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(eq  t  u)));v2)]
else  filter(\mlambda{}t.((\mneg{}\msubb{}t  \mmember{}\msubb{}  v)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(eq  t  u)));v2)
fi    \msim{}  if  \mneg{}\msubb{}((eq  u  u1)  \mvee{}\msubb{}u1  \mmember{}\msubb{}  v)
then  [u1  /  filter(\mlambda{}x.(\mneg{}\msubb{}((eq  u  x)  \mvee{}\msubb{}x  \mmember{}\msubb{}  v));v2)]
else  filter(\mlambda{}x.(\mneg{}\msubb{}((eq  u  x)  \mvee{}\msubb{}x  \mmember{}\msubb{}  v));v2)
fi 


By

---

Latex:
RepeatFor  3  (AutoSplit)

---

Home Index