Nuprl Definition : OARcast_DelivererForSenderSeq

OARcast_DelivererForSenderSeq(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;mf) ==
λsndr,seq. (OARcast_deliverer_for_sender_seq_output(M;deliverhdr;flrs;oarcasthdr;orderedhdr;orderhdr;mf) sndr

              seq o OARcast_DelivererForSenderSeqState(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: OARcast_DelivererForSenderSeqState(M;deliverhdr;deqM;oarcasthdr;orderedhdr;orderers;orderhdr;mf), eclass0: (f o X), apply: f a, lambda: λx.A[x]
FDL editor aliases : OARcast_DelivererForSenderSeq

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