---

Step * 1 of Lemma mk-extended-eo_wf


1. Info : Type@i'
2. E : Type@i'
3. info : E ─→ Info@i
4. v : EO@i'
5. es-base-E(v) = E ∈ Type@i'
⊢ v["info" := info] ∈ EO
BY
{ ((GenConcl ⌈info = x ∈ Top⌉⋅ THENA Auto)
   THEN All Thin
   THEN Unfold `event_ordering` 1
   THEN D 1
   THEN MemTypeCD
   THEN Auto
   THEN Try ((D 2 THEN D 0 THEN Reduce 0 THEN Trivial))) }

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

---

Latex:



1.  Info  :  Type@i'
2.  E  :  Type@i'
3.  info  :  E  {}\mrightarrow{}  Info@i
4.  v  :  EO@i'
5.  es-base-E(v)  =  E@i'
\mvdash{}  v["info"  :=  info]  \mmember{}  EO


By

((GenConcl  \mkleeneopen{}info  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Unfold  `event\_ordering`  1
  THEN  D  1
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  ((D  2  THEN  D  0  THEN  Reduce  0  THEN  Trivial)))

---

Home Index