---

Step * of Lemma event-caused-by_wf

∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[S:EClass(Interface)]. ∀[e1,e2:E].  (e2 caused by e1 in S ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index