Step
*
of Lemma
pDVfire_wf
pDVfire() ∈ PiDataVal()
BY
{ Unfolds ``PiDataVal pDVfire`` 0 THEN Auto THEN MemTypeCD THEN Auto }
Latex:
Latex:
pDVfire()  \mmember{}  PiDataVal()
By
Latex:
Unfolds  ``PiDataVal  pDVfire``  0  THEN  Auto  THEN  MemTypeCD  THEN  Auto
Home
Index