---

Step * 1 1 1 of Lemma es-interval-eq2


1. es : EO
2. e : E
3. e' : E
4. e = e' ∈ E
⊢ (∀x∈before(e').¬↑((λev.e ≤loc ev) x))
BY
{ (Reduce 0 THEN BLemma `l_all_iff` THEN Auto) }

1
1. es : EO
2. e : E
3. e' : E
4. e = e' ∈ E
5. x : E@i
6. (x ∈ before(e'))@i
⊢ ¬↑e ≤loc x

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  e'  :  E
4.  e  =  e'
\mvdash{}  (\mforall{}x\mmember{}before(e').\mneg{}\muparrow{}((\mlambda{}ev.e  \mleq{}loc  ev)  x))


By

(Reduce  0  THEN  BLemma  `l\_all\_iff`  THEN  Auto)

---

Home Index