{ 
es:EO. p,w:E 
(E + Top).
(causal-predecessor(es;p)
causal-weak-predecessor(es;w)
causal-predecessor(es;p o w)) }
{ Proof }
Definitions occuring in Statement :
causal-weak-predecessor: causal-weak-predecessor(es;p),
causal-predecessor: causal-predecessor(es;p),
es-E: E,
event_ordering: EO,
top: Top,
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
union: left + right,
p-compose: f o g
Definitions :
equal: s = t,
member: t 
T,
function: x:A B[x],
all: x:A. B[x],
event_ordering: EO,
top: Top,
union: left + right,
es-E: E,
void: Void,
isect: 
x:A. B[x],
subtype: S 
T,
implies: P Q,
do-apply: do-apply(f;x),
es-causl: (e < e'),
universe: Type,
prop: 
,
suptype: suptype(S; T),
can-apply: can-apply(f;x),
assert: 
b,
es-causle: e c
e',
p-compose: f o g,
subtype_rel: A r B,
strong-subtype: strong-subtype(A;B),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
apply: f a,
record-select: r.x,
or: P 
Q,
infix_ap: x f y,
dep-isect: Error :dep-isect,
eq_atom: x =a y,
eq_atom: eq_atom$n(x;y),
record+: record+,
causal-predecessor: causal-predecessor(es;p),
causal-weak-predecessor: causal-weak-predecessor(es;p),
false: False,
inr: inr x ,
isl: isl(x),
inl: inl x ,
true: True,
lambda: 
x.A[x],
outl: outl(x),
es-le: e loc e' ,
es-locl: (e <loc e'),
bool: 
Lemmas :
es-causl_transitivity2,
true_wf,
outl_wf,
isl_wf,
false_wf,
p-compose_wf,
es-causle_wf,
assert_wf,
can-apply_wf,
es-causl_wf,
do-apply_wf,
member_wf,
es-E_wf,
top_wf,
event_ordering_wf
\mforall{}es:EO. \mforall{}p,w:E {}\mrightarrow{} (E + Top).
(causal-predecessor(es;p) {}\mRightarrow{} causal-weak-predecessor(es;w) {}\mRightarrow{} causal-predecessor(es;p o w))
Date html generated:
2011_08_16-AM-11_14_48
Last ObjectModification:
2010_09_24-PM-08_45_55
Home
Index