Nuprl Definition : OARcast_OrdererForSenderState

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


Definitions occuring in Statement :  OARcast_orderer_for_sender: OARcast_orderer_for_sender(M),  OARcast_oastate_init: OARcast_oastate_init(M),  OARcast_order'verify: OARcast_order'verify(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf),  state-class1: state-class1(init;tr;X),  apply: f a,  lambda: λx.A[x]
FDL editor aliases :  OARcast_OrdererForSenderState
Latex:
OARcast\_OrdererForSenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)  ==
    \mlambda{}sndr.state-class1(\mlambda{}slf.OARcast\_oastate\_init(M);OARcast\_orderer\_for\_sender(M) 
                                                                                                    sndr;OARcast\_order'verify(M;...;...;...;...;mf))


Date html generated: 2015_07_23-PM-00_31_18
Last ObjectModification: 2014_08_20-PM-00_03_27

Home Index