{
es:EO.
e,e':E.
(e
loc
e'
e
c
e')
}
{
Proof
}
Definitions occuring in Statement
:
es-causle:
e
c
e'
,
es-le:
e
loc
e'
,
es-E:
E
,
event_ordering:
EO
,
all:
x:A.
B[x]
,
implies:
P
Q
Definitions
:
all:
x:A.
B[x]
,
implies:
P
Q
,
member:
t
T
,
prop:
Lemmas
:
es-causle_weakening_locl
,
es-le_wf
,
es-E_wf
,
event_ordering_wf
\mforall{}es:EO. \mforall{}e,e':E. (e \mleq{}loc e' {}\mRightarrow{} e c\mleq{} e')
Date html generated: 2011_08_16-AM-10_30_29
Last ObjectModification: 2010_09_24-PM-09_12_16
Home
Index
e', 
es:EO. e,e':E. (e loc e' 
e c e') } e', loc e' , x:A. B[x], Qx:A. B[x], Q, 
T, 