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: 2016_05_17-PM-01_10_18 Last ObjectModification: 2014_08_20-PM-00_07_35 Theory : event-logic-applications Home Index