{ 
es:EO
[R:E 
E 
]
((e,e':E. Dec(R e' e))
R => 
x,y.(x < y)
(e,e':E. Dec(es-r-immediate-pred(es;R;e';e)))) }
{ Proof }
Definitions occuring in Statement :
es-r-immediate-pred: es-r-immediate-pred(es;R;e';e),
es-causl: (e < e'),
es-E: E,
event_ordering: EO,
decidable: Dec(P),
uall: [x:A]. B[x],
prop: ,
all: x:A. B[x],
implies: P Q,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
rel_implies: R1 => R2
Definitions :
all: x:A. B[x],
uall: [x:A]. B[x],
prop: ,
implies: P Q,
rel_implies: R1 => R2,
es-r-immediate-pred: es-r-immediate-pred(es;R;e';e),
infix_ap: x f y,
rel-immediate: R!,
and: P 
Q,
member: t 
T,
so_lambda: 
x.t[x],
decidable: Dec(P),
not: 
A,
or: P 
Q,
false: False,
exists: 
x:A. B[x],
cand: A c B,
so_apply: x[s]
Lemmas :
decidable__and,
not_wf,
es-E_wf,
es-causl_wf,
decidable_wf,
event_ordering_wf,
decidable__existse-causl
\mforall{}es:EO
\mforall{}[R:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}]
((\mforall{}e,e':E. Dec(R e' e))
{}\mRightarrow{} R => \mlambda{}x,y.(x < y)
{}\mRightarrow{} (\mforall{}e,e':E. Dec(es-r-immediate-pred(es;R;e';e))))
Date html generated:
2011_08_16-AM-11_14_20
Last ObjectModification:
2011_06_20-AM-00_21_31
Home
Index