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