---

Step * 1 of Lemma implies-es-pred2


1. es : EO
2. e : E
3. e' : E
4. ¬↑first(e)
5. pred(e) ≤loc e' 
6. (e' <loc e)
7. (e' <loc e)
8. e1 : E@i
9. (pred(e) <loc e)
10. ∀e':E. (¬((pred(e) <loc e') ∧ (e' <loc e)))
11. (e1 <loc e)@i
12. (e' <loc e1)@i
⊢ (pred(e) <loc e1)
BY
{ ((Using [`b',⌈e'⌉] (BLemma `es-le-trans2`))⋅ THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  e'  :  E
4.  \mneg{}\muparrow{}first(e)
5.  pred(e)  \mleq{}loc  e' 
6.  (e'  <loc  e)
7.  (e'  <loc  e)
8.  e1  :  E@i
9.  (pred(e)  <loc  e)
10.  \mforall{}e':E.  (\mneg{}((pred(e)  <loc  e')  \mwedge{}  (e'  <loc  e)))
11.  (e1  <loc  e)@i
12.  (e'  <loc  e1)@i
\mvdash{}  (pred(e)  <loc  e1)


By

((Using  [`b',\mkleeneopen{}e'\mkleeneclose{}]  (BLemma  `es-le-trans2`))\mcdot{}  THEN  Auto)

---

Home Index