Nuprl Definition : OARcast

Nuprl Definition : OARcast_DelivererState

OARcast_DelivererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) ==

  state-class1(λslf.[];OARcast_on_ordered_update(M);OARcast_ordered'verify(M;deliverhdr;oarcasthdr;orderedhdr;...;mf))

Definitions occuring in Statement : OARcast_on_ordered_update: OARcast_on_ordered_update(M), OARcast_ordered'verify: OARcast_ordered'verify(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf), state-class1: state-class1(init;tr;X), nil: [], lambda: λx.A[x]
FDL editor aliases : OARcast_DelivererState

Latex:
OARcast\_DelivererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) == state-class1(\mlambda{}slf.[];OARcast\_on\_ordered\_update(M);OARcast\_ordered'verify(M;...;...;...;...;mf)) Date html generated: 2015_07_23-PM-00_34_55 Last ObjectModification: 2014_08_20-PM-00_08_46 Home Index