---

Step * of Lemma mk-tagged_wf_pCom_create

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

---

Latex:

---

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


By

---

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

---

Home Index