Nuprl Definition : OARcast_main-program
OARcast_main-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;receivers;senders;mf) ==
(OARcast_Orderer-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf))@orderers
|| (OARcast_Deliverer-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf))@receivers
|| (OARcast_Sender-program(M;deliverhdr;oarcasthdr;orderedhdr;orderers;orderhdr;mf))@senders
Definitions occuring in Statement :
OARcast_Deliverer-program: OARcast_Deliverer-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf),
OARcast_Orderer-program: OARcast_Orderer-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf),
OARcast_Sender-program: OARcast_Sender-program(M;deliverhdr;oarcasthdr;orderedhdr;orderers;orderhdr;mf),
class-at-program: (pr)@locs,
parallel-class-program: X || Y
FDL editor aliases :
OARcast_main-program
Latex:
OARcast\_main-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;...;...;mf) ==
(OARcast\_Orderer-program(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf))@orderers
|| (OARcast\_Deliverer-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;...;mf))@...
|| (OARcast\_Sender-program(M;deliverhdr;oarcasthdr;orderedhdr;orderers;orderhdr;mf))@senders
Date html generated:
2015_07_23-PM-00_35_33
Last ObjectModification:
2014_08_20-PM-00_09_48
Home
Index