-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathratio.txt
114 lines (110 loc) · 4.47 KB
/
ratio.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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
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)
_ :: Integer
_ :: Ratio Integer
id :: Ratio Integer -> Ratio Integer
abs :: Ratio Integer -> Ratio Integer
negate :: Ratio Integer -> Ratio Integer
(+) :: Ratio Integer -> Ratio Integer -> Ratio Integer
(*) :: Ratio Integer -> Ratio Integer -> Ratio Integer
(/) :: Ratio Integer -> Ratio Integer -> Ratio Integer
(%) :: Integer -> Integer -> Ratio Integer
recip :: Ratio Integer -> Ratio Integer
numerator :: Ratio Integer -> Integer
denominator :: Ratio Integer -> Integer
0 % 1 :: Ratio Integer
1 % 1 :: Ratio Integer
0 :: Integer
1 :: Integer
denominator (abs q) == denominator q
denominator (negate q) == denominator q
numerator (x % 1) == x
denominator (x % 1) == 1
denominator (q + 1 % 1) == denominator q
numerator (1 % denominator q) == 1
denominator (1 % denominator q) == denominator q
denominator (q * abs r) == denominator (q * r)
id q == q
negate (negate q) == q
q + 0 % 1 == q
q * (1 % 1) == q
q / (1 % 1) == q
q * (0 % 1) == 0 % 1
abs (abs q) == abs q
abs (negate q) == abs q
q + negate q == 0 % 1
0 % denominator q == 0 % 1
q + r == r + q
q * r == r * q
numerator q % denominator q == q
q / negate (1 % 1) == negate q
denominator q % denominator q == 1 % 1
abs (q * q) == q * q
q * negate r == negate (q * r)
abs (q * abs r) == abs (q * r)
negate q + r == negate (q + negate r)
abs q * abs r == abs (q * r)
abs (q + abs q) == q + abs q
abs q + abs q == abs (q + q)
abs (1 % 1 + abs q) == 1 % 1 + abs q
abs (1 % denominator q) == 1 % denominator q
abs (denominator q % 1) == denominator q % 1
recip (1 % denominator q) == denominator q % 1
recip (denominator q % 1) == 1 % denominator q
x % numerator (negate (1 % 1)) == negate (x % 1)
(q + r) + s == q + (r + s)
(q * r) * s == q * (r * s)
(q + q) * r == q * (r + r)
q * (r + 1 % 1) == q + q * r
numerator (abs q) % 1 == abs (numerator q % 1)
numerator (negate q) % 1 == negate (numerator q % 1)
0 <= denominator q
1 <= denominator q
0 <= numerator (abs q)
numerator q <= numerator (abs q)
0 <= numerator (q * q)
numerator (negate (abs q)) <= 0
numerator q <= numerator (q * q)
denominator q <= denominator (q * q)
denominator (q + q) <= denominator q
numerator q <= numerator (q + 1 % 1)
numerator (negate q) <= numerator (abs q)
numerator (negate (abs q)) <= numerator q
numerator (abs q) <= numerator (q * q)
numerator (negate (abs q)) <= numerator (negate q)
q <= abs q
0 % 1 <= abs q
q <= q + 1 % 1
0 % 1 <= q * q
negate q <= abs q
negate (abs q) <= q
negate (abs q) <= 0 % 1
q <= q + abs r
q <= abs (q + q)
negate (abs q) <= negate q
q <= 1 % 1 + abs q
0 % 1 <= q + abs q
negate (q * q) <= 0 % 1
q + negate (1 % 1) <= q
0 % 1 <= 1 % denominator q
0 % 1 <= denominator q % 1
1 % 1 <= denominator q % 1
1 % denominator q <= 1 % 1
abs q <= abs (q + q)
negate (q + 1 % 1) <= negate q
q + r <= q + abs r
q * abs q <= q * q
negate (q + 1 % 1) <= q * q
negate (q * q) <= q + 1 % 1
q + negate (1 % 1) <= q * q
q * abs r <= abs (q * r)
q + negate r <= q + abs r
x % denominator q <= abs (x % 1)
q + abs q <= abs (q + q)
negate (q * q) <= q * abs q
negate (q * q) <= 1 % 1 + negate q
abs (q + 1 % 1) <= 1 % 1 + abs q