---

Step * 1 of Lemma l_exists-interface-predecessors


1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. [P] : E(X) ─→ ℙ
5. e : E@i
6. e' : {a:E(X)| loc(a) = loc(e) ∈ Id} @i
7. (e' ∈ ≤(X)(e))@i
8. P[e']@i
⊢ e' ≤loc e 
BY
{ (RWO "member-interface-predecessors<" 0⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  [P]  :  E(X)  {}\mrightarrow{}  \mBbbP{}
5.  e  :  E@i
6.  e'  :  \{a:E(X)|  loc(a)  =  loc(e)\}  @i
7.  (e'  \mmember{}  \mleq{}(X)(e))@i
8.  P[e']@i
\mvdash{}  e'  \mleq{}loc  e 


By

---

Latex:
(RWO  "member-interface-predecessors<"  0\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index