---

Step * 1 1 of Lemma PiDataVal_ind_pDVselex_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. rndv1 : Top@i
⊢ selex[rndv1] ~ selex[rndv1]
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. rndv1 : Top@i
⊢ selex[rndv1] ~ selex[rndv1]

---

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.  rndv1  :  Top@i
\mvdash{}  selex[rndv1]  \msim{}  selex[rndv1]


By

---

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

---

Home Index