Nuprl Definition : OARcast_OrdererForSenderState-program

OARcast_OrdererForSenderState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) ==
λsndr.state-class1-program(λslf.OARcast_oastate_init(M);OARcast_orderer_for_sender(M) sndr;

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

Definitions occuring in Statement : OARcast_orderer_for_sender: OARcast_orderer_for_sender(M), OARcast_oastate_init: OARcast_oastate_init(M), OARcast_order'verify-program: OARcast_order'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_OrdererForSenderState-program

Latex:
OARcast\_OrdererForSenderState-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) == \mlambda{}sndr.state-class1-program(\mlambda{}slf.OARcast\_oastate\_init(M);OARcast\_orderer\_for\_sender(M) sndr; OARcast\_order'verify-program(M;deliverhdr;oarcasthdr;...;orderhdr;mf)) Date html generated: 2015_07_23-PM-00_31_26 Last ObjectModification: 2014_08_20-PM-00_03_39 Home Index