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:
\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