{ 
es:EO
[Ack,Req:E 
].
f:{e:E| Ack[e]} {e:E| Req[e]}
(e.f e is c< preserving on e.Ack[e]
(e,e':{e:E| Ack[e]} . (e < e') supposing 
e' c
e)
(e,e':{e:E| Req[e]} . (e < e') supposing e' c e)
(e,e':{e:E| Req[e]} .
((e < e') (
a:{e:E| Ack[e]} . ((e < a) 
(a < e')))))
(e:E. (Req[e] (a:E. (Ack[a] e c a e c f a))))) }
{ Proof }
Definitions occuring in Statement :
causal-order-preserving: a.f[a] is c< preserving on e.P[e],
es-causle: e c e',
es-causl: (e < e'),
es-E: E,
event_ordering: EO,
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
so_apply: x[s],
all: x:A. B[x],
exists: x:A. B[x],
not: A,
implies: P Q,
and: P Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x]
Definitions :
all: x:A. B[x],
uall: [x:A]. B[x],
prop: ,
so_apply: x[s],
implies: P Q,
uimplies: b supposing a,
exists: x:A. B[x],
and: P Q,
member: t 
T,
so_lambda: 
x.t[x],
squash: 
T,
true: True,
cand: A c B,
not: A,
decidable: Dec(P),
or: P 
Q,
sq_stable: SqStable(P),
wellfounded: WellFnd{i}(A;x,y.R[x; y]),
guard: {T},
false: False,
causal-order-preserving: a.f[a] is c< preserving on e.P[e]
Lemmas :
es-E_wf,
not_wf,
es-causle_wf,
es-causl_wf,
causal-order-preserving_wf,
event_ordering_wf,
decidable__es-causle,
sq_stable_from_decidable,
es-causl-wellfnd,
es-causl_transitivity2,
es-causl_irreflexivity,
es-causle_weakening
\mforall{}es:EO
\mforall{}[Ack,Req:E {}\mrightarrow{} \mBbbP{}].
\mforall{}f:\{e:E| Ack[e]\} {}\mrightarrow{} \{e:E| Req[e]\}
(e.f e is c< preserving on e.Ack[e]
{}\mRightarrow{} (\mforall{}e,e':\{e:E| Ack[e]\} . (e < e') supposing \mneg{}e' c\mleq{} e)
{}\mRightarrow{} (\mforall{}e,e':\{e:E| Req[e]\} . (e < e') supposing \mneg{}e' c\mleq{} e)
{}\mRightarrow{} (\mforall{}e,e':\{e:E| Req[e]\} . ((e < e') {}\mRightarrow{} (\mexists{}a:\{e:E| Ack[e]\} . ((e < a) \mwedge{} (a < e')))))
{}\mRightarrow{} (\mforall{}e:E. (Req[e] {}\mRightarrow{} (\mforall{}a:E. (Ack[a] {}\mRightarrow{} e c\mleq{} a {}\mRightarrow{} e c\mleq{} f a)))))
Date html generated:
2011_08_16-AM-11_20_17
Last ObjectModification:
2011_06_20-AM-00_25_08
Home
Index