Nuprl Definition : OARcast_DelivererForSender-program

OARcast_DelivererForSender-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf) ==
λsndr.eclass1-program(OARcast_deliverer_for_sender_output(M) sndr;

                        OARcast_ordered'verify-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf))

o OARcast_DelivererForSenderState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) sndr

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

sndr
z)

Definitions occuring in Statement : OARcast_DelivererForSenderState-program: OARcast_DelivererForSenderState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf), OARcast_deliverer_for_sender_output: OARcast_deliverer_for_sender_output(M), OARcast_DelivererForSenderSeq-program: OARcast_DelivererForSenderSeq-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_DelivererForSender-program

Latex:
OARcast\_DelivererForSender-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;...;mf) == \mlambda{}sndr.eclass1-program(OARcast\_deliverer\_for\_sender\_output(M) sndr; OARcast\_ordered'verify-program(M;deliverhdr;oarcasthdr;orderedhdr;...;mf)) o OARcast\_DelivererForSenderState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) sndr >>= \mlambda{}z.(OARcast\_DelivererForSenderSeq-program(M;deliverhdr;deqM;flrs;...;...;...;...;mf) sndr z) Date html generated: 2015_07_23-PM-00_34_33 Last ObjectModification: 2014_08_20-PM-00_08_09 Home Index