Nuprl Definition : pv11_p1_Leader-program
pv11_p1_Leader-program(Cmd;accpts;ldrs_uid;reps;mf) ==
pv11_p1_SpawnFirstScout-program(Cmd;accpts;mf) || pv11_p1_LeaderPropose-program(Cmd;ldrs_uid;mf)
|| pv11_p1_LeaderAdopted-program(Cmd;ldrs_uid;mf)
>>= λz.(pv11_p1_Commander-program(Cmd;accpts;reps;mf) z)
|| pv11_p1_LeaderPreempted-program(Cmd;ldrs_uid;mf) >>= λz.(pv11_p1_Scout-program(Cmd;accpts;mf) z)
Definitions occuring in Statement :
pv11_p1_SpawnFirstScout-program: pv11_p1_SpawnFirstScout-program(Cmd;accpts;mf),
pv11_p1_LeaderPreempted-program: pv11_p1_LeaderPreempted-program(Cmd;ldrs_uid;mf),
pv11_p1_LeaderAdopted-program: pv11_p1_LeaderAdopted-program(Cmd;ldrs_uid;mf),
pv11_p1_LeaderPropose-program: pv11_p1_LeaderPropose-program(Cmd;ldrs_uid;mf),
pv11_p1_Scout-program: pv11_p1_Scout-program(Cmd;accpts;mf),
pv11_p1_Commander-program: pv11_p1_Commander-program(Cmd;accpts;reps;mf),
parallel-class-program: X || Y,
bind-class-program: xpr >>= ypr,
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
pv11_p1_Leader-program
Latex:
pv11\_p1\_Leader-program(Cmd;accpts;ldrs$_{uid}$;reps;mf) ==
pv11\_p1\_SpawnFirstScout-program(Cmd;accpts;mf)
|| pv11\_p1\_LeaderPropose-program(Cmd;ldrs$_{uid}$;mf) || pv11\_p1\_LeaderAdopted\000C-program(Cmd;ldrs$_{uid}$;mf)
>>= \mlambda{}z.(pv11\_p1\_Commander-program(Cmd;accpts;reps;mf) z)
|| pv11\_p1\_LeaderPreempted-program(Cmd;ldrs$_{uid}$;mf) >>= \mlambda{}z.(pv11\_p1\_Scout-\000Cprogram(Cmd;accpts;mf) z)
Date html generated:
2015_07_23-PM-04_34_00
Last ObjectModification:
2014_11_26-AM-11_31_14
Home
Index