arith-negate-abs.out

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

_ :: Int  (holes: 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)
  abs (x * abs y) == abs (x * y)
     negate x + y == negate (x + negate y)
    abs x * abs y == abs (x * y)
  abs (x + abs x) == x + abs x
    abs x + abs x == abs (x + x)
  abs (1 + abs x) == 1 + abs x
      (x + y) + z == x + (y + z)
      (x * y) * z == x * (y * z)
      (x + x) * y == x * (y + y)
      x * (y + 1) == x + 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
             x <= x + abs y
             x <= abs (x + x)
         abs x <= x * x
negate (x * x) <= x
negate (abs x) <= negate x
             x <= 1 + abs x
             0 <= x + abs x
negate (x * x) <= 0
  x + negate 1 <= x
         abs x <= abs (x + x)
negate (x * x) <= negate x
negate (x + 1) <= negate x
         x + y <= x + abs y
     x * abs x <= x * x
negate (x * x) <= negate (abs x)
     x * abs y <= abs (x * y)
  x + negate y <= x + abs y
     x + abs x <= abs (x + x)
negate (x * x) <= x * abs x
   abs (x + 1) <= 1 + abs x