---

Step * 1 2 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. x = e' ∈ E@i
⊢ e ≤loc e' ∨b(¬bloc(e') = loc(e)) = tt
BY
{ (AutoBoolCase ⌈e ≤loc e'⌉⋅ THEN AutoBoolCase ⌈loc(e') = loc(e)⌉⋅) }

1
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

---

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.  x  =  e'@i
\mvdash{}  e  \mleq{}loc  e'  \mvee{}\msubb{}(\mneg{}\msubb{}loc(e')  =  loc(e))  =  tt


By

(AutoBoolCase  \mkleeneopen{}e  \mleq{}loc  e'\mkleeneclose{}\mcdot{}  THEN  AutoBoolCase  \mkleeneopen{}loc(e')  =  loc(e)\mkleeneclose{}\mcdot{})

---

Home Index