---

Step * 2 of Lemma int-list-index-property


1. x : ℤ
2. u : ℤ
3. v : ℤ List
4. ((x ∈ v) ⇐⇒ int-list-index(v;x) < ||v||) ∧ ((x ∈ v) ⇒ (v[int-list-index(v;x)] = x ∈ ℤ))
⊢ ((x ∈ [u / v]) ⇐⇒ int-list-index([u / v];x) < ||[u / v]||)
∧ ((x ∈ [u / v]) ⇒ ([u / v][int-list-index([u / v];x)] = x ∈ ℤ))
BY
{ (Unfold `int-list-index` 0
   THEN Reduce 0
   THEN Fold `int-list-index` 0
   THEN (D 0 THENA Auto)
   THEN AutoSplit
   THEN Auto
   THEN Try ((RWO "cons_member" (-1) THENM D -1))
   THEN Auto
   THEN ThinTrivial
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  u  :  \mBbbZ{}
3.  v  :  \mBbbZ{}  List
4.  ((x  \mmember{}  v)  \mLeftarrow{}{}\mRightarrow{}  int-list-index(v;x)  <  ||v||)  \mwedge{}  ((x  \mmember{}  v)  {}\mRightarrow{}  (v[int-list-index(v;x)]  =  x))
\mvdash{}  ((x  \mmember{}  [u  /  v])  \mLeftarrow{}{}\mRightarrow{}  int-list-index([u  /  v];x)  <  ||[u  /  v]||)
\mwedge{}  ((x  \mmember{}  [u  /  v])  {}\mRightarrow{}  ([u  /  v][int-list-index([u  /  v];x)]  =  x))


By

---

Latex:
(Unfold  `int-list-index`  0
  THEN  Reduce  0
  THEN  Fold  `int-list-index`  0
  THEN  (D  0  THENA  Auto)
  THEN  AutoSplit
  THEN  Auto
  THEN  Try  ((RWO  "cons\_member"  (-1)  THENM  D  -1))
  THEN  Auto
  THEN  ThinTrivial
  THEN  Auto)

---

Home Index