---

e,x,y. eX(x) c  reply Y(y)@loc1[x] such that
                    R[e; x; y]loc2[y]=loc(e)
                   unless loc(e)  failset ==
  (e:E(Y)
     e':E(X)
      (e' c e
       ((loc(e) = loc1[X(e')])  (loc(e') = loc2[Y(e)]))
       R[e'; X(e'); Y(e)]))
   (e':E(X)
       ((e:E(Y)
          (e' c e
           ((loc(e) = loc1[X(e')])  (loc(e') = loc2[Y(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),  equal: s = t,  and: P  Q,  es-causle: e c e',  es-E-interface: E(X),  exists: x:A. B[x],  or: P  Q,  all: x:A. B[x]
FDL editor aliases :  es-class-reply-or-fail

---

\mforall{}e,x,y.  e\mmember{}X(x)  \mLeftarrow{}c\mRightarrow{}  \mexists{}  reply  Y(y)@loc1[x]  such  that
                                        R[e;  x;  y]\mwedge{}loc2[y]=loc(e)
                                      unless  loc(e)  \mmember{}  failset  ==
    (\mforall{}e:E(Y)
          \mexists{}e':E(X).  (e'  c\mleq{}  e  \mwedge{}  ((loc(e)  =  loc1[X(e')])  \mwedge{}  (loc(e')  =  loc2[Y(e)]))  \mwedge{}  R[e';  X(e');  Y(e)]))
    \mwedge{}  (\mforall{}e':E(X)
              ((\mexists{}e:E(Y)
                    (e'  c\mleq{}  e  \mwedge{}  ((loc(e)  =  loc1[X(e')])  \mwedge{}  (loc(e')  =  loc2[Y(e)]))  \mwedge{}  R[e';  X(e');  Y(e)]))
              \mvee{}  (loc(e')  \mmember{}  failset)))


Date html generated: 2010_08_27-PM-03_34_29
Last ObjectModification: 2010_07_15-PM-10_05_51

Home Index