Step
*
of Lemma
pDVmsg-index_wf
∀[x:PiDataVal()]. pDVmsg-index(x) ∈ ℕ supposing ↑pDVmsg?(x)
BY
{ DatatypeSelectorWf `` pDVloc pDVloc_tag pDVguards pDVmsg pDVfire pDVcontinue pDVselex pDVrequest`` }
Latex:
Latex:
\mforall{}[x:PiDataVal()].  pDVmsg-index(x)  \mmember{}  \mBbbN{}  supposing  \muparrow{}pDVmsg?(x)
By
Latex:
DatatypeSelectorWf  ``  pDVloc  pDVloc\_tag  pDVguards  pDVmsg  pDVfire  pDVcontinue  pDVselex  pDVrequest``
Home
Index