---

Step * 1 1 of Lemma PiDataVal_ind_pDVrequest_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. counter : Top@i
10. rndv2 : Top@i
⊢ request[rndv2;counter] ~ request[rndv2;counter]
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. counter : Top@i
10. rndv2 : Top@i
⊢ request[rndv2;counter] ~ request[rndv2;counter]

---

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.  counter  :  Top@i
10.  rndv2  :  Top@i
\mvdash{}  request[rndv2;counter]  \msim{}  request[rndv2;counter]


By

---

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

---

Home Index