Nuprl Definition : OARcast_DelivererForSenderSeq-program

OARcast_DelivererForSenderSeq-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf) ==

  λsndr,seq. eclass0-program(OARcast_deliverer_for_sender_seq_output(M;deliverhdr;flrs;oarcasthdr;orderedhdr;...;mf)

sndr
seq;

             OARcast_DelivererForSenderSeqState-program(M;deliverhdr;deqM;oarcasthdr;orderedhdr;orderers;orderhdr;mf)

sndr
seq)

Definitions occuring in Statement : OARcast_deliverer_for_sender_seq_output: OARcast_deliverer_for_sender_seq_output(M;deliverhdr;flrs;oarcasthdr;orderedhdr;orderhdr;mf), OARcast_DelivererForSenderSeqState-program: OARcast_DelivererForSenderSeqState-program(M;deliverhdr;deqM;oarcasthdr;orderedhdr;orderers;orderhdr;mf), eclass0-program: eclass0-program(f;pr), apply: f a, lambda: λx.A[x]
FDL editor aliases : OARcast_DelivererForSenderSeq-program

Latex:
OARcast\_DelivererForSenderSeq-program(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;...;...;mf) == \mlambda{}sndr,seq. eclass0-program(OARcast\_deliverer\_for\_sender\_seq\_output(M;...;flrs;...;...;orderhdr;mf) sndr seq; OARcast\_DelivererForSenderSeqState-program(M;deliverhdr;deqM;oarcasthdr;...;...;...;mf) sndr seq) Date html generated: 2015_07_23-PM-00_33_48 Last ObjectModification: 2014_08_20-PM-00_06_57 Home Index