{ 
the_es:EO. e',e:E. Dec(e c
e') }
{ Proof }
Definitions occuring in Statement :
es-causle: e c e',
es-E: E,
event_ordering: EO,
decidable: Dec(P),
all: x:A. B[x]
Definitions :
all: x:A. B[x],
es-causle: e c e',
prop: 
,
member: t 
T,
implies: P 
Q
Lemmas :
decidable__or,
es-causl_wf,
decidable__es-causl,
decidable__es-E-equal,
es-E_wf,
event_ordering_wf
\mforall{}the$_{es}$:EO. \mforall{}e',e:E. Dec(e c\mleq{} e')
Date html generated:
2011_08_16-AM-10_35_22
Last ObjectModification:
2010_09_24-PM-09_08_26
Home
Index