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