---

Step * 1 1 1 1 1 of Lemma es-fset-last_wf


∀es:EO. ∀e':E. ∀v:E List.  ((¬↑null(v)) ⇒ sorted-by(λe,e'. e ≤loc e' ;v) ⇒ (last(v) <loc e') ⇒ (e' ∈ v) ⇒ False)
BY
{ Auto }

1
1. es : EO@i'
2. e' : E@i
3. v : E List@i
4. ¬↑null(v)@i
5. sorted-by(λe,e'. e ≤loc e' ;v)@i
6. (last(v) <loc e')@i
7. (e' ∈ v)@i
⊢ False

---

Latex:

---

Latex:

\mforall{}es:EO.  \mforall{}e':E.  \mforall{}v:E  List.
    ((\mneg{}\muparrow{}null(v))  {}\mRightarrow{}  sorted-by(\mlambda{}e,e'.  e  \mleq{}loc  e'  ;v)  {}\mRightarrow{}  (last(v)  <loc  e')  {}\mRightarrow{}  (e'  \mmember{}  v)  {}\mRightarrow{}  False)


By

---

Latex:
Auto

---

Home Index