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
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:
2015_07_17-AM-09_10_46
Last ObjectModification:
2012_02_25-AM-10_52_05
Home
Index