---

{ es:EO. e,e',ev:E.  ((ev  (e, e'))  (e <loc ev)  (ev <loc e')) }

{ Proof }

---

Definitions occuring in Statement :  es-open-interval: (e, e'),  es-locl: (e <loc e'),  es-E: E,  event_ordering: EO,  all: x:A. B[x],  iff: P  Q,  and: P  Q,  l_member: (x  l)
Definitions :  member: t  T,  all: x:A. B[x],  es-open-interval: (e, e'),  rev_implies: P  Q,  implies: P  Q,  iff: P  Q,  and: P  Q,  prop:
Lemmas :  event_ordering_wf,  es-E_wf,  member_filter,  assert-es-bless,  member-es-before,  and_functionality_wrt_iff,  iff_functionality_wrt_iff,  es-locl_wf,  assert_wf,  es-before_wf,  es-bless_wf,  filter_wf,  l_member_wf

---

\mforall{}es:EO.  \mforall{}e,e',ev:E.    ((ev  \mmember{}  (e,  e'))  \mLeftarrow{}{}\mRightarrow{}  (e  <loc  ev)  \mwedge{}  (ev  <loc  e'))


Date html generated: 2011_08_16-AM-10_38_58
Last ObjectModification: 2010_11_15-PM-10_32_28

Home Index