Nuprl Definition : pv11_p1_LeaderState-program
pv11_p1_LeaderState-program(Cmd;ldrs_uid;mf) ==
memory-class3-program(pv11_p1_init_leader(Cmd);pv11_p1_on_propose(Cmd);pv11_p1_propose'base-program(Cmd;mf);
pv11_p1_when_adopted(Cmd;ldrs_uid);pv11_p1_adopted'base-program(Cmd;mf);
pv11_p1_when_preempted(Cmd;ldrs_uid);pv11_p1_preempted'base-program(Cmd;mf))
Definitions occuring in Statement :
pv11_p1_when_preempted: pv11_p1_when_preempted(Cmd;ldrs_uid),
pv11_p1_when_adopted: pv11_p1_when_adopted(Cmd;ldrs_uid),
pv11_p1_on_propose: pv11_p1_on_propose(Cmd),
pv11_p1_init_leader: pv11_p1_init_leader(Cmd),
pv11_p1_propose'base-program: pv11_p1_propose'base-program(Cmd;mf),
pv11_p1_adopted'base-program: pv11_p1_adopted'base-program(Cmd;mf),
pv11_p1_preempted'base-program: pv11_p1_preempted'base-program(Cmd;mf),
memory-class3-program: memory-class3-program(init;tr1;pr1;tr2;pr2;tr3;pr3)
FDL editor aliases :
pv11_p1_LeaderState-program
Latex:
pv11\_p1\_LeaderState-program(Cmd;ldrs$_{uid}$;mf) ==
memory-class3-program(pv11\_p1\_init\_leader(Cmd);pv11\_p1\_on\_propose(Cmd);
pv11\_p1\_propose'base-program(Cmd;mf);pv11\_p1\_when\_adopted(Cmd;ldrs$_\000C{uid}$);
pv11\_p1\_adopted'base-program(Cmd;mf);pv11\_p1\_when\_preempted(Cmd;ldrs$\mbackslash{}ff\000C5f{uid}$);
pv11\_p1\_preempted'base-program(Cmd;mf))
Date html generated:
2015_07_23-PM-04_33_15
Last ObjectModification:
2014_11_26-AM-11_29_54
Home
Index