Step
*
1
of Lemma
es-le-not-locl
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. loc(e) = loc(e') ∈ Id
5. ¬(e' <loc e)@i
⊢ e ≤loc e' 
BY
{ (((Inst_ES_Axiom [⌈e⌉; ⌈e'⌉] 3)⋅ THENA Auto)
   THEN (D (-1))
   THEN (Thin (-1))
   THEN (D (-1))
   THEN Try (Trivial)
   THEN Unfold `es-le` 0
   THEN SplitOrHyps
   THEN Auto) }
Latex:
1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  loc(e)  =  loc(e')
5.  \mneg{}(e'  <loc  e)@i
\mvdash{}  e  \mleq{}loc  e' 
By
(((Inst\_ES\_Axiom  [\mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{}]  3)\mcdot{}  THENA  Auto)
  THEN  (D  (-1))
  THEN  (Thin  (-1))
  THEN  (D  (-1))
  THEN  Try  (Trivial)
  THEN  Unfold  `es-le`  0
  THEN  SplitOrHyps
  THEN  Auto)
Home
Index