---

Step * 2 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':E(X). (e' ≤loc e  ⇒ P[e'])@i
7. e' : {a:E(X)| loc(a) = loc(e) ∈ Id} @i
8. (e' ∈ ≤(X)(e))@i
⊢ P[e']
BY
{ (BackThruSomeHyp THEN (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.  \mforall{}e':E(X).  (e'  \mleq{}loc  e    {}\mRightarrow{}  P[e'])@i
7.  e'  :  \{a:E(X)|  loc(a)  =  loc(e)\}  @i
8.  (e'  \mmember{}  \mleq{}(X)(e))@i
\mvdash{}  P[e']


By

---

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

---

Home Index