---

Step * of Lemma pDVloc_tag_wf

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

---

Latex:

---

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


By

---

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

---

Home Index