---

global-order-preserving(es;X;f) ==
  a,a':E(X).
    (a is f*(a')
     (b,b':E(X).
          (b is f*(b')
           (loc(a) = loc(b))
           (loc(a') = loc(b'))
           ((a <loc b)  (a' <loc b')))))

---

Definitions :  all: x:A. B[x],  fun-connected: y is f*(x),  es-E-interface: E(X),  implies: P  Q,  equal: s = t,  Id: Id,  es-loc: loc(e),  iff: P  Q,  es-locl: (e <loc e')
FDL editor aliases :  global-order-preserving

---

global-order-preserving(es;X;f)  ==
    \mforall{}a,a':E(X).
        (a  is  f*(a')
        {}\mRightarrow{}  (\mforall{}b,b':E(X).
                    (b  is  f*(b')
                    {}\mRightarrow{}  (loc(a)  =  loc(b))
                    {}\mRightarrow{}  (loc(a')  =  loc(b'))
                    {}\mRightarrow{}  ((a  <loc  b)  \mLeftarrow{}{}\mRightarrow{}  (a'  <loc  b')))))


Date html generated: 2010_08_27-PM-02_08_55
Last ObjectModification: 2009_12_16-AM-01_32_23

Home Index