---

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


1. x : ℤ
⊢ ((x ∈ []) ⇐⇒ int-list-index([];x) < ||[]||) ∧ ((x ∈ []) ⇒ ([][int-list-index([];x)] = x ∈ ℤ))
BY
{ xxx(Reduce 0 THEN Auto')xxx }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
\mvdash{}  ((x  \mmember{}  [])  \mLeftarrow{}{}\mRightarrow{}  int-list-index([];x)  <  ||[]||)  \mwedge{}  ((x  \mmember{}  [])  {}\mRightarrow{}  ([][int-list-index([];x)]  =  x))


By

---

Latex:
xxx(Reduce  0  THEN  Auto')xxx

---

Home Index