---

Step * 1 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) = (f e') ∈ E
11. (e <loc e')
12. (e <loc e')@i
⊢ (f e <loc f e')
BY
{ (InstHyp [⌈e'⌉;⌈e⌉] 5⋅ THEN 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)  =  (f  e')
11.  (e  <loc  e')
12.  (e  <loc  e')@i
\mvdash{}  (f  e  <loc  f  e')


By

(InstHyp  [\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  5\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index