Nuprl Definition : OARcast_DelivererForSender

OARcast_DelivererForSender(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf) ==
  λsndr.((OARcast_deliverer_for_sender_output(M) sndr o
         OARcast_ordered'verify(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)) o
        OARcast_DelivererForSenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) sndr)

         >z> OARcast_DelivererForSenderSeq(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf) sndr z

Definitions occuring in Statement : OARcast_DelivererForSenderState: OARcast_DelivererForSenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf), OARcast_deliverer_for_sender_output: OARcast_deliverer_for_sender_output(M), OARcast_DelivererForSenderSeq: OARcast_DelivererForSenderSeq(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf), OARcast_ordered'verify: OARcast_ordered'verify(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf), bind-class: X >x> Y[x], eclass2: (X o Y), eclass1: (f o X), apply: f a, lambda: λx.A[x]
FDL editor aliases : OARcast_DelivererForSender

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