{ 
es:EO. e:E. 
x:E. (x 
loc e 
(
first(x))) }
{ Proof }
Definitions occuring in Statement :
es-le: e loc e' ,
es-first: first(e),
es-E: E,
event_ordering: EO,
assert: b,
all: x:A. B[x],
exists: x:A. B[x],
and: P Q
Definitions :
implies: P 
Q,
cand: A c B,
all: x:A. B[x],
and: P Q,
exists: x:A. B[x],
prop: 
,
member: t 
T,
guard: {T},
or: P 
Q,
es-le: e loc e' ,
decidable: Dec(P)
Lemmas :
event_ordering_wf,
es-causl_wf,
es-first_wf,
assert_wf,
es-le_wf,
es-E_wf,
decidable__assert,
es-locl_wf,
es-pred-causl,
es-pred_wf,
es-loc-pred,
es-le_weakening,
es-locl_transitivity1,
es-pred-locl
\mforall{}es:EO. \mforall{}e:E. \mexists{}x:E. (x \mleq{}loc e \mwedge{} (\muparrow{}first(x)))
Date html generated:
2011_08_16-AM-11_19_31
Last ObjectModification:
2010_09_24-PM-07_03_04
Home
Index