Nuprl Definition : pv11_p1_on_propose

pv11_p1_on_propose(Cmd) ==
  λloc,zq,z. let s,p = zq 
             in let ballot_num,active,proposals = z in 
                let proposals' = if pv11_p1_in_domain(Cmd) s proposals
                                 then proposals
                                 else pv11_p1_add_if_new() pv11_p1_same_proposal(Cmd) <s, p> proposals
                                 fi  in
                    <ballot_num, active, proposals'>


Definitions occuring in Statement :  pv11_p1_add_if_new: pv11_p1_add_if_new(),  pv11_p1_same_proposal: pv11_p1_same_proposal(Cmd),  pv11_p1_in_domain: pv11_p1_in_domain(Cmd),  ifthenelse: if b then t else f fi ,  let: let,  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
FDL editor aliases :  pv11_p1_on_propose
Latex:
pv11\_p1\_on\_propose(Cmd)  ==
    \mlambda{}loc,zq,z.  let  s,p  =  zq 
                          in  let  ballot$_{num}$,active,proposals  =  z  in 
                                let  proposals'  =  if  pv11\_p1\_in\_domain(Cmd)  s  proposals
                                                                  then  proposals
                                                                  else  pv11\_p1\_add\_if\_new()  pv11\_p1\_same\_proposal(Cmd)  <s,  p>  proposa\000Cls
                                                                  fi    in
                                        <ballot$_{num}$,  active,  proposals'>


Date html generated: 2015_07_23-PM-04_32_54
Last ObjectModification: 2014_11_26-AM-11_29_23

Home Index