---

Step * 1 1 of Lemma PiDataVal_ind_pDVguards_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. preList : Top@i
10. from : Top@i
⊢ guards[from;preList] ~ guards[from;preList]
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. preList : Top@i
10. from : Top@i
⊢ guards[from;preList] ~ guards[from;preList]

---

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.  preList  :  Top@i
10.  from  :  Top@i
\mvdash{}  guards[from;preList]  \msim{}  guards[from;preList]


By

---

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

---

Home Index