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