Step * 1 of Lemma implies-es-pred2


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