Nuprl Definition : OARcast

Nuprl Definition : OARcast_Orderer

OARcast_Orderer(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf) ==
  ((OARcast_on_order_output(M) o OARcast_order'verify(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)) o
  OARcast_OrdererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf))
   >z> OARcast_OrdererForSender(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf) z

Definitions occuring in Statement : OARcast_OrdererState: OARcast_OrdererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf), OARcast_on_order_output: OARcast_on_order_output(M), OARcast_OrdererForSender: OARcast_OrdererForSender(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf), OARcast_order'verify: OARcast_order'verify(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf), bind-class: X >x> Y[x], eclass2: (X o Y), eclass1: (f o X), apply: f a
FDL editor aliases : OARcast_Orderer

Latex:
OARcast\_Orderer(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf) == ((OARcast\_on\_order\_output(M) o OARcast\_order'verify(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)) o OARcast\_OrdererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)) >z> OARcast\_OrdererForSender(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf) z Date html generated: 2015_07_23-PM-00_32_23 Last ObjectModification: 2014_08_20-PM-00_05_15 Home Index