Nuprl Definition : OARcast_DelivererForSenderSeqState

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

            state-class1(λslf.OARcast_init_odstate(M;orderers);OARcast_deliverer_for_sender_seq_update(M;deqM) sndr

                                                               seq;OARcast_ordered'verify(M;deliverhdr;...;...;...;mf))

Definitions occuring in Statement : OARcast_deliverer_for_sender_seq_update: OARcast_deliverer_for_sender_seq_update(M;deqM), OARcast_init_odstate: OARcast_init_odstate(M;orderers), OARcast_ordered'verify: OARcast_ordered'verify(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf), state-class1: state-class1(init;tr;X), apply: f a, lambda: λx.A[x]
FDL editor aliases : OARcast_DelivererForSenderSeqState

Latex:
OARcast\_DelivererForSenderSeqState(M;deliverhdr;deqM;oarcasthdr;orderedhdr;orderers;orderhdr;mf) == \mlambda{}sndr,seq. state-class1(\mlambda{}slf.OARcast\_init\_odstate(M;orderers);... sndr seq;...) Date html generated: 2015_07_23-PM-00_32_56 Last ObjectModification: 2014_08_20-PM-00_06_06 Home Index