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 THEN Auto) }

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


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

(Auto  THEN  D  0  THEN  Auto)




Home Index