---

Step * 1 of Lemma es-pred?_wf


1. es : EO
2. e : E
3. ↑first(e)
4. e' : E
5. (e' <loc e)
⊢ ¬↑first(e)
BY
{ ((RWO "assert-es-first" 0 THEN Auto) THEN D 0 THEN Auto) }

1
1. es : EO
2. e : E
3. ↑first(e)
4. e' : E
5. (e' <loc e)
6. ∀[e':E]. ¬(e' < e) supposing loc(e') = loc(e) ∈ Id@i
⊢ False

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  \muparrow{}first(e)
4.  e'  :  E
5.  (e'  <loc  e)
\mvdash{}  \mneg{}\muparrow{}first(e)


By

((RWO  "assert-es-first"  0  THEN  Auto)  THEN  D  0  THEN  Auto)

---

Home Index