---

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


By

---

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

---

Home Index