Nuprl Definition : OARcast_orderer_for_sender

OARcast_orderer_for_sender(M) ==
  λsndr,loc,za,z. let l,seqm = za 
                  in let z,state = z 
                     in if l = sndr then process-ordered-message(state;seqm) else <[], state> fi 


Definitions occuring in Statement :  process-ordered-message: process-ordered-message(nL;km),  eq_id: a = b,  nil: [],  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
FDL editor aliases :  OARcast_orderer_for_sender
Latex:
OARcast\_orderer\_for\_sender(M)  ==
    \mlambda{}sndr,loc,za,z.  let  l,seqm  =  za 
                                    in  let  z,state  =  z 
                                          in  if  l  =  sndr  then  process-ordered-message(state;seqm)  else  <[],  state>  fi 


Date html generated: 2016_05_17-PM-01_04_28
Last ObjectModification: 2014_08_20-PM-00_03_14

Theory : event-logic-applications


Home Index