% It is attainable for a process to always get a number that is at least the
% number that is currently circulating
% Taken from "Model-Checking Processes with Data"
% J.F. Groote and T.A.C. Willemse

nu Z(i: Nat= 0).((exists b:Bool. exists n:Nat. <c(b,n)>(val(n + Pos2Nat(1) > i) && Z(n))) ||
              <forall b':Bool. forall n':Nat. !c(b',n')>Z(i))
