---

e,x,y. eX(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)
       ((ilocs.e:E(Y). ((loc(e) = i)  e' c e  R[e'; X(e'); Y(e)]))
        (loc(e')  failset)))

---

Definitions :  all: x:A. B[x],  or: P  Q,  l_all: (xL.P[x]),  exists: x:A. B[x],  es-E-interface: E(X),  equal: s = t,  and: P  Q,  es-causle: e c e',  eclass-val: X(e),  l_member: (x  l),  es-loc: loc(e),  Id: Id
FDL editor aliases :  es-class-causal-mrel-fail

---

\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: 2010_08_27-PM-03_34_24
Last ObjectModification: 2010_04_15-PM-11_22_48

Home Index