---

Step * 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) ⇒ (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' )
BY
{ ((UnivCD THENA Auto)
   THEN ((InstLemma `es-locl-total` [⌈es⌉; ⌈e⌉; ⌈e'⌉])⋅ THENM SplitOrHyps)
   THEN Auto
   THEN (FHyp 5 [-1])
   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{}  (loc(f  e)  =  loc(f  e'))  {}\mRightarrow{}  ((f  e  <loc  f  e')  \mLeftarrow{}{}\mRightarrow{}  (e  <loc  e')))@i
\mvdash{}  \mforall{}e,e':E(X).    ((loc(e)  =  loc(e'))  {}\mRightarrow{}  f  e  \mleq{}loc  f  e'    {}\mRightarrow{}  e  \mleq{}loc  e'  )


By

((UnivCD  THENA  Auto)
  THEN  ((InstLemma  `es-locl-total`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{}])\mcdot{}  THENM  SplitOrHyps)
  THEN  Auto
  THEN  (FHyp  5  [-1])
  THEN  Auto)

---

Home Index