---

{ [Info:Type]
    es:EO+(Info). X:EClass(Top). f:E(X)  E(X).
      (interface-order-preserving(es;X;f)
       tree-flow{i:l}(es;X;f)
       global-order-preserving(es;X;f)) }

{ Proof }

---

Definitions occuring in Statement :  tree-flow: tree-flow{i:l}(es;X;f),  global-order-preserving: global-order-preserving(es;X;f),  interface-order-preserving: interface-order-preserving(es;X;f),  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  uall: [x:A]. B[x],  top: Top,  all: x:A. B[x],  implies: P  Q,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  member: t  T,  subtype: S  T,  suptype: suptype(S; T),  so_lambda: x y.t[x; y],  uimplies: b supposing a,  so_apply: x[s1;s2],  prop:
Lemmas :  convergent-flow-order-preserving,  tree-flow-convergent,  tree-flow_wf,  interface-order-preserving_wf,  es-E-interface_wf,  es-E-interface-subtype,  eclass_wf,  top_wf,  es-E_wf,  event-ordering+_wf

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:E(X)  {}\mrightarrow{}  E(X).
        (interface-order-preserving(es;X;f)
        {}\mRightarrow{}  tree-flow\{i:l\}(es;X;f)
        {}\mRightarrow{}  global-order-preserving(es;X;f))


Date html generated: 2011_08_16-PM-04_03_30
Last ObjectModification: 2011_06_20-AM-00_38_23

Home Index