---

Step * 1 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
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
{ ((D (-2) THEN D -1) THEN 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 = e' ∈ E
12. (f e <loc f e')@i
⊢ (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) = (f e') ∈ E
11. (e <loc e')
12. (e <loc e')@i
⊢ (f e <loc f 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
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

((D  (-2)  THEN  D  -1)  THEN  Auto)\mcdot{}

---

Home Index