Nuprl Definition : RSC_newvote

RSC_newvote(Cmd) ==
  ni,zg.
   let zh,sender = zg 
   in let ni',c = zh 
      in z.let zf,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 :  RSC_newvote
RSC\_newvote(Cmd)  ==
    \mlambda{}ni,zg.
      let  zh,sender  =  zg 
      in  let  ni',c  =  zh 
            in  \mlambda{}z.let  zf,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-03_39_52
Last ObjectModification: 2012_02_02-PM-01_58_16

Home Index