---

Step * 1 1 of Lemma PiDataVal_ind_pDVmsg_lemma


1. request : Top@i
2. selex : Top@i
3. continue : Top@i
4. fire : Top@i
5. msg : Top@i
6. guards : Top@i
7. loc_tag : Top@i
8. loc : Top@i
9. index : Top@i
10. val : Top@i
⊢ msg[val;index] ~ msg[val;index]
BY
{ Try (RW (AddrC [2] (IdC)) 0)⋅ }

1
1. request : Top@i
2. selex : Top@i
3. continue : Top@i
4. fire : Top@i
5. msg : Top@i
6. guards : Top@i
7. loc_tag : Top@i
8. loc : Top@i
9. index : Top@i
10. val : Top@i
⊢ msg[val;index] ~ msg[val;index]

---

Latex:

---

Latex:

1.  request  :  Top@i
2.  selex  :  Top@i
3.  continue  :  Top@i
4.  fire  :  Top@i
5.  msg  :  Top@i
6.  guards  :  Top@i
7.  loc$_{tag}$  :  Top@i
8.  loc  :  Top@i
9.  index  :  Top@i
10.  val  :  Top@i
\mvdash{}  msg[val;index]  \msim{}  msg[val;index]


By

---

Latex:
Try  (RW  (AddrC  [2]  (IdC))  0)\mcdot{}

---

Home Index