---

Step * 1 1 of Lemma event-ordering+_cumulative2

.....aux..... 
1. T : Type
2. x : self:EO ∩ x:Atom ─→ if x =a "info" then es-base-E(self) ─→ T else Top fi 
3. x ∈ EO
4. x ∈ x@0:Atom ─→ if x@0 =a "info" then es-base-E(x) ─→ T else Top fi 
5. (x "info") = (x "info") ∈ if "info" =a "info" then es-base-E(x) ─→ T else Top fi 
⊢ es-base-E(x) ─→ T ∈ Type
BY
{ Auto }

---

Latex:


.....aux..... 
1.  T  :  Type
2.  x  :  self:EO  \mcap{}  x:Atom  {}\mrightarrow{}  if  x  =a  "info"  then  es-base-E(self)  {}\mrightarrow{}  T  else  Top  fi 
3.  x  \mmember{}  EO
4.  x  \mmember{}  x@0:Atom  {}\mrightarrow{}  if  x@0  =a  "info"  then  es-base-E(x)  {}\mrightarrow{}  T  else  Top  fi 
5.  (x  "info")  =  (x  "info")
\mvdash{}  es-base-E(x)  {}\mrightarrow{}  T  \mmember{}  Type


By

Auto

---

Home Index