{ 
es:EO. e,a:E.
((a <loc e) 
(
b:E. ((
first(b)) c
((a = pred(b)) b 
loc e )))) }
{ Proof }
Definitions occuring in Statement :
es-le: e loc e' ,
es-locl: (e <loc e'),
es-pred: pred(e),
es-first: first(e),
es-E: E,
event_ordering: EO,
assert: b,
cand: A c B,
all: x:A. B[x],
exists: x:A. B[x],
not: A,
implies: P Q,
and: P Q,
equal: s = t
Definitions :
all: x:A. B[x],
implies: P Q,
exists: x:A. B[x],
cand: A c B,
and: P Q,
member: t 
T,
prop: 
,
so_lambda: 
x.t[x],
es-le: e loc e' ,
or: P 
Q,
guard: {T},
iff: P 
Q,
wellfounded: WellFnd{i}(A;x,y.R[x; y]),
so_apply: x[s]
Lemmas :
event_ordering_wf,
es-E_wf,
es-locl_wf,
not_wf,
assert_wf,
es-first_wf,
es-pred_wf,
es-le_wf,
es-locl-iff,
es-locl-wellfnd,
es-pred-locl,
es-locl_transitivity1,
es-le_weakening
\mforall{}es:EO. \mforall{}e,a:E. ((a <loc e) {}\mRightarrow{} (\mexists{}b:E. ((\mneg{}\muparrow{}first(b)) c\mwedge{} ((a = pred(b)) \mwedge{} b \mleq{}loc e ))))
Date html generated:
2011_08_16-AM-10_33_38
Last ObjectModification:
2010_09_24-PM-09_09_09
Home
Index