Nuprl Definition : pv11_p1_leader_propose

pv11_p1_leader_propose(Cmd) ==
  λloc,zt,z. let slt,p = zt 
             in let ballot_num,active,proposals = z in 
                if active ∧b (¬b(pv11_p1_in_domain(Cmd) slt proposals)) then {<ballot_num, slt, p>} else {} fi 


Definitions occuring in Statement :  pv11_p1_in_domain: pv11_p1_in_domain(Cmd),  band: p ∧b q,  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  pv11_p1_leader_propose
Latex:
pv11\_p1\_leader\_propose(Cmd)  ==
    \mlambda{}loc,zt,z.  let  slt,p  =  zt 
                          in  let  ballot$_{num}$,active,proposals  =  z  in 
                                if  active  \mwedge{}\msubb{}  (\mneg{}\msubb{}(pv11\_p1\_in\_domain(Cmd)  slt  proposals))
                                then  \{<ballot$_{num}$,  slt,  p>\}
                                else  \{\}
                                fi 


Date html generated: 2016_05_17-PM-02_57_08
Last ObjectModification: 2014_11_26-AM-11_30_03

Theory : paxos!synod


Home Index