Nuprl Definition : OARcast_DelivererForSenderState

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


Definitions occuring in Statement :  OARcast_deliverer_for_sender_update: OARcast_deliverer_for_sender_update(M),  OARcast_ordered'verify: OARcast_ordered'verify(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf),  state-class1: state-class1(init;tr;X),  nil: [],  apply: f a,  lambda: λx.A[x]
FDL editor aliases :  OARcast_DelivererForSenderState
Latex:
OARcast\_DelivererForSenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)  ==
    \mlambda{}sndr.state-class1(\mlambda{}slf.[];OARcast\_deliverer\_for\_sender\_update(M) 
                                                          sndr;OARcast\_ordered'verify(M;deliverhdr;oarcasthdr;orderedhdr;...;mf))


Date html generated: 2015_07_23-PM-00_34_09
Last ObjectModification: 2014_08_20-PM-00_07_35

Home Index