---

{ [Info:Type]. [es:EO+(Info)]. [P:E  ].
    (last(P)  e:E  ((e':{E| ((e' <loc e)
                       ((P e'))
                       (e'':E
                           ((e' <loc e'')  (e'' <loc e)  ((P e'')))))})
                       ((e':{E| ((e' <loc e)  ((P e')))})))) }

{ Proof }

---

Definitions occuring in Statement :  es-local-pred: last(P),  event-ordering+: EO+(Info),  es-locl: (e <loc e'),  es-E: E,  assert: b,  bool: ,  uall: [x:A]. B[x],  all: x:A. B[x],  sq_exists: x:{A| B[x]},  not: A,  implies: P  Q,  or: P  Q,  and: P  Q,  member: t  T,  apply: f a,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  es-local-pred: last(P),  top: Top,  ycomb: Y,  all: x:A. B[x],  subtype: S  T,  suptype: suptype(S; T),  prop:
Lemmas :  es-local-pred_wf2,  es-E_wf,  event-ordering+_inc,  bool_wf,  event-ordering+_wf,  es-locl_wf

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[P:E  {}\mrightarrow{}  \mBbbB{}].
    (last(P)  \mmember{}  e:E  {}\mrightarrow{}  ((\mexists{}e':\{E|  ((e'  <loc  e)
                                        \mwedge{}  (\muparrow{}(P  e'))
                                        \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e'')))))\})
                                        \mvee{}  (\mneg{}(\mexists{}e':\{E|  ((e'  <loc  e)  \mwedge{}  (\muparrow{}(P  e')))\}))))


Date html generated: 2011_08_16-PM-04_40_02
Last ObjectModification: 2011_06_20-AM-01_02_04

Home Index