Nuprl Lemma : PiDataVal_ind_pDVfire_lemma
∀request,selex,continue,fire,msg,guards,loc_tag,loc:Top.
  (F((pDVfire()) 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] ~ fire)
Proof
Definitions occuring in Statement : 
PiDataVal_ind: PiDataVal_ind, 
pDVfire: pDVfire()
, 
top: Top
, 
so_apply: x[s1;s2]
, 
so_apply: x[s]
, 
all: ∀x:A. B[x]
, 
sqequal: s ~ t
Lemmas : 
top_wf
Latex:
\mforall{}request,selex,continue,fire,msg,guards,loc$_{tag}$,loc:Top.
    (F((pDVfire())  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{}  fire)
Date html generated:
2015_07_23-AM-11_35_06
Last ObjectModification:
2015_01_29-AM-07_41_30
Home
Index