% Information Flow Control, Nonlinear Variant

off rlabout;



rlset z;


{}


phi := ex(n,
   (a < b and cong(a+b,0,2) and 2*n = a+b and
      ((a<b and b-a=n^2) or (a >= b and a-b = n^2))) or
   (a < b and ncong(a+b,0,2) and 2*n = a+b+1 and
      ((a < b and b-a = n^2) or (a >= b and a-b = n^2))))$



rlwqe phi;


             2            2                2            2
bex _k2 [ - a  + 2*a*b - b  - 2 <= _k2 <= a  - 2*a*b + b  + 2] (a - b < 0

                                                  2
 and a + b #2# 0 and 2*_k2 - a - b - 1 = 0 and _k2  + a - b = 0) or bex _k1 [

    2            2                2            2
 - a  + 2*a*b - b  - 2 <= _k1 <= a  - 2*a*b + b  + 2] (a - b < 0 and a + b ~2~ 0

                              2
 and 2*_k1 - a - b = 0 and _k1  + a - b = 0)


end;

