Nuprl Definition : local-simulation-input-consistency

local-simulation-input-consistency(g;X;hdr;locs;es;i;j) ==
  ∀e1,e2:E.
    ((loc(e1) = i ∈ Id)
    ⇒ (loc(e2) = j ∈ Id)
    ⇒ local-simulation-inputs(es;e1;hdr;locs) || local-simulation-inputs(es;e2;hdr;locs))

Definitions occuring in Statement : local-simulation-inputs: local-simulation-inputs(es;e;hdr;locs), Message: Message(f), global-order-compat: L1 || L2, es-loc: loc(e), es-E: E, Id: Id, all: ∀x:A. B[x], implies: P ⇒ Q, equal: s = t ∈ T
FDL editor aliases : local-simulation-input-consistency

Latex:
local-simulation-input-consistency(g;X;hdr;locs;es;i;j) == \mforall{}e1,e2:E. ((loc(e1) = i) {}\mRightarrow{} (loc(e2) = j) {}\mRightarrow{} local-simulation-inputs(es;e1;hdr;locs) || local-simulation-inputs(es;e2;hdr;locs)) Date html generated: 2016_05_17-AM-09_02_00 Last ObjectModification: 2014_08_15-PM-02_51_22 Theory : messages Home Index