Nuprl Definition : pv11_p1_on_p2a

pv11_p1_on_p2a(Cmd;ldrs_uid) ==
  λloc,zf,z. let loc,zg = zf 
             in let b,sp = zg 
                in let ballot_num,accepted = z 
                   in let ballot_num' = pv11_p1_max_bnum(ldrs_uid) b ballot_num in
                       let accepted' = if pv11_p1_leq_bnum(ldrs_uid) ballot_num b
                                       then pv11_p1_add_if_new() pv11_p1_same_pvalue(Cmd) <b, sp> accepted
                                       else accepted
                                       fi  in
                       <ballot_num', accepted'>


Definitions occuring in Statement :  pv11_p1_add_if_new: pv11_p1_add_if_new(),  pv11_p1_same_pvalue: pv11_p1_same_pvalue(Cmd),  pv11_p1_max_bnum: pv11_p1_max_bnum(ldrs_uid),  pv11_p1_leq_bnum: pv11_p1_leq_bnum(ldrs_uid),  ifthenelse: if b then t else f fi ,  let: let,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
FDL editor aliases :  pv11_p1_on_p2a
Latex:
pv11\_p1\_on\_p2a(Cmd;ldrs$_{uid}$)  ==
    \mlambda{}loc,zf,z.  let  loc,zg  =  zf 
                          in  let  b,sp  =  zg 
                                in  let  ballot$_{num}$,accepted  =  z 
                                      in  let  ballot$_{num'}$  =  pv11\_p1\_max\_bnum(ldrs$_{\000Cuid}$)  b  ballot$_{num}$  in
                                              let  accepted'  =  if  pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  ballot\mbackslash{}\000Cff24_{num}$  b
                                                                              then  pv11\_p1\_add\_if\_new()  pv11\_p1\_same\_pvalue(Cmd)  <b,  sp>  ac\000Ccepted
                                                                              else  accepted
                                                                              fi    in
                                              <ballot$_{num'}$,  accepted'>


Date html generated: 2015_07_23-PM-04_12_49
Last ObjectModification: 2014_11_26-AM-11_25_36

Home Index