---

Step * of Lemma es-first-le

∀es:EO. ∀e,e':E.  (e ≤loc e' ) supposing ((loc(e) = loc(e') ∈ Id) and (↑first(e)))
BY
{ (Auto THEN (InstLemma `es-first-implies` [⌈es⌉; ⌈e⌉; ⌈e'⌉])⋅ THEN Auto) }

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

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':E.    (e  \mleq{}loc  e'  )  supposing  ((loc(e)  =  loc(e'))  and  (\muparrow{}first(e)))


By

(Auto  THEN  (InstLemma  `es-first-implies`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{}])\mcdot{}  THEN  Auto)

---

Home Index