---

Step * of Lemma assert-int-list-member

∀i:ℤ. ∀xs:ℤ List.  (↑int-list-member(i;xs) ⇐⇒ (i ∈ xs))
BY
{ xxx(InductionOnList THEN (Unfold `int-list-member` 0 THEN Reduce 0) THEN Try (Fold `int-list-member` 0))xxx }

1
1. i : ℤ
⊢ False ⇐⇒ (i ∈ [])

2
1. i : ℤ
2. u : ℤ
3. v : ℤ List
4. ↑int-list-member(i;v) ⇐⇒ (i ∈ v)
⊢ ↑((i =z u) ∨bint-list-member(i;v)) ⇐⇒ (i ∈ [u / v])

---

Latex:

---

Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}xs:\mBbbZ{}  List.    (\muparrow{}int-list-member(i;xs)  \mLeftarrow{}{}\mRightarrow{}  (i  \mmember{}  xs))


By

---

Latex:
xxx(InductionOnList
        THEN  (Unfold  `int-list-member`  0  THEN  Reduce  0)
        THEN  Try  (Fold  `int-list-member`  0))xxx

---

Home Index