{
the_es:EO.
SWellFounded((x
<
loc
y))
}
{
Proof
}
Definitions occuring in Statement
:
es-locl:
(e
<
loc
e')
,
es-E:
E
,
event_ordering:
EO
,
all:
x:A.
B[x]
,
strongwellfounded:
SWellFounded(R[x;
y])
Definitions
:
all:
x:A.
B[x]
,
member:
t
T
,
and:
P
Q
Lemmas
:
pes-axioms
,
event_ordering_wf
\mforall{}the$_{es}$:EO. SWellFounded((x <loc y))
Date html generated: 2011_08_16-AM-10_30_59
Last ObjectModification: 2010_09_24-PM-09_11_43
Home
Index
x:A. B[x], the_es:EO. SWellFounded((x <loc y)) }x:A. B[x], x:A. B[x], 
T, 
Q