{
[es:EO].
(TR
E
)
}
{
Proof
}
Definitions occuring in Statement
:
es-TR:
TR
,
es-E:
E
,
event_ordering:
EO
,
uall:
[x:A].
B[x]
,
prop:
,
member:
t
T
,
function:
x:A
B[x]
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
,
prop:
,
es-TR:
TR
Lemmas
:
true_wf
,
es-E_wf
,
event_ordering_wf
\mforall{}[es:EO]. (TR \mmember{} E {}\mrightarrow{} \mBbbP{})
Date html generated: 2011_08_16-AM-10_50_05
Last ObjectModification: 2011_06_18-AM-09_25_19
Home
Index
[x:A]. B[x], [es:EO]. (TR 
E 
) }[x:A]. B[x], , T, B[x][x:A]. B[x], T, ,