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