---

Step * 1 of Lemma es-interval-last


1. es : EO
2. e2 : E
3. e1 : E
4. e1 ≤loc e2 
⊢ last([e1, e2]) ~ e2
BY
{ ((Unfold `es-interval` 0 THEN RWO "filter_append_sq" 0) THENA Auto) }

1
1. es : EO
2. e2 : E
3. e1 : E
4. e1 ≤loc e2 
⊢ last(filter(λev.e1 ≤loc ev;before(e2)) @ filter(λev.e1 ≤loc ev;[e2])) ~ e2

---

Latex:

---

Latex:

1.  es  :  EO
2.  e2  :  E
3.  e1  :  E
4.  e1  \mleq{}loc  e2 
\mvdash{}  last([e1,  e2])  \msim{}  e2


By

---

Latex:
((Unfold  `es-interval`  0  THEN  RWO  "filter\_append\_sq"  0)  THENA  Auto)

---

Home Index