---

Step * 1 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
⊢ ∀e,e':E(X).  ((loc(e) = loc(e') ∈ Id) ⇒ (loc(f e) = loc(f e') ∈ Id) ⇒ ((f e <loc f e') ⇐⇒ (e <loc e')))
BY
{ ((UnivCD THENA Auto)
   THEN (((InstLemma `es-le-total` [⌈es⌉; ⌈f e⌉; ⌈f e'⌉])⋅ THENM D -1 THENM (FHyp 5 [-1])) THENA Auto)
   ) }

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

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) ⇒ 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')

---

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
\mvdash{}  \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')))


By

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

---

Home Index