{ 
es:EO
[R:E 
E 
]
((e,e':E. Dec(R e' e))
R => 
x,y.(x < y)
(e:E
((
e':E. (R e' e)) (e':E. 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],
exists: 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,
exists: x:A. B[x],
es-r-immediate-pred: es-r-immediate-pred(es;R;e';e),
member: t 
T,
so_lambda: 
x y.t[x; y],
rel_implies: R1 => R2,
infix_ap: x f y,
so_apply: x[s1;s2],
decidable: Dec(P),
and: P 
Q,
so_lambda: x.t[x],
or: P 
Q,
not: 
A,
cand: A c B,
guard: {T},
so_apply: x[s],
false: False
Lemmas :
rel-immediate-exists,
es-E_wf,
rel_implies_wf,
es-causl_wf,
decidable_wf,
event_ordering_wf,
strongwf-monotone,
es-causl-swellfnd,
decidable__existse-causl,
decidable__and,
not_wf
\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. ((\mexists{}e':E. (R e' e)) {}\mRightarrow{} (\mexists{}e':E. es-r-immediate-pred(es;R;e';e)))))
Date html generated:
2011_08_16-AM-11_14_34
Last ObjectModification:
2011_06_20-AM-00_21_43
Home
Index