Nuprl Definition : OARcast_deliverer_for_sender_update
OARcast_deliverer_for_sender_update(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 state else [seq / state] fi 
Definitions occuring in Statement : 
deq-member: x ∈b L)
, 
int-deq: IntDeq
, 
cons: [a / b]
, 
ifthenelse: if b then t else f fi 
, 
lambda: λx.A[x]
, 
spread: spread def
FDL editor aliases : 
OARcast_deliverer_for_sender_update
Latex:
OARcast\_deliverer\_for\_sender\_update(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  state  else  [seq  /  state]  fi 
Date html generated:
2015_07_23-PM-00_33_55
Last ObjectModification:
2014_08_20-PM-00_07_11
Home
Index