---

Step * of Lemma int-list-index-property

∀x:ℤ. ∀L:ℤ List.  (((x ∈ L) ⇐⇒ int-list-index(L;x) < ||L||) ∧ ((x ∈ L) ⇒ (L[int-list-index(L;x)] = x ∈ ℤ)))
BY
{ xxxInductionOnListxxx }

1
1. x : ℤ
⊢ ((x ∈ []) ⇐⇒ int-list-index([];x) < ||[]||) ∧ ((x ∈ []) ⇒ ([][int-list-index([];x)] = x ∈ ℤ))

2
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 ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}x:\mBbbZ{}.  \mforall{}L:\mBbbZ{}  List.
    (((x  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  int-list-index(L;x)  <  ||L||)  \mwedge{}  ((x  \mmember{}  L)  {}\mRightarrow{}  (L[int-list-index(L;x)]  =  x)))


By

---

Latex:
xxxInductionOnListxxx

---

Home Index