---

Step * 1 1 of Lemma es-pred?_wf


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
BY
{ (D -2 THEN InstHyp [⌈e'⌉] (-1)⋅ THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  \muparrow{}first(e)
4.  e'  :  E
5.  (e'  <loc  e)
6.  \mforall{}[e':E].  \mneg{}(e'  <  e)  supposing  loc(e')  =  loc(e)@i
\mvdash{}  False


By

(D  -2  THEN  InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index