---

Step * of Lemma remove-repeats-append-one-member

∀[T:Type]
  ∀eq:EqDecider(T). ∀L:T List. ∀x:T.
    (((x ∈ L) ∧ (||remove-repeats(eq;L @ [x])|| = ||remove-repeats(eq;L)|| ∈ ℤ))
    ∨ ((¬(x ∈ L)) ∧ (||remove-repeats(eq;L @ [x])|| = (||remove-repeats(eq;L)|| + 1) ∈ ℤ)))
BY
{ (Auto THEN (InstLemma `decidable__l_member` [⌜T⌝;⌜x⌝;⌜L⌝]⋅ THENA Auto))⋅ }

1
1. [T] : Type
2. eq : EqDecider(T)
3. L : T List
4. x : T
5. Dec((x ∈ L))
⊢ ((x ∈ L) ∧ (||remove-repeats(eq;L @ [x])|| = ||remove-repeats(eq;L)|| ∈ ℤ))
∨ ((¬(x ∈ L)) ∧ (||remove-repeats(eq;L @ [x])|| = (||remove-repeats(eq;L)|| + 1) ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}x:T.
        (((x  \mmember{}  L)  \mwedge{}  (||remove-repeats(eq;L  @  [x])||  =  ||remove-repeats(eq;L)||))
        \mvee{}  ((\mneg{}(x  \mmember{}  L))  \mwedge{}  (||remove-repeats(eq;L  @  [x])||  =  (||remove-repeats(eq;L)||  +  1))))


By

---

Latex:
(Auto  THEN  (InstLemma  `decidable\_\_l\_member`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto))\mcdot{}

---

Home Index