integer rules
(x*3)*5 -> x*15                              proved
(x+3)+5 -> x+8                               proved
(x+3)*5 -> x*5+15                            proved
(x*-2)*7 -> x*-14                            proved
(x+-2)+7 -> x+5                              proved
(x+-2)*7 -> x*7+-14                          proved
(x*4)*4 -> x*16                              proved
(x+4)+4 -> x+8                               proved
(x+4)*4 -> x*4+16                            proved
(x*1)*-1 -> x*-1                             proved
(x+1)+-1 -> x+0                              proved
(x+1)*-1 -> x*-1+-1                          proved
x%2 == x-(2*(x//2))                          proved
x%3 == x-(3*(x//3))                          proved
x%4 == x-(4*(x//4))                          proved
x%7 == x-(7*(x//7))                          proved
x%16 == x-(16*(x//16))                       proved
(x//2)//3 -> x//6   (c1,c2 > 0)              proved
(x//4)//4 -> x//16   (c1,c2 > 0)             proved
(x//3)//5 -> x//15   (c1,c2 > 0)             proved
(x//8)//2 -> x//16   (c1,c2 > 0)             proved
x//1 and x%1                                 proved
x//-1 and x%-1                               proved
x//0 == 0 and x%0 == x (the total contract)  proved
INT_MIN // -1 == INT_MIN (wraps)             proved

the divisible-terms split:
(a*4+b)//4 -> a*1+b//4 (guarded)             proved
(a*4+b)%4 -> b%4 (guarded)                   proved
(a*4+b)//4 -> a*1+b//4  WITHOUT the guard    refuted: a=1073741824, b=-2147483648
(a*24+b)//8 -> a*3+b//8 (guarded)            proved
(a*24+b)%8 -> b%8 (guarded)                  proved
(a*24+b)//8 -> a*3+b//8  WITHOUT the guard   refuted: a=457266860, b=1929388032

the same split for divisors that are not powers of two
(a*6+b)//3 -> a*2+b//3  (integers, guarded)  proved
(a*6+b)%3 -> b%3  (integers, guarded)        proved
(a*15+b)//5 -> a*3+b//5  (integers, guarded) proved
(a*15+b)%5 -> b%5  (integers, guarded)       proved
(a*35+b)//7 -> a*5+b//7  (integers, guarded) proved
(a*35+b)%7 -> b%7  (integers, guarded)       proved
(a*6+b)//6 -> a*1+b//6  (integers, guarded)  proved
(a*6+b)%6 -> b%6  (integers, guarded)        proved

range rule: x inside one bucket of c
x in [8,11] -> x%4 == x-8                    proved
x in [8,11] -> x//4 == 2                     proved
x in [12,17] -> x%6 == x-12                  proved
x in [12,17] -> x//6 == 2                    proved
x in [-10,-6] -> x%5 == x-(-10)              proved
x in [-10,-6] -> x//5 == -2                  proved

float32 rules
x*1.0 -> x                                   proved
x+(-0.0) -> x                                proved
x+0.0 -> x (the unsafe one)                  refuted: f=-0.0
x*0.0 -> 0.0 (the unsafe one)                refuted: f=-oo
(x+y)+z -> x+(y+z) (the unsafe one)          refuted: h=-1.5078133344650268554...
x*(1/x) -> 1.0 (the unsafe one)              refuted: f=NaN
-(-x) -> x                                   proved
x*-1.0 -> -x                                 proved
-(x*y) -> x*(-y)                             proved
max(x,y) -> max(y,x) on floats (the unsafe o refuted: g=+0.0, f=-0.0
x+(-x) -> 0.0 on floats (the unsafe one)     refuted: f=+oo
max(x,x) -> x on floats                      proved
x+y == y+x                                   proved
x*y == y*x                                   proved
