Nuprl Definition : OARcast

Nuprl Definition : OARcast_Orderer-program

OARcast_Orderer-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf) ==
  eclass1-program(OARcast_on_order_output(M);
                  OARcast_order'verify-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf))
  o OARcast_OrdererState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)
   >>= λz.(OARcast_OrdererForSender-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf) z)

Definitions occuring in Statement : OARcast_OrdererState-program: OARcast_OrdererState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf), OARcast_on_order_output: OARcast_on_order_output(M), OARcast_OrdererForSender-program: OARcast_OrdererForSender-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf), OARcast_order'verify-program: OARcast_order'verify-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf), bind-class-program: xpr >>= ypr, eclass2-program: Xpr o Ypr, eclass1-program: eclass1-program(f;pr), apply: f a, lambda: λx.A[x]
FDL editor aliases : OARcast_Orderer-program

Latex:
OARcast\_Orderer-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf) == eclass1-program(OARcast\_on\_order\_output(M); OARcast\_order'verify-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)) o OARcast\_OrdererState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) >>= \mlambda{}z.(OARcast\_OrdererForSender-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;...;mf) z) Date html generated: 2015_07_23-PM-00_32_32 Last ObjectModification: 2014_08_20-PM-00_05_27 Home Index