{
[the_es:EO].
[e,e':E].
(e
c
e'
)
}
{
Proof
}
Definitions occuring in Statement
:
es-causle:
e
c
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-causle:
e
c
e'
,
or:
P
Q
Lemmas
:
es-causl_wf
,
es-E_wf
,
event_ordering_wf
\mforall{}[the$_{es}$:EO]. \mforall{}[e,e':E]. (e c\mleq{} e' \mmember{} \mBbbP{})
Date html generated: 2011_08_16-AM-10_28_54
Last ObjectModification: 2011_06_18-AM-09_11_12
Home
Index
e', 
[the_es:EO]. [e,e':E]. (e c e' 
) } e', [x:A]. B[x], , T[x:A]. B[x], T, , e', 
Q