Nuprl Definition : new_23_sig_when_new_round

new_23_sig_when_new_round(Cmd) ==
  λn,loc,z,round. let z,c = z in let m,i = z in if (n =z m) ∧b round <z i then {<<m, i>, c>} else {} fi 


Definitions occuring in Statement :  band: p ∧b q,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  new_23_sig_when_new_round
Latex:
new\_23\_sig\_when\_new\_round(Cmd)  ==
    \mlambda{}n,loc,z,round.  let  z,c  =  z 
                                    in  let  m,i  =  z 
                                          in  if  (n  =\msubz{}  m)  \mwedge{}\msubb{}  round  <z  i  then  \{<<m,  i>,  c>\}  else  \{\}  fi 


Date html generated: 2016_05_17-PM-02_04_10
Last ObjectModification: 2013_11_23-PM-09_55_20

Theory : 2!3!consensus!with!signatures


Home Index