Nuprl Definition : OARcast_DelivererForSenderState-program

OARcast_DelivererForSenderState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) ==
λsndr.state-class1-program(λslf.[];OARcast_deliverer_for_sender_update(M) sndr;

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

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

Latex:
OARcast\_DelivererForSenderState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) == \mlambda{}sndr.state-class1-program(\mlambda{}slf.[];OARcast\_deliverer\_for\_sender\_update(M) sndr; OARcast\_ordered'verify-program(M;deliverhdr;oarcasthdr;...;...;mf)) Date html generated: 2015_07_23-PM-00_34_18 Last ObjectModification: 2014_08_20-PM-00_07_46 Home Index