---

Step * of Lemma PiDataVal_ind_pDVrequest_lemma

∀request,selex,continue,fire,msg,guards,loc_tag,loc,counter,rndv2:Top.
  (F((pDVrequest(rndv2;counter)) 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] ~ request[rndv2;counter])
BY
{ (UnivCD THENA Auto) }

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
⊢ F((pDVrequest(rndv2;counter)) 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] ~ request[rndv2;counter]

---

Latex:

---

Latex:
\mforall{}request,selex,continue,fire,msg,guards,loc$_{tag}$,loc,counter,rndv2:Top.
    (F((pDVrequest(rndv2;counter))  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{}  request[rndv2;counter])


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index