Nuprl Definition : pv11_p1

Nuprl Definition : pv11_p1_Leader

pv11_p1_Leader(Cmd;accpts;ldrs_uid;reps;mf) ==
pv11_p1_SpawnFirstScout(Cmd;accpts;mf) || pv11_p1_LeaderPropose(Cmd;ldrs_uid;mf)

                                            || pv11_p1_LeaderAdopted(Cmd;ldrs_uid;mf)

                                             >z> pv11_p1_Commander(Cmd;accpts;reps;mf) z

|| pv11_p1_LeaderPreempted(Cmd;ldrs_uid;mf) >z> pv11_p1_Scout(Cmd;accpts;mf) z

Definitions occuring in Statement : pv11_p1_SpawnFirstScout: pv11_p1_SpawnFirstScout(Cmd;accpts;mf), pv11_p1_LeaderPreempted: pv11_p1_LeaderPreempted(Cmd;ldrs_uid;mf), pv11_p1_LeaderAdopted: pv11_p1_LeaderAdopted(Cmd;ldrs_uid;mf), pv11_p1_LeaderPropose: pv11_p1_LeaderPropose(Cmd;ldrs_uid;mf), pv11_p1_Scout: pv11_p1_Scout(Cmd;accpts;mf), pv11_p1_Commander: pv11_p1_Commander(Cmd;accpts;reps;mf), parallel-class: X || Y, bind-class: X >x> Y[x], apply: f a
FDL editor aliases : pv11_p1_Leader

Latex:
pv11\_p1\_Leader(Cmd;accpts;ldrs$_{uid}$;reps;mf) == pv11\_p1\_SpawnFirstScout(Cmd;accpts;mf) || pv11\_p1\_LeaderPropose(Cmd;ldrs$_{uid}$;mf) || pv11\_p1\_LeaderAdopted(Cmd;ldr\000Cs$_{uid}$;mf) >z> pv11\_p1\_Commander(Cmd;accpts;reps;mf) z || pv11\_p1\_LeaderPreempted(Cmd;ldrs$_{uid}$;mf) >z> pv11\_p1\_Scout(Cmd;accpts;m\000Cf) z Date html generated: 2015_07_23-PM-04_33_56 Last ObjectModification: 2014_11_26-AM-11_31_07 Home Index