{
the_es:EO.
e,e':E.
Dec(e
=
e')
}
{
Proof
}
Definitions occuring in Statement
:
es-E:
E
,
event_ordering:
EO
,
decidable:
Dec(P)
,
all:
x:A.
B[x]
,
equal:
s
=
t
Definitions
:
all:
x:A.
B[x]
,
member:
t
T
Lemmas
:
decidable__equal-es-E
,
es-E_wf
,
event_ordering_wf
\mforall{}the$_{es}$:EO. \mforall{}e,e':E. Dec(e = e')
Date html generated: 2011_08_16-AM-10_27_16
Last ObjectModification: 2010_09_24-PM-09_14_27
Home
Index
x:A. B[x], the_es:EO. e,e':E. Dec(e = e') }x:A. B[x], x:A. B[x], 
T