Nuprl Definition : OARcast_Deliverer
OARcast_Deliverer(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf) ==
((OARcast_on_ordered_output(M) o OARcast_ordered'verify(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)) o
OARcast_DelivererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf))
>z> OARcast_DelivererForSender(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf) z
Definitions occuring in Statement :
OARcast_DelivererState: OARcast_DelivererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf),
OARcast_on_ordered_output: OARcast_on_ordered_output(M),
OARcast_DelivererForSender: OARcast_DelivererForSender(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf),
OARcast_ordered'verify: OARcast_ordered'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_Deliverer
Latex:
OARcast\_Deliverer(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf) ==
((OARcast\_on\_ordered\_output(M) o
OARcast\_ordered'verify(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)) o
OARcast\_DelivererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf))
>z> OARcast\_DelivererForSender(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;...;mf)
z
Date html generated:
2015_07_23-PM-00_35_10
Last ObjectModification:
2014_08_20-PM-00_09_09
Home
Index