Nuprl Definition : OARcast_deliverer_for_sender_output

OARcast_deliverer_for_sender_output(M) ==
  λsndr,slf,z,state. let orderer,z = z in let sndr,z = z in let seq,m = z in if seq ∈b state) then {} else {seq} fi 


Definitions occuring in Statement :  deq-member: x ∈b L),  int-deq: IntDeq,  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  spread: spread def,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  OARcast_deliverer_for_sender_output
Latex:
OARcast\_deliverer\_for\_sender\_output(M)  ==
    \mlambda{}sndr,slf,z,state.  let  orderer,z  =  z 
                                          in  let  sndr,z  =  z 
                                                in  let  seq,m  =  z 
                                                      in  if  seq  \mmember{}\msubb{}  state)  then  \{\}  else  \{seq\}  fi 


Date html generated: 2015_07_23-PM-00_34_02
Last ObjectModification: 2014_08_20-PM-00_07_22

Home Index