---

Step * of Lemma eo-reset-dom_wf_extended

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[d:es-base-E(es) ─→ 𝔹].  (eo-reset-dom(es;d) ∈ EO+(Info))
BY
{ (Auto THEN (Assert es ∈ EO BY Auto) THEN Unfold `event-ordering+` 0⋅ THEN RecordPlusTypeCD⋅ THEN Auto) }

1
1. Info : Type
2. es : EO+(Info)
3. d : es-base-E(es) ─→ 𝔹
4. es ∈ EO
⊢ eo-reset-dom(es;d)."info" ∈ es-base-E(eo-reset-dom(es;d)) ─→ Info

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[d:es-base-E(es)  {}\mrightarrow{}  \mBbbB{}].    (eo-reset-dom(es;d)  \mmember{}  EO+(Info))


By

(Auto
  THEN  (Assert  es  \mmember{}  EO  BY
                          Auto)
  THEN  Unfold  `event-ordering+`  0\mcdot{}
  THEN  RecordPlusTypeCD\mcdot{}
  THEN  Auto)

---

Home Index