Nuprl Definition : pv11_p1_on_p2b

pv11_p1_on_p2b() ==
  λbnum,slt,loc,z,waitfor. let acloc,b,s,b' = z 
                           in if (pv11_p1_eq_bnums() bnum b) ∧b (slt =z s) ∧b (pv11_p1_eq_bnums() bnum b')
                              then waitfor - acloc
                              else waitfor
                              fi   


Definitions occuring in Statement :  pv11_p1_eq_bnums: pv11_p1_eq_bnums(),  id-deq: IdDeq,  band: p ∧b q,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  spreadn: spread4,  apply: f a,  lambda: λx.A[x],  bag-remove: bs - x
FDL editor aliases :  pv11_p1_on_p2b
Latex:
pv11\_p1\_on\_p2b()  ==
    \mlambda{}bnum,slt,loc,z,waitfor.  let  acloc,b,s,b'  =  z 
                                                      in  if  (pv11\_p1\_eq\_bnums()  bnum  b)
                                                                  \mwedge{}\msubb{}  (slt  =\msubz{}  s)
                                                                  \mwedge{}\msubb{}  (pv11\_p1\_eq\_bnums()  bnum  b')
                                                            then  waitfor  -  acloc
                                                            else  waitfor
                                                            fi     


Date html generated: 2016_05_17-PM-02_53_05
Last ObjectModification: 2014_11_26-AM-11_26_43

Theory : paxos!synod


Home Index