---

Step * 1 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. (a ∈ remove-repeats-fun(eq;f;v))
10. ¬((f a) = (f u) ∈ B)
11. i : ℕ||v||
12. v[i] = a ∈ A
13. ∀j:ℕi. (¬((f v[j]) = (f a) ∈ B))
⊢ ∃i:ℕ||v|| + 1. (([u / v][i] = a ∈ A) ∧ (∀j:ℕi. (¬((f [u / v][j]) = (f a) ∈ B))))
BY
{ (InstConcl [⌜i + 1⌝]⋅
   THEN Reduce 0
   THEN Auto
   THEN Try (Complete ((RWO "select_cons_tl" 0 THEN Auto)))
   THEN (Decide ⌜j = 0 ∈ ℤ⌝⋅ THENA Auto)
   THEN Try (Complete ((RWO "-1" 0 THEN Reduce 0 THEN Auto)))
   THEN RWO "select_cons_tl" 0
   THEN Reduce 0
   THEN Auto) }

---

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.  (a  \mmember{}  remove-repeats-fun(eq;f;v))
10.  \mneg{}((f  a)  =  (f  u))
11.  i  :  \mBbbN{}||v||
12.  v[i]  =  a
13.  \mforall{}j:\mBbbN{}i.  (\mneg{}((f  v[j])  =  (f  a)))
\mvdash{}  \mexists{}i:\mBbbN{}||v||  +  1.  (([u  /  v][i]  =  a)  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}((f  [u  /  v][j])  =  (f  a)))))


By

---

Latex:
(InstConcl  [\mkleeneopen{}i  +  1\mkleeneclose{}]\mcdot{}
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (Complete  ((RWO  "select\_cons\_tl"  0  THEN  Auto)))
  THEN  (Decide  \mkleeneopen{}j  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  ((RWO  "-1"  0  THEN  Reduce  0  THEN  Auto)))
  THEN  RWO  "select\_cons\_tl"  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index