Nuprl Definition : local-simulation-input-validity
local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i) ==
∀e:E
((loc(e) = i ∈ Id)
⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
⇒ (msg-header(snd(msgval(e))) ∈ hdrs)
⇒ (↓∃e':E. ((e' <loc e) ∧ (∃del:ℤ. <del, msgval(e)> ∈ local-simulation-class(X;locs;hdr)(e')))))
Definitions occuring in Statement :
msg-interface: Interface,
has-header-and-in-locs: has-header-and-in-locs(msg;hdr;locs),
local-simulation-class: local-simulation-class(X;locs;hdr),
es-info-body: msgval(e),
msg-header: msg-header(m),
classrel: v ∈ X(e),
es-info: info(e),
es-locl: (e <loc e'),
es-loc: loc(e),
es-E: E,
Id: Id,
name: Name,
l_member: (x ∈ l),
assert: ↑b,
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
pair: <a, b>,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
local-simulation-input-validity
Latex:
local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i) ==
\mforall{}e:E
((loc(e) = i)
{}\mRightarrow{} (\muparrow{}has-header-and-in-locs(info(e);hdr;locs))
{}\mRightarrow{} (msg-header(snd(msgval(e))) \mmember{} hdrs)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E
((e' <loc e) \mwedge{} (\mexists{}del:\mBbbZ{}. <del, msgval(e)> \mmember{} local-simulation-class(X;locs;hdr)(e')))))
Date html generated:
2016_05_17-AM-09_01_51
Last ObjectModification:
2014_08_15-AM-09_55_09
Theory : messages
Home
Index