Nuprl Definition : es-weak-broadcast
X ⇐⇒ Y@locs ==
∃f:E(X) ─→ i:{i:Id| (i ∈ locs)} ─→ E(Y@i)
(Bij(E(X) × {i:Id| (i ∈ locs)} ;E(Y);λp.let e,i = p
in f e i)
∧ (∀e:E(X). ∀i:{i:Id| (i ∈ locs)} . ((Y(f e i) = X(e) ∈ T) ∧ (e < f e i))))
Definitions occuring in Statement :
es-interface-at: X@i,
es-E-interface: E(X),
eclass-val: X(e),
es-causl: (e < e'),
Id: Id,
l_member: (x ∈ l),
biject: Bij(A;B;f),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
function: x:A ─→ B[x],
spread: spread def,
product: x:A × B[x],
equal: s = t ∈ T
FDL editor aliases :
es-weak-broadcast
Latex:
X \mLeftarrow{}{}\mRightarrow{} Y@locs ==
\mexists{}f:E(X) {}\mrightarrow{} i:\{i:Id| (i \mmember{} locs)\} {}\mrightarrow{} E(Y@i)
(Bij(E(X) \mtimes{} \{i:Id| (i \mmember{} locs)\} ;E(Y);\mlambda{}p.let e,i = p
in f e i)
\mwedge{} (\mforall{}e:E(X). \mforall{}i:\{i:Id| (i \mmember{} locs)\} . ((Y(f e i) = X(e)) \mwedge{} (e < f e i))))
Date html generated:
2015_07_21-PM-03_28_39
Last ObjectModification:
2012_02_25-PM-02_27_53
Home
Index