---

Step * 3 1 of Lemma remove-repeats_property


1. [T] : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. no_repeats(T;remove-repeats(eq;v))
6. ∀a:T. ((a ∈ remove-repeats(eq;v)) ⇐⇒ (a ∈ v))
7. no_repeats(T;[u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))])
8. a : T
9. (a = u ∈ T) ∨ (a ∈ v)
⊢ (a = u ∈ T) ∨ (a ∈ filter(λx.(¬b(eq x u));remove-repeats(eq;v)))
BY
{ Assert ⌜Dec(a = u ∈ T)⌝⋅ }

1
.....assertion..... 
1. [T] : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. no_repeats(T;remove-repeats(eq;v))
6. ∀a:T. ((a ∈ remove-repeats(eq;v)) ⇐⇒ (a ∈ v))
7. no_repeats(T;[u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))])
8. a : T
9. (a = u ∈ T) ∨ (a ∈ v)
⊢ Dec(a = u ∈ T)

2
1. [T] : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. no_repeats(T;remove-repeats(eq;v))
6. ∀a:T. ((a ∈ remove-repeats(eq;v)) ⇐⇒ (a ∈ v))
7. no_repeats(T;[u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))])
8. a : T
9. (a = u ∈ T) ∨ (a ∈ v)
10. Dec(a = u ∈ T)
⊢ (a = u ∈ T) ∨ (a ∈ filter(λx.(¬b(eq x u));remove-repeats(eq;v)))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  eq  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  no\_repeats(T;remove-repeats(eq;v))
6.  \mforall{}a:T.  ((a  \mmember{}  remove-repeats(eq;v))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  v))
7.  no\_repeats(T;[u  /  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;v))])
8.  a  :  T
9.  (a  =  u)  \mvee{}  (a  \mmember{}  v)
\mvdash{}  (a  =  u)  \mvee{}  (a  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;v)))


By

---

Latex:
Assert  \mkleeneopen{}Dec(a  =  u)\mkleeneclose{}\mcdot{}

---

Home Index