---

Step * 1 of Lemma PiDataVal_ind_pDVloc_tag_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. name : Top@i
10. id : Top@i
⊢ F((pDVloc_tag(id;name)) where  
  F(id) = loc[id]  
  F(id,name) = loc_tag[id;name]  
  F(from,preList) = guards[from;preList]  
  F(val,index) = msg[val;index]  
  F(fire) = fire  
  F(continue) = continue  
  F(rndv1) = selex[rndv1]  
  F(rndv2,counter) = request[rndv2;counter] ~ loc_tag[id;name]
BY
{ Try (RW (AddrC [1] (UnfoldC `pDVloc_tag` ANDTHENC UnfoldC `PiDataVal_ind` ANDTHENC ReduceC)) 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. name : Top@i
10. id : Top@i
⊢ loc_tag[id;name] ~ loc_tag[id;name]

---

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.  name  :  Top@i
10.  id  :  Top@i
\mvdash{}  F((pDVloc\_tag(id;name))  where   
    F(id)  =  loc[id]   
    F(id,name)  =  loc$_{tag}$[id;name]   
    F(from,preList)  =  guards[from;preList]   
    F(val,index)  =  msg[val;index]   
    F(fire)  =  fire   
    F(continue)  =  continue   
    F(rndv1)  =  selex[rndv1]   
    F(rndv2,counter)  =  request[rndv2;counter]  \msim{}  loc$_{tag}$[id;name]


By

---

Latex:
Try  (RW  (AddrC  [1]  (UnfoldC  `pDVloc\_tag`  ANDTHENC  UnfoldC  `PiDataVal\_ind`  ANDTHENC  ReduceC))  0)\mcdot{}

---

Home Index