Nuprl Definition : pv11_p1

Nuprl Definition : pv11_p1_LeaderState

pv11_p1_LeaderState(Cmd;ldrs_uid;mf) ==
memory-class3(pv11_p1_init_leader(Cmd);pv11_p1_on_propose(Cmd);pv11_p1_propose'base(Cmd;mf);

                pv11_p1_when_adopted(Cmd;ldrs_uid);pv11_p1_adopted'base(Cmd;mf);pv11_p1_when_preempted(Cmd;ldrs_uid)

;pv11_p1_preempted'base(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: pv11_p1_propose'base(Cmd;mf), pv11_p1_adopted'base: pv11_p1_adopted'base(Cmd;mf), pv11_p1_preempted'base: pv11_p1_preempted'base(Cmd;mf), memory-class3: memory-class3(init;tr1;X1;tr2;X2;tr3;X3)
FDL editor aliases : pv11_p1_LeaderState

Latex:
pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;mf) == memory-class3(pv11\_p1\_init\_leader(Cmd);pv11\_p1\_on\_propose(Cmd);pv11\_p1\_propose'base(Cmd;mf); pv11\_p1\_when\_adopted(Cmd;ldrs$_{uid}$);pv11\_p1\_adopted'base(Cmd;\000Cmf); pv11\_p1\_when\_preempted(Cmd;ldrs$_{uid}$);pv11\_p1\_preempted'base(\000CCmd;mf)) Date html generated: 2015_07_23-PM-04_33_03 Last ObjectModification: 2014_11_26-AM-11_29_39 Home Index