---

Step * of Lemma pDVrequest_wf

∀[rndv2:ℕ × Id × ℕ × Name]. ∀[counter:ℕ].  (pDVrequest(rndv2;counter) ∈ PiDataVal())
BY
{ Unfolds ``PiDataVal pDVrequest`` 0 THEN Auto THEN MemTypeCD THEN Auto }

---

Latex:

---

Latex:
\mforall{}[rndv2:\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name].  \mforall{}[counter:\mBbbN{}].    (pDVrequest(rndv2;counter)  \mmember{}  PiDataVal())


By

---

Latex:
Unfolds  ``PiDataVal  pDVrequest``  0  THEN  Auto  THEN  MemTypeCD  THEN  Auto

---

Home Index