---

Step * 2 1 1 1 1 of Lemma eo-forward-trivial


1. v : EO@i'
⊢ v["dom" := v."dom"] ∈ EO
BY
{ (All (Unfold `event_ordering`) THEN D -1 THEN MemTypeCD) }

1
1. v : eo_record{i:l}()@i'
2. eo_axioms(v)@i'
⊢ v["dom" := v."dom"] ∈ eo_record{i:l}()

2
.....set predicate..... 
1. v : eo_record{i:l}()@i'
2. eo_axioms(v)@i'
⊢ eo_axioms(v["dom" := v."dom"])

3
.....wf..... 
1. v : eo_record{i:l}()@i'
2. eo_axioms(v)@i'
3. r : eo_record{i:l}()
⊢ eo_axioms(r) ∈ Type

---

Latex:



1.  v  :  EO@i'
\mvdash{}  v["dom"  :=  v."dom"]  \mmember{}  EO


By

(All  (Unfold  `event\_ordering`)  THEN  D  -1  THEN  MemTypeCD)

---

Home Index