plus-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)

_ :: Bool
_ :: Int
(+) :: Int -> Int -> Int
id :: Int -> Int
abs :: Int -> Int
0 :: Int
1 :: Int
(<=) :: Int -> Int -> Bool
(<) :: Int -> Int -> Bool
True :: Bool
False :: Bool
(==) :: Bool -> Bool -> Bool
(==) :: Int -> Int -> Bool

(x <= abs x) == True
 (abs x < x) == False
(0 <= abs x) == True
 (abs x < 0) == False
(abs x <= x) == (0 <= x)
 (x < abs x) == (x < 0)
(x == abs x) == (0 <= x)
    (x == 0) == (abs x <= 0)
        id x == x
       x + 0 == x
 abs (abs x) == abs x
       x + y == y + x

x <= abs x
0 <= abs x
x <= x + 1

x <= 0 ==> x + abs x == 0