---

Step * 2 of Lemma eo-forward-E-subtype

.....eq aux..... 
1. eo : EO
2. e : E
⊢ {e@0:es-base-E(eo)| ↑((es-dom(eo) e@0) ∧b (e ≤loc e@0 ∨b(¬bloc(e@0) = loc(e))))}  ∈ Type
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. eo : EO
2. e : E
⊢ es-base-E(eo) ∈ Type

2
.....subterm..... T:t
2:n
1. eo : EO
2. e : E
3. e@0 : es-base-E(eo)
⊢ ↑((es-dom(eo) e@0) ∧b (e ≤loc e@0 ∨b(¬bloc(e@0) = loc(e)))) ∈ Type

---

Latex:


.....eq  aux..... 
1.  eo  :  EO
2.  e  :  E
\mvdash{}  \{e@0:es-base-E(eo)|  \muparrow{}((es-dom(eo)  e@0)  \mwedge{}\msubb{}  (e  \mleq{}loc  e@0  \mvee{}\msubb{}(\mneg{}\msubb{}loc(e@0)  =  loc(e))))\}    \mmember{}  Type


By

MemCD

---

Home Index