{ 
es:EO. e':E. 
e:E. ((
first(e)) 
e 
loc e' ) }
{ 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 :
all: x:A. B[x],
exists: x:A. B[x],
and: P Q,
member: t 
T,
prop: 
,
implies: P 
Q,
so_lambda: 
x.t[x],
es-le: e loc e' ,
or: P 
Q,
guard: {T},
cand: A c B,
wellfounded: WellFnd{i}(A;x,y.R[x; y]),
so_apply: x[s],
decidable: Dec(P),
trans: Trans(T;x,y.E[x; y])
Lemmas :
event_ordering_wf,
es-E_wf,
assert_wf,
es-first_wf,
es-le_wf,
es-locl_wf,
es-locl-wellfnd,
decidable__assert,
es-pred_wf,
es-pred-locl,
es-le-trans
\mforall{}es:EO. \mforall{}e':E. \mexists{}e:E. ((\muparrow{}first(e)) \mwedge{} e \mleq{}loc e' )
Date html generated:
2011_08_16-AM-10_44_57
Last ObjectModification:
2010_09_24-PM-09_04_03
Home
Index