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