Nuprl Definition : Paxos-spec8-spec77
AcceptOrReject ==  (let lbv,m = lbvm in let l,b,v = lbv in <lbv, m ≤z b> where lbvm from (MaxReserve'?-1) when x2)
Definitions occuring in Statement : 
abbreviation: MaxReserve
, 
le_int: i ≤z j
, 
spreadn: spread3, 
spread: spread def, 
pair: <a, b>
, 
minus: -n
, 
natural_number: $n
Latex:
AcceptOrReject  ==    (let  lbv,m  =  lbvm  in  let  l,b,v  =  lbv  in  <lbv,  m  \mleq{}z  b>  where  lbvm  from  (MaxReserve\000C'?-1)  when  x2)
Date html generated:
2016_05_16-AM-10_53_05
Last ObjectModification:
2012_02_25-AM-10_52_05
Theory : event-ordering
Home
Index