---

Step * of Lemma mk-tagged_wf_pCom_new

∀[M:Type ⟶ Type]
  ∀[Q:Type]. ∀[m:Unit]. (mk-tagged("new";m) ∈ Com(P.M[P]) Q) supposing Process(P.M[P]) ⊆r Q supposing Monotone(T.M[T])
BY
{ (RepUR ``pMsg Com`` 0⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[Q:Type].  \mforall{}[m:Unit].  (mk-tagged("new";m)  \mmember{}  Com(P.M[P])  Q)  supposing  Process(P.M[P])  \msubseteq{}r  Q 
    supposing  Monotone(T.M[T])


By

---

Latex:
(RepUR  ``pMsg  Com``  0\mcdot{}  THEN  Auto)

---

Home Index