---

Step * of Lemma csm-msg_wf

∀[V:Type]. ∀[sm:CSM(V)]. ∀[i,j:V]. ∀[a:Type(sm;i)]. ∀[b:csm-aux(sm;i)]. ∀[c:Cmd(sm) + Msg(sm)].
  csm-msg(sm;i;j;a;b;c) ∈ Msg(sm) supposing ↑csm-sends(sm;i;j;a;b;c)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[V:Type].  \mforall{}[sm:CSM(V)].  \mforall{}[i,j:V].  \mforall{}[a:Type(sm;i)].  \mforall{}[b:csm-aux(sm;i)].  \mforall{}[c:Cmd(sm)  +  Msg(sm)].
    csm-msg(sm;i;j;a;b;c)  \mmember{}  Msg(sm)  supposing  \muparrow{}csm-sends(sm;i;j;a;b;c)


By

---

Latex:
Auto

---

Home Index