---

Step * 1 2 1 of Lemma eo-forward-trivial


1. Info : Type
2. eo : EO+(Info)
3. e : E
4. ↑first(e)
5. x : es-base-E(eo)
6. ↑(es-dom(eo) x)
7. e' : E@i
8. ¬e ≤loc e' 
9. x = e' ∈ E@i
10. loc(e') = loc(e) ∈ Id
⊢ ff = tt
BY
{ ((FLemma `es-le-total` [-1] THENM RepeatFor 2 (D -1)) THEN Auto THEN (RelRST THEN Auto)⋅) }

---

Latex:



1.  Info  :  Type
2.  eo  :  EO+(Info)
3.  e  :  E
4.  \muparrow{}first(e)
5.  x  :  es-base-E(eo)
6.  \muparrow{}(es-dom(eo)  x)
7.  e'  :  E@i
8.  \mneg{}e  \mleq{}loc  e' 
9.  x  =  e'@i
10.  loc(e')  =  loc(e)
\mvdash{}  ff  =  tt


By

((FLemma  `es-le-total`  [-1]  THENM  RepeatFor  2  (D  -1))  THEN  Auto  THEN  (RelRST  THEN  Auto)\mcdot{})

---

Home Index