---

interface-order-preserving(es;X;f) ==
  e,e':E(X).
    ((loc(e) = loc(e'))
     (loc(f e) = loc(f e'))
     ((f e <loc f e')  (e <loc e')))

---

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

---

interface-order-preserving(es;X;f)  ==
    \mforall{}e,e':E(X).    ((loc(e)  =  loc(e'))  {}\mRightarrow{}  (loc(f  e)  =  loc(f  e'))  {}\mRightarrow{}  ((f  e  <loc  f  e')  \mLeftarrow{}{}\mRightarrow{}  (e  <loc  e')))


Date html generated: 2010_08_27-PM-02_08_43
Last ObjectModification: 2009_12_16-AM-01_32_05

Home Index