Nuprl Definition : pv11_p1_CommanderOutput-program

pv11_p1_CommanderOutput-program(Cmd;accpts;reps;mf) ==
  λz.let bnum,slt,cmd = z in 
     once-class-program(eclass1-program(pv11_p1_commander_output(Cmd;accpts;reps;mf) <bnum, slt, cmd>;pv11_p1_p2b'base-p\000Crogram(Cmd;mf))
                        o pv11_p1_CommanderState-program(Cmd;accpts;mf) bnum slt)


Definitions occuring in Statement :  pv11_p1_commander_output: pv11_p1_commander_output(Cmd;accpts;reps;mf),  pv11_p1_CommanderState-program: pv11_p1_CommanderState-program(Cmd;accpts;mf),  pv11_p1_p2b'base-program: pv11_p1_p2b'base-program(Cmd;mf),  once-class-program: once-class-program(pr),  eclass2-program: Xpr o Ypr,  eclass1-program: eclass1-program(f;pr),  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  pair: <a, b>
FDL editor aliases :  pv11_p1_CommanderOutput-program
Latex:
pv11\_p1\_CommanderOutput-program(Cmd;accpts;reps;mf)  ==
    \mlambda{}z.let  bnum,slt,cmd  =  z  in 
          once-class-program(eclass1-program(pv11\_p1\_commander\_output(Cmd;accpts;reps;mf) 
                                                                                <bnum,  slt,  cmd>pv11\_p1\_p2b'base-program(Cmd;mf))
                                                o  pv11\_p1\_CommanderState-program(Cmd;accpts;mf)  bnum  slt)


Date html generated: 2016_05_17-PM-02_54_06
Last ObjectModification: 2014_11_26-AM-11_27_19

Theory : paxos!synod


Home Index