Nuprl Definition : OARcast_Deliverer-program

OARcast_Deliverer-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf) ==
  eclass1-program(OARcast_on_ordered_output(M);
                  OARcast_ordered'verify-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf))
  o OARcast_DelivererState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)

   >>= λz.(OARcast_DelivererForSender-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf) z)

Definitions occuring in Statement : OARcast_DelivererState-program: OARcast_DelivererState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf), OARcast_on_ordered_output: OARcast_on_ordered_output(M), OARcast_DelivererForSender-program: OARcast_DelivererForSender-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf), OARcast_ordered'verify-program: OARcast_ordered'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_Deliverer-program

Latex:
OARcast\_Deliverer-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf) == eclass1-program(OARcast\_on\_ordered\_output(M); OARcast\_ordered'verify-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)) o OARcast\_DelivererState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) >>= \mlambda{}z.(OARcast\_DelivererForSender-program(M;deliverhdr;deqM;flrs;oarcasthdr;...;...;...;mf) z) Date html generated: 2016_05_17-PM-01_12_28 Last ObjectModification: 2014_08_20-PM-00_09_22 Theory : event-logic-applications Home Index