---

Step * of Lemma eo-restrict_wf_extended

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[P:E ─→ 𝔹].  (eo-restrict(es;P) ∈ 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. P : E ─→ 𝔹
4. es ∈ EO
⊢ eo-restrict(es;P)."info" ∈ es-base-E(eo-restrict(es;P)) ─→ Info

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[P:E  {}\mrightarrow{}  \mBbbB{}].    (eo-restrict(es;P)  \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