---

Step * 2 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. (([u / v][i] = a ∈ A) ∧ (∀j:ℕi. (¬((f [u / v][j]) = (f a) ∈ B))))
⊢ (a ∈ [u / filter(λx.(¬b(eq (f x) (f u)));remove-repeats-fun(eq;f;v))])
BY
{ (ExRepD
   THEN (RW ListC 0 THENA Auto)
   THEN (Decide ⌜i = 0 ∈ ℤ⌝⋅ THENA Auto)
   THEN Try (Complete (((RWO "-1" (-3) THENA Auto) THEN AllReduce THEN OrLeft THEN Auto)))
   THEN (RWO "select_cons_tl" (-3) THENA 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 ∈ ℤ)
⊢ (a = u ∈ A) ∨ (a ∈ filter(λx.(¬b(eq (f x) (f u)));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.  \mexists{}i:\mBbbN{}||v||  +  1.  (([u  /  v][i]  =  a)  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}((f  [u  /  v][j])  =  (f  a)))))
\mvdash{}  (a  \mmember{}  [u  /  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  (f  x)  (f  u)));remove-repeats-fun(eq;f;v))])


By

---

Latex:
(ExRepD
  THEN  (RW  ListC  0  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}i  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  (((RWO  "-1"  (-3)  THENA  Auto)  THEN  AllReduce  THEN  OrLeft  THEN  Auto)))
  THEN  (RWO  "select\_cons\_tl"  (-3)  THENA  Auto))

---

Home Index