Step * 1 2 1 of Lemma event-ordering+_cumulative


1. Type
2. self:EO ∩ x:Atom ─→ if =a "info" then es-base-E(self) ─→ 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
BY
(Unfold `record+` THEN DepIsectCD) }

1
1. Type
2. self:EO ∩ x:Atom ─→ if =a "info" then es-base-E(self) ─→ else Top fi 
3. x ∈ EO
4. x."info" ∈ es-base-E(x) ─→ T
⊢ x ∈ event_ordering{i':l}

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


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\}
            "info":es-base-E(self)  {}\mrightarrow{}  T


By

(Unfold  `record+`  0  THEN  DepIsectCD)




Home Index