Nuprl Lemma : std-components-property
∀[M:Type ⟶ Type]
∀n2m:ℕ ⟶ pMsg(P.M[P]). ∀l2m:Id ⟶ pMsg(P.M[P]). ∀Cs:component(P.M[P]) List.
assuming(env,r.reliable-env(env; r))
<Cs, lg-nil()> |= es.∃cause:E ⟶ (E?)
(∀C∈Cs.∀e:E
let G = last(data-stream(snd(C);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 ∈ Id)
∧ (e < e')
∧ (∃n:ℕ
∃nm:Id
(info(e') = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
∧ ((cause e') = (inl e) ∈ (E?))))
supposing loc(e) = (fst(C)) ∈ Id)
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),
component: component(P.M[P]),
com-kind: com-kind(c),
pMsg: pMsg(P.M[P]),
data-stream: data-stream(P;L),
lg-all: ∀x∈G.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,
Id: Id,
l_all: (∀x∈L.P[x]),
last: last(L),
l_member: (x ∈ l),
map: map(f;as),
cons: [a / b],
nil: [],
list: T List,
strong-type-continuous: Continuous+(T.F[T]),
nat: ℕ,
let: let,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
pi1: fst(t),
pi2: snd(t),
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,
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],
System: System(P.M[P]),
so_lambda: λ2x.t[x],
so_apply: x[s],
system-strongly-realizes: system-strongly-realizes,
implies: P ⇒ Q,
system-realizes: system-realizes,
InitialSystem: InitialSystem(P.M[P]),
let: let,
run-eo: EO(r),
es-E: E,
mk-extended-eo: mk-extended-eo,
top: Top,
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
bfalse: ff,
mk-eo: mk-eo(E;dom;l;R;locless;pred;rank),
mk-eo-record: mk-eo-record(E;dom;l;R;locless;pred;rank),
btrue: tt,
assert: ↑b,
cand: A c∧ B,
prop: ℙ,
true: True,
es-loc: loc(e),
runEO: runEO(n2m;l2m;env;S),
stdEO: stdEO(n2m;l2m;env;S),
es-le-before: ≤loc(e),
exists: ∃x:A. B[x],
l_all: (∀x∈L.P[x]),
int_seg: {i..j-},
guard: {T},
lelt: i ≤ j < k,
decidable: Dec(P),
or: P ∨ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
false: False,
not: ¬A,
less_than: a < b,
squash: ↓T,
l_member: (x ∈ l),
le: A ≤ B,
less_than': less_than'(a;b),
nat: ℕ,
ge: i ≥ j ,
sub-system: sub-system(P.M[P];S1;S2),
iff: P ⇐⇒ Q,
component: component(P.M[P]),
pi2: snd(t),
iterate-Process: iterate-Process(P;msgs),
Process-stream: Process-stream(P;msgs),
last: last(L),
subtract: n - m,
select: L[n],
cons: [a / b],
es-info: info(e),
es-causl: (e < e'),
dataflow-ap: df(a),
run-event-msg: run-event-msg(r;e),
runEvents: runEvents(r),
run-event-step: run-event-step(e),
pi1: fst(t),
nat_plus: ℕ+,
lg-all: ∀x∈G.P[x],
Process-apply: Process-apply(P;m),
pExt: pExt(P.M[P]),
ldag: LabeledDAG(T),
infix_ap: x f y,
es-before: before(e),
bool: 𝔹,
unit: Unit,
it: ⋅,
uiff: uiff(P;Q),
sq_type: SQType(T),
bnot: ¬bb,
run-prior-state: run-prior-state(S0;r;e),
run-event-local-pred: run-event-local-pred(r;e),
Id: Id,
rev_implies: P ⇐ Q,
run-event-state-when: run-event-state-when(r;e),
pRun: pRun(S0;env;nat2msg;loc2msg),
ycomb: Y,
eq_int: (i =z j),
spreadn: spread3,
std-initial: std-initial(S),
run-event-loc: run-event-loc(e),
exposed-bfalse: exposed-bfalse,
mapfilter: mapfilter(f;P;L),
es-base-E: es-base-E(es),
es-causle: e c≤ e',
run-event-state: run-event-state(r;e),
fulpRunType: fulpRunType(T.M[T]),
record-select: r.x,
record-update: r[x := v],
run-info: run-info(r;e),
so_lambda: λ2x y.t[x; y],
trans: Trans(T;x,y.E[x; y]),
anti_sym: AntiSym(T;x,y.R[x; y]),
set-equal: set-equal(T;x;y),
sorted-by: sorted-by(R;L),
run-event-interval: run-event-interval(r;e1;e2),
map: map(f;as),
list_ind: list_ind,
filter: filter(P;l),
reduce: reduce(f;k;as),
nil: [],
sq_stable: SqStable(P),
es-interval: [e, e'],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_apply: x[s1;s2;s3]
Latex:
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P]). \mforall{}l2m:Id {}\mrightarrow{} pMsg(P.M[P]). \mforall{}Cs:component(P.M[P]) List.
assuming(env,r.reliable-env(env; r))
<Cs, lg-nil()> |= es.\mexists{}cause:E {}\mrightarrow{} (E?)
(\mforall{}C\mmember{}Cs.\mforall{}e:E
let G = last(data-stream(snd(C);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) = (fst(C)))
supposing Continuous+(P.M[P])
Date html generated:
2016_05_17-AM-11_09_24
Last ObjectModification:
2016_01_18-AM-00_25_30
Theory : process-model
Home
Index