{
[the_es:EO].
[e,e':E].
(e
loc
e'
)
}
{
Proof
}
Definitions occuring in Statement
:
es-le:
e
loc
e'
,
es-E:
E
,
event_ordering:
EO
,
uall:
[x:A].
B[x]
,
prop:
,
member:
t
T
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
,
prop:
,
es-le:
e
loc
e'
,
or:
P
Q
Lemmas
:
es-locl_wf
,
es-E_wf
,
event_ordering_wf
\mforall{}[the$_{es}$:EO]. \mforall{}[e,e':E]. (e \mleq{}loc e' \mmember{} \mBbbP{})
Date html generated: 2011_08_16-AM-10_25_49
Last ObjectModification: 2011_06_18-AM-09_10_04
Home
Index
loc e' , 
[the_es:EO]. [e,e':E]. (e loc e' 
) }loc e' , [x:A]. B[x], , T[x:A]. B[x], T, , loc e' , 
Q