---

Step * of Lemma es-happened-before_wf

∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[S:EClass(Interface)]. ∀[e1,e2:E].  (e1 ─→ e2 ∈ ℙ)
BY
{ ((UnivCD THENA Auto) THEN MoveToConcl (-1) THEN CausalInd' THEN RecUnfold `es-happened-before` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[S:EClass(Interface)].  \mforall{}[e1,e2:E].    (e1  {}\mrightarrow{}  e2  \mmember{}  \mBbbP{})


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'
  THEN  RecUnfold  `es-happened-before`  0
  THEN  Auto)

---

Home Index