---

Step * 1 2 of Lemma event-ordering+_cumulative2


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."info" ∈ es-base-E(x) ─→ T
⊢ x ∈ event_ordering{i':l}
BY
{ Auto }

---

Latex:



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."info"  \mmember{}  es-base-E(x)  {}\mrightarrow{}  T
\mvdash{}  x  \mmember{}  event\_ordering\{i':l\}


By

Auto

---

Home Index