Nuprl Definition : pv11_p1_ScoutOutput-program

pv11_p1_ScoutOutput-program(Cmd;accpts;mf) ==
  λb.once-class-program(eclass1-program(pv11_p1_scout_output(Cmd;accpts;mf) b;pv11_p1_p1b'base-program(Cmd;mf))
                        o pv11_p1_ScoutState-program(Cmd;accpts;mf) b)


Definitions occuring in Statement :  pv11_p1_scout_output: pv11_p1_scout_output(Cmd;accpts;mf),  pv11_p1_ScoutState-program: pv11_p1_ScoutState-program(Cmd;accpts;mf),  pv11_p1_p1b'base-program: pv11_p1_p1b'base-program(Cmd;mf),  once-class-program: once-class-program(pr),  eclass2-program: Xpr o Ypr,  eclass1-program: eclass1-program(f;pr),  apply: f a,  lambda: λx.A[x]
FDL editor aliases :  pv11_p1_ScoutOutput-program
Latex:
pv11\_p1\_ScoutOutput-program(Cmd;accpts;mf)  ==
    \mlambda{}b.once-class-program(eclass1-program(pv11\_p1\_scout\_output(Cmd;accpts;mf)  b;
                                                                                pv11\_p1\_p1b'base-program(Cmd;mf))
                                                o  pv11\_p1\_ScoutState-program(Cmd;accpts;mf)  b)


Date html generated: 2015_07_23-PM-04_32_44
Last ObjectModification: 2014_11_26-AM-11_29_05

Home Index