{
[the_es:EO].
[e,e':E].
(e
=
e'
)
}
{
Proof
}
Definitions occuring in Statement
:
es-eq-E:
e
=
e'
,
es-E:
E
,
event_ordering:
EO
,
bool:
,
uall:
[x:A].
B[x]
,
member:
t
T
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
,
es-eq-E:
e
=
e'
Lemmas
:
eqof_wf
,
es-eq_wf
,
es-E_wf
,
event_ordering_wf
\mforall{}[the$_{es}$:EO]. \mforall{}[e,e':E]. (e = e' \mmember{} \mBbbB{})
Date html generated: 2011_08_16-AM-10_27_01
Last ObjectModification: 2011_06_18-AM-09_10_48
Home
Index
, 
[the_es:EO]. [e,e':E]. (e = e' 
) }, [x:A]. B[x], T[x:A]. B[x], T,