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: 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

\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