---

Step * of Lemma pDVrequest-rndv2_wf

∀[x:PiDataVal()]. pDVrequest-rndv2(x) ∈ ℕ × Id × ℕ × Name supposing ↑pDVrequest?(x)
BY
{ DatatypeSelectorWf `` pDVloc pDVloc_tag pDVguards pDVmsg pDVfire pDVcontinue pDVselex pDVrequest`` }

---

Latex:

---

Latex:
\mforall{}[x:PiDataVal()].  pDVrequest-rndv2(x)  \mmember{}  \mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name  supposing  \muparrow{}pDVrequest?(x)


By

---

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

---

Home Index