---

fifo-information-flow(es;T;S;F;In;X;f) ==
  solves-information-flow(es;T;S;F;In;X;f)
   (e1,e2:E(X).
       ((((f e1) = e1))
        (((f e2) = e2))
        (f e1 <loc f e2)
        (loc(e1) = loc(e2))
        (e1 <loc e2)))

---

Definitions :  and: P  Q,  solves-information-flow: solves-information-flow(es;T;S;F;In;X;f),  all: x:A. B[x],  not: A,  es-E-interface: E(X),  apply: f a,  implies: P  Q,  equal: s = t,  Id: Id,  es-loc: loc(e),  es-locl: (e <loc e')
FDL editor aliases :  fifo-information-flow

---

fifo-information-flow(es;T;S;F;In;X;f)  ==
    solves-information-flow(es;T;S;F;In;X;f)
    \mwedge{}  (\mforall{}e1,e2:E(X).
              ((\mneg{}((f  e1)  =  e1))
              {}\mRightarrow{}  (\mneg{}((f  e2)  =  e2))
              {}\mRightarrow{}  (f  e1  <loc  f  e2)
              {}\mRightarrow{}  (loc(e1)  =  loc(e2))
              {}\mRightarrow{}  (e1  <loc  e2)))


Date html generated: 2010_08_27-PM-02_26_02
Last ObjectModification: 2009_12_16-AM-08_22_52

Home Index