Nuprl Definition : new_23_sig_newvote

new_23_sig_newvote(Cmd) ==
  λni,zd,z. let ze,sender = zd 
            in let ni',c = ze 
               in let cmds,locs = z 
                  in (product-deq(ℤ;ℤ;IntDeq;IntDeq) ni ni') ∧b (¬bsender ∈b locs))


Definitions occuring in Statement :  id-deq: IdDeq,  deq-member: x ∈b L),  product-deq: product-deq(A;B;a;b),  int-deq: IntDeq,  band: p ∧b q,  bnot: ¬bb,  apply: f a,  lambda: λx.A[x],  spread: spread def,  int: ℤ
FDL editor aliases :  new_23_sig_newvote
Latex:
new\_23\_sig\_newvote(Cmd)  ==
    \mlambda{}ni,zd,z.  let  ze,sender  =  zd 
                        in  let  ni',c  =  ze 
                              in  let  cmds,locs  =  z 
                                    in  (product-deq(\mBbbZ{};\mBbbZ{};IntDeq;IntDeq)  ni  ni')  \mwedge{}\msubb{}  (\mneg{}\msubb{}sender  \mmember{}\msubb{}  locs))


Date html generated: 2015_07_23-PM-03_50_30
Last ObjectModification: 2013_11_23-PM-09_54_42

Home Index