---

Step * of Lemma member-eo-forward-E

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e,e':E].  e' ∈ E supposing (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' 
BY
{ (Auto THEN SubsumeC ⌈{e':E| (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' } ⌉⋅) }

1
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e' : E
5. (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' 
⊢ e' ∈ {e':E| (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' } 

2
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e' : E
5. (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' 
6. e' = e' ∈ {e':E| (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' } 
⊢ {e':E| (loc(e') = loc(e) ∈ Id) ⇒ e ≤loc e' }  ⊆r E

---

Latex:


\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e,e':E].    e'  \mmember{}  E  supposing  (loc(e')  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e' 


By

(Auto  THEN  SubsumeC  \mkleeneopen{}\{e':E|  (loc(e')  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e'  \}  \mkleeneclose{}\mcdot{})

---

Home Index