Nuprl Definition : pv11_p1_leader_preempted

pv11_p1_leader_preempted(Cmd;ldrs_uid) ==
  λldr,bnum,z. let ballot_num,zv,z = z in 
              if (pv11_p1_is_bnum() bnum) ∧b (ballot_num  < bnum) then {pv11_p1_upd_bnum() bnum ldr} else {} fi 


Definitions occuring in Statement :  pv11_p1_lt_bnum: pv11_p1_lt_bnum(ldrs_uid),  pv11_p1_upd_bnum: pv11_p1_upd_bnum(),  pv11_p1_is_bnum: pv11_p1_is_bnum(),  band: p ∧b q,  ifthenelse: if b then t else f fi ,  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  single-bag: {x},  empty-bag: {}
FDL editor aliases :  pv11_p1_leader_preempted
Latex:
pv11\_p1\_leader\_preempted(Cmd;ldrs$_{uid}$)  ==
    \mlambda{}ldr,bnum,z.  let  ballot$_{num}$,zv,z  =  z  in 
                            if  (pv11\_p1\_is\_bnum()  bnum)  \mwedge{}\msubb{}  (ballot$_{num}$    <  bnum)
                            then  \{pv11\_p1\_upd\_bnum()  bnum  ldr\}
                            else  \{\}
                            fi 


Date html generated: 2015_07_23-PM-04_33_40
Last ObjectModification: 2014_11_26-AM-11_30_35

Home Index