Nuprl Definition : mu_ex_v5_State
mu_ex_v5_State(initial_token) ==
SM4-class-du(mu_ex_v5_initState(initial_token);<mu_ex_v5_onRequest(), mu_ex_v5_Request()>;<mu_ex_v5_onToken()
, mu_ex_v5_Token()
>;<mu_ex_v5_onUseSR(), mu_ex_v5_UseSR()>;<mu_ex_v5_onLeaveCS(), mu_ex_v5_LeaveCS()>)
Definitions occuring in Statement :
mu_ex_v5_initState: mu_ex_v5_initState(initial_token),
mu_ex_v5_onLeaveCS: mu_ex_v5_onLeaveCS(),
mu_ex_v5_onUseSR: mu_ex_v5_onUseSR(),
mu_ex_v5_onToken: mu_ex_v5_onToken(),
mu_ex_v5_onRequest: mu_ex_v5_onRequest(),
mu_ex_v5_UseSR: mu_ex_v5_UseSR(),
mu_ex_v5_LeaveCS: mu_ex_v5_LeaveCS(),
mu_ex_v5_Token: mu_ex_v5_Token(),
mu_ex_v5_Request: mu_ex_v5_Request(),
SM4-class-du: SM4-class-du(init;trX1;trX2;trX3;trX4),
pair: <a, b>
FDL editor aliases :
mu_ex_v5_State
mu\_ex\_v5\_State(initial$_{token}$) ==
SM4-class-du(mu\_ex\_v5\_initState(initial$_{token}$);<mu\_ex\_v5\_onRequest()
, mu\_ex\_v5\_Request()
><mu\_ex\_v5\_onToken(), mu\_ex\_v5\_Token()><mu\_ex\_v5\_onUseSR()
, mu\_ex\_v5\_UseSR()
><mu\_ex\_v5\_onLeaveCS(), mu\_ex\_v5\_LeaveCS()>)
Date html generated:
2012_02_20-PM-06_54_36
Last ObjectModification:
2012_02_02-PM-02_58_22
Home
Index