---

Step * of Lemma intransit-to-info_wf

∀[M:Type ─→ Type]. ∀[r:fulpRunType(P.M[P])]. ∀[n2m:ℕ ─→ pMsg(P.M[P])]. ∀[l2m:Id ─→ pMsg(P.M[P])].
∀[env:pEnvType(P.M[P])]. ∀[t:ℕ+]. ∀[lbl:pInTransit(P.M[P])].
  (intransit-to-info(n2m;l2m;r;env;t;lbl) ∈ ℤ × Id × pMsg(P.M[P]))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:fulpRunType(P.M[P])].  \mforall{}[n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])].  \mforall{}[l2m:Id  {}\mrightarrow{}  pMsg(P.M[P])].
\mforall{}[env:pEnvType(P.M[P])].  \mforall{}[t:\mBbbN{}\msupplus{}].  \mforall{}[lbl:pInTransit(P.M[P])].
    (intransit-to-info(n2m;l2m;r;env;t;lbl)  \mmember{}  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P]))


By

---

Latex:
ProveWfLemma

---

Home Index