---

Step * of Lemma deliver-msg_wf

∀[M:Type ─→ Type]
  ∀[t:ℕ]. ∀[x:Id]. ∀[m:pMsg(P.M[P])]. ∀[L:LabeledDAG(pInTransit(P.M[P]))]. ∀[Cs:component(P.M[P]) List].
    (deliver-msg(t;m;x;Cs;L) ∈ System(P.M[P])) 
  supposing Continuous+(P.M[P])
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[t:\mBbbN{}].  \mforall{}[x:Id].  \mforall{}[m:pMsg(P.M[P])].  \mforall{}[L:LabeledDAG(pInTransit(P.M[P]))].
    \mforall{}[Cs:component(P.M[P])  List].
        (deliver-msg(t;m;x;Cs;L)  \mmember{}  System(P.M[P])) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
ProveWfLemma

---

Home Index