---

e,x,y. eX(x) mcast to each of locs a
                      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 :  Id: Id,  es-loc: loc(e),  l_member: (x  l),  eclass-val: X(e),  es-causle: e c e',  and: P  Q,  equal: s = t,  es-E-interface: E(X),  exists: x:A. B[x],  l_all: (xL.P[x]),  or: P  Q,  all: x:A. B[x]
FDL editor aliases :  es-class-mcast-fail

---

\mforall{}e,x,y.  e\mmember{}X(x)  mcast  to  each  of  locs  a
                                            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_36
Last ObjectModification: 2010_07_15-PM-11_17_21

Home Index