{ 
[M:Type 
Type]
n2m:
pMsg(P.M[P]). l2m:Id pMsg(P.M[P]). x:Id. Q:Process(P.M[P]).
assuming(env,r.reliable-env(env; r))
<[<x, Q>], lg-nil()> |=
es.
cause:E (E?)
e:E
let G = last(data-stream(Q;map(
e.info(e);
loc(e)))) in
p
G.let y,c = p
in (com-kind(c) ``msg choose new``)
(e':E
((loc(e') = y)
(e < e')
(n:
nm:Id
(info(e') = command-to-msg(c;n2m n;l2m nm)))
((cause e') = (inl e ))))
supposing loc(e) = x
supposing Continuous+(P.M[P]) }
{ Proof }
Definitions occuring in Statement :
system-strongly-realizes: system-strongly-realizes,
command-to-msg: command-to-msg(c;nmsg;lmsg),
reliable-env: reliable-env(env; r),
com-kind: com-kind(c),
pMsg: pMsg(P.M[P]),
Process: Process(P.M[P]),
lg-all: xG.P[x],
lg-nil: lg-nil(),
es-info: info(e),
es-le-before: loc(e),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
data-stream: data-stream(P;L),
Id: Id,
strong-type-continuous: Continuous+(T.F[T]),
map: map(f;as),
nat: ,
let: let,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
unit: Unit,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
spread: spread def,
pair: <a, b>,
inl: inl x ,
union: left + right,
cons: [car / cdr],
nil: [],
token: "$token",
atom: Atom,
universe: Type,
equal: s = t,
last: last(L),
l_member: (x l)
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
strong-type-continuous: Continuous+(T.F[T]),
so_apply: x[s],
all: x:A. B[x],
system-strongly-realizes: system-strongly-realizes,
let: let,
implies: P Q,
and: P Q,
component: component(P.M[P]),
member: t T,
ext-eq: A 
B,
system-realizes: system-realizes,
so_lambda: 
x.t[x],
exists: x:A. B[x],
or: P 
Q,
Process-stream: Process-stream(P;msgs),
subtype: S 
T,
top: Top,
prop: 
,
cand: A c B,
false: False,
not: 
A,
assert: 
b,
null: null(as),
bfalse: ff,
ifthenelse: if b then t else f fi ,
System: System(P.M[P]),
InitialSystem: InitialSystem(P.M[P]),
l_all: (xL.P[x]),
iff: P 
Q,
rev_implies: P Q,
pi1: fst(t),
pi2: snd(t),
map: map(f;as),
es-le-before: loc(e),
ycomb: Y,
pExt: pExt(P.M[P]),
ldag: LabeledDAG(T),
runEO: runEO(n2m;l2m;env;S),
stdEO: stdEO(n2m;l2m;env;S)
Lemmas :
std-components-property,
nat_wf,
reliable-env_wf,
pRun_wf2,
pEnvType_wf,
sub-system_wf,
InitialSystem_wf,
Process_wf,
Id_wf,
pMsg_wf,
strong-type-continuous_wf,
cons_member,
component_wf,
l_member_wf,
es-E_wf,
stdEO_wf,
event-ordering+_inc,
event-ordering+_wf,
es-loc_wf,
last_wf,
pExt_wf,
Process-stream_wf,
map_wf,
es-le-before_wf,
es-info_wf,
map_append_sq,
es-before_wf2,
top_wf,
iff_weakening_uiff,
es-before_wf,
append_is_nil,
data-stream-cons,
false_wf,
lg-all_wf,
pCom_wf,
com-kind_wf,
es-causl_wf,
command-to-msg_wf,
unit_wf,
lg-nil_wf_dag,
pInTransit_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P]). \mforall{}l2m:Id {}\mrightarrow{} pMsg(P.M[P]). \mforall{}x:Id. \mforall{}Q:Process(P.M[P]).
assuming(env,r.reliable-env(env; r))
<[<x, Q>], lg-nil()> |= es.\mexists{}cause:E {}\mrightarrow{} (E?)
\mforall{}e:E
let G = last(data-stream(Q;map(\mlambda{}e.info(e);\mleq{}loc(e)))) in
\mforall{}p\mmember{}G.let y,c = p
in (com-kind(c) \mmember{} ``msg choose new``)
{}\mRightarrow{} (\mexists{}e':E
((loc(e') = y)
\mwedge{} (e < e')
\mwedge{} (\mexists{}n:\mBbbN{}
\mexists{}nm:Id
(info(e')
= command-to-msg(c;n2m n;l2m nm)))
\mwedge{} ((cause e') = (inl e ))))
supposing loc(e) = x
supposing Continuous+(P.M[P])
Date html generated:
2011_08_17-PM-03_57_10
Last ObjectModification:
2011_06_18-AM-11_28_40
Home
Index