Nuprl Definition : ohc_v2_newvote

ohc_v2_newvote() ==
  ni,za.
   let zb,sndr = za 
   in let ni',zc = zb 
      in z.let cmds,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 :  ohc_v2_newvote
ohc\_v2\_newvote()  ==
    \mlambda{}ni,za.
      let  zb,sndr  =  za 
      in  let  ni',zc  =  zb 
            in  \mlambda{}z.let  cmds,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_32_47
Last ObjectModification: 2012_02_17-PM-10_21_22

Home Index