Nuprl Lemma : PiDataVal_ind_pDVrequest

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: s ~ 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