---

Step * of Lemma pDVloc_wf

∀[id:Id]. (pDVloc(id) ∈ PiDataVal())
BY
{ Unfolds ``PiDataVal pDVloc`` 0 THEN Auto THEN MemTypeCD THEN Auto }

---

Latex:

---

Latex:
\mforall{}[id:Id].  (pDVloc(id)  \mmember{}  PiDataVal())


By

---

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

---

Home Index