---

Step * of Lemma record-update-update

∀[z,r,v1,v2:Top].  (r[z := v1][z := v2] ~ r[z := v2])
BY
{ ((UnivCD THENA Auto) THEN RW (BasicSymbolicComputeC [] ) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[z,r,v1,v2:Top].    (r[z  :=  v1][z  :=  v2]  \msim{}  r[z  :=  v2])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RW  (BasicSymbolicComputeC  []  )  0  THEN  Auto)

---

Home Index