---

Step * 2 1 of Lemma remove-repeats-fun-member


1. [A] : Type
2. [B] : Type
3. eq : EqDecider(B)
4. f : A ⟶ B
5. u : A
6. v : A List
7. ∀a:A. ((a ∈ remove-repeats-fun(eq;f;v)) ⇐⇒ ∃i:ℕ||v||. ((v[i] = a ∈ A) ∧ (∀j:ℕi. (¬((f v[j]) = (f a) ∈ B)))))
8. a : A
9. i : ℕ||v|| + 1
10. v[i - 1] = a ∈ A
11. ∀j:ℕi. (¬((f [u / v][j]) = (f a) ∈ B))
12. ¬(i = 0 ∈ ℤ)
⊢ (a = u ∈ A) ∨ (a ∈ filter(λx.(¬b(eq (f x) (f u)));remove-repeats-fun(eq;f;v)))
BY
{ ((InstHyp [⌜0⌝] (-2)⋅ THENA Auto) THEN Reduce (-1) THEN (OrRight THENA Auto) THEN Reduce 0 THEN Auto) }

1
1. [A] : Type
2. [B] : Type
3. eq : EqDecider(B)
4. f : A ⟶ B
5. u : A
6. v : A List
7. ∀a:A. ((a ∈ remove-repeats-fun(eq;f;v)) ⇐⇒ ∃i:ℕ||v||. ((v[i] = a ∈ A) ∧ (∀j:ℕi. (¬((f v[j]) = (f a) ∈ B)))))
8. a : A
9. i : ℕ||v|| + 1
10. v[i - 1] = a ∈ A
11. ∀j:ℕi. (¬((f [u / v][j]) = (f a) ∈ B))
12. ¬(i = 0 ∈ ℤ)
13. ¬((f u) = (f a) ∈ B)
⊢ (a ∈ remove-repeats-fun(eq;f;v))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  eq  :  EqDecider(B)
4.  f  :  A  {}\mrightarrow{}  B
5.  u  :  A
6.  v  :  A  List
7.  \mforall{}a:A
          ((a  \mmember{}  remove-repeats-fun(eq;f;v))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||.  ((v[i]  =  a)  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}((f  v[j])  =  (f  a))))))
8.  a  :  A
9.  i  :  \mBbbN{}||v||  +  1
10.  v[i  -  1]  =  a
11.  \mforall{}j:\mBbbN{}i.  (\mneg{}((f  [u  /  v][j])  =  (f  a)))
12.  \mneg{}(i  =  0)
\mvdash{}  (a  =  u)  \mvee{}  (a  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  (f  x)  (f  u)));remove-repeats-fun(eq;f;v)))


By

---

Latex:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  (OrRight  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index