{ 
[p:EO 
']. [e:PossibleEvent(p)]. (pe-es(e) 
EO) }
{ Proof }
Definitions occuring in Statement :
pe-es: pe-es(e),
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: ,
possible-event: PossibleEvent(poss),
member: t T,
pe-es: pe-es(e),
top: Top,
all: x:A. B[x],
subtype: S 
T
Lemmas :
pi1_wf_top,
event_ordering_wf,
es-E_wf
\mforall{}[p:EO {}\mrightarrow{} \mBbbP{}']. \mforall{}[e:PossibleEvent(p)]. (pe-es(e) \mmember{} EO)
Date html generated:
2011_08_16-AM-10_53_48
Last ObjectModification:
2011_06_18-AM-09_27_06
Home
Index