arith-negate-abs-s4.out

max expr size  =    4
  |- on ineqs  =    3
  |- on conds  =    3
max  #-tests   =  500
min  #-tests   =   25  (to consider p ==> q true)
max  #-vars    =    2  (for inequational and conditional laws)

_ :: Int
0 :: Int
1 :: Int
id :: Int -> Int
abs :: Int -> Int
negate :: Int -> Int
(+) :: Int -> Int -> Int
(*) :: Int -> Int -> Int

             id x == x
negate (negate x) == x
            x + 0 == x
            x * 1 == x
            x * 0 == 0
      abs (abs x) == abs x
   abs (negate x) == abs x
     x + negate x == 0
            x + y == y + x
            x * y == y * x
      abs (x * x) == x * x
     x * negate y == negate (x * y)

             x <= abs x
             0 <= abs x
             x <= x * x
             x <= x + 1
             0 <= x * x
      negate x <= abs x
negate (abs x) <= x
negate (abs x) <= 0
         abs x <= x * x
negate (abs x) <= negate x