u-speculate.out

Equations about _, 0, (+), abs:
abs 0  =  0
x + 0  =  x
0 + x  =  x
abs (abs x)  =  abs x
x + y  =  y + x
abs (x + y)  =  abs (y + x)
abs (x + abs x)  =  x + abs x
abs (abs x + x)  =  x + abs x
abs x + abs x  =  abs (x + x)
x + (y + z)  =  x + (z + y)
x + (y + z)  =  y + (x + z)
x + (y + z)  =  y + (z + x)
x + (y + z)  =  z + (x + y)
x + (y + z)  =  z + (y + x)
(x + y) + z  =  x + (y + z)
(x + y) + z  =  x + (z + y)
(x + y) + z  =  y + (x + z)
(x + y) + z  =  y + (z + x)
(x + y) + z  =  z + (y + x)
(x + y) + z  =  (x + z) + y
(x + y) + z  =  (y + x) + z
(x + y) + z  =  (y + z) + x
(x + y) + z  =  (z + x) + y
(x + y) + z  =  (z + y) + x

Equations about _, False, True, not:
not False  =  True
not True  =  False
not (not p)  =  p

Equations about _, _, [], (:), (++), sort:
sort []  =  []
xs ++ []  =  xs
[] ++ xs  =  xs
sort (sort xs)  =  sort xs
sort [x]  =  [x]
[x] ++ xs  =  x:xs
sort (xs ++ ys)  =  sort (ys ++ xs)
sort (x:sort xs)  =  sort (x:xs)
sort (xs ++ sort ys)  =  sort (xs ++ ys)
sort (sort xs ++ ys)  =  sort (xs ++ ys)
(x:xs) ++ ys  =  x:(xs ++ ys)
(xs ++ ys) ++ zs  =  xs ++ (ys ++ zs)