{ 
[p:EO 
']. [e:PossibleEvent(p)]. (pe-loc(e) 
Id) }
{ Proof }
Definitions occuring in Statement :
pe-loc: pe-loc(p),
possible-event: PossibleEvent(poss),
event_ordering: EO,
Id: Id,
uall: [x:A]. B[x],
prop: ,
member: t T,
function: x:A B[x]
Definitions :
uall: [x:A]. B[x],
prop: ,
member: t T,
pe-loc: pe-loc(p)
Lemmas :
es-loc_wf,
pe-es_wf,
pe-e_wf,
possible-event_wf,
event_ordering_wf
\mforall{}[p:EO {}\mrightarrow{} \mBbbP{}']. \mforall{}[e:PossibleEvent(p)]. (pe-loc(e) \mmember{} Id)
Date html generated:
2011_08_16-AM-10_53_58
Last ObjectModification:
2011_06_18-AM-09_27_17
Home
Index