Nuprl Lemma : reliable-env-property2
∀[M:Type ⟶ Type]
∀S:InitialSystem(P.M[P]). ∀n2m:ℕ ⟶ pMsg(P.M[P]). ∀l2m:Id ⟶ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]).
let r = pRun(S;env;n2m;l2m) in
reliable-env(env; r)
⇒ (∀e:runEvents(r). ∀P:Process(P.M[P]).
((P ∈ run-event-state-when(r;e))
⇒ ∀p∈snd((P (snd(run-info(r;e))))).let y,c = p
in (com-kind(c) ∈ ``msg choose new``)
⇒ (∃e':runEvents(r)
((run-event-loc(e') = y ∈ Id)
∧ (e run-lt(r) e')
∧ (∃n:ℕ
∃nm:Id
((snd(run-info(r;e')))
= command-to-msg(c;n2m n;l2m nm)
∈ pMsg(P.M[P])))
∧ ((run-cause(r) e') = (inl e) ∈ (runEvents(r)?))))))
supposing Continuous+(P.M[P])
Proof
Definitions occuring in Statement :
command-to-msg: command-to-msg(c;nmsg;lmsg),
reliable-env: reliable-env(env; r),
InitialSystem: InitialSystem(P.M[P]),
run-lt: run-lt(r),
run-cause: run-cause(r),
run-event-loc: run-event-loc(e),
run-event-state-when: run-event-state-when(r;e),
runEvents: runEvents(r),
run-info: run-info(r;e),
pRun: pRun(S0;env;nat2msg;loc2msg),
pEnvType: pEnvType(T.M[T]),
com-kind: com-kind(c),
pMsg: pMsg(P.M[P]),
Process: Process(P.M[P]),
lg-all: ∀x∈G.P[x],
Id: Id,
l_member: (x ∈ l),
cons: [a / b],
nil: [],
strong-type-continuous: Continuous+(T.F[T]),
nat: ℕ,
let: let,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
infix_ap: x f y,
so_apply: x[s],
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
unit: Unit,
apply: f a,
function: x:A ⟶ B[x],
spread: spread def,
inl: inl x,
union: left + right,
token: "$token",
atom: Atom,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
strong-type-continuous: Continuous+(T.F[T]),
ext-eq: A ≡ B,
and: P ∧ Q,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
let: let,
so_lambda: λ2x.t[x],
so_apply: x[s],
InitialSystem: InitialSystem(P.M[P]),
implies: P ⇒ Q,
run-event-step: run-event-step(e),
prop: ℙ,
runEvents: runEvents(r),
pi1: fst(t),
pi2: snd(t),
nat_plus: ℕ+,
nat: ℕ,
Process-apply: Process-apply(P;m),
run-info: run-info(r;e),
pExt: pExt(P.M[P]),
lg-all: ∀x∈G.P[x],
ldag: LabeledDAG(T),
sq_stable: SqStable(P),
squash: ↓T,
is-run-event: is-run-event(r;t;x),
pRun: pRun(S0;env;nat2msg;loc2msg),
ycomb: Y,
exposed-bfalse: exposed-bfalse,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
ifthenelse: if b then t else f fi ,
isl: isl(x),
outl: outl(x),
bfalse: ff,
band: p ∧b q,
assert: ↑b,
false: False,
exists: ∃x:A. B[x],
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
bnot: ¬bb,
le: A ≤ B,
less_than': less_than'(a;b),
not: ¬A,
ge: i ≥ j ,
int_upper: {i...},
run-event-state-when: run-event-state-when(r;e),
fulpRunType: fulpRunType(T.M[T]),
int_seg: {i..j-},
lelt: i ≤ j < k,
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
top: Top,
System: System(P.M[P]),
spreadn: spread3,
pEnvType: pEnvType(T.M[T]),
pRunType: pRunType(T.M[T]),
do-chosen-command: do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm),
component: component(P.M[P]),
lg-is-source: lg-is-source(g;i),
pInTransit: pInTransit(P.M[P]),
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
cand: A c∧ B,
l_member: (x ∈ l),
true: True,
Id: Id,
deliver-msg: deliver-msg(t;m;x;Cs;L),
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
select: L[n],
nil: [],
less_than: a < b,
deliver-msg-to-comp: deliver-msg-to-comp(t;m;x;S;C),
lg-contains: g1 ⊆ g2,
add-cause: add-cause(ev;ext),
lg-map: lg-map(f;g),
lg-size: lg-size(g),
labeled-graph: LabeledGraph(T),
run-msg-commands: run-msg-commands(r),
run-command: run-command(r;t;n),
run-command-node: run-command-node(r;t;n),
intransit-to-info: intransit-to-info(n2m;l2m;r;env;t;lbl),
run-lt: run-lt(r),
run-pred: run-pred(r),
infix_ap: x f y,
run-event-loc: run-event-loc(e),
run-cause: run-cause(r),
rev_uimplies: rev_uimplies(P;Q)
Latex:
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}S:InitialSystem(P.M[P]). \mforall{}n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P]). \mforall{}l2m:Id {}\mrightarrow{} pMsg(P.M[P]). \mforall{}env:pEnvType(P.M[P]).
let r = pRun(S;env;n2m;l2m) in
reliable-env(env; r)
{}\mRightarrow{} (\mforall{}e:runEvents(r). \mforall{}P:Process(P.M[P]).
((P \mmember{} run-event-state-when(r;e))
{}\mRightarrow{} \mforall{}p\mmember{}snd((P (snd(run-info(r;e))))).let y,c = p
in (com-kind(c) \mmember{} ``msg choose new``)
{}\mRightarrow{} (\mexists{}e':runEvents(r)
((run-event-loc(e') = y)
\mwedge{} (e run-lt(r) e')
\mwedge{} (\mexists{}n:\mBbbN{}
\mexists{}nm:Id
((snd(run-info(r;e')))
= command-to-msg(c;n2m n;l2m nm)))
\mwedge{} ((run-cause(r) e') = (inl e))))))
supposing Continuous+(P.M[P])
Date html generated:
2016_05_17-AM-11_03_08
Last ObjectModification:
2016_01_18-AM-00_25_58
Theory : process-model
Home
Index