---

Step * of Lemma es-causl-max-list

∀es:EO. ∀L:E List.  (0 < ||L|| ⇒ (¬(∀e:{e:E| (e ∈ L)} . ∃e':{e:E| (e ∈ L)} . (e < e'))))
BY
{ (Auto THEN D 0 THEN Auto) }

1
1. es : EO@i'
2. L : E List@i
3. 0 < ||L||@i
4. ∀e:{e:E| (e ∈ L)} . ∃e':{e:E| (e ∈ L)} . (e < e')@i
⊢ False

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}L:E  List.    (0  <  ||L||  {}\mRightarrow{}  (\mneg{}(\mforall{}e:\{e:E|  (e  \mmember{}  L)\}  .  \mexists{}e':\{e:E|  (e  \mmember{}  L)\}  .  (e  <  e'))))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index