Nuprl Definition : OARcast_DelivererForSenderSeqState-program

OARcast_DelivererForSenderSeqState-program(M;deliverhdr;deqM;oarcasthdr;orderedhdr;orderers;orderhdr;mf) ==

  λsndr,seq. state-class1-program(λslf.OARcast_init_odstate(M;orderers);OARcast_deliverer_for_sender_seq_update(M;deqM)

                                                                        sndr

                                                                        seq;

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

Definitions occuring in Statement : OARcast_deliverer_for_sender_seq_update: OARcast_deliverer_for_sender_seq_update(M;deqM), OARcast_init_odstate: OARcast_init_odstate(M;orderers), OARcast_ordered'verify-program: OARcast_ordered'verify-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf), state-class1-program: state-class1-program(init;tr;pr), apply: f a, lambda: λx.A[x]
FDL editor aliases : OARcast_DelivererForSenderSeqState-program

Latex:
OARcast\_DelivererForSenderSeqState-program(M;deliverhdr;deqM;oarcasthdr;orderedhdr;...;...;mf) == \mlambda{}sndr,seq. state-class1-program(\mlambda{}slf.OARcast\_init\_odstate(M;orderers); OARcast\_deliverer\_for\_sender\_seq\_update(M;deqM) sndr seq; OARcast\_ordered'verify-program(M;deliverhdr;oarcasthdr;...;...;mf)) Date html generated: 2015_07_23-PM-00_33_03 Last ObjectModification: 2014_08_20-PM-00_06_18 Home Index