Nuprl Definition : pv11_p1_ScoutOutput
pv11_p1_ScoutOutput(Cmd;accpts;mf) ==
λb.(((pv11_p1_scout_output(Cmd;accpts;mf) b o pv11_p1_p1b'base(Cmd;mf)) o pv11_p1_ScoutState(Cmd;accpts;mf) b) once)
Definitions occuring in Statement :
pv11_p1_scout_output: pv11_p1_scout_output(Cmd;accpts;mf),
pv11_p1_ScoutState: pv11_p1_ScoutState(Cmd;accpts;mf),
pv11_p1_p1b'base: pv11_p1_p1b'base(Cmd;mf),
once-class: (X once),
eclass2: (X o Y),
eclass1: (f o X),
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
pv11_p1_ScoutOutput
Latex:
pv11\_p1\_ScoutOutput(Cmd;accpts;mf) ==
\mlambda{}b.(((pv11\_p1\_scout\_output(Cmd;accpts;mf) b o pv11\_p1\_p1b'base(Cmd;mf)) o
pv11\_p1\_ScoutState(Cmd;accpts;mf) b) once)
Date html generated:
2016_05_17-PM-02_55_35
Last ObjectModification:
2014_11_26-AM-11_29_00
Theory : paxos!synod
Home
Index