---

Step * 1 1 1 of Lemma eo-forward-interval


1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e : E
6. e ≤loc e1 
7. e1 ≤loc e2 
⊢ before(e2) = before(e2) ∈ (E List)
BY
{ (SubsumeC ⌈E List⌉⋅ THEN Auto)⋅ }

1
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e : E
6. e ≤loc e1 
7. e1 ≤loc e2 
⊢ before(e2) = before(e2) ∈ (E List)

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e1  :  E
4.  e2  :  E
5.  e  :  E
6.  e  \mleq{}loc  e1 
7.  e1  \mleq{}loc  e2 
\mvdash{}  before(e2)  =  before(e2)


By

(SubsumeC  \mkleeneopen{}E  List\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index