---

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


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
6. e : E(X)@i
7. e' : E(X)@i
8. loc(e) = loc(e') ∈ Id@i
9. loc(f e) = loc(f e') ∈ Id@i
10. f e' ≤loc f e 
11. e' ≤loc e 
⊢ (f e <loc f e') ⇐⇒ (e <loc e')
BY
{ Auto }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  f  :  E(X)  {}\mrightarrow{}  E@i
5.  \mforall{}e,e':E(X).    ((loc(e)  =  loc(e'))  {}\mRightarrow{}  f  e  \mleq{}loc  f  e'    {}\mRightarrow{}  e  \mleq{}loc  e'  )@i
6.  e  :  E(X)@i
7.  e'  :  E(X)@i
8.  loc(e)  =  loc(e')@i
9.  loc(f  e)  =  loc(f  e')@i
10.  f  e'  \mleq{}loc  f  e 
11.  e'  \mleq{}loc  e 
\mvdash{}  (f  e  <loc  f  e')  \mLeftarrow{}{}\mRightarrow{}  (e  <loc  e')


By

Auto

---

Home Index