(MOD-EXPT-MOD
 (3660 70 (:LINEAR MOD-TYPE . 2))
 (3174 58 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (2944 58 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (2522 42 (:REWRITE MOD-WHEN-MULTIPLE))
 (2055 1325 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (2055 1325 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (2055 1325 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (1789 1113 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (1442 42 (:REWRITE MOD-WHEN-<))
 (1325 1325 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (1325 1325 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (1136 44 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (1133 44 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (1130 44 (:REWRITE MOD-WHEN-<-OF-0))
 (1061 1061 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (1061 1061 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (747 247 (:REWRITE DEFAULT-<-2))
 (718 247 (:REWRITE DEFAULT-<-1))
 (687 184 (:REWRITE DEFAULT-*-2))
 (597 184 (:REWRITE DEFAULT-*-1))
 (530 30 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (521 42 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (479 30 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (462 30 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (244 70 (:LINEAR MOD-TYPE . 3))
 (244 70 (:LINEAR MOD-TYPE . 1))
 (210 30 (:REWRITE DEFAULT-UNARY-/))
 (179 39 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (168 28 (:REWRITE MOD-OF-2-WHEN-EVEN-CHEAP))
 (120 30 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (106 106 (:LINEAR EXPT-BOUND-LINEAR-WEAK))
 (88 88 (:REWRITE INTEGERP-OF-*))
 (85 34 (:REWRITE DEFAULT-UNARY-MINUS))
 (78 39 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (58 58 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 (53 53 (:LINEAR EXPT-BOUND-LINEAR-2))
 (44 44 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (36 36 (:REWRITE RATIONALP-OF-MOD))
 (36 36 (:REWRITE RATIONALP-MOD))
 (30 30 (:REWRITE MOD-TYPE))
 (10 10 (:REWRITE MOD-OF-MOD-WHEN-MULTIPLE-SAFE))
 (6 6 (:TYPE-PRESCRIPTION NATP-OF-EXPT))
 (6 6 (:REWRITE INTEGERP-MOD))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(INTEGERP-OF-*-OF-/-AND-MOD
 (1254 1245 (:REWRITE DEFAULT-*-2))
 (1245 1245 (:REWRITE DEFAULT-*-1))
 (606 597 (:REWRITE DEFAULT-<-2))
 (597 597 (:REWRITE DEFAULT-<-1))
 (593 593 (:REWRITE DEFAULT-+-2))
 (593 593 (:REWRITE DEFAULT-+-1))
 (147 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (145 145 (:REWRITE DEFAULT-UNARY-MINUS))
 (135 111 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (135 111 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (111 111 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (111 111 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (111 111 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (111 111 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (111 111 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (111 111 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (93 3 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (92 92 (:REWRITE DEFAULT-UNARY-/))
 (86 6 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (85 25 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (85 25 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (46 6 (:REWRITE MOD-WHEN-MULTIPLE))
 (42 14 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (32 32 (:REWRITE *-OF-*-COMBINE-CONSTANTS))
 (28 28 (:REWRITE INTEGERP-OF-*))
 (21 7 (:LINEAR MOD-TYPE . 4))
 (21 7 (:LINEAR MOD-TYPE . 3))
 (21 7 (:LINEAR MOD-TYPE . 2))
 (21 7 (:LINEAR MOD-TYPE . 1))
 (21 7 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (21 7 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (16 16 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (16 6 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (16 6 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (16 6 (:REWRITE MOD-WHEN-<-OF-0))
 (16 6 (:REWRITE MOD-WHEN-<))
 (15 3 (:REWRITE INTEGERP-OF-*-OF-/-AND-MOD-SAME))
 (9 3 (:DEFINITION NATP))
 (8 8 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (7 7 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (6 6 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (6 6 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (6 6 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (6 6 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (6 6 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (3 3 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (3 3 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (3 3 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (3 3 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (3 3 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (3 3 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (3 3 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (3 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 )
(MOD-NON-NEGATIVE-CONSTANT
 (1 1 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (1 1 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (1 1 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (1 1 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (1 1 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 )
(MOD-NON-NEGATIVE-CONSTANT-GEN
 (11 11 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (11 11 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (11 11 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (11 11 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (11 11 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 )
(MOD-NON-NEGATIVE-CONSTANT-POS-REWRITE
 (55 55 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (55 55 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (55 55 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (55 55 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (18 2 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (12 12 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (12 12 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (10 2 (:REWRITE MOD-WHEN-MULTIPLE))
 (9 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE DEFAULT-<-1))
 (6 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (6 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (5 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (4 4 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (4 2 (:REWRITE MOD-WHEN-<-OF-0))
 (4 2 (:REWRITE MOD-WHEN-<))
 (3 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (3 3 (:REWRITE INTEGERP-OF-*))
 (3 3 (:REWRITE DEFAULT-UNARY-/))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (2 2 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (2 2 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(MOD-OF-MOD-OF-EXPT-OF-2-AND-2
 (17684 86 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (15757 172 (:REWRITE MOD-WHEN-<))
 (14483 227 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (13135 227 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (12720 69 (:LINEAR MOD-TYPE . 2))
 (9022 9022 (:TYPE-PRESCRIPTION NATP-OF-EXPT))
 (7476 172 (:REWRITE MOD-WHEN-MULTIPLE))
 (7066 338 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (6158 338 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (5968 338 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (4902 2080 (:REWRITE DEFAULT-<-2))
 (4314 406 (:REWRITE DEFAULT-UNARY-/))
 (3420 2080 (:REWRITE DEFAULT-<-1))
 (3098 578 (:REWRITE DEFAULT-*-2))
 (1952 338 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (1949 13 (:REWRITE MOD-TYPE))
 (1859 1043 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (1671 855 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (1288 380 (:REWRITE DEFAULT-UNARY-MINUS))
 (1208 1208 (:LINEAR EXPT-BOUND-LINEAR-WEAK))
 (1208 1208 (:LINEAR EXPT-BOUND-LINEAR))
 (1144 578 (:REWRITE DEFAULT-*-1))
 (1100 13 (:REWRITE REWRITE-MOD-MOD))
 (1044 172 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (1043 1043 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (1043 1043 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (964 86 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (867 227 (:REWRITE MOD-WHEN-<-OF-0))
 (828 172 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (824 86 (:REWRITE COMMUTATIVITY-OF-*))
 (604 604 (:LINEAR EXPT-BOUND-LINEAR-2))
 (448 64 (:REWRITE INTEGERP-OF-EXPT-WHEN-NATP))
 (388 172 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (388 172 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (371 69 (:LINEAR MOD-TYPE . 3))
 (371 69 (:LINEAR MOD-TYPE . 1))
 (250 34 (:REWRITE MOD-OF-2-WHEN-EVEN-CHEAP))
 (227 227 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (86 86 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 (64 64 (:REWRITE INTEGERP-OF-EXPT2))
 (57 3 (:REWRITE INTEGERP-OF-MOD))
 (57 3 (:REWRITE INTEGERP-MOD))
 (27 9 (:DEFINITION POSP))
 (20 1 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (16 16 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (16 16 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (16 16 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (16 4 (:REWRITE DEFAULT-+-2))
 (13 13 (:REWRITE MOD-OF-MOD-WHEN-MULTIPLE-SAFE))
 (13 13 (:REWRITE MOD-NON-NEGATIVE-CONSTANT-POS-REWRITE))
 (13 13 (:REWRITE INTEGERP-OF-*-OF-1/2-AND-EXPT-2))
 (13 13 (:REWRITE <-OF-0-AND-EXPT))
 (9 9 (:TYPE-PRESCRIPTION POSP))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE ZP-OPEN))
 )
(MOD-OF-MOD-2-EXPT-2
 (1923 44 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (1247 9 (:REWRITE MOD-NON-NEGATIVE-CONSTANT-POS-REWRITE))
 (809 36 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (748 78 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (671 36 (:REWRITE MOD-WHEN-MULTIPLE))
 (598 9 (:REWRITE REWRITE-MOD-MOD))
 (536 10 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (518 10 (:LINEAR MOD-TYPE . 2))
 (484 424 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (484 424 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (484 424 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (424 424 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (424 424 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (349 78 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (274 78 (:REWRITE COMMUTATIVITY-OF-*))
 (258 208 (:REWRITE DEFAULT-<-1))
 (235 208 (:REWRITE DEFAULT-<-2))
 (232 165 (:REWRITE DEFAULT-*-2))
 (205 165 (:REWRITE DEFAULT-*-1))
 (202 9 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (195 87 (:REWRITE INTEGERP-OF-*))
 (151 36 (:REWRITE MOD-WHEN-<))
 (109 36 (:REWRITE MOD-WHEN-<-OF-0))
 (91 13 (:REWRITE DEFAULT-UNARY-/))
 (90 78 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 (46 36 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (44 10 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (43 36 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (43 36 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (39 36 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (36 36 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (36 12 (:REWRITE INTEGERP-OF-/-OF-EXPT-2))
 (36 9 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (36 9 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (36 9 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (35 35 (:REWRITE MOD-OF-2-WHEN-EVEN-CHEAP))
 (20 20 (:LINEAR EXPT-BOUND-LINEAR-WEAK))
 (18 18 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (16 10 (:LINEAR MOD-TYPE . 3))
 (16 10 (:LINEAR MOD-TYPE . 1))
 (14 14 (:LINEAR EXPT-BOUND-LINEAR-2))
 (6 6 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (6 6 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (6 6 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (4 2 (:REWRITE INTEGERP-OF-MOD))
 (2 2 (:TYPE-PRESCRIPTION NATP-OF-EXPT))
 (2 2 (:REWRITE INTEGERP-MOD))
 (2 2 (:DEFINITION FIX))
 (1 1 (:REWRITE MOD-OF-MOD-WHEN-MULTIPLE-SAFE))
 )
(<-OF-MOD
 (34 2 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (33 33 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (33 33 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (33 33 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (33 33 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (33 33 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (18 2 (:REWRITE MOD-WHEN-MULTIPLE))
 (17 17 (:REWRITE DEFAULT-<-2))
 (17 17 (:REWRITE DEFAULT-<-1))
 (17 1 (:LINEAR MOD-TYPE . 2))
 (14 5 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (14 5 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (11 5 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (6 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (6 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (6 2 (:REWRITE MOD-WHEN-<-OF-0))
 (6 2 (:REWRITE MOD-WHEN-<))
 (5 5 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (5 5 (:REWRITE INTEGERP-OF-*))
 (5 5 (:REWRITE DEFAULT-UNARY-/))
 (5 5 (:REWRITE DEFAULT-*-2))
 (5 5 (:REWRITE DEFAULT-*-1))
 (2 2 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (2 2 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (2 2 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (2 2 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (2 2 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (1 1 (:LINEAR MOD-TYPE . 3))
 (1 1 (:LINEAR MOD-TYPE . 1))
 )
(MOD-OF-*-OF-SAME-2
 (54 6 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (34 34 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (34 34 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (34 34 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (34 34 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (34 34 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (33 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (33 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (33 2 (:REWRITE MOD-WHEN-<-OF-0))
 (30 21 (:REWRITE DEFAULT-<-2))
 (28 28 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (27 21 (:REWRITE DEFAULT-<-1))
 (18 18 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (18 18 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (18 6 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (13 8 (:REWRITE DEFAULT-*-1))
 (12 12 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (12 12 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (12 12 (:LINEAR <-OF-*-AND-*-LINEAR))
 (11 8 (:REWRITE DEFAULT-*-2))
 (10 3 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (9 3 (:LINEAR MOD-TYPE . 4))
 (9 3 (:LINEAR MOD-TYPE . 3))
 (9 3 (:LINEAR MOD-TYPE . 2))
 (9 3 (:LINEAR MOD-TYPE . 1))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (5 3 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (5 3 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (4 4 (:REWRITE RATIONALP-*))
 (4 4 (:REWRITE INTEGERP-OF-*))
 (4 4 (:REWRITE <-OF-CONSTANT-AND-*-OF-CONSTANT))
 (4 4 (:REWRITE *-OF-*-COMBINE-CONSTANTS))
 (4 1 (:REWRITE DEFAULT-UNARY-/))
 (3 2 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (2 2 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (2 2 (:REWRITE <-OF-*-AND-0))
 (1 1 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(MOD-OF-MOD-WHEN-MULT-CHEAP
 (13 13 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (13 13 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (13 13 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (13 13 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (13 13 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (13 13 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (13 13 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (13 13 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (13 13 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 )
(+-OF-MOD-AND-*-OF-FLOOR-SAME
 (468 4 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (140 2 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (136 2 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (117 1 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (108 90 (:REWRITE DEFAULT-<-2))
 (90 90 (:REWRITE DEFAULT-<-1))
 (77 5 (:REWRITE FLOOR-=-X/Y . 3))
 (48 48 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (48 48 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (48 48 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (48 48 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (48 48 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (48 48 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (48 48 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (48 48 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (45 5 (:REWRITE FLOOR-=-X/Y . 2))
 (31 31 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (31 31 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (31 31 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (31 31 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (31 31 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (31 31 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (31 31 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (31 31 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (27 12 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (27 12 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (26 17 (:REWRITE DEFAULT-*-2))
 (22 12 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (18 2 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (18 2 (:REWRITE <-OF-/-AND-CONSTANT-1))
 (17 17 (:REWRITE DEFAULT-*-1))
 (16 16 (:REWRITE DEFAULT-UNARY-/))
 (15 5 (:REWRITE FLOOR-WHEN-<))
 (15 5 (:REWRITE FLOOR-TYPE-4 . 3))
 (15 5 (:REWRITE FLOOR-TYPE-4 . 2))
 (15 5 (:REWRITE FLOOR-TYPE-3 . 3))
 (15 5 (:REWRITE FLOOR-TYPE-3 . 2))
 (12 12 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (12 12 (:REWRITE INTEGERP-OF-*))
 (12 4 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (10 10 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 2 (:REWRITE MOD-WHEN-MULTIPLE))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (8 8 (:LINEAR <-OF-*-AND-*-LINEAR))
 (6 2 (:REWRITE <-OF-/-AND-CONSTANT))
 (6 2 (:LINEAR MY-FLOOR-LOWER-BOUND-ALT-LINEAR))
 (6 2 (:LINEAR MOD-TYPE . 4))
 (6 2 (:LINEAR MOD-TYPE . 3))
 (6 2 (:LINEAR MOD-TYPE . 2))
 (6 2 (:LINEAR MOD-TYPE . 1))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (6 2 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (6 2 (:LINEAR FLOOR-TYPE-2 . 2))
 (6 2 (:LINEAR FLOOR-TYPE-2 . 1))
 (6 2 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (6 2 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-NEGATIVE-AND-POSITIVE-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NONNEGATIVE-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NEGATIVE-LINEAR))
 (6 2 (:LINEAR *-OF-FLOOR-UPPER-BOUND-LINEAR))
 (5 5 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (5 5 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (5 5 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (5 5 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (5 5 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (4 4 (:LINEAR <=-OF-/-LINEAR))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (4 2 (:REWRITE MOD-WHEN-<-OF-0))
 (4 2 (:REWRITE MOD-WHEN-<))
 (2 2 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (2 2 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (2 2 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (2 2 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (2 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (2 2 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (2 2 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 )
(MOD-OF-+-WHEN-MULT-ARG1
 (99 99 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (99 99 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (99 99 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (99 99 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (99 99 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (99 99 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (99 99 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (99 99 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (50 5 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (46 46 (:REWRITE DEFAULT-<-2))
 (46 46 (:REWRITE DEFAULT-<-1))
 (39 4 (:REWRITE MOD-WHEN-MULTIPLE))
 (26 2 (:REWRITE DISTRIBUTIVITY))
 (23 23 (:REWRITE DEFAULT-*-2))
 (23 23 (:REWRITE DEFAULT-*-1))
 (23 8 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (23 8 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (18 8 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (16 7 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (14 12 (:REWRITE DEFAULT-UNARY-/))
 (14 1 (:REWRITE MOD-OF-+-SUBST-CONSTANT))
 (13 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (13 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (13 5 (:REWRITE MOD-WHEN-<-OF-0))
 (12 12 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (12 4 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (10 10 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 4 (:REWRITE MOD-WHEN-<))
 (8 8 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (8 8 (:REWRITE INTEGERP-OF-*))
 (7 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 2 (:LINEAR MOD-TYPE . 4))
 (6 2 (:LINEAR MOD-TYPE . 3))
 (6 2 (:LINEAR MOD-TYPE . 2))
 (6 2 (:LINEAR MOD-TYPE . 1))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (5 5 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (4 4 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (1 1 (:REWRITE EQUAL-OF-MOD-OF-+-WHEN-CONSTANTS))
 )
(MOD-OF-+-WHEN-MULT-ARG1-ALT
 (82 82 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (82 82 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (82 82 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (82 82 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (53 4 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (38 38 (:REWRITE DEFAULT-<-2))
 (38 38 (:REWRITE DEFAULT-<-1))
 (36 4 (:REWRITE MOD-WHEN-MULTIPLE))
 (35 2 (:REWRITE CANCEL-MOD-+-BASIC))
 (22 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (22 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (18 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (16 16 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (15 6 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (15 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (15 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (12 10 (:REWRITE DEFAULT-UNARY-/))
 (12 4 (:REWRITE MOD-WHEN-<-OF-0))
 (12 4 (:REWRITE MOD-WHEN-<))
 (10 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (10 10 (:REWRITE INTEGERP-OF-*))
 (10 10 (:REWRITE DEFAULT-*-2))
 (10 10 (:REWRITE DEFAULT-*-1))
 (8 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (4 4 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (4 4 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 1 (:LINEAR MOD-TYPE . 4))
 (3 1 (:LINEAR MOD-TYPE . 3))
 (3 1 (:LINEAR MOD-TYPE . 2))
 (3 1 (:LINEAR MOD-TYPE . 1))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (1 1 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 )
(MOD-OF-+-WHEN-MULT-ARG1-ALT-CHEAP
 (82 82 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (82 82 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (82 82 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (82 82 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (53 4 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (38 38 (:REWRITE DEFAULT-<-2))
 (38 38 (:REWRITE DEFAULT-<-1))
 (36 4 (:REWRITE MOD-WHEN-MULTIPLE))
 (35 2 (:REWRITE CANCEL-MOD-+-BASIC))
 (22 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (22 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (18 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (16 16 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (15 6 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (15 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (15 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (12 10 (:REWRITE DEFAULT-UNARY-/))
 (12 4 (:REWRITE MOD-WHEN-<-OF-0))
 (12 4 (:REWRITE MOD-WHEN-<))
 (10 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (10 10 (:REWRITE INTEGERP-OF-*))
 (10 10 (:REWRITE DEFAULT-*-2))
 (10 10 (:REWRITE DEFAULT-*-1))
 (8 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (4 4 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (4 4 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 1 (:LINEAR MOD-TYPE . 4))
 (3 1 (:LINEAR MOD-TYPE . 3))
 (3 1 (:LINEAR MOD-TYPE . 2))
 (3 1 (:LINEAR MOD-TYPE . 1))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (1 1 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 )
(FLOOR-WHEN-MOD-0-CHEAP
 (1389 1344 (:REWRITE DEFAULT-*-2))
 (1371 1344 (:REWRITE DEFAULT-*-1))
 (587 560 (:REWRITE DEFAULT-+-2))
 (560 560 (:REWRITE DEFAULT-+-1))
 (539 521 (:REWRITE DEFAULT-<-2))
 (521 521 (:REWRITE DEFAULT-<-1))
 (453 5 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (384 4 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (159 132 (:REWRITE DEFAULT-UNARY-MINUS))
 (134 134 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (134 134 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (134 134 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (134 134 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (134 134 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (134 134 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (134 134 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (134 134 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (98 2 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (94 2 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (81 81 (:REWRITE DEFAULT-UNARY-/))
 (47 47 (:REWRITE *-OF-*-COMBINE-CONSTANTS))
 (36 9 (:REWRITE FLOOR-=-X/Y . 2))
 (27 27 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (27 27 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (27 27 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (27 27 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (27 27 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (27 27 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (27 27 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (27 27 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (23 9 (:REWRITE FLOOR-WHEN-<))
 (23 9 (:REWRITE FLOOR-TYPE-4 . 3))
 (23 9 (:REWRITE FLOOR-TYPE-4 . 2))
 (23 9 (:REWRITE FLOOR-TYPE-3 . 3))
 (23 9 (:REWRITE FLOOR-TYPE-3 . 2))
 (20 20 (:REWRITE EQUAL-OF-*-AND-CONSTANT))
 (18 2 (:REWRITE <-OF-/-AND-CONSTANT-1))
 (12 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (12 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (10 4 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (10 4 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (10 4 (:REWRITE MOD-WHEN-<-OF-0))
 (10 4 (:REWRITE MOD-WHEN-<))
 (9 9 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (9 9 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (9 9 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (9 9 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (9 9 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (9 9 (:REWRITE FLOOR-=-X/Y . 3))
 (9 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (8 8 (:LINEAR <-OF-*-AND-*-LINEAR))
 (6 2 (:REWRITE <-OF-/-AND-CONSTANT))
 (6 2 (:LINEAR MY-FLOOR-LOWER-BOUND-ALT-LINEAR))
 (6 2 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (6 2 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (6 2 (:LINEAR FLOOR-TYPE-2 . 2))
 (6 2 (:LINEAR FLOOR-TYPE-2 . 1))
 (6 2 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (6 2 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-NEGATIVE-AND-POSITIVE-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NONNEGATIVE-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NEGATIVE-LINEAR))
 (6 2 (:LINEAR *-OF-FLOOR-UPPER-BOUND-LINEAR))
 (5 5 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (4 4 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (4 4 (:REWRITE MOD-WHEN-MULTIPLE))
 (4 4 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (4 4 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (4 4 (:LINEAR <=-OF-/-LINEAR))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (3 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (3 3 (:REWRITE INTEGERP-OF-*))
 (3 1 (:LINEAR MOD-TYPE . 4))
 (3 1 (:LINEAR MOD-TYPE . 3))
 (3 1 (:LINEAR MOD-TYPE . 2))
 (3 1 (:LINEAR MOD-TYPE . 1))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (2 2 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (2 2 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (1 1 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 )
(EQUAL-OF-0-AND-MOD-OF--
 (1506 15 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (762 6 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (286 259 (:REWRITE DEFAULT-<-2))
 (275 275 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (275 275 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (275 275 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (275 275 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (275 275 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (275 275 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (275 275 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (275 275 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (259 259 (:REWRITE DEFAULT-<-1))
 (241 106 (:REWRITE DEFAULT-*-2))
 (240 3 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (237 21 (:REWRITE FLOOR-=-X/Y . 3))
 (234 3 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (210 21 (:REWRITE FLOOR-WHEN-MOD-0-CHEAP))
 (203 50 (:REWRITE DEFAULT-UNARY-MINUS))
 (187 106 (:REWRITE DEFAULT-*-1))
 (184 31 (:REWRITE DEFAULT-+-2))
 (141 21 (:REWRITE FLOOR-=-X/Y . 2))
 (100 100 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (100 100 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (100 100 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (100 100 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (100 100 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (100 100 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (100 100 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (100 100 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (98 13 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (88 46 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (88 46 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (82 13 (:REWRITE MOD-WHEN-MULTIPLE))
 (74 46 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (56 56 (:REWRITE DEFAULT-UNARY-/))
 (51 21 (:REWRITE FLOOR-WHEN-<))
 (51 21 (:REWRITE FLOOR-TYPE-4 . 3))
 (51 21 (:REWRITE FLOOR-TYPE-4 . 2))
 (51 21 (:REWRITE FLOOR-TYPE-3 . 3))
 (51 21 (:REWRITE FLOOR-TYPE-3 . 2))
 (46 46 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (46 46 (:REWRITE INTEGERP-OF-*))
 (36 12 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (31 31 (:REWRITE DEFAULT-+-1))
 (31 13 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (31 13 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (31 13 (:REWRITE MOD-WHEN-<-OF-0))
 (28 12 (:REWRITE MOD-WHEN-<))
 (27 3 (:REWRITE <-OF-/-AND-CONSTANT-1))
 (21 21 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (21 21 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (21 21 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (21 21 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (21 21 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (18 6 (:LINEAR MOD-TYPE . 4))
 (18 6 (:LINEAR MOD-TYPE . 3))
 (18 6 (:LINEAR MOD-TYPE . 2))
 (18 6 (:LINEAR MOD-TYPE . 1))
 (18 6 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (18 6 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (13 13 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (12 12 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (12 12 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (12 12 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (12 12 (:LINEAR <-OF-*-AND-*-LINEAR))
 (9 9 (:REWRITE EQUAL-OF-*-AND-CONSTANT))
 (9 3 (:REWRITE <-OF-/-AND-CONSTANT))
 (9 3 (:LINEAR MY-FLOOR-LOWER-BOUND-ALT-LINEAR))
 (9 3 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (9 3 (:LINEAR FLOOR-TYPE-2 . 2))
 (9 3 (:LINEAR FLOOR-TYPE-2 . 1))
 (9 3 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (9 3 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (9 3 (:LINEAR <=-OF-*-OF-/-WHEN-NEGATIVE-AND-POSITIVE-LINEAR))
 (9 3 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NONNEGATIVE-LINEAR))
 (9 3 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NEGATIVE-LINEAR))
 (9 3 (:LINEAR *-OF-FLOOR-UPPER-BOUND-LINEAR))
 (8 2 (:REWRITE *-OF---ARG1))
 (6 6 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (6 6 (:LINEAR <=-OF-/-LINEAR))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (4 4 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (3 3 (:REWRITE FOLD-CONSTS-IN-+))
 (3 3 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (3 3 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (2 2 (:REWRITE *-OF-*-COMBINE-CONSTANTS))
 (2 2 (:DEFINITION IFF))
 )
(MOD-OF-+-SUBST-CONSTANT-ARG1
 (885 18 (:REWRITE MOD-OF-+-SUBST-CONSTANT))
 (692 124 (:REWRITE COMMUTATIVITY-OF-*))
 (681 44 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (665 44 (:REWRITE MOD-WHEN-MULTIPLE))
 (648 36 (:REWRITE CANCEL-MOD-+-BASIC))
 (630 6 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (602 86 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (348 324 (:REWRITE DEFAULT-*-2))
 (336 324 (:REWRITE DEFAULT-*-1))
 (308 38 (:REWRITE DISTRIBUTIVITY))
 (286 286 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (286 286 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (286 286 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (237 27 (:REWRITE MOD-OF-+-WHEN-MULT-ARG1-ALT-CHEAP))
 (231 219 (:REWRITE DEFAULT-<-1))
 (219 219 (:REWRITE DEFAULT-<-2))
 (196 6 (:LINEAR MOD-TYPE . 2))
 (174 86 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (133 133 (:REWRITE DEFAULT-UNARY-/))
 (128 44 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (128 44 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (128 44 (:REWRITE MOD-WHEN-<-OF-0))
 (128 44 (:REWRITE MOD-WHEN-<))
 (86 86 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 (86 86 (:REWRITE INTEGERP-OF-*))
 (85 67 (:REWRITE DEFAULT-+-2))
 (85 67 (:REWRITE DEFAULT-+-1))
 (44 44 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (44 44 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (44 44 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (44 44 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (44 44 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (34 34 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (34 34 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (28 28 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (22 22 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (6 6 (:LINEAR MOD-TYPE . 3))
 (6 6 (:LINEAR MOD-TYPE . 1))
 )
(MOD-OF-+-SUBST-CONSTANT-ARG2
 (1093 22 (:REWRITE MOD-OF-+-SUBST-CONSTANT))
 (839 149 (:REWRITE COMMUTATIVITY-OF-*))
 (817 52 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (801 52 (:REWRITE MOD-WHEN-MULTIPLE))
 (800 44 (:REWRITE CANCEL-MOD-+-BASIC))
 (714 102 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (633 7 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (416 392 (:REWRITE DEFAULT-*-2))
 (404 392 (:REWRITE DEFAULT-*-1))
 (380 47 (:REWRITE DISTRIBUTIVITY))
 (301 301 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (301 301 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (301 301 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (272 260 (:REWRITE DEFAULT-<-1))
 (260 260 (:REWRITE DEFAULT-<-2))
 (217 31 (:REWRITE MOD-OF-+-WHEN-MULT-ARG1-ALT-CHEAP))
 (206 102 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (195 7 (:LINEAR MOD-TYPE . 2))
 (158 158 (:REWRITE DEFAULT-UNARY-/))
 (152 52 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (152 52 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (152 52 (:REWRITE MOD-WHEN-<-OF-0))
 (152 52 (:REWRITE MOD-WHEN-<))
 (102 102 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 (102 102 (:REWRITE INTEGERP-OF-*))
 (102 84 (:REWRITE DEFAULT-+-2))
 (84 84 (:REWRITE DEFAULT-+-1))
 (52 52 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (52 52 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (52 52 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (52 52 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (52 52 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (34 34 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (34 34 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (31 31 (:REWRITE MOD-OF-+-SUBST-CONSTANT-ARG1))
 (28 28 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (22 22 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (7 7 (:LINEAR MOD-TYPE . 3))
 (7 7 (:LINEAR MOD-TYPE . 1))
 )
(SAME-REMAINDER-WHEN-CLOSE-HELPER
 (1359 22 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (1255 12 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (1025 108 (:REWRITE DEFAULT-+-2))
 (958 12 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (759 58 (:REWRITE FLOOR-=-X/Y . 3))
 (622 321 (:REWRITE DEFAULT-*-2))
 (577 24 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (573 321 (:REWRITE DEFAULT-*-1))
 (546 448 (:REWRITE DEFAULT-<-2))
 (544 8 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (528 8 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (527 58 (:REWRITE FLOOR-=-X/Y . 2))
 (490 448 (:REWRITE DEFAULT-<-1))
 (486 4 (:REWRITE MOD-OF-+-SUBST-CONSTANT))
 (472 472 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (472 472 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (472 472 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (472 472 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (472 472 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (464 58 (:REWRITE FLOOR-WHEN-MOD-0-CHEAP))
 (460 460 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (460 460 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (460 460 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (460 460 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (460 460 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (460 460 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (430 28 (:LINEAR <=-OF-/-LINEAR))
 (381 108 (:REWRITE DEFAULT-UNARY-MINUS))
 (379 211 (:REWRITE DEFAULT-UNARY-/))
 (312 35 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (280 154 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (280 154 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (248 35 (:REWRITE MOD-WHEN-MULTIPLE))
 (246 154 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (190 5 (:REWRITE EQUAL-OF-0-AND-+-OF--))
 (171 108 (:REWRITE DEFAULT-+-1))
 (154 154 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (154 154 (:REWRITE INTEGERP-OF-*))
 (146 58 (:REWRITE FLOOR-TYPE-4 . 3))
 (146 58 (:REWRITE FLOOR-TYPE-4 . 2))
 (104 8 (:REWRITE CANCEL-MOD-+-BASIC))
 (80 40 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (75 35 (:REWRITE MOD-WHEN-<-OF-0))
 (75 35 (:REWRITE MOD-WHEN-<))
 (72 8 (:REWRITE CANCEL-FLOOR-+-BASIC))
 (70 70 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (58 58 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (58 58 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (58 58 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (58 58 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (57 3 (:LINEAR MOD-TYPE . 2))
 (46 46 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (40 26 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (36 4 (:REWRITE FLOOR-OF-+-WHEN-MULT-ARG2))
 (36 4 (:REWRITE FLOOR-OF-+-WHEN-MULT-ARG1))
 (36 2 (:REWRITE FLOOR-TYPE-2))
 (35 35 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (35 35 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (35 35 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (35 35 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (35 35 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (32 4 (:REWRITE MOD-OF-+-WHEN-MULT-ARG1-ALT-CHEAP))
 (24 24 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (24 24 (:LINEAR <-OF-*-AND-*-LINEAR))
 (24 8 (:REWRITE <-OF-/-AND-CONSTANT))
 (24 8 (:LINEAR FLOOR-TYPE-2 . 2))
 (24 8 (:LINEAR FLOOR-TYPE-2 . 1))
 (24 8 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (24 8 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (24 8 (:LINEAR <=-OF-*-OF-/-WHEN-NEGATIVE-AND-POSITIVE-LINEAR))
 (24 8 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NONNEGATIVE-LINEAR))
 (24 8 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NEGATIVE-LINEAR))
 (12 12 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (12 12 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (12 12 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (12 12 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (11 1 (:REWRITE <-OF-FLOOR-AND-0))
 (10 10 (:REWRITE FOLD-CONSTS-IN-+))
 (9 3 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (8 8 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (8 8 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (6 2 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (5 5 (:REWRITE EQUAL-OF-*-AND-CONSTANT))
 (4 4 (:REWRITE MOD-OF-+-SUBST-CONSTANT-ARG2))
 (4 4 (:REWRITE MOD-OF-+-SUBST-CONSTANT-ARG1))
 (4 4 (:REWRITE FLOOR-PEEL-OFF-CONSTANT))
 (4 4 (:REWRITE FLOOR-OF-PLUS-NORMALIZE-NEGATIVE-CONSTANT))
 (3 3 (:LINEAR MOD-TYPE . 3))
 (3 3 (:LINEAR MOD-TYPE . 1))
 (3 3 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (3 1 (:REWRITE <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE))
 (1 1 (:REWRITE <-OF-FLOOR-OF-CONSTANT-AND-CONSTANT-GEN))
 )
(MOD-RECOLLAPSE-LEMMA2
 (364 3 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (276 4 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (98 44 (:REWRITE DEFAULT-<-2))
 (58 44 (:REWRITE DEFAULT-<-1))
 (51 51 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (51 51 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (51 51 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (51 51 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (51 51 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (51 51 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (51 51 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (51 51 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (47 47 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (39 10 (:REWRITE DEFAULT-*-2))
 (36 3 (:REWRITE FLOOR-WHEN-MOD-0-CHEAP))
 (34 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (31 10 (:REWRITE DEFAULT-*-1))
 (30 3 (:REWRITE DEFAULT-+-2))
 (28 3 (:REWRITE FLOOR-=-X/Y . 3))
 (16 16 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (16 16 (:TYPE-PRESCRIPTION RATIONALP-MOD))
 (16 16 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (16 16 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (16 16 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (16 16 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (16 16 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (16 16 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (16 16 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (16 16 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (16 4 (:LINEAR MY-FLOOR-LOWER-BOUND-ALT-LINEAR))
 (16 4 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (16 4 (:LINEAR FLOOR-TYPE-2 . 2))
 (16 4 (:LINEAR FLOOR-TYPE-2 . 1))
 (16 4 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (16 4 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (16 4 (:LINEAR *-OF-FLOOR-UPPER-BOUND-LINEAR))
 (11 3 (:REWRITE FLOOR-=-X/Y . 2))
 (10 2 (:REWRITE MOD-WHEN-MULTIPLE))
 (10 2 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (9 5 (:REWRITE DEFAULT-UNARY-/))
 (9 4 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (8 8 (:LINEAR <-OF-*-AND-*-LINEAR))
 (8 4 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (8 4 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (8 3 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (7 4 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (6 6 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (6 3 (:REWRITE FLOOR-TYPE-4 . 3))
 (6 3 (:REWRITE FLOOR-TYPE-4 . 2))
 (5 3 (:REWRITE FLOOR-WHEN-<))
 (5 3 (:REWRITE FLOOR-TYPE-3 . 3))
 (5 3 (:REWRITE FLOOR-TYPE-3 . 2))
 (5 3 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (4 4 (:REWRITE INTEGERP-OF-*))
 (4 4 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (4 4 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (4 4 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (4 3 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (4 2 (:REWRITE MOD-WHEN-<-OF-0))
 (4 2 (:REWRITE MOD-WHEN-<))
 (3 3 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (3 3 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (3 3 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (3 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (3 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (2 2 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (2 1 (:REWRITE EQUAL-OF-0-AND-+-OF--))
 (2 1 (:DEFINITION NOT))
 (1 1 (:REWRITE RATIONALP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (1 1 (:REWRITE RATIONALP-*))
 )
(MOD-RECOLLAPSE-LEMMA
 (715 4 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (275 2 (:REWRITE MOD-OF-+-SUBST-CONSTANT))
 (268 4 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (125 68 (:REWRITE DEFAULT-<-2))
 (121 20 (:REWRITE DEFAULT-+-2))
 (89 48 (:REWRITE DEFAULT-*-2))
 (80 48 (:REWRITE DEFAULT-*-1))
 (77 68 (:REWRITE DEFAULT-<-1))
 (67 5 (:REWRITE DISTRIBUTIVITY))
 (62 62 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (62 62 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (62 62 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (62 62 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (62 62 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (62 62 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (62 62 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (54 54 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (53 6 (:REWRITE CANCEL-FLOOR-+-BASIC))
 (48 4 (:REWRITE FLOOR-WHEN-MOD-0-CHEAP))
 (47 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (37 4 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (33 4 (:REWRITE FLOOR-=-X/Y . 3))
 (31 4 (:REWRITE MOD-WHEN-MULTIPLE))
 (31 4 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (31 4 (:REWRITE FLOOR-=-X/Y . 2))
 (25 25 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (25 25 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (25 25 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (25 25 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (25 25 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (25 25 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (25 25 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (25 25 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (25 25 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (24 2 (:REWRITE MOD-OF-+-WHEN-MULT-ARG1-ALT-CHEAP))
 (22 20 (:REWRITE DEFAULT-+-1))
 (20 16 (:REWRITE DEFAULT-UNARY-/))
 (20 4 (:REWRITE CANCEL-MOD-+-BASIC))
 (19 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (19 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (17 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (16 4 (:LINEAR MY-FLOOR-LOWER-BOUND-ALT-LINEAR))
 (16 4 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (16 4 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (16 4 (:LINEAR *-OF-FLOOR-UPPER-BOUND-LINEAR))
 (12 4 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (12 4 (:LINEAR FLOOR-TYPE-2 . 2))
 (12 4 (:LINEAR FLOOR-TYPE-2 . 1))
 (12 4 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (11 3 (:REWRITE FLOOR-OF-+-WHEN-MULT-ARG2))
 (11 3 (:REWRITE FLOOR-OF-+-WHEN-MULT-ARG1))
 (10 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (10 10 (:REWRITE INTEGERP-OF-*))
 (10 8 (:REWRITE RATIONALP-+))
 (9 4 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (8 8 (:LINEAR <-OF-*-AND-*-LINEAR))
 (8 4 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (8 4 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (8 4 (:REWRITE MOD-WHEN-<-OF-0))
 (8 4 (:REWRITE MOD-WHEN-<))
 (8 4 (:REWRITE FLOOR-WHEN-<))
 (8 4 (:REWRITE FLOOR-TYPE-4 . 3))
 (8 4 (:REWRITE FLOOR-TYPE-4 . 2))
 (8 4 (:REWRITE FLOOR-TYPE-3 . 3))
 (8 4 (:REWRITE FLOOR-TYPE-3 . 2))
 (8 4 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (8 4 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (8 2 (:LINEAR MOD-TYPE . 4))
 (8 2 (:LINEAR MOD-TYPE . 3))
 (8 2 (:LINEAR MOD-TYPE . 2))
 (8 2 (:LINEAR MOD-TYPE . 1))
 (7 7 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (7 4 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (6 3 (:REWRITE NOT-RATIONALP-RATIONALP-UNARY---PLUS))
 (6 3 (:REWRITE NOT-RATIONALP-RATIONALP-PLUS))
 (5 4 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (5 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (5 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (5 4 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (4 4 (:REWRITE RATIONALP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (4 4 (:REWRITE RATIONALP-*))
 (4 4 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (4 4 (:REWRITE FOLD-CONSTS-IN-+))
 (4 4 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (4 4 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (4 4 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (4 4 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (3 3 (:REWRITE FLOOR-PEEL-OFF-CONSTANT))
 (3 3 (:REWRITE FLOOR-OF-PLUS-NORMALIZE-NEGATIVE-CONSTANT))
 (2 2 (:REWRITE MOD-OF-+-SUBST-CONSTANT-ARG2))
 (2 2 (:REWRITE MOD-OF-+-SUBST-CONSTANT-ARG1))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (2 1 (:DEFINITION NOT))
 )
(SAME-REMAINDER-WHEN-CLOSE-HELPER2
 (123 8 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (119 119 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (119 119 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (119 119 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (119 119 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (119 119 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (119 119 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (117 117 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (66 66 (:REWRITE DEFAULT-<-2))
 (66 66 (:REWRITE DEFAULT-<-1))
 (64 8 (:REWRITE MOD-WHEN-MULTIPLE))
 (43 16 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (43 16 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (35 2 (:LINEAR MOD-TYPE . 2))
 (34 16 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (22 22 (:REWRITE DEFAULT-UNARY-MINUS))
 (22 8 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (22 8 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (22 8 (:REWRITE MOD-WHEN-<-OF-0))
 (22 8 (:REWRITE MOD-WHEN-<))
 (20 16 (:REWRITE DEFAULT-UNARY-/))
 (16 16 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (16 16 (:REWRITE INTEGERP-OF-*))
 (16 16 (:REWRITE DEFAULT-*-2))
 (16 16 (:REWRITE DEFAULT-*-1))
 (8 8 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (8 8 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (8 8 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (8 8 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (8 8 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (8 8 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (8 8 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (6 2 (:LINEAR MOD-TYPE . 3))
 (6 2 (:LINEAR MOD-TYPE . 1))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 )
(SAME-REMAINDER-WHEN-CLOSE-HELPER3
 (192 12 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (131 131 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (131 131 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (131 131 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (131 131 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (131 131 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (121 121 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (100 12 (:REWRITE MOD-WHEN-MULTIPLE))
 (97 97 (:REWRITE DEFAULT-<-2))
 (97 97 (:REWRITE DEFAULT-<-1))
 (63 24 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (63 24 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (50 24 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (35 2 (:LINEAR MOD-TYPE . 2))
 (34 12 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (34 12 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (34 12 (:REWRITE MOD-WHEN-<-OF-0))
 (34 12 (:REWRITE MOD-WHEN-<))
 (29 29 (:REWRITE DEFAULT-UNARY-MINUS))
 (29 24 (:REWRITE DEFAULT-UNARY-/))
 (27 9 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (24 24 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (24 24 (:REWRITE INTEGERP-OF-*))
 (24 24 (:REWRITE DEFAULT-*-2))
 (24 24 (:REWRITE DEFAULT-*-1))
 (18 18 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (12 12 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (12 12 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (6 2 (:LINEAR MOD-TYPE . 3))
 (6 2 (:LINEAR MOD-TYPE . 1))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 )
(SAME-REMAINDER-WHEN-CLOSE
 (245 14 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (231 231 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (231 231 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (231 231 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (231 231 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (231 231 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (231 231 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (231 231 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (231 231 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (126 14 (:REWRITE MOD-WHEN-MULTIPLE))
 (115 115 (:REWRITE DEFAULT-<-2))
 (115 115 (:REWRITE DEFAULT-<-1))
 (84 21 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (70 28 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (70 28 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (56 28 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (47 47 (:REWRITE DEFAULT-UNARY-MINUS))
 (42 14 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (42 14 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (42 14 (:REWRITE MOD-WHEN-<-OF-0))
 (42 14 (:REWRITE MOD-WHEN-<))
 (35 28 (:REWRITE DEFAULT-UNARY-/))
 (28 28 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (28 28 (:REWRITE INTEGERP-OF-*))
 (28 28 (:REWRITE DEFAULT-*-2))
 (28 28 (:REWRITE DEFAULT-*-1))
 (24 24 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (14 14 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (14 14 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (14 14 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (14 14 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (14 14 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (12 12 (:REWRITE DEFAULT-+-2))
 (12 12 (:REWRITE DEFAULT-+-1))
 )
(SAME-REMAINDER-WHEN-CLOSE-LEMMA
 (6297 26 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (4864 132 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (2097 29 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (1818 28 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (1516 132 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (1061 980 (:REWRITE DEFAULT-<-1))
 (1052 980 (:REWRITE DEFAULT-<-2))
 (759 91 (:REWRITE FLOOR-WHEN-MOD-0-CHEAP))
 (737 449 (:REWRITE DEFAULT-*-2))
 (691 131 (:REWRITE MOD-WHEN-MULTIPLE))
 (691 131 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (634 12 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (622 12 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (622 12 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (603 297 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (576 297 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (554 12 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (525 525 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (525 525 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (525 525 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (525 525 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (525 525 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (523 523 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (519 77 (:REWRITE FLOOR-=-X/Y . 3))
 (515 23 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (485 449 (:REWRITE DEFAULT-*-1))
 (483 297 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (445 58 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (381 356 (:REWRITE DEFAULT-UNARY-/))
 (374 1 (:REWRITE <-OF-*-AND-0))
 (362 362 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (362 362 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (362 362 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (362 362 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (345 345 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (345 1 (:REWRITE <-OF-*-SAME-ARG3))
 (333 23 (:LINEAR MOD-TYPE . 2))
 (297 297 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (297 297 (:REWRITE INTEGERP-OF-*))
 (271 131 (:REWRITE MOD-WHEN-<))
 (253 131 (:REWRITE MOD-WHEN-<-OF-0))
 (253 77 (:REWRITE FLOOR-=-X/Y . 2))
 (220 202 (:REWRITE DEFAULT-UNARY-MINUS))
 (211 79 (:REWRITE FLOOR-TYPE-4 . 3))
 (172 14 (:LINEAR FLOOR-TYPE-2 . 1))
 (163 79 (:REWRITE FLOOR-TYPE-4 . 2))
 (152 20 (:REWRITE MOD-=-0 . 1))
 (143 79 (:REWRITE FLOOR-TYPE-3 . 3))
 (139 79 (:REWRITE FLOOR-TYPE-3 . 2))
 (131 131 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (131 131 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (131 131 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (131 131 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (131 131 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (126 45 (:REWRITE DEFAULT-+-2))
 (121 77 (:REWRITE FLOOR-WHEN-<))
 (116 116 (:LINEAR <=-OF-/-LINEAR))
 (110 12 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (99 1 (:REWRITE DISTRIBUTIVITY))
 (88 22 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NONNEGATIVE-LINEAR))
 (77 77 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (77 77 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (77 77 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (77 77 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (77 77 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (70 52 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (69 23 (:REWRITE <-OF-/-AND-CONSTANT))
 (69 23 (:LINEAR MOD-TYPE . 3))
 (69 23 (:LINEAR MOD-TYPE . 1))
 (66 22 (:LINEAR <=-OF-*-OF-/-WHEN-NEGATIVE-AND-POSITIVE-LINEAR))
 (63 45 (:REWRITE DEFAULT-+-1))
 (62 4 (:REWRITE FLOOR-TYPE-2))
 (58 58 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (58 58 (:LINEAR <-OF-*-AND-*-LINEAR))
 (44 22 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NEGATIVE-LINEAR))
 (42 14 (:LINEAR FLOOR-TYPE-2 . 2))
 (35 35 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (35 35 (:REWRITE <-OF-/-AND-0))
 (35 35 (:REWRITE /-EQUAL-CONSTANT-ALT))
 (34 1 (:REWRITE *-OF---ARG2))
 (28 28 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (28 28 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (28 28 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (24 24 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (12 12 (:REWRITE *-OF-0))
 (12 12 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (2 2 (:REWRITE EQUAL-OF-*-AND-CONSTANT))
 (2 2 (:REWRITE <-OF-CONSTANT-AND-*-OF-CONSTANT))
 (1 1 (:REWRITE <-OF-FLOOR-OF-CONSTANT-AND-CONSTANT-GEN))
 (1 1 (:REWRITE *-OF-*-COMBINE-CONSTANTS))
 )

(MOD-EXPT-MOD
 (3660 70 (:LINEAR MOD-TYPE . 2))
 (3174 58 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (2944 58 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (2522 42 (:REWRITE MOD-WHEN-MULTIPLE))
 (2055 1325 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (2055 1325 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (2055 1325 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (1789 1113 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (1442 42 (:REWRITE MOD-WHEN-<))
 (1325 1325 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (1325 1325 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (1136 44 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (1133 44 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (1130 44 (:REWRITE MOD-WHEN-<-OF-0))
 (1061 1061 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (1061 1061 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (747 247 (:REWRITE DEFAULT-<-2))
 (718 247 (:REWRITE DEFAULT-<-1))
 (687 184 (:REWRITE DEFAULT-*-2))
 (597 184 (:REWRITE DEFAULT-*-1))
 (530 30 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (521 42 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (479 30 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (462 30 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (244 70 (:LINEAR MOD-TYPE . 3))
 (244 70 (:LINEAR MOD-TYPE . 1))
 (210 30 (:REWRITE DEFAULT-UNARY-/))
 (179 39 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (168 28 (:REWRITE MOD-OF-2-WHEN-EVEN-CHEAP))
 (120 30 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (106 106 (:LINEAR EXPT-BOUND-LINEAR-WEAK))
 (88 88 (:REWRITE INTEGERP-OF-*))
 (85 34 (:REWRITE DEFAULT-UNARY-MINUS))
 (78 39 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (58 58 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 (53 53 (:LINEAR EXPT-BOUND-LINEAR-2))
 (44 44 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (36 36 (:REWRITE RATIONALP-OF-MOD))
 (36 36 (:REWRITE RATIONALP-MOD))
 (30 30 (:REWRITE MOD-TYPE))
 (10 10 (:REWRITE MOD-OF-MOD-WHEN-MULTIPLE-SAFE))
 (6 6 (:TYPE-PRESCRIPTION NATP-OF-EXPT))
 (6 6 (:REWRITE INTEGERP-MOD))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(INTEGERP-OF-*-OF-/-AND-MOD
 (1254 1245 (:REWRITE DEFAULT-*-2))
 (1245 1245 (:REWRITE DEFAULT-*-1))
 (606 597 (:REWRITE DEFAULT-<-2))
 (597 597 (:REWRITE DEFAULT-<-1))
 (593 593 (:REWRITE DEFAULT-+-2))
 (593 593 (:REWRITE DEFAULT-+-1))
 (147 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (145 145 (:REWRITE DEFAULT-UNARY-MINUS))
 (135 111 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (135 111 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (111 111 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (111 111 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (111 111 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (111 111 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (111 111 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (111 111 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (93 3 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (92 92 (:REWRITE DEFAULT-UNARY-/))
 (86 6 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (85 25 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (85 25 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (46 6 (:REWRITE MOD-WHEN-MULTIPLE))
 (42 14 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (32 32 (:REWRITE *-OF-*-COMBINE-CONSTANTS))
 (28 28 (:REWRITE INTEGERP-OF-*))
 (21 7 (:LINEAR MOD-TYPE . 4))
 (21 7 (:LINEAR MOD-TYPE . 3))
 (21 7 (:LINEAR MOD-TYPE . 2))
 (21 7 (:LINEAR MOD-TYPE . 1))
 (21 7 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (21 7 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (16 16 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (16 6 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (16 6 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (16 6 (:REWRITE MOD-WHEN-<-OF-0))
 (16 6 (:REWRITE MOD-WHEN-<))
 (15 3 (:REWRITE INTEGERP-OF-*-OF-/-AND-MOD-SAME))
 (9 3 (:DEFINITION NATP))
 (8 8 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (7 7 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (6 6 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (6 6 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (6 6 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (6 6 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (6 6 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (3 3 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (3 3 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (3 3 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (3 3 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (3 3 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (3 3 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (3 3 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (3 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 )
(MOD-NON-NEGATIVE-CONSTANT
 (1 1 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (1 1 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (1 1 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (1 1 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (1 1 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 )
(MOD-NON-NEGATIVE-CONSTANT-GEN
 (11 11 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (11 11 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (11 11 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (11 11 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (11 11 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 )
(MOD-NON-NEGATIVE-CONSTANT-POS-REWRITE
 (55 55 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (55 55 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (55 55 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (55 55 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (18 2 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (12 12 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (12 12 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (10 2 (:REWRITE MOD-WHEN-MULTIPLE))
 (9 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE DEFAULT-<-1))
 (6 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (6 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (5 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (4 4 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (4 2 (:REWRITE MOD-WHEN-<-OF-0))
 (4 2 (:REWRITE MOD-WHEN-<))
 (3 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (3 3 (:REWRITE INTEGERP-OF-*))
 (3 3 (:REWRITE DEFAULT-UNARY-/))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (2 2 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (2 2 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(MOD-OF-MOD-OF-EXPT-OF-2-AND-2
 (17684 86 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (15757 172 (:REWRITE MOD-WHEN-<))
 (14483 227 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (13135 227 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (12720 69 (:LINEAR MOD-TYPE . 2))
 (9022 9022 (:TYPE-PRESCRIPTION NATP-OF-EXPT))
 (7476 172 (:REWRITE MOD-WHEN-MULTIPLE))
 (7066 338 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (6158 338 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (5968 338 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (4902 2080 (:REWRITE DEFAULT-<-2))
 (4314 406 (:REWRITE DEFAULT-UNARY-/))
 (3420 2080 (:REWRITE DEFAULT-<-1))
 (3098 578 (:REWRITE DEFAULT-*-2))
 (1952 338 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (1949 13 (:REWRITE MOD-TYPE))
 (1859 1043 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (1671 855 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (1288 380 (:REWRITE DEFAULT-UNARY-MINUS))
 (1208 1208 (:LINEAR EXPT-BOUND-LINEAR-WEAK))
 (1208 1208 (:LINEAR EXPT-BOUND-LINEAR))
 (1144 578 (:REWRITE DEFAULT-*-1))
 (1100 13 (:REWRITE REWRITE-MOD-MOD))
 (1044 172 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (1043 1043 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (1043 1043 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (964 86 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (867 227 (:REWRITE MOD-WHEN-<-OF-0))
 (828 172 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (824 86 (:REWRITE COMMUTATIVITY-OF-*))
 (604 604 (:LINEAR EXPT-BOUND-LINEAR-2))
 (448 64 (:REWRITE INTEGERP-OF-EXPT-WHEN-NATP))
 (388 172 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (388 172 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (371 69 (:LINEAR MOD-TYPE . 3))
 (371 69 (:LINEAR MOD-TYPE . 1))
 (250 34 (:REWRITE MOD-OF-2-WHEN-EVEN-CHEAP))
 (227 227 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (86 86 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 (64 64 (:REWRITE INTEGERP-OF-EXPT2))
 (57 3 (:REWRITE INTEGERP-OF-MOD))
 (57 3 (:REWRITE INTEGERP-MOD))
 (27 9 (:DEFINITION POSP))
 (20 1 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (16 16 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (16 16 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (16 16 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (16 4 (:REWRITE DEFAULT-+-2))
 (13 13 (:REWRITE MOD-OF-MOD-WHEN-MULTIPLE-SAFE))
 (13 13 (:REWRITE MOD-NON-NEGATIVE-CONSTANT-POS-REWRITE))
 (13 13 (:REWRITE INTEGERP-OF-*-OF-1/2-AND-EXPT-2))
 (13 13 (:REWRITE <-OF-0-AND-EXPT))
 (9 9 (:TYPE-PRESCRIPTION POSP))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE ZP-OPEN))
 )
(MOD-OF-MOD-2-EXPT-2
 (1923 44 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (1247 9 (:REWRITE MOD-NON-NEGATIVE-CONSTANT-POS-REWRITE))
 (809 36 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (748 78 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (671 36 (:REWRITE MOD-WHEN-MULTIPLE))
 (598 9 (:REWRITE REWRITE-MOD-MOD))
 (536 10 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (518 10 (:LINEAR MOD-TYPE . 2))
 (484 424 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (484 424 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (484 424 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (424 424 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (424 424 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (349 78 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (274 78 (:REWRITE COMMUTATIVITY-OF-*))
 (258 208 (:REWRITE DEFAULT-<-1))
 (235 208 (:REWRITE DEFAULT-<-2))
 (232 165 (:REWRITE DEFAULT-*-2))
 (205 165 (:REWRITE DEFAULT-*-1))
 (202 9 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (195 87 (:REWRITE INTEGERP-OF-*))
 (151 36 (:REWRITE MOD-WHEN-<))
 (109 36 (:REWRITE MOD-WHEN-<-OF-0))
 (91 13 (:REWRITE DEFAULT-UNARY-/))
 (90 78 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 (46 36 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (44 10 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (43 36 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (43 36 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (39 36 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (36 36 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (36 12 (:REWRITE INTEGERP-OF-/-OF-EXPT-2))
 (36 9 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (36 9 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (36 9 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (35 35 (:REWRITE MOD-OF-2-WHEN-EVEN-CHEAP))
 (20 20 (:LINEAR EXPT-BOUND-LINEAR-WEAK))
 (18 18 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (16 10 (:LINEAR MOD-TYPE . 3))
 (16 10 (:LINEAR MOD-TYPE . 1))
 (14 14 (:LINEAR EXPT-BOUND-LINEAR-2))
 (6 6 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (6 6 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (6 6 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (4 2 (:REWRITE INTEGERP-OF-MOD))
 (2 2 (:TYPE-PRESCRIPTION NATP-OF-EXPT))
 (2 2 (:REWRITE INTEGERP-MOD))
 (2 2 (:DEFINITION FIX))
 (1 1 (:REWRITE MOD-OF-MOD-WHEN-MULTIPLE-SAFE))
 )
(<-OF-MOD
 (34 2 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (33 33 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (33 33 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (33 33 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (33 33 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (33 33 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (18 2 (:REWRITE MOD-WHEN-MULTIPLE))
 (17 17 (:REWRITE DEFAULT-<-2))
 (17 17 (:REWRITE DEFAULT-<-1))
 (17 1 (:LINEAR MOD-TYPE . 2))
 (14 5 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (14 5 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (11 5 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (6 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (6 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (6 2 (:REWRITE MOD-WHEN-<-OF-0))
 (6 2 (:REWRITE MOD-WHEN-<))
 (5 5 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (5 5 (:REWRITE INTEGERP-OF-*))
 (5 5 (:REWRITE DEFAULT-UNARY-/))
 (5 5 (:REWRITE DEFAULT-*-2))
 (5 5 (:REWRITE DEFAULT-*-1))
 (2 2 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (2 2 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (2 2 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (2 2 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (2 2 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (1 1 (:LINEAR MOD-TYPE . 3))
 (1 1 (:LINEAR MOD-TYPE . 1))
 )
(MOD-OF-*-OF-SAME-2
 (54 6 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (34 34 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (34 34 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (34 34 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (34 34 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (34 34 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (33 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (33 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (33 2 (:REWRITE MOD-WHEN-<-OF-0))
 (30 21 (:REWRITE DEFAULT-<-2))
 (28 28 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (27 21 (:REWRITE DEFAULT-<-1))
 (18 18 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (18 18 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (18 6 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (13 8 (:REWRITE DEFAULT-*-1))
 (12 12 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (12 12 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (12 12 (:LINEAR <-OF-*-AND-*-LINEAR))
 (11 8 (:REWRITE DEFAULT-*-2))
 (10 3 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (9 3 (:LINEAR MOD-TYPE . 4))
 (9 3 (:LINEAR MOD-TYPE . 3))
 (9 3 (:LINEAR MOD-TYPE . 2))
 (9 3 (:LINEAR MOD-TYPE . 1))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (5 3 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (5 3 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (4 4 (:REWRITE RATIONALP-*))
 (4 4 (:REWRITE INTEGERP-OF-*))
 (4 4 (:REWRITE <-OF-CONSTANT-AND-*-OF-CONSTANT))
 (4 4 (:REWRITE *-OF-*-COMBINE-CONSTANTS))
 (4 1 (:REWRITE DEFAULT-UNARY-/))
 (3 2 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (2 2 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (2 2 (:REWRITE <-OF-*-AND-0))
 (1 1 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(MOD-OF-MOD-WHEN-MULT-CHEAP
 (13 13 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (13 13 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (13 13 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (13 13 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (13 13 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (13 13 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (13 13 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (13 13 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (13 13 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 )
(+-OF-MOD-AND-*-OF-FLOOR-SAME
 (468 4 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (140 2 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (136 2 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (117 1 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (108 90 (:REWRITE DEFAULT-<-2))
 (90 90 (:REWRITE DEFAULT-<-1))
 (77 5 (:REWRITE FLOOR-=-X/Y . 3))
 (48 48 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (48 48 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (48 48 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (48 48 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (48 48 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (48 48 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (48 48 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (48 48 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (45 5 (:REWRITE FLOOR-=-X/Y . 2))
 (31 31 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (31 31 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (31 31 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (31 31 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (31 31 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (31 31 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (31 31 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (31 31 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (27 12 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (27 12 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (26 17 (:REWRITE DEFAULT-*-2))
 (22 12 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (18 2 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (18 2 (:REWRITE <-OF-/-AND-CONSTANT-1))
 (17 17 (:REWRITE DEFAULT-*-1))
 (16 16 (:REWRITE DEFAULT-UNARY-/))
 (15 5 (:REWRITE FLOOR-WHEN-<))
 (15 5 (:REWRITE FLOOR-TYPE-4 . 3))
 (15 5 (:REWRITE FLOOR-TYPE-4 . 2))
 (15 5 (:REWRITE FLOOR-TYPE-3 . 3))
 (15 5 (:REWRITE FLOOR-TYPE-3 . 2))
 (12 12 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (12 12 (:REWRITE INTEGERP-OF-*))
 (12 4 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (10 10 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 2 (:REWRITE MOD-WHEN-MULTIPLE))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (8 8 (:LINEAR <-OF-*-AND-*-LINEAR))
 (6 2 (:REWRITE <-OF-/-AND-CONSTANT))
 (6 2 (:LINEAR MY-FLOOR-LOWER-BOUND-ALT-LINEAR))
 (6 2 (:LINEAR MOD-TYPE . 4))
 (6 2 (:LINEAR MOD-TYPE . 3))
 (6 2 (:LINEAR MOD-TYPE . 2))
 (6 2 (:LINEAR MOD-TYPE . 1))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (6 2 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (6 2 (:LINEAR FLOOR-TYPE-2 . 2))
 (6 2 (:LINEAR FLOOR-TYPE-2 . 1))
 (6 2 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (6 2 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-NEGATIVE-AND-POSITIVE-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NONNEGATIVE-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NEGATIVE-LINEAR))
 (6 2 (:LINEAR *-OF-FLOOR-UPPER-BOUND-LINEAR))
 (5 5 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (5 5 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (5 5 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (5 5 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (5 5 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (4 4 (:LINEAR <=-OF-/-LINEAR))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (4 2 (:REWRITE MOD-WHEN-<-OF-0))
 (4 2 (:REWRITE MOD-WHEN-<))
 (2 2 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (2 2 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (2 2 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (2 2 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (2 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (2 2 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (2 2 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 )
(MOD-OF-+-WHEN-MULT-ARG1
 (99 99 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (99 99 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (99 99 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (99 99 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (99 99 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (99 99 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (99 99 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (99 99 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (50 5 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (46 46 (:REWRITE DEFAULT-<-2))
 (46 46 (:REWRITE DEFAULT-<-1))
 (39 4 (:REWRITE MOD-WHEN-MULTIPLE))
 (26 2 (:REWRITE DISTRIBUTIVITY))
 (23 23 (:REWRITE DEFAULT-*-2))
 (23 23 (:REWRITE DEFAULT-*-1))
 (23 8 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (23 8 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (18 8 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (16 7 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (14 12 (:REWRITE DEFAULT-UNARY-/))
 (14 1 (:REWRITE MOD-OF-+-SUBST-CONSTANT))
 (13 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (13 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (13 5 (:REWRITE MOD-WHEN-<-OF-0))
 (12 12 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (12 4 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (10 10 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 4 (:REWRITE MOD-WHEN-<))
 (8 8 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (8 8 (:REWRITE INTEGERP-OF-*))
 (7 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 2 (:LINEAR MOD-TYPE . 4))
 (6 2 (:LINEAR MOD-TYPE . 3))
 (6 2 (:LINEAR MOD-TYPE . 2))
 (6 2 (:LINEAR MOD-TYPE . 1))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (5 5 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (4 4 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (1 1 (:REWRITE EQUAL-OF-MOD-OF-+-WHEN-CONSTANTS))
 )
(MOD-OF-+-WHEN-MULT-ARG1-ALT
 (82 82 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (82 82 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (82 82 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (82 82 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (53 4 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (38 38 (:REWRITE DEFAULT-<-2))
 (38 38 (:REWRITE DEFAULT-<-1))
 (36 4 (:REWRITE MOD-WHEN-MULTIPLE))
 (35 2 (:REWRITE CANCEL-MOD-+-BASIC))
 (22 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (22 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (18 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (16 16 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (15 6 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (15 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (15 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (12 10 (:REWRITE DEFAULT-UNARY-/))
 (12 4 (:REWRITE MOD-WHEN-<-OF-0))
 (12 4 (:REWRITE MOD-WHEN-<))
 (10 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (10 10 (:REWRITE INTEGERP-OF-*))
 (10 10 (:REWRITE DEFAULT-*-2))
 (10 10 (:REWRITE DEFAULT-*-1))
 (8 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (4 4 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (4 4 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 1 (:LINEAR MOD-TYPE . 4))
 (3 1 (:LINEAR MOD-TYPE . 3))
 (3 1 (:LINEAR MOD-TYPE . 2))
 (3 1 (:LINEAR MOD-TYPE . 1))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (1 1 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 )
(MOD-OF-+-WHEN-MULT-ARG1-ALT-CHEAP
 (82 82 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (82 82 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (82 82 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (82 82 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (82 82 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (53 4 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (38 38 (:REWRITE DEFAULT-<-2))
 (38 38 (:REWRITE DEFAULT-<-1))
 (36 4 (:REWRITE MOD-WHEN-MULTIPLE))
 (35 2 (:REWRITE CANCEL-MOD-+-BASIC))
 (22 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (22 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (18 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (16 16 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (15 6 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (15 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (15 5 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (12 10 (:REWRITE DEFAULT-UNARY-/))
 (12 4 (:REWRITE MOD-WHEN-<-OF-0))
 (12 4 (:REWRITE MOD-WHEN-<))
 (10 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (10 10 (:REWRITE INTEGERP-OF-*))
 (10 10 (:REWRITE DEFAULT-*-2))
 (10 10 (:REWRITE DEFAULT-*-1))
 (8 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (4 4 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (4 4 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 1 (:LINEAR MOD-TYPE . 4))
 (3 1 (:LINEAR MOD-TYPE . 3))
 (3 1 (:LINEAR MOD-TYPE . 2))
 (3 1 (:LINEAR MOD-TYPE . 1))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (1 1 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 )
(FLOOR-WHEN-MOD-0-CHEAP
 (1389 1344 (:REWRITE DEFAULT-*-2))
 (1371 1344 (:REWRITE DEFAULT-*-1))
 (587 560 (:REWRITE DEFAULT-+-2))
 (560 560 (:REWRITE DEFAULT-+-1))
 (539 521 (:REWRITE DEFAULT-<-2))
 (521 521 (:REWRITE DEFAULT-<-1))
 (453 5 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (384 4 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (159 132 (:REWRITE DEFAULT-UNARY-MINUS))
 (134 134 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (134 134 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (134 134 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (134 134 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (134 134 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (134 134 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (134 134 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (134 134 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (98 2 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (94 2 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (81 81 (:REWRITE DEFAULT-UNARY-/))
 (47 47 (:REWRITE *-OF-*-COMBINE-CONSTANTS))
 (36 9 (:REWRITE FLOOR-=-X/Y . 2))
 (27 27 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (27 27 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (27 27 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (27 27 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (27 27 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (27 27 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (27 27 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (27 27 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (23 9 (:REWRITE FLOOR-WHEN-<))
 (23 9 (:REWRITE FLOOR-TYPE-4 . 3))
 (23 9 (:REWRITE FLOOR-TYPE-4 . 2))
 (23 9 (:REWRITE FLOOR-TYPE-3 . 3))
 (23 9 (:REWRITE FLOOR-TYPE-3 . 2))
 (20 20 (:REWRITE EQUAL-OF-*-AND-CONSTANT))
 (18 2 (:REWRITE <-OF-/-AND-CONSTANT-1))
 (12 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (12 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (10 4 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (10 4 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (10 4 (:REWRITE MOD-WHEN-<-OF-0))
 (10 4 (:REWRITE MOD-WHEN-<))
 (9 9 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (9 9 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (9 9 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (9 9 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (9 9 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (9 9 (:REWRITE FLOOR-=-X/Y . 3))
 (9 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (8 8 (:LINEAR <-OF-*-AND-*-LINEAR))
 (6 2 (:REWRITE <-OF-/-AND-CONSTANT))
 (6 2 (:LINEAR MY-FLOOR-LOWER-BOUND-ALT-LINEAR))
 (6 2 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (6 2 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (6 2 (:LINEAR FLOOR-TYPE-2 . 2))
 (6 2 (:LINEAR FLOOR-TYPE-2 . 1))
 (6 2 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (6 2 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-NEGATIVE-AND-POSITIVE-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NONNEGATIVE-LINEAR))
 (6 2 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NEGATIVE-LINEAR))
 (6 2 (:LINEAR *-OF-FLOOR-UPPER-BOUND-LINEAR))
 (5 5 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (4 4 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (4 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (4 4 (:REWRITE MOD-WHEN-MULTIPLE))
 (4 4 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (4 4 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (4 4 (:LINEAR <=-OF-/-LINEAR))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (3 3 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (3 3 (:REWRITE INTEGERP-OF-*))
 (3 1 (:LINEAR MOD-TYPE . 4))
 (3 1 (:LINEAR MOD-TYPE . 3))
 (3 1 (:LINEAR MOD-TYPE . 2))
 (3 1 (:LINEAR MOD-TYPE . 1))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (3 1 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (2 2 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (2 2 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (1 1 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 )
(EQUAL-OF-0-AND-MOD-OF--
 (1506 15 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (762 6 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (286 259 (:REWRITE DEFAULT-<-2))
 (275 275 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (275 275 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (275 275 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (275 275 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (275 275 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (275 275 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (275 275 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (275 275 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (259 259 (:REWRITE DEFAULT-<-1))
 (241 106 (:REWRITE DEFAULT-*-2))
 (240 3 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (237 21 (:REWRITE FLOOR-=-X/Y . 3))
 (234 3 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (210 21 (:REWRITE FLOOR-WHEN-MOD-0-CHEAP))
 (203 50 (:REWRITE DEFAULT-UNARY-MINUS))
 (187 106 (:REWRITE DEFAULT-*-1))
 (184 31 (:REWRITE DEFAULT-+-2))
 (141 21 (:REWRITE FLOOR-=-X/Y . 2))
 (100 100 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (100 100 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (100 100 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (100 100 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (100 100 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (100 100 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (100 100 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (100 100 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (98 13 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (88 46 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (88 46 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (82 13 (:REWRITE MOD-WHEN-MULTIPLE))
 (74 46 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (56 56 (:REWRITE DEFAULT-UNARY-/))
 (51 21 (:REWRITE FLOOR-WHEN-<))
 (51 21 (:REWRITE FLOOR-TYPE-4 . 3))
 (51 21 (:REWRITE FLOOR-TYPE-4 . 2))
 (51 21 (:REWRITE FLOOR-TYPE-3 . 3))
 (51 21 (:REWRITE FLOOR-TYPE-3 . 2))
 (46 46 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (46 46 (:REWRITE INTEGERP-OF-*))
 (36 12 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (31 31 (:REWRITE DEFAULT-+-1))
 (31 13 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (31 13 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (31 13 (:REWRITE MOD-WHEN-<-OF-0))
 (28 12 (:REWRITE MOD-WHEN-<))
 (27 3 (:REWRITE <-OF-/-AND-CONSTANT-1))
 (21 21 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (21 21 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (21 21 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (21 21 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (21 21 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (18 6 (:LINEAR MOD-TYPE . 4))
 (18 6 (:LINEAR MOD-TYPE . 3))
 (18 6 (:LINEAR MOD-TYPE . 2))
 (18 6 (:LINEAR MOD-TYPE . 1))
 (18 6 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (18 6 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (13 13 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (12 12 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (12 12 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (12 12 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (12 12 (:LINEAR <-OF-*-AND-*-LINEAR))
 (9 9 (:REWRITE EQUAL-OF-*-AND-CONSTANT))
 (9 3 (:REWRITE <-OF-/-AND-CONSTANT))
 (9 3 (:LINEAR MY-FLOOR-LOWER-BOUND-ALT-LINEAR))
 (9 3 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (9 3 (:LINEAR FLOOR-TYPE-2 . 2))
 (9 3 (:LINEAR FLOOR-TYPE-2 . 1))
 (9 3 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (9 3 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (9 3 (:LINEAR <=-OF-*-OF-/-WHEN-NEGATIVE-AND-POSITIVE-LINEAR))
 (9 3 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NONNEGATIVE-LINEAR))
 (9 3 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NEGATIVE-LINEAR))
 (9 3 (:LINEAR *-OF-FLOOR-UPPER-BOUND-LINEAR))
 (8 2 (:REWRITE *-OF---ARG1))
 (6 6 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (6 6 (:LINEAR <=-OF-/-LINEAR))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (6 6 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (4 4 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (3 3 (:REWRITE FOLD-CONSTS-IN-+))
 (3 3 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (3 3 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (2 2 (:REWRITE *-OF-*-COMBINE-CONSTANTS))
 (2 2 (:DEFINITION IFF))
 )
(MOD-OF-+-SUBST-CONSTANT-ARG1
 (885 18 (:REWRITE MOD-OF-+-SUBST-CONSTANT))
 (692 124 (:REWRITE COMMUTATIVITY-OF-*))
 (681 44 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (665 44 (:REWRITE MOD-WHEN-MULTIPLE))
 (648 36 (:REWRITE CANCEL-MOD-+-BASIC))
 (630 6 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (602 86 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (348 324 (:REWRITE DEFAULT-*-2))
 (336 324 (:REWRITE DEFAULT-*-1))
 (308 38 (:REWRITE DISTRIBUTIVITY))
 (286 286 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (286 286 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (286 286 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (237 27 (:REWRITE MOD-OF-+-WHEN-MULT-ARG1-ALT-CHEAP))
 (231 219 (:REWRITE DEFAULT-<-1))
 (219 219 (:REWRITE DEFAULT-<-2))
 (196 6 (:LINEAR MOD-TYPE . 2))
 (174 86 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (133 133 (:REWRITE DEFAULT-UNARY-/))
 (128 44 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (128 44 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (128 44 (:REWRITE MOD-WHEN-<-OF-0))
 (128 44 (:REWRITE MOD-WHEN-<))
 (86 86 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 (86 86 (:REWRITE INTEGERP-OF-*))
 (85 67 (:REWRITE DEFAULT-+-2))
 (85 67 (:REWRITE DEFAULT-+-1))
 (44 44 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (44 44 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (44 44 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (44 44 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (44 44 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (34 34 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (34 34 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (28 28 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (22 22 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (6 6 (:LINEAR MOD-TYPE . 3))
 (6 6 (:LINEAR MOD-TYPE . 1))
 )
(MOD-OF-+-SUBST-CONSTANT-ARG2
 (1093 22 (:REWRITE MOD-OF-+-SUBST-CONSTANT))
 (839 149 (:REWRITE COMMUTATIVITY-OF-*))
 (817 52 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (801 52 (:REWRITE MOD-WHEN-MULTIPLE))
 (800 44 (:REWRITE CANCEL-MOD-+-BASIC))
 (714 102 (:REWRITE MULTIPLE-WHEN-MOD-0-CHEAP))
 (633 7 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (416 392 (:REWRITE DEFAULT-*-2))
 (404 392 (:REWRITE DEFAULT-*-1))
 (380 47 (:REWRITE DISTRIBUTIVITY))
 (301 301 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (301 301 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (301 301 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (272 260 (:REWRITE DEFAULT-<-1))
 (260 260 (:REWRITE DEFAULT-<-2))
 (217 31 (:REWRITE MOD-OF-+-WHEN-MULT-ARG1-ALT-CHEAP))
 (206 102 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE))
 (195 7 (:LINEAR MOD-TYPE . 2))
 (158 158 (:REWRITE DEFAULT-UNARY-/))
 (152 52 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (152 52 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (152 52 (:REWRITE MOD-WHEN-<-OF-0))
 (152 52 (:REWRITE MOD-WHEN-<))
 (102 102 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP-ALT))
 (102 102 (:REWRITE INTEGERP-OF-*))
 (102 84 (:REWRITE DEFAULT-+-2))
 (84 84 (:REWRITE DEFAULT-+-1))
 (52 52 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (52 52 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (52 52 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (52 52 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (52 52 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (34 34 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (34 34 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (31 31 (:REWRITE MOD-OF-+-SUBST-CONSTANT-ARG1))
 (28 28 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (22 22 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (7 7 (:LINEAR MOD-TYPE . 3))
 (7 7 (:LINEAR MOD-TYPE . 1))
 )
(SAME-REMAINDER-WHEN-CLOSE-HELPER
 (1359 22 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (1255 12 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (1025 108 (:REWRITE DEFAULT-+-2))
 (958 12 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (759 58 (:REWRITE FLOOR-=-X/Y . 3))
 (622 321 (:REWRITE DEFAULT-*-2))
 (577 24 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (573 321 (:REWRITE DEFAULT-*-1))
 (546 448 (:REWRITE DEFAULT-<-2))
 (544 8 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (528 8 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (527 58 (:REWRITE FLOOR-=-X/Y . 2))
 (490 448 (:REWRITE DEFAULT-<-1))
 (486 4 (:REWRITE MOD-OF-+-SUBST-CONSTANT))
 (472 472 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (472 472 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (472 472 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (472 472 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (472 472 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (464 58 (:REWRITE FLOOR-WHEN-MOD-0-CHEAP))
 (460 460 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (460 460 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (460 460 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (460 460 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (460 460 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (460 460 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (430 28 (:LINEAR <=-OF-/-LINEAR))
 (381 108 (:REWRITE DEFAULT-UNARY-MINUS))
 (379 211 (:REWRITE DEFAULT-UNARY-/))
 (312 35 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (280 154 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (280 154 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (248 35 (:REWRITE MOD-WHEN-MULTIPLE))
 (246 154 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (190 5 (:REWRITE EQUAL-OF-0-AND-+-OF--))
 (171 108 (:REWRITE DEFAULT-+-1))
 (154 154 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (154 154 (:REWRITE INTEGERP-OF-*))
 (146 58 (:REWRITE FLOOR-TYPE-4 . 3))
 (146 58 (:REWRITE FLOOR-TYPE-4 . 2))
 (104 8 (:REWRITE CANCEL-MOD-+-BASIC))
 (80 40 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (75 35 (:REWRITE MOD-WHEN-<-OF-0))
 (75 35 (:REWRITE MOD-WHEN-<))
 (72 8 (:REWRITE CANCEL-FLOOR-+-BASIC))
 (70 70 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (58 58 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (58 58 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (58 58 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (58 58 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (57 3 (:LINEAR MOD-TYPE . 2))
 (46 46 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (40 26 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (36 4 (:REWRITE FLOOR-OF-+-WHEN-MULT-ARG2))
 (36 4 (:REWRITE FLOOR-OF-+-WHEN-MULT-ARG1))
 (36 2 (:REWRITE FLOOR-TYPE-2))
 (35 35 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (35 35 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (35 35 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (35 35 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (35 35 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (32 4 (:REWRITE MOD-OF-+-WHEN-MULT-ARG1-ALT-CHEAP))
 (24 24 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (24 24 (:LINEAR <-OF-*-AND-*-LINEAR))
 (24 8 (:REWRITE <-OF-/-AND-CONSTANT))
 (24 8 (:LINEAR FLOOR-TYPE-2 . 2))
 (24 8 (:LINEAR FLOOR-TYPE-2 . 1))
 (24 8 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (24 8 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (24 8 (:LINEAR <=-OF-*-OF-/-WHEN-NEGATIVE-AND-POSITIVE-LINEAR))
 (24 8 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NONNEGATIVE-LINEAR))
 (24 8 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NEGATIVE-LINEAR))
 (12 12 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (12 12 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (12 12 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (12 12 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (11 1 (:REWRITE <-OF-FLOOR-AND-0))
 (10 10 (:REWRITE FOLD-CONSTS-IN-+))
 (9 3 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (8 8 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (8 8 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (6 2 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (5 5 (:REWRITE EQUAL-OF-*-AND-CONSTANT))
 (4 4 (:REWRITE MOD-OF-+-SUBST-CONSTANT-ARG2))
 (4 4 (:REWRITE MOD-OF-+-SUBST-CONSTANT-ARG1))
 (4 4 (:REWRITE FLOOR-PEEL-OFF-CONSTANT))
 (4 4 (:REWRITE FLOOR-OF-PLUS-NORMALIZE-NEGATIVE-CONSTANT))
 (3 3 (:LINEAR MOD-TYPE . 3))
 (3 3 (:LINEAR MOD-TYPE . 1))
 (3 3 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (3 1 (:REWRITE <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE))
 (1 1 (:REWRITE <-OF-FLOOR-OF-CONSTANT-AND-CONSTANT-GEN))
 )
(MOD-RECOLLAPSE-LEMMA2
 (364 3 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (276 4 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (98 44 (:REWRITE DEFAULT-<-2))
 (58 44 (:REWRITE DEFAULT-<-1))
 (51 51 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (51 51 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (51 51 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (51 51 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (51 51 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (51 51 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (51 51 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (51 51 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (47 47 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (39 10 (:REWRITE DEFAULT-*-2))
 (36 3 (:REWRITE FLOOR-WHEN-MOD-0-CHEAP))
 (34 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (31 10 (:REWRITE DEFAULT-*-1))
 (30 3 (:REWRITE DEFAULT-+-2))
 (28 3 (:REWRITE FLOOR-=-X/Y . 3))
 (16 16 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (16 16 (:TYPE-PRESCRIPTION RATIONALP-MOD))
 (16 16 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (16 16 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (16 16 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (16 16 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (16 16 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (16 16 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (16 16 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (16 16 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (16 4 (:LINEAR MY-FLOOR-LOWER-BOUND-ALT-LINEAR))
 (16 4 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (16 4 (:LINEAR FLOOR-TYPE-2 . 2))
 (16 4 (:LINEAR FLOOR-TYPE-2 . 1))
 (16 4 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (16 4 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (16 4 (:LINEAR *-OF-FLOOR-UPPER-BOUND-LINEAR))
 (11 3 (:REWRITE FLOOR-=-X/Y . 2))
 (10 2 (:REWRITE MOD-WHEN-MULTIPLE))
 (10 2 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (9 5 (:REWRITE DEFAULT-UNARY-/))
 (9 4 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (8 8 (:LINEAR <-OF-*-AND-*-LINEAR))
 (8 4 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (8 4 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (8 3 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (7 4 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (6 6 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (6 3 (:REWRITE FLOOR-TYPE-4 . 3))
 (6 3 (:REWRITE FLOOR-TYPE-4 . 2))
 (5 3 (:REWRITE FLOOR-WHEN-<))
 (5 3 (:REWRITE FLOOR-TYPE-3 . 3))
 (5 3 (:REWRITE FLOOR-TYPE-3 . 2))
 (5 3 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (4 4 (:REWRITE INTEGERP-OF-*))
 (4 4 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (4 4 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (4 4 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (4 3 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (4 2 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (4 2 (:REWRITE MOD-WHEN-<-OF-0))
 (4 2 (:REWRITE MOD-WHEN-<))
 (3 3 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (3 3 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (3 3 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (3 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (3 2 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (2 2 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (2 2 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (2 1 (:REWRITE EQUAL-OF-0-AND-+-OF--))
 (2 1 (:DEFINITION NOT))
 (1 1 (:REWRITE RATIONALP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (1 1 (:REWRITE RATIONALP-*))
 )
(MOD-RECOLLAPSE-LEMMA
 (715 4 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (275 2 (:REWRITE MOD-OF-+-SUBST-CONSTANT))
 (268 4 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (125 68 (:REWRITE DEFAULT-<-2))
 (121 20 (:REWRITE DEFAULT-+-2))
 (89 48 (:REWRITE DEFAULT-*-2))
 (80 48 (:REWRITE DEFAULT-*-1))
 (77 68 (:REWRITE DEFAULT-<-1))
 (67 5 (:REWRITE DISTRIBUTIVITY))
 (62 62 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 1))
 (62 62 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (62 62 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (62 62 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (62 62 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONNEGATIVE-TYPE))
 (62 62 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (62 62 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (54 54 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (53 6 (:REWRITE CANCEL-FLOOR-+-BASIC))
 (48 4 (:REWRITE FLOOR-WHEN-MOD-0-CHEAP))
 (47 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (37 4 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (33 4 (:REWRITE FLOOR-=-X/Y . 3))
 (31 4 (:REWRITE MOD-WHEN-MULTIPLE))
 (31 4 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (31 4 (:REWRITE FLOOR-=-X/Y . 2))
 (25 25 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (25 25 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (25 25 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (25 25 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (25 25 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (25 25 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (25 25 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (25 25 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (25 25 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (24 2 (:REWRITE MOD-OF-+-WHEN-MULT-ARG1-ALT-CHEAP))
 (22 20 (:REWRITE DEFAULT-+-1))
 (20 16 (:REWRITE DEFAULT-UNARY-/))
 (20 4 (:REWRITE CANCEL-MOD-+-BASIC))
 (19 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (19 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (17 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (16 4 (:LINEAR MY-FLOOR-LOWER-BOUND-ALT-LINEAR))
 (16 4 (:LINEAR MOD-BOUNDED-BY-MODULUS))
 (16 4 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (16 4 (:LINEAR *-OF-FLOOR-UPPER-BOUND-LINEAR))
 (12 4 (:LINEAR FLOOR-UPPER-BOUND-ALT-LINEAR))
 (12 4 (:LINEAR FLOOR-TYPE-2 . 2))
 (12 4 (:LINEAR FLOOR-TYPE-2 . 1))
 (12 4 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (11 3 (:REWRITE FLOOR-OF-+-WHEN-MULT-ARG2))
 (11 3 (:REWRITE FLOOR-OF-+-WHEN-MULT-ARG1))
 (10 10 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (10 10 (:REWRITE INTEGERP-OF-*))
 (10 8 (:REWRITE RATIONALP-+))
 (9 4 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (8 8 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (8 8 (:LINEAR <-OF-*-AND-*-LINEAR))
 (8 4 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (8 4 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (8 4 (:REWRITE MOD-WHEN-<-OF-0))
 (8 4 (:REWRITE MOD-WHEN-<))
 (8 4 (:REWRITE FLOOR-WHEN-<))
 (8 4 (:REWRITE FLOOR-TYPE-4 . 3))
 (8 4 (:REWRITE FLOOR-TYPE-4 . 2))
 (8 4 (:REWRITE FLOOR-TYPE-3 . 3))
 (8 4 (:REWRITE FLOOR-TYPE-3 . 2))
 (8 4 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (8 4 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (8 2 (:LINEAR MOD-TYPE . 4))
 (8 2 (:LINEAR MOD-TYPE . 3))
 (8 2 (:LINEAR MOD-TYPE . 2))
 (8 2 (:LINEAR MOD-TYPE . 1))
 (7 7 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (7 4 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (6 3 (:REWRITE NOT-RATIONALP-RATIONALP-UNARY---PLUS))
 (6 3 (:REWRITE NOT-RATIONALP-RATIONALP-PLUS))
 (5 4 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (5 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (5 4 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (5 4 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (4 4 (:REWRITE RATIONALP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (4 4 (:REWRITE RATIONALP-*))
 (4 4 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (4 4 (:REWRITE FOLD-CONSTS-IN-+))
 (4 4 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (4 4 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (4 4 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (4 4 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (4 4 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (3 3 (:REWRITE FLOOR-PEEL-OFF-CONSTANT))
 (3 3 (:REWRITE FLOOR-OF-PLUS-NORMALIZE-NEGATIVE-CONSTANT))
 (2 2 (:REWRITE MOD-OF-+-SUBST-CONSTANT-ARG2))
 (2 2 (:REWRITE MOD-OF-+-SUBST-CONSTANT-ARG1))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (2 1 (:DEFINITION NOT))
 )
(SAME-REMAINDER-WHEN-CLOSE-HELPER2
 (123 8 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (119 119 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (119 119 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (119 119 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (119 119 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (119 119 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (119 119 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (117 117 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (66 66 (:REWRITE DEFAULT-<-2))
 (66 66 (:REWRITE DEFAULT-<-1))
 (64 8 (:REWRITE MOD-WHEN-MULTIPLE))
 (43 16 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (43 16 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (35 2 (:LINEAR MOD-TYPE . 2))
 (34 16 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (22 22 (:REWRITE DEFAULT-UNARY-MINUS))
 (22 8 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (22 8 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (22 8 (:REWRITE MOD-WHEN-<-OF-0))
 (22 8 (:REWRITE MOD-WHEN-<))
 (20 16 (:REWRITE DEFAULT-UNARY-/))
 (16 16 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (16 16 (:REWRITE INTEGERP-OF-*))
 (16 16 (:REWRITE DEFAULT-*-2))
 (16 16 (:REWRITE DEFAULT-*-1))
 (8 8 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (8 8 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (8 8 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (8 8 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (8 8 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (8 8 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (8 8 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (6 2 (:LINEAR MOD-TYPE . 3))
 (6 2 (:LINEAR MOD-TYPE . 1))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 )
(SAME-REMAINDER-WHEN-CLOSE-HELPER3
 (192 12 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (131 131 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (131 131 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (131 131 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (131 131 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (131 131 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (121 121 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (100 12 (:REWRITE MOD-WHEN-MULTIPLE))
 (97 97 (:REWRITE DEFAULT-<-2))
 (97 97 (:REWRITE DEFAULT-<-1))
 (63 24 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (63 24 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (50 24 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (35 2 (:LINEAR MOD-TYPE . 2))
 (34 12 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (34 12 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (34 12 (:REWRITE MOD-WHEN-<-OF-0))
 (34 12 (:REWRITE MOD-WHEN-<))
 (29 29 (:REWRITE DEFAULT-UNARY-MINUS))
 (29 24 (:REWRITE DEFAULT-UNARY-/))
 (27 9 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (24 24 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (24 24 (:REWRITE INTEGERP-OF-*))
 (24 24 (:REWRITE DEFAULT-*-2))
 (24 24 (:REWRITE DEFAULT-*-1))
 (18 18 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (12 12 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (12 12 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (12 12 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (6 2 (:LINEAR MOD-TYPE . 3))
 (6 2 (:LINEAR MOD-TYPE . 1))
 (6 2 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR MOD-BOUND-LINEAR-ARG2-STRONG))
 )
(SAME-REMAINDER-WHEN-CLOSE
 (245 14 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (231 231 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE-2))
 (231 231 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (231 231 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (231 231 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (231 231 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (231 231 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (231 231 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (231 231 (:TYPE-PRESCRIPTION INTEGERP-MOD))
 (126 14 (:REWRITE MOD-WHEN-MULTIPLE))
 (115 115 (:REWRITE DEFAULT-<-2))
 (115 115 (:REWRITE DEFAULT-<-1))
 (84 21 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (70 28 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (70 28 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (56 28 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (47 47 (:REWRITE DEFAULT-UNARY-MINUS))
 (42 14 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (42 14 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (42 14 (:REWRITE MOD-WHEN-<-OF-0))
 (42 14 (:REWRITE MOD-WHEN-<))
 (35 28 (:REWRITE DEFAULT-UNARY-/))
 (28 28 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (28 28 (:REWRITE INTEGERP-OF-*))
 (28 28 (:REWRITE DEFAULT-*-2))
 (28 28 (:REWRITE DEFAULT-*-1))
 (24 24 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (14 14 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (14 14 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (14 14 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (14 14 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (14 14 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (12 12 (:REWRITE DEFAULT-+-2))
 (12 12 (:REWRITE DEFAULT-+-1))
 )
(SAME-REMAINDER-WHEN-CLOSE-LEMMA
 (6297 26 (:REWRITE *-OF-FLOOR-OF-SAME-WHEN-MULTIPLE))
 (4864 132 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 2))
 (2097 29 (:LINEAR <-OF-*-SAME-LINEAR-SPECIAL))
 (1818 28 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-2))
 (1516 132 (:REWRITE MOD-X-Y-=-X-FOR-RATIONALS . 3))
 (1061 980 (:REWRITE DEFAULT-<-1))
 (1052 980 (:REWRITE DEFAULT-<-2))
 (759 91 (:REWRITE FLOOR-WHEN-MOD-0-CHEAP))
 (737 449 (:REWRITE DEFAULT-*-2))
 (691 131 (:REWRITE MOD-WHEN-MULTIPLE))
 (691 131 (:REWRITE MOD-WHEN-INTEGERP-OF-QUOTIENT))
 (634 12 (:LINEAR MY-FLOOR-LOWER-BOUND-LINEAR))
 (622 12 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR-1))
 (622 12 (:LINEAR FLOOR-UPPER-BOUND-LINEAR))
 (603 297 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-2))
 (576 297 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-MIXED-1))
 (554 12 (:LINEAR FLOOR-BOUND-ARG1-LINEAR))
 (525 525 (:TYPE-PRESCRIPTION FLOOR-TYPE-3 . 2))
 (525 525 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONPOSITIVE-AND-NONNEGATIVE-TYPE))
 (525 525 (:TYPE-PRESCRIPTION <=-OF-FLOOR-AND-0-WHEN-NONNEGATIVE-AND-NONPOSITIVE-TYPE))
 (525 525 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-POSITIVE-AND-NEGATIVE-TYPE))
 (525 525 (:TYPE-PRESCRIPTION <-OF-FLOOR-AND-0-WHEN-NEGATIVE-AND-POSITIVE-TYPE))
 (523 523 (:TYPE-PRESCRIPTION <=-OF-0-AND-FLOOR-WHEN-BOTH-NONPOSITIVE-TYPE))
 (519 77 (:REWRITE FLOOR-=-X/Y . 3))
 (515 23 (:LINEAR MOD-BOUND-LINEAR-ARG1))
 (485 449 (:REWRITE DEFAULT-*-1))
 (483 297 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-<-AND-NEGATIVE-ALT))
 (445 58 (:LINEAR <=-OF-*-AND-*-SAME-LINEAR))
 (381 356 (:REWRITE DEFAULT-UNARY-/))
 (374 1 (:REWRITE <-OF-*-AND-0))
 (362 362 (:TYPE-PRESCRIPTION MOD-TYPE . 4))
 (362 362 (:TYPE-PRESCRIPTION MOD-TYPE . 3))
 (362 362 (:TYPE-PRESCRIPTION MOD-TYPE . 2))
 (362 362 (:TYPE-PRESCRIPTION MOD-TYPE . 1))
 (345 345 (:TYPE-PRESCRIPTION NONNEG-OF-MOD-TYPE))
 (345 1 (:REWRITE <-OF-*-SAME-ARG3))
 (333 23 (:LINEAR MOD-TYPE . 2))
 (297 297 (:REWRITE INTEGERP-OF-*-OF-/-WHEN-RATIONALP-AND-COMPLEX-RATIONALP))
 (297 297 (:REWRITE INTEGERP-OF-*))
 (271 131 (:REWRITE MOD-WHEN-<))
 (253 131 (:REWRITE MOD-WHEN-<-OF-0))
 (253 77 (:REWRITE FLOOR-=-X/Y . 2))
 (220 202 (:REWRITE DEFAULT-UNARY-MINUS))
 (211 79 (:REWRITE FLOOR-TYPE-4 . 3))
 (172 14 (:LINEAR FLOOR-TYPE-2 . 1))
 (163 79 (:REWRITE FLOOR-TYPE-4 . 2))
 (152 20 (:REWRITE MOD-=-0 . 1))
 (143 79 (:REWRITE FLOOR-TYPE-3 . 3))
 (139 79 (:REWRITE FLOOR-TYPE-3 . 2))
 (131 131 (:REWRITE MOD-WHEN-RATIONALP-ARG1-AND-NOT-RATIONALP-ARG2))
 (131 131 (:REWRITE MOD-WHEN-NOT-RATIONALP-ARG1-AND-RATIONALP-ARG2))
 (131 131 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG2))
 (131 131 (:REWRITE MOD-WHEN-NOT-ACL2-NUMBERP-ARG1))
 (131 131 (:REWRITE MOD-WHEN-EQUAL-OF-MOD-AND-0-FREE-CHEAP))
 (126 45 (:REWRITE DEFAULT-+-2))
 (121 77 (:REWRITE FLOOR-WHEN-<))
 (116 116 (:LINEAR <=-OF-/-LINEAR))
 (110 12 (:LINEAR FLOOR-BOUND-STRICT-LINEAR))
 (99 1 (:REWRITE DISTRIBUTIVITY))
 (88 22 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NONNEGATIVE-LINEAR))
 (77 77 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-OF-QUOTIENT))
 (77 77 (:REWRITE FLOOR-WHEN-NOT-RATIONALP-ARG1))
 (77 77 (:REWRITE FLOOR-WHEN-NEGATIVE-AND-SMALL-CHEAP))
 (77 77 (:REWRITE FLOOR-WHEN-I-IS-NOT-AN-ACL2-NUMBERP))
 (77 77 (:REWRITE FLOOR-MINUS-NEGATIVE-CONSTANT))
 (70 52 (:REWRITE EQUAL-OF-BOOLEANS-CHEAP))
 (69 23 (:REWRITE <-OF-/-AND-CONSTANT))
 (69 23 (:LINEAR MOD-TYPE . 3))
 (69 23 (:LINEAR MOD-TYPE . 1))
 (66 22 (:LINEAR <=-OF-*-OF-/-WHEN-NEGATIVE-AND-POSITIVE-LINEAR))
 (63 45 (:REWRITE DEFAULT-+-1))
 (62 4 (:REWRITE FLOOR-TYPE-2))
 (58 58 (:LINEAR <=-OF-*-AND-*-SAME-ALT-LINEAR))
 (58 58 (:LINEAR <-OF-*-AND-*-LINEAR))
 (44 22 (:LINEAR <=-OF-*-OF-/-WHEN-BOTH-NEGATIVE-LINEAR))
 (42 14 (:LINEAR FLOOR-TYPE-2 . 2))
 (35 35 (:TYPE-PRESCRIPTION INTEGERP-OF-MOD-TYPE))
 (35 35 (:REWRITE <-OF-/-AND-0))
 (35 35 (:REWRITE /-EQUAL-CONSTANT-ALT))
 (34 1 (:REWRITE *-OF---ARG2))
 (28 28 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-4))
 (28 28 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-3))
 (28 28 (:LINEAR <-OF-*-AND-*-SAME-LINEAR-1))
 (24 24 (:TYPE-PRESCRIPTION RATIONALP-OF-MOD))
 (12 12 (:REWRITE *-OF-0))
 (12 12 (:LINEAR FLOOR-WEAK-MONOTONE-LINEAR=-2))
 (2 2 (:REWRITE EQUAL-OF-*-AND-CONSTANT))
 (2 2 (:REWRITE <-OF-CONSTANT-AND-*-OF-CONSTANT))
 (1 1 (:REWRITE <-OF-FLOOR-OF-CONSTANT-AND-CONSTANT-GEN))
 (1 1 (:REWRITE *-OF-*-COMBINE-CONSTANTS))
 )
