Nuprl Definition : pv11_p1_AcceptorState-program
pv11_p1_AcceptorState-program(Cmd;ldrs_uid;mf) ==
state-class2-program(λloc.pv11_p1_init_acceptor(Cmd);pv11_p1_on_p1a(Cmd;ldrs_uid);pv11_p1_p1a'base-program(Cmd;mf);
pv11_p1_on_p2a(Cmd;ldrs_uid);pv11_p1_p2a'base-program(Cmd;mf))
Definitions occuring in Statement :
pv11_p1_on_p2a: pv11_p1_on_p2a(Cmd;ldrs_uid),
pv11_p1_on_p1a: pv11_p1_on_p1a(Cmd;ldrs_uid),
pv11_p1_init_acceptor: pv11_p1_init_acceptor(Cmd),
pv11_p1_p2a'base-program: pv11_p1_p2a'base-program(Cmd;mf),
pv11_p1_p1a'base-program: pv11_p1_p1a'base-program(Cmd;mf),
state-class2-program: state-class2-program(init;tr1;pr1;tr2;pr2),
lambda: λx.A[x]
FDL editor aliases :
pv11_p1_AcceptorState-program
Latex:
pv11\_p1\_AcceptorState-program(Cmd;ldrs$_{uid}$;mf) ==
state-class2-program(\mlambda{}loc.pv11\_p1\_init\_acceptor(Cmd);pv11\_p1\_on\_p1a(Cmd;ldrs$_{uid\mbackslash{}ff7\000Cd$);
pv11\_p1\_p1a'base-program(Cmd;mf);pv11\_p1\_on\_p2a(Cmd;ldrs$_{uid\mbackslash{}ff\000C7d$);
pv11\_p1\_p2a'base-program(Cmd;mf))
Date html generated:
2015_07_23-PM-04_12_59
Last ObjectModification:
2014_11_26-AM-11_25_55
Home
Index