Step * 1 of Lemma es-le-not-locl


1. es EO@i'
2. 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