{ 
es:EO. p:E 
(E + Top).
((causal-predecessor(es;p) 
p-inject(E;E;p))
(e,e':E.
(e p< e' 
(e = e')) e' p< e supposing same-thread(es;p;e;e'))) }
{ Proof }
Definitions occuring in Statement :
same-thread: same-thread(es;p;e;e'),
es-p-locl: e p< e',
causal-predecessor: causal-predecessor(es;p),
es-E: E,
event_ordering: EO,
uimplies: b supposing a,
top: Top,
all: x:A. B[x],
implies: P Q,
or: P Q,
and: P Q,
function: x:A B[x],
union: left + right,
equal: s = t,
p-inject: p-inject(A;B;f)
Definitions :
all: x:A. B[x],
implies: P Q,
and: P Q,
uimplies: b supposing a,
same-thread: same-thread(es;p;e;e'),
member: t 
T,
prop: 
,
es-p-le: e p
e',
or: P Q,
guard: {T},
es-p-locl: e p< e',
exists: 
x:A. B[x],
nat_plus: 
,
uall: [x:A]. B[x],
nat: ,
decidable: Dec(P),
sq_type: SQType(T),
p-graph: p-graph(A;f),
p-fun-exp: f^n,
assert: 
b,
can-apply: can-apply(f;x),
primrec: primrec(n;b;c),
p-id: p-id(),
do-apply: do-apply(f;x),
ycomb: Y,
ifthenelse: if b then t else f fi ,
eq_int: (i =
j),
btrue: tt,
isl: isl(x),
outl: outl(x),
cand: A c B,
not: 
A,
le: A B,
false: False,
es-causle: e c e',
subtype: S 
T
Lemmas :
same-thread_wf,
es-E_wf,
causal-predecessor_wf,
p-inject_wf,
top_wf,
event_ordering_wf,
same-final-iterate-one-one,
causal-pred-wellfounded,
decidable__equal_int,
subtype_base_sq,
int_subtype_base,
es-p-locl_wf,
p-graph_wf2,
p-fun-exp_wf,
nat_plus_inc,
es-causle_weakening_p-le,
decidable__es-E-equal
\mforall{}es:EO. \mforall{}p:E {}\mrightarrow{} (E + Top).
((causal-predecessor(es;p) \mwedge{} p-inject(E;E;p))
{}\mRightarrow{} (\mforall{}e,e':E. (e p< e' \mvee{} (e = e')) \mvee{} e' p< e supposing same-thread(es;p;e;e')))
Date html generated:
2011_08_16-AM-11_17_20
Last ObjectModification:
2011_06_20-AM-00_22_46
Home
Index