---

Step * of Lemma pDVguards_wf

∀[from:Id]. ∀[preList:pi_prefix() List].  (pDVguards(from;preList) ∈ PiDataVal())
BY
{ Unfolds ``PiDataVal pDVguards`` 0 THEN Auto THEN MemTypeCD THEN Auto }

---

Latex:

---

Latex:
\mforall{}[from:Id].  \mforall{}[preList:pi\_prefix()  List].    (pDVguards(from;preList)  \mmember{}  PiDataVal())


By

---

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

---

Home Index