Nuprl Definition : rsc2_newvote

rsc2_newvote(Cmd) ==
  ni,zd.
   let ze,sender = zd 
   in let ni',c = ze 
      in z.let cmds,z = z 
            in (product-deq(;;IntDeq;IntDeq) ni ni')  (deq-member(IdDeq;sender;z))


Definitions occuring in Statement :  id-deq: IdDeq,  band: p  q,  bnot: b,  apply: f a,  lambda: x.A[x],  spread: spread def,  int: ,  deq-member: deq-member(eq;x;L),  product-deq: product-deq(A;B;a;b),  int-deq: IntDeq
FDL editor aliases :  rsc2_newvote
rsc2\_newvote(Cmd)  ==
    \mlambda{}ni,zd.
      let  ze,sender  =  zd 
      in  let  ni',c  =  ze 
            in  \mlambda{}z.let  cmds,z  =  z 
                        in  (product-deq(\mBbbZ{};\mBbbZ{};IntDeq;IntDeq)  ni  ni')  \mwedge{}\msubb{}  (\mneg{}\msubb{}deq-member(IdDeq;sender;z))


Date html generated: 2012_02_20-PM-04_42_04
Last ObjectModification: 2012_02_02-PM-02_05_37

Home Index