arith-negate-abs.out

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

== Laws ==
  1. id x = x
  2. abs 0 = 0
  3. abs 1 = 1
  4. negate 0 = 0
  5. x * 0 = 0
  6. x * 1 = x
  7. 0 * x = 0
  8. 1 * x = x
  9. x + 0 = x
 10. 0 + x = x
 11. abs (abs x) = abs x
 12. abs (negate x) = abs x
 13. negate (negate x) = x
 14. x * y = y * x
 15. x + y = y + x
 16. negate x * y = x * negate y
 17. x + negate x = 0
 18. abs (x * x) = x * x
 19. negate (x * y) = x * negate y
 20. abs (1 + 1) = 1 + 1
 21. (x * y) * z = x * (y * z)
 22. (x + y) + z = x + (y + z)
 23. x * (y + 1) = x + (x * y)
 24. abs x * abs y = abs (x * y)
 25. abs x + abs x = abs (x + x)
 26. negate x + negate y = negate (x + y)
 27. abs (x + abs x) = x + abs x
 28. abs (1 + abs x) = 1 + abs x
 29. x * (y + y) = y * (x + x)