---

Step * 4 2 of Lemma pes-axioms


1. the_es : EO@i'
2. e : E@i
3. ∀e':E. (¬(e' <loc e))@i
4. e' : E
5. loc(e') = loc(e) ∈ Id
⊢ ¬(e' < e)
BY
{ ((InstHyp [⌈e'⌉] 3⋅ THEN Auto)⋅ THEN ParallelLast THEN D 0 THEN Auto) }

---

Latex:



1.  the$_{es}$  :  EO@i'
2.  e  :  E@i
3.  \mforall{}e':E.  (\mneg{}(e'  <loc  e))@i
4.  e'  :  E
5.  loc(e')  =  loc(e)
\mvdash{}  \mneg{}(e'  <  e)


By

((InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  3\mcdot{}  THEN  Auto)\mcdot{}  THEN  ParallelLast  THEN  D  0  THEN  Auto)

---

Home Index