---

Step * of Lemma tree-flow-order-preserving

∀[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))
BY
{ (Auto THEN BLemma `convergent-flow-order-preserving` THEN Auto THEN BLemma `tree-flow-convergent` THEN Auto) }

---

Latex:


\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))


By

(Auto
  THEN  BLemma  `convergent-flow-order-preserving`
  THEN  Auto
  THEN  BLemma  `tree-flow-convergent`
  THEN  Auto)

---

Home Index