---

Step * 2 3 1 1 1 of Lemma imax-list_functionality


1. L : ℤ List
2. 0 < ||L||
3. imax-list(L) ≤ imax-list([])
4. imax-list([]) ≤ imax-list(L)
5. (hd(L) ∈ L) ⇒ (hd(L) ∈ [])
6. (hd(L) ∈ L) ⇐ (hd(L) ∈ [])
⊢ 0 < ||[]||
BY
{ (D -2 THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
2.  0  <  ||L||
3.  imax-list(L)  \mleq{}  imax-list([])
4.  imax-list([])  \mleq{}  imax-list(L)
5.  (hd(L)  \mmember{}  L)  {}\mRightarrow{}  (hd(L)  \mmember{}  [])
6.  (hd(L)  \mmember{}  L)  \mLeftarrow{}{}  (hd(L)  \mmember{}  [])
\mvdash{}  0  <  ||[]||


By

---

Latex:
(D  -2  THEN  Auto)

---

Home Index