Nuprl Lemma : std-component-property
∀[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 ∈ 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) = x ∈ 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),
com-kind: com-kind(c),
pMsg: pMsg(P.M[P]),
Process: Process(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,
last: last(L),
l_member: (x ∈ l),
map: map(f;as),
cons: [a / b],
nil: [],
strong-type-continuous: Continuous+(T.F[T]),
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,
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],
component: component(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,
let: let,
prop: ℙ,
InitialSystem: InitialSystem(P.M[P]),
System: System(P.M[P]),
exists: ∃x:A. B[x],
l_all: (∀x∈L.P[x]),
top: Top,
int_seg: {i..j-},
lelt: i ≤ j < k,
le: A ≤ B,
less_than': less_than'(a;b),
false: False,
not: ¬A,
less_than: a < b,
squash: ↓T,
true: True,
select: L[n],
cons: [a / b],
pi1: fst(t),
pi2: snd(t),
runEO: runEO(n2m;l2m;env;S),
stdEO: stdEO(n2m;l2m;env;S),
Process-stream: Process-stream(P;msgs),
es-le-before: ≤loc(e),
or: P ∨ Q,
guard: {T},
uiff: uiff(P;Q),
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_apply: x[s1;s2;s3],
sq_type: SQType(T),
assert: ↑b,
ifthenelse: if b then t else f fi ,
bfalse: ff,
pExt: pExt(P.M[P]),
ldag: LabeledDAG(T),
sub-system: sub-system(P.M[P];S1;S2)
Latex:
\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:
2016_05_17-AM-11_09_36
Last ObjectModification:
2016_01_18-AM-00_11_19
Theory : process-model
Home
Index