---

Step * 1 of Lemma eo-forward-E-subtype2

.....subterm..... T:t
1:n
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. x : {e':E| (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' } @i
⊢ x ∈ {e@0:es-base-E(eo)| ↑((es-dom(eo) e@0) ∧b (e ≤loc e@0 ∨b(¬bloc(e@0) = loc(e))))} 
BY
{ D (-1) }

1
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. x : E@i
5. (loc(x) = loc(e) ∈ Id) ⇒ e ≤loc x @i
⊢ x ∈ {e@0:es-base-E(eo)| ↑((es-dom(eo) e@0) ∧b (e ≤loc e@0 ∨b(¬bloc(e@0) = loc(e))))} 

---

Latex:


.....subterm.....  T:t
1:n
1.  Info  :  Type
2.  eo  :  EO+(Info)
3.  e  :  E
4.  x  :  \{e':E|  (loc(e')  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e'  \}  @i
\mvdash{}  x  \mmember{}  \{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))))\} 


By

D  (-1)

---

Home Index