{ 
[poss:EO 
']. [e1,e2:PossibleEvent(poss)]. (e1 
e2 
') }
{ Proof }
Definitions occuring in Statement :
poss-le: e1 e2,
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,
poss-le: e1 e2,
cand: A c
B,
pi1: fst(t),
top: Top,
so_lambda: 
x.t[x],
all: x:A. B[x],
subtype: S 
T,
implies: P 
Q,
and: P Q,
so_apply: x[s]
Lemmas :
event_ordering_wf,
pi1_wf_top,
es-le_wf,
es-E_wf,
pi2_wf
\mforall{}[poss:EO {}\mrightarrow{} \mBbbP{}']. \mforall{}[e1,e2:PossibleEvent(poss)]. (e1 \mleq{} e2 \mmember{} \mBbbP{}')
Date html generated:
2011_08_16-AM-10_54_33
Last ObjectModification:
2011_06_18-AM-09_27_58
Home
Index