---

Step * of Lemma remove-repeats-append-one

∀[T:Type]
  ∀eq:EqDecider(T). ∀L:T List. ∀x:T.
    ((||remove-repeats(eq;L @ [x])|| = ||remove-repeats(eq;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))
⊢ (||remove-repeats(eq;L @ [x])|| = ||remove-repeats(eq;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.
        ((||remove-repeats(eq;L  @  [x])||  =  ||remove-repeats(eq;L)||)
        \mvee{}  (||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))

---

Home Index