---

Step * 1 of Lemma member-interface-predecessors2

.....assertion..... 
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E@i
5. e' : E(X)@i
6. (e' ∈ filter(λe.e ∈b X;≤loc(e)))@i
⊢ (e' ∈ filter(λe.e ∈b X;≤loc(e)))
BY
{ RepeatFor 3 (ParallelLast) }

1
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

---

Latex:

---

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


By

---

Latex:
RepeatFor  3  (ParallelLast)

---

Home Index