Nuprl Definition : pv11_p1_on_p1b

pv11_p1_on_p1b(Cmd) ==
  λbnum,loc,zn,z. let acloc,b,b',pvals = zn 
                  in let waitfor,pvalues = z 
                     in if (pv11_p1_eq_bnums() bnum b) ∧b (pv11_p1_eq_bnums() bnum b')
                        then let waitfor' = waitfor - acloc in
                              let pvalues' = pv11_p1_append_news(Cmd) pv11_p1_same_pvalue(Cmd) pvalues pvals in
                              <waitfor', pvalues'>
                        else <waitfor, pvalues>
                        fi   


Definitions occuring in Statement :  pv11_p1_append_news: pv11_p1_append_news(Cmd),  pv11_p1_same_pvalue: pv11_p1_same_pvalue(Cmd),  pv11_p1_eq_bnums: pv11_p1_eq_bnums(),  id-deq: IdDeq,  band: p ∧b q,  ifthenelse: if b then t else f fi ,  let: let,  spreadn: spread4,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  bag-remove: bs - x
FDL editor aliases :  pv11_p1_on_p1b
Latex:
pv11\_p1\_on\_p1b(Cmd)  ==
    \mlambda{}bnum,loc,zn,z.  let  acloc,b,b',pvals  =  zn 
                                    in  let  waitfor,pvalues  =  z 
                                          in  if  (pv11\_p1\_eq\_bnums()  bnum  b)  \mwedge{}\msubb{}  (pv11\_p1\_eq\_bnums()  bnum  b')
                                                then  let  waitfor'  =  waitfor  -  acloc  in
                                                            let  pvalues'  =  pv11\_p1\_append\_news(Cmd)  pv11\_p1\_same\_pvalue(Cmd) 
                                                                                          pvalues 
                                                                                          pvals  in
                                                            <waitfor',  pvalues'>
                                                else  <waitfor,  pvalues>
                                                fi     


Date html generated: 2015_07_23-PM-04_32_18
Last ObjectModification: 2014_11_26-AM-11_27_44

Home Index