plus-abs.txt

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)

_ :: 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
       (0 <= abs x) == True
       (1 == x + x) == False
       (abs x <= x) == (0 <= x)
       (x == abs x) == (0 <= x)
           (x == 0) == (abs x <= 0)
           (0 <= x) == (y <= x + y)
       (x + y <= x) == (y <= 0)
            (x < y) == (x + 1 <= y)
       (0 <= x + x) == (0 <= x)
       (1 <= x + x) == (1 <= x)
       (x + x <= 0) == (x <= 0)
       (x + x <= 1) == (x <= 0)
       (x == x + y) == (abs y <= 0)
(False == (x <= y)) == (y + 1 <= x)
               id x == x
              x + 0 == x
        abs (abs x) == abs x
              x + y == y + x
        abs (x + x) == abs x + abs x
    abs (x + abs x) == x + abs x
    abs (1 + abs x) == 1 + abs x
        (x + y) + z == x + (y + z)

     x <= y ==> x <= abs y
 abs x <= y ==> x <= y
  abs x < y ==> x < y
     x <= 0 ==> x <= abs y
 abs x <= y ==> 0 <= y
  abs x < y ==> 1 <= y
     x == 1 ==> 1 == abs x
      x < 0 ==> 1 <= abs x
          x <=  abs x
          0 <=  abs x
          x <=  x + 1
          x <=  x + abs y
          x <=  abs (x + x)
          x <=  1 + abs x
          0 <=  x + abs x
      x + y <=  x + abs y
abs (x + 1) <=  1 + abs x

    x <= 0 ==>       x + abs x == 0
abs x <= y ==>     abs (x + y) == x + y
abs y <= x ==>     abs (x + y) == x + y
    y <= x ==> abs (x + abs y) == x + abs y