---

Step * of Lemma processComm_wf2

∀[l_comm,l_choose:Id].  (processComm(l_comm;l_choose) ∈ pi-process())
BY
{ (((Using [`S',⌜Comm-state()⌝] ProveWfLemma⋅ THEN (Assert ⌜"msg"×PiDataVal() ⊆r (Com(T.piM(T)) cSt)⌝⋅ THEN Auto)⋅)
    THEN All Thin
    )
   THEN RepUR ``Comm-output Com piM`` 0
   ) }

1
1. cSt : Type
⊢ "msg"×PiDataVal() ⊆r "msg":PiDataVal() |+ "create":cSt |+ "choose":Id |+ "new":Unit

---

Latex:

---

Latex:
\mforall{}[l$_{comm}$,l$_{choose}$:Id].    (processComm(l$_\mbackslash{}ff7\000Cbcomm}$;l$_{choose}$)  \mmember{}  pi-process())


By

---

Latex:
(((Using  [`S',\mkleeneopen{}Comm-state()\mkleeneclose{}]  ProveWfLemma\mcdot{}
      THEN  (Assert  \mkleeneopen{}"msg"\mtimes{}PiDataVal()  \msubseteq{}r  (Com(T.piM(T))  cSt)\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}
      )
    THEN  All  Thin
    )
  THEN  RepUR  ``Comm-output  Com  piM``  0
  )

---

Home Index