---

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
         THEN RepeatFor 3 (((SubtypeReasoning1 THENA Auto)
                            THEN Try ((BLemma `tag-by-subtype-tag-case`⋅ THEN Reduce 0 THEN Auto))
                            ))
         )⋅) }

---

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
              THEN  RepeatFor  3  (((SubtypeReasoning1  THENA  Auto)
                                                    THEN  Try  ((BLemma  `tag-by-subtype-tag-case`\mcdot{}  THEN  Reduce  0  THEN  Auto))
                                                    ))
              )\mcdot{})

---

Home Index