---

Step * 2 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' : E(X)@i
7. e' ≤loc e @i
8. P[e']@i
⊢ (e' ∈ ≤(X)(e))
BY
{ (RWO "member-interface-predecessors<" (-2)⋅ 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'  :  E(X)@i
7.  e'  \mleq{}loc  e  @i
8.  P[e']@i
\mvdash{}  (e'  \mmember{}  \mleq{}(X)(e))


By

---

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

---

Home Index