---

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


∀es:EO. ∀e,e':E.  (e' ≤loc e  ⇒ ([e', e] = (if e' <loc e then [e'] else [] fi  @ (e', e) @ [e]) ∈ (E List)))
BY
{ ((D 0 THENA Auto) THEN CausalInd' THEN (D 0 THENA Auto) THEN RepUR ``es-open-interval es-interval`` 0) }

1
1. es : EO@i'
2. e : E@i
3. ∀e1:E
     ((e1 < e)
     ⇒ (∀e':E. (e' ≤loc e1  ⇒ ([e', e1] = (if e' <loc e1 then [e'] else [] fi  @ (e', e1) @ [e1]) ∈ (E List)))))
4. e' : E@i
⊢ e' ≤loc e 
⇒ (filter(λev.e' ≤loc ev;before(e) @ [e])
   = (if e' <loc e then [e'] else [] fi  @ filter(λev.e' <loc ev;before(e)) @ [e])
   ∈ (E List))

---

Latex:



\mforall{}es:EO.  \mforall{}e,e':E.    (e'  \mleq{}loc  e    {}\mRightarrow{}  ([e',  e]  =  (if  e'  <loc  e  then  [e']  else  []  fi    @  (e',  e)  @  [e])))


By

((D  0  THENA  Auto)
  THEN  CausalInd'
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``es-open-interval  es-interval``  0)

---

Home Index