Nuprl Definition : es-class-causal-mrel

e∈X(x) ⇐c⇒ Y(y)
            @locs such that
            R[e; x; y] ==
  (∀e:E(Y). ((loc(e) ∈ locs) ∧ (∃e':E(X). (e' c≤ e ∧ R[e'; X(e'); Y(e)]))))
  ∧ (∀e':E(X). (∀i∈locs.∃e:E(Y). ((loc(e) = i ∈ Id) ∧ e' c≤ e ∧ R[e'; X(e'); Y(e)])))

Definitions occuring in Statement : es-E-interface: E(X), eclass-val: X(e), es-causle: e c≤ e', es-loc: loc(e), Id: Id, l_all: (∀x∈L.P[x]), l_member: (x ∈ l), all: ∀x:A. B[x], exists: ∃x:A. B[x], and: P ∧ Q, equal: s = t ∈ T
FDL editor aliases : es-class-causal-mrel

Latex:
e\mmember{}X(x) \mLeftarrow{}c\mRightarrow{} Y(y) @locs such that R[e; x; y] == (\mforall{}e:E(Y). ((loc(e) \mmember{} locs) \mwedge{} (\mexists{}e':E(X). (e' c\mleq{} e \mwedge{} R[e'; X(e'); Y(e)])))) \mwedge{} (\mforall{}e':E(X). (\mforall{}i\mmember{}locs.\mexists{}e:E(Y). ((loc(e) = i) \mwedge{} e' c\mleq{} e \mwedge{} R[e'; X(e'); Y(e)]))) Date html generated: 2015_07_21-PM-04_26_10 Last ObjectModification: 2012_07_16-AM-10_34_31 Home Index