Nuprl Definition : OARcast_deliverer_for_sender_seq_update

OARcast_deliverer_for_sender_seq_update(M;deqM) ==
  λsndr,seq,slf,z,state. let orderer,z = z 
                         in let l,z = z 
                            in let s,m = z 
                               in if sndr = l ∧b (seq =z s) then update-oarcast-deliver(deqM;state;<orderer, m>) else st\000Cate fi 


Definitions occuring in Statement :  update-oarcast-deliver: update-oarcast-deliver(eq;s;p),  eq_id: a = b,  band: p ∧b q,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
FDL editor aliases :  OARcast_deliverer_for_sender_seq_update
Latex:
OARcast\_deliverer\_for\_sender\_seq\_update(M;deqM)  ==
    \mlambda{}sndr,seq,slf,z,state.  let  orderer,z  =  z 
                                                  in  let  l,z  =  z 
                                                        in  let  s,m  =  z 
                                                              in  if  sndr  =  l  \mwedge{}\msubb{}  (seq  =\msubz{}  s)
                                                                    then  update-oarcast-deliver(deqM;state;<orderer,  m>)
                                                                    else  state
                                                                    fi 


Date html generated: 2015_07_23-PM-00_32_48
Last ObjectModification: 2014_08_20-PM-00_05_52

Home Index