Nuprl 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])


Proof




Definitions occuring in Statement :  PiDataVal_ind: PiDataVal_ind pDVrequest: pDVrequest(rndv2;counter) top: Top so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] sqequal: t
Lemmas :  top_wf

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])



Date html generated: 2015_07_23-AM-11_35_12
Last ObjectModification: 2015_01_29-AM-07_41_39

Home Index