---

Step * 1 1 of Lemma member-interface-predecessors2


1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E@i
5. e' : E(X)@i
6. i : ℕ@i
7. i < ||filter(λe.e ∈b X;≤loc(e))||@i
8. e' = filter(λe.e ∈b X;≤loc(e))[i] ∈ E(X)@i
⊢ e' = filter(λe.e ∈b X;≤loc(e))[i] ∈ E
BY
{ (RevHypSubst (-1) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  e  :  E@i
5.  e'  :  E(X)@i
6.  i  :  \mBbbN{}@i
7.  i  <  ||filter(\mlambda{}e.e  \mmember{}\msubb{}  X;\mleq{}loc(e))||@i
8.  e'  =  filter(\mlambda{}e.e  \mmember{}\msubb{}  X;\mleq{}loc(e))[i]@i
\mvdash{}  e'  =  filter(\mlambda{}e.e  \mmember{}\msubb{}  X;\mleq{}loc(e))[i]


By

---

Latex:
(RevHypSubst  (-1)  0  THEN  Auto)

---

Home Index