---

Step * of Lemma csm-sends_wf

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

---

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-sends(sm;i;j;a;b;c)  \mmember{}  \mBbbB{})


By

---

Latex:
ProveWfLemma

---

Home Index