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
|
(FLOOR-INT-1
(3 3 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
(3 3 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
(3 3 (:TYPE-PRESCRIPTION FLOOR-TYPE-1 . 2))
(3 3 (:TYPE-PRESCRIPTION FLOOR-TYPE-1 . 1))
(2 2 (:TYPE-PRESCRIPTION |x < y => 0 < -x+y|))
(2 2 (:REWRITE DEFAULT-*-2))
(2 2 (:REWRITE DEFAULT-*-1))
)
(FLOOR-X-1
(73 10 (:REWRITE FLOOR-=-X/Y . 3))
(73 10 (:REWRITE FLOOR-=-X/Y . 2))
(70 66 (:REWRITE DEFAULT-*-2))
(70 66 (:REWRITE DEFAULT-*-1))
(63 63 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
(63 63 (:TYPE-PRESCRIPTION FLOOR-TYPE-1 . 2))
(63 63 (:TYPE-PRESCRIPTION FLOOR-TYPE-1 . 1))
(60 60 (:META CANCEL_PLUS-LESSP-CORRECT))
(52 52 (:REWRITE DEFAULT-<-2))
(52 52 (:REWRITE DEFAULT-<-1))
(49 17 (:REWRITE DEFAULT-+-2))
(37 10 (:REWRITE FLOOR-TYPE-4 . 3))
(37 10 (:REWRITE FLOOR-TYPE-4 . 2))
(37 10 (:REWRITE FLOOR-TYPE-3 . 3))
(37 10 (:REWRITE FLOOR-TYPE-3 . 2))
(30 15 (:REWRITE FLOOR-INT-1))
(24 4 (:LINEAR FLOOR-TYPE-2 . 2))
(24 4 (:LINEAR FLOOR-TYPE-2 . 1))
(24 4 (:LINEAR FLOOR-TYPE-1 . 2))
(24 4 (:LINEAR FLOOR-TYPE-1 . 1))
(17 17 (:REWRITE DEFAULT-+-1))
(16 4 (:REWRITE <-0-+-NEGATIVE-1))
(16 4 (:REWRITE <-+-NEGATIVE-0-1))
)
(MOD-1-PROPERTY
(675 12 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
(469 24 (:REWRITE NIQ-TYPE . 3))
(170 12 (:REWRITE DISTRIBUTIVITY))
(169 24 (:REWRITE NIQ-TYPE . 2))
(135 108 (:REWRITE DEFAULT-*-2))
(135 108 (:REWRITE DEFAULT-*-1))
(119 19 (:REWRITE FUNCTIONAL-COMMUTATIVITY-OF-MINUS-*-RIGHT))
(115 115 (:TYPE-PRESCRIPTION |x < y => 0 < -x+y|))
(102 73 (:REWRITE DEFAULT-<-1))
(90 63 (:REWRITE DEFAULT-+-2))
(73 73 (:REWRITE DEFAULT-<-2))
(65 63 (:REWRITE DEFAULT-+-1))
(60 60 (:REWRITE /R-WHEN-ABS-NUMERATOR=1))
(48 12 (:DEFINITION NFIX))
(47 37 (:REWRITE DEFAULT-UNARY-MINUS))
(34 34 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
(34 34 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
(34 34 (:TYPE-PRESCRIPTION INTEGERP-MOD))
(30 30 (:REWRITE DEFAULT-UNARY-/))
(16 4 (:LINEAR NIQ-TYPE))
(16 2 (:REWRITE FLOOR-=-X/Y . 2))
(12 12 (:REWRITE INVERSE-OF-*))
(12 12 (:DEFINITION IFIX))
(8 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
(8 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
(8 2 (:REWRITE MOD-X-Y-=-X+Y-FOR-RATIONALS . 3))
(8 2 (:REWRITE MOD-X-Y-=-X+Y-FOR-RATIONALS . 2))
(8 2 (:REWRITE FLOOR-TYPE-4 . 3))
(8 2 (:REWRITE FLOOR-TYPE-4 . 2))
(8 2 (:REWRITE FLOOR-TYPE-3 . 3))
(8 2 (:REWRITE FLOOR-TYPE-3 . 2))
(5 5 (:REWRITE NUMERATOR-WHEN-INTEGERP))
(5 5 (:REWRITE DEFAULT-NUMERATOR))
(4 4 (:REWRITE INTEGERP==>DENOMINATOR=1))
(4 4 (:REWRITE DEFAULT-DENOMINATOR))
(2 2 (:REWRITE MOD-=-0 . 2))
(2 2 (:REWRITE FOLD-CONSTS-IN-+))
(2 2 (:REWRITE FLOOR-INT-1))
(2 2 (:REWRITE FLOOR-=-X/Y . 3))
)
|
