Nuprl Definition : pv11_p1_CommanderState-program

pv11_p1_CommanderState-program(Cmd;accpts;mf) ==
  λb,s. state-class1-program(λloc.accpts;pv11_p1_on_p2b() s;pv11_p1_p2b'base-program(Cmd;mf))



Definitions occuring in Statement :  pv11_p1_on_p2b: pv11_p1_on_p2b() pv11_p1_p2b'base-program: pv11_p1_p2b'base-program(Cmd;mf) state-class1-program: state-class1-program(init;tr;pr) apply: a lambda: λx.A[x]
FDL editor aliases :  pv11_p1_CommanderState-program

Latex:
pv11\_p1\_CommanderState-program(Cmd;accpts;mf)  ==
    \mlambda{}b,s.  state-class1-program(\mlambda{}loc.accpts;pv11\_p1\_on\_p2b()  b  s;pv11\_p1\_p2b'base-program(Cmd;mf))



Date html generated: 2015_07_23-PM-04_13_52
Last ObjectModification: 2014_11_26-AM-11_27_02

Home Index