---

Step * of Lemma strong-interface-fifo-order-preserving

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top). ∀f:E(X) ─→ E.  (strong-interface-fifo(es;X;f) ⇐⇒ interface-order-preserving(es;X;f))
BY
{ (Auto THEN UnfoldTopAb (-1) THEN UnfoldTopAb (0)) }

1
1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : E(X) ─→ E@i
5. ∀e,e':E(X).  ((loc(e) = loc(e') ∈ Id) ⇒ f e ≤loc f e'  ⇒ e ≤loc e' )@i
⊢ ∀e,e':E(X).  ((loc(e) = loc(e') ∈ Id) ⇒ (loc(f e) = loc(f e') ∈ Id) ⇒ ((f e <loc f e') ⇐⇒ (e <loc e')))

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : E(X) ─→ E@i
5. ∀e,e':E(X).  ((loc(e) = loc(e') ∈ Id) ⇒ (loc(f e) = loc(f e') ∈ Id) ⇒ ((f e <loc f e') ⇐⇒ (e <loc e')))@i
⊢ ∀e,e':E(X).  ((loc(e) = loc(e') ∈ Id) ⇒ f e ≤loc f e'  ⇒ e ≤loc e' )

---

Latex:


\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:E(X)  {}\mrightarrow{}  E.
        (strong-interface-fifo(es;X;f)  \mLeftarrow{}{}\mRightarrow{}  interface-order-preserving(es;X;f))


By

(Auto  THEN  UnfoldTopAb  (-1)  THEN  UnfoldTopAb  (0))

---

Home Index