Nuprl Definition : es-class-causal-rel-fail

∀e,x,y. e∈X(x) ⇐c⇒ ∃ Y(y) such that
                    R[e; x; y]
                   unless loc(e) ∈ failset ==
  (∀e:E(Y). ∃e':E(X). (e' c≤ e ∧ R[e'; X(e'); Y(e)]))
  ∧ (∀e':E(X). ((∃e:E(Y). (e' c≤ e ∧ R[e'; X(e'); Y(e)])) ∨ (loc(e') ∈ failset)))

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_member: (x ∈ l), all: ∀x:A. B[x], exists: ∃x:A. B[x], or: P ∨ Q, and: P ∧ Q
FDL editor aliases : es-class-causal-rel-fail

Latex:
\mforall{}e,x,y. e\mmember{}X(x) \mLeftarrow{}c\mRightarrow{} \mexists{} Y(y) such that R[e; x; y] unless loc(e) \mmember{} failset == (\mforall{}e:E(Y). \mexists{}e':E(X). (e' c\mleq{} e \mwedge{} R[e'; X(e'); Y(e)])) \mwedge{} (\mforall{}e':E(X). ((\mexists{}e:E(Y). (e' c\mleq{} e \mwedge{} R[e'; X(e'); Y(e)])) \mvee{} (loc(e') \mmember{} failset))) Date html generated: 2015_07_21-PM-04_25_23 Last ObjectModification: 2012_02_25-PM-03_15_19 Home Index