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