---

Step * 1 of Lemma es-interface-predecessors-le


1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E@i
5. a : E(X)@i
6. (a ∈ eclass-events(es;X;≤loc(e)))@i
⊢ a ≤loc e 
BY
{ (RWO "member-es-interface-events" (-1)⋅ THEN Auto THEN RWO "member-es-le-before" (-1)⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  e  :  E@i
5.  a  :  E(X)@i
6.  (a  \mmember{}  eclass-events(es;X;\mleq{}loc(e)))@i
\mvdash{}  a  \mleq{}loc  e 


By

---

Latex:
(RWO  "member-es-interface-events"  (-1)\mcdot{}  THEN  Auto  THEN  RWO  "member-es-le-before"  (-1)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index