Nuprl Definition : mu_ex_v6_P
mu_ex_v6_P(initial_token;m1;m2;proc1;proc2) ==
mu_ex_v6_Handle(initial_token) mu_ex_v6_handleRequest(proc1;proc2) mu_ex_v6_request'base()
|| mu_ex_v6_Handle(initial_token) mu_ex_v6_handleLeaveCS(proc1;proc2) mu_ex_v6_leaveCS'base()
|| mu_ex_v6_Handle(initial_token) mu_ex_v6_handleToken(m1;m2;proc1) mu_ex_v6_token'base()
|| mu_ex_v6_Handle(initial_token) mu_ex_v6_handleUseSR(m1;m2;proc1;proc2) mu_ex_v6_useSR'base()
Definitions occuring in Statement :
mu_ex_v6_handleLeaveCS: mu_ex_v6_handleLeaveCS(proc1;proc2),
mu_ex_v6_handleToken: mu_ex_v6_handleToken(m1;m2;proc1),
mu_ex_v6_handleUseSR: mu_ex_v6_handleUseSR(m1;m2;proc1;proc2),
mu_ex_v6_handleRequest: mu_ex_v6_handleRequest(proc1;proc2),
mu_ex_v6_Handle: mu_ex_v6_Handle(initial_token),
mu_ex_v6_useSR'base: mu_ex_v6_useSR'base(),
parallel-class: X || Y,
apply: f a
FDL editor aliases :
mu_ex_v6_P
mu\_ex\_v6\_P(initial$_{token}$;m1;m2;proc1;proc2) ==
mu\_ex\_v6\_Handle(initial$_{token}$) mu\_ex\_v6\_handleRequest(proc1;proc2) mu\_ex\_v\000C6\_request'base()
|| mu\_ex\_v6\_Handle(initial$_{token}$) mu\_ex\_v6\_handleLeaveCS(proc1;proc2) mu\_e\000Cx\_v6\_leaveCS'base()
|| mu\_ex\_v6\_Handle(initial$_{token}$) mu\_ex\_v6\_handleToken(m1;m2;proc1) mu\_ex\_\000Cv6\_token'base()
|| mu\_ex\_v6\_Handle(initial$_{token}$) mu\_ex\_v6\_handleUseSR(m1;m2;proc1;proc2) \000Cmu\_ex\_v6\_useSR'base()
Date html generated:
2012_02_20-PM-07_11_42
Last ObjectModification:
2012_02_02-PM-03_07_25
Home
Index