Nuprl Definition : mu_ex_v5_P
mu_ex_v5_P(initial_token;m1;m2;proc1;proc2) ==
l.mu_ex_v5_HandleRequests(initial_token;proc1;proc2) l || mu_ex_v5_HandleUseSR(initial_token;m1;m2;proc1;proc2) l
|| mu_ex_v5_HandleToken(initial_token;m1;m2;proc1) || mu_ex_v5_HandleLeaveCS(initial_token;proc1;proc2) l
Definitions occuring in Statement :
mu_ex_v5_HandleLeaveCS: mu_ex_v5_HandleLeaveCS(initial_token;proc1;proc2),
mu_ex_v5_HandleToken: mu_ex_v5_HandleToken(initial_token;m1;m2;proc1),
mu_ex_v5_HandleUseSR: mu_ex_v5_HandleUseSR(initial_token;m1;m2;proc1;proc2),
mu_ex_v5_HandleRequests: mu_ex_v5_HandleRequests(initial_token;proc1;proc2),
parallel-class: X || Y,
apply: f a,
lambda: x.A[x]
FDL editor aliases :
mu_ex_v5_P
mu\_ex\_v5\_P(initial$_{token}$;m1;m2;proc1;proc2) ==
\mlambda{}l.mu\_ex\_v5\_HandleRequests(initial$_{token}$;proc1;proc2) l
|| mu\_ex\_v5\_HandleUseSR(initial$_{token}$;m1;m2;proc1;proc2) l
|| mu\_ex\_v5\_HandleToken(initial$_{token}$;m1;m2;proc1)
|| mu\_ex\_v5\_HandleLeaveCS(initial$_{token}$;proc1;proc2) l
Date html generated:
2012_02_20-PM-06_56_44
Last ObjectModification:
2012_02_02-PM-02_59_35
Home
Index