-
Notifications
You must be signed in to change notification settings - Fork 2
/
u-speculate.txt
45 lines (42 loc) · 1.09 KB
/
u-speculate.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
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)