---

Step * 1 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 = e' ∈ E
12. (f e <loc f e')@i
⊢ (e <loc e')
BY
{ ContradictionViaCongruence `reference_environment`
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  <loc  f  e')
11.  e  =  e'
12.  (f  e  <loc  f  e')@i
\mvdash{}  (e  <loc  e')


By

ContradictionViaCongruence  `reference\_environment`
THEN  Auto

---

Home Index