---

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

{ Proof }

---

Definitions occuring in Statement :  es-closed-open-interval: [e;e'),  es-le: e loc 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 :  uall: [x:A]. B[x],  function: x:A  B[x],  all: x:A. B[x],  equal: s = t,  member: t  T,  isect: x:A. B[x],  es-E: E,  event_ordering: EO,  product: x:A  B[x],  and: P  Q,  iff: P  Q,  CollapseTHENM: Error :CollapseTHENM,  CollapseTHEN: Error :CollapseTHEN,  l_member: (x  l),  assert: b,  es-le: e loc e' ,  es-locl: (e <loc e'),  implies: P  Q,  es-closed-open-interval: [e;e'),  rev_implies: P  Q,  filter: filter(P;l),  top: Top,  set: {x:A| B[x]} ,  es-before: before(e),  lambda: x.A[x],  es-ble: Error :es-ble,  prop: ,  universe: Type
Lemmas :  member_filter,  iff_functionality_wrt_iff,  and_functionality_wrt_iff,  member-es-before,  assert-es-ble,  iff_wf,  rev_implies_wf,  filter_wf,  es-before_wf,  l_member_wf,  assert_wf,  Error :es-ble_wf,  es-locl_wf,  es-le_wf,  event_ordering_wf,  es-E_wf

---

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


Date html generated: 2011_08_16-AM-10_39_13
Last ObjectModification: 2010_11_15-PM-10_33_23

Home Index