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

e,x,y. e∈X(x) c at each of locs
                   ∃ Y(y) such that
                    R[e; x; y]
                   unless loc(e) ∈ failset ==
  (∀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)])) ∨ (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_all: (∀x∈L.P[x]) l_member: (x ∈ l) all: x:A. B[x] exists: x:A. B[x] or: P ∨ Q and: P ∧ Q equal: t ∈ T
FDL editor aliases :  es-class-causal-mrel-fail

Latex:
\mforall{}e,x,y.  e\mmember{}X(x)  \mLeftarrow{}c\mRightarrow{}  at  each  of  locs
                                      \mexists{}  Y(y)  such  that
                                        R[e;  x;  y]
                                      unless  loc(e)  \mmember{}  failset  ==
    (\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)]))  \mvee{}  (loc(e')  \mmember{}  failset)))



Date html generated: 2015_07_21-PM-04_26_36
Last ObjectModification: 2012_07_16-AM-10_33_39

Home Index