---

X   Y@locs ==
  f:E(X)  i:{i:Id| (i  locs)}   E(Y@i)
   (Bij(E(X)  {i:Id| (i  locs)} ;E(Y);p.let e,i = p in
                                            f e i)
    (e:E(X). i:{i:Id| (i  locs)} .  ((Y(f e i) = X(e))  (e < f e i))))

---

Definitions :  exists: x:A. B[x],  function: x:A  B[x],  es-interface-at: X@i,  biject: Bij(A;B;f),  product: x:A  B[x],  lambda: x.A[x],  spread: spread def,  es-E-interface: E(X),  all: x:A. B[x],  set: {x:A| B[x]} ,  l_member: (x  l),  Id: Id,  and: P  Q,  equal: s = t,  eclass-val: X(e),  es-causl: (e < e'),  apply: f a
FDL editor aliases :  es-weak-broadcast

---

X  \mLeftarrow{}{}\mRightarrow{}    Y@locs  ==
    \mexists{}f:E(X)  {}\mrightarrow{}  i:\{i:Id|  (i  \mmember{}  locs)\}    {}\mrightarrow{}  E(Y@i)
      (Bij(E(X)  \mtimes{}  \{i:Id|  (i  \mmember{}  locs)\}  ;E(Y);\mlambda{}p.let  e,i  =  p  in
                                                                                        f  e  i)
      \mwedge{}  (\mforall{}e:E(X).  \mforall{}i:\{i:Id|  (i  \mmember{}  locs)\}  .    ((Y(f  e  i)  =  X(e))  \mwedge{}  (e  <  f  e  i))))


Date html generated: 2010_08_27-PM-02_42_12
Last ObjectModification: 2010_03_24-PM-03_20_07

Home Index