Nuprl Definition : rsc5_newvote

rsc5_newvote(Cmd) ==
  ni,za.
   let zb,sndr = za 
   in let ni',c = zb 
      in z.let pmaj,z = z 
            in (eqof(product-deq(;;IntDeq;IntDeq)) ni ni')  (deq-member(IdDeq;sndr;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,  eqof: eqof(d)
FDL editor aliases :  rsc5_newvote
rsc5\_newvote(Cmd)  ==
    \mlambda{}ni,za.
      let  zb,sndr  =  za 
      in  let  ni',c  =  zb 
            in  \mlambda{}z.let  pmaj,z  =  z 
                        in  (eqof(product-deq(\mBbbZ{};\mBbbZ{};IntDeq;IntDeq))  ni  ni')  \mwedge{}\msubb{}  (\mneg{}\msubb{}deq-member(IdDeq;sndr;z))


Date html generated: 2012_02_20-PM-05_05_02
Last ObjectModification: 2012_02_02-PM-02_17_51

Home Index