---

Step * of Lemma pDVloc_tag?_wf

∀[x:PiDataVal()]. (pDVloc_tag?(x) ∈ 𝔹)
BY
{ Auto THEN RW (AddrC [2] (UnfoldTopAbC)) 0 THEN Auto }

---

Latex:

---

Latex:
\mforall{}[x:PiDataVal()].  (pDVloc\_tag?(x)  \mmember{}  \mBbbB{})


By

---

Latex:
Auto  THEN  RW  (AddrC  [2]  (UnfoldTopAbC))  0  THEN  Auto

---

Home Index