---

Step * 1 2 of Lemma event-ordering+_cumulative


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 ∈ EO+(T)
BY
{ Unfold `event-ordering+` 0 }

1
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}
      "info":es-base-E(self) ─→ T

---

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{}  EO+(T)


By

Unfold  `event-ordering+`  0

---

Home Index