Nuprl Definition : pv11_p1_when_preempted

pv11_p1_when_preempted(Cmd;ldrs_uid) ==
  λldr,bnum,z. let ballot_num,active,proposals = z in 
              if (pv11_p1_is_bnum() bnum) ∧b (ballot_num  < bnum)
              then <pv11_p1_upd_bnum() bnum ldr, ff, proposals>
              else <ballot_num, active, proposals>
              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 ,  bfalse: ff,  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  pair: <a, b>
FDL editor aliases :  pv11_p1_when_preempted
Latex:
pv11\_p1\_when\_preempted(Cmd;ldrs$_{uid}$)  ==
    \mlambda{}ldr,bnum,z.  let  ballot$_{num}$,active,proposals  =  z  in 
                            if  (pv11\_p1\_is\_bnum()  bnum)  \mwedge{}\msubb{}  (ballot$_{num}$    <  bnum)
                            then  <pv11\_p1\_upd\_bnum()  bnum  ldr,  ff,  proposals>
                            else  <ballot$_{num}$,  active,  proposals>
                            fi 


Date html generated: 2015_07_23-PM-04_33_00
Last ObjectModification: 2014_11_26-AM-11_29_34

Home Index