Step * of Lemma pDVloc_tag-id_wf

[x:PiDataVal()]. pDVloc_tag-id(x) ∈ Id supposing ↑pDVloc_tag?(x)
BY
DatatypeSelectorWf `` pDVloc pDVloc_tag pDVguards pDVmsg pDVfire pDVcontinue pDVselex pDVrequest`` }


Latex:



Latex:
\mforall{}[x:PiDataVal()].  pDVloc\_tag-id(x)  \mmember{}  Id  supposing  \muparrow{}pDVloc\_tag?(x)


By


Latex:
DatatypeSelectorWf  ``  pDVloc  pDVloc\_tag  pDVguards  pDVmsg  pDVfire  pDVcontinue  pDVselex  pDVrequest``




Home Index