{ 
the_es:EO. WellFnd{i}(E;x,y.(x <loc y)) }
{ Proof }
Definitions occuring in Statement :
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
wellfounded: WellFnd{i}(A;x,y.R[x; y]),
all: x:A. B[x]
Definitions :
all: x:A. B[x],
implies: P 
Q,
strongwellfounded: SWellFounded(R[x; y]),
member: t 
T,
so_lambda: 
x y.t[x; y],
prop: 
,
exists: 
x:A. B[x],
so_apply: x[s1;s2],
nat: 
,
es-locl: (e <loc e'),
and: P 
Q
Lemmas :
strongwf-implies,
es-E_wf,
es-locl_wf,
es-causl-swellfnd,
nat_wf,
event_ordering_wf
\mforall{}the$_{es}$:EO. WellFnd\{i\}(E;x,y.(x <loc y))
Date html generated:
2011_08_16-AM-10_25_53
Last ObjectModification:
2010_09_24-PM-09_15_37
Home
Index