(ACL2S::ACL2S-INTEGER-LIST-UNDEFINED-INTEGER-LISTP)
(ACL2S::MERGE2-CONTRACT
 (63 63 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (35 35 (:REWRITE DEFAULT-CAR))
 (35 35 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (25 25 (:REWRITE DEFAULT-CDR))
 (20 20 (:REWRITE REDUCE-INTEGERP-+))
 (20 20 (:REWRITE INTEGERP-MINUS-X))
 (20 20 (:META META-INTEGERP-CORRECT))
 (13 13 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (13 13 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (13 13 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (13 13 (:REWRITE CONSP-BY-LEN))
 (4 4 (:REWRITE THE-FLOOR-BELOW))
 (4 4 (:REWRITE THE-FLOOR-ABOVE))
 (4 4 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (4 4 (:REWRITE DEFAULT-LESS-THAN-2))
 (4 4 (:REWRITE DEFAULT-LESS-THAN-1))
 (3 3 (:REWRITE SIMPLIFY-SUMS-<))
 (3 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3 3 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (3 3 (:REWRITE INTEGERP-<-CONSTANT))
 (3 3 (:REWRITE CONSTANT-<-INTEGERP))
 (3 3 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (3 3 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (3 3 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (3 3 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (3 3 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (3 3 (:REWRITE |(< c (- x))|))
 (3 3 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (3 3 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (3 3 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (3 3 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (3 3 (:REWRITE |(< (/ x) (/ y))|))
 (3 3 (:REWRITE |(< (- x) c)|))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:REWRITE CONSP-OF-CDR-BY-LEN))
 )
(ACL2S::MERGE2-CONTRACT-TP)
(ACL2S::MERGE2-CONTRACT-GENRULE)
(ACL2S::MERGE2)
(ACL2S::MERGE2-INDUCTION-SCHEME)
(ACL2S::MERGE2-DEFINITION-RULE)
(ACL2S::EVENS-POLYMORPHIC-SIG
 (1031 170 (:REWRITE ACL2S::CDR-POLYMORPHIC-SIG))
 (467 401 (:REWRITE DEFAULT-CDR))
 (223 214 (:REWRITE DEFAULT-CAR))
 (214 214 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (59 59 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (59 59 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (59 59 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (59 59 (:REWRITE CONSP-BY-LEN))
 (33 33 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (15 15 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 )
(ACL2S::EVENS-L-STR-ALLP-SIG
 (67 10 (:REWRITE ACL2S::CDR-L-STR-ALLP-SIG))
 (16 16 (:REWRITE ACL2S::DEF=>L-STR-ALL))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 )
(ACL2S::EVENS-TRUE-LIST-LISTP-SIG
 (6663 8 (:DEFINITION TRUE-LISTP))
 (2733 8 (:REWRITE ACL2S::CDR-TRUE-LISTP-SIG))
 (1986 42 (:DEFINITION NAT-LISTP))
 (1728 21 (:REWRITE ACL2S::CDR-TRUE-LIST-LISTP-SIG))
 (1386 42 (:DEFINITION NATP))
 (1234 26 (:REWRITE DEFDATA::NAT-LISTP--TRUE-LISTP))
 (964 26 (:REWRITE ACL2S::NAT-LISTP-IMPLIES-TLP))
 (958 26 (:REWRITE ACL2S::POS-LISTP-IMPLIES-TLP))
 (910 26 (:REWRITE ACL2S::PROPER-SYMBOL-LISTP-IMPLIES-TLP))
 (858 18 (:DEFINITION ACL2S::POS-LISTP))
 (810 18 (:DEFINITION ACL2S::PROPER-SYMBOL-LISTP))
 (802 26 (:REWRITE ACL2S::KEYWORD-LISTP-IMPLIES-TLP))
 (796 26 (:REWRITE ACL2S::L-STR-ALLP-IMPLIES-TLP))
 (744 36 (:DEFINITION KEYWORDP))
 (730 26 (:REWRITE ACL2S::BOOLEAN-LISTP-IMPLIES-TLP))
 (702 18 (:DEFINITION ACL2S::KEYWORD-LISTP))
 (696 18 (:DEFINITION ACL2S::L-STR-ALLP))
 (630 18 (:DEFINITION BOOLEAN-LISTP))
 (576 18 (:DEFINITION POSP))
 (550 26 (:REWRITE ACL2S::ATOM-LISTP-IMPLIES-TLP))
 (523 26 (:REWRITE ACL2S::TRUE-LIST-LISTP-IMPLIES-TLP))
 (504 252 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (502 26 (:REWRITE ACL2S::SYMBOL-LISTP-IMPLIES-TLP))
 (492 18 (:DEFINITION ACL2S::PROPER-SYMBOLP))
 (460 26 (:REWRITE ACL2S::RATIONAL-LISTP-IMPLIES-TLP))
 (450 18 (:DEFINITION ATOM-LISTP))
 (424 26 (:REWRITE ACL2S::INTEGER-LISTP-IMPLIES-TLP))
 (414 18 (:DEFINITION ACL2S::STR-ALLP))
 (388 26 (:REWRITE ACL2S::ACL2-NUMBER-LISTP-IMPLIES-TLP))
 (382 26 (:REWRITE ACL2S::COMPLEX-RATIONAL-LISTP-IMPLIES-TLP))
 (370 26 (:REWRITE ACL2S::STRING-LISTP-IMPLIES-TLP))
 (366 54 (:REWRITE ACL2S::CDR-NAT-LISTP-SIG))
 (366 18 (:DEFINITION SYMBOL-LISTP))
 (360 18 (:DEFINITION RATIONAL-LISTP))
 (352 352 (:REWRITE DEFAULT-CDR))
 (324 18 (:DEFINITION INTEGER-LISTP))
 (307 307 (:REWRITE DEFAULT-CAR))
 (307 307 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (297 136 (:REWRITE CONSP-OF-CAR-WHEN-ALISTP))
 (288 18 (:DEFINITION ACL2-NUMBER-LISTP))
 (282 18 (:DEFINITION ACL2S::COMPLEX-RATIONAL-LISTP))
 (274 274 (:TYPE-PRESCRIPTION NAT-LISTP))
 (270 18 (:DEFINITION STRING-LISTP))
 (252 252 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (252 252 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (252 252 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (252 252 (:REWRITE CONSP-BY-LEN))
 (234 234 (:TYPE-PRESCRIPTION STRINGP-SYMBOL-PACKAGE-NAME))
 (227 26 (:REWRITE TRUE-LISTP-WHEN-ATOM))
 (222 136 (:REWRITE O-P-O-INFP-CAR))
 (176 176 (:TYPE-PRESCRIPTION BOOLEAN-LISTP))
 (124 26 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (122 122 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (122 122 (:TYPE-PRESCRIPTION STRING-LISTP))
 (122 122 (:TYPE-PRESCRIPTION RATIONAL-LISTP))
 (122 122 (:TYPE-PRESCRIPTION ACL2S::PROPER-SYMBOL-LISTP))
 (122 122 (:TYPE-PRESCRIPTION ACL2S::POS-LISTP))
 (122 122 (:TYPE-PRESCRIPTION ACL2S::L-STR-ALLP))
 (122 122 (:TYPE-PRESCRIPTION ACL2S::KEYWORD-LISTP))
 (122 122 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (122 122 (:TYPE-PRESCRIPTION ACL2S::COMPLEX-RATIONAL-LISTP))
 (122 122 (:TYPE-PRESCRIPTION ATOM-LISTP))
 (122 122 (:TYPE-PRESCRIPTION ACL2-NUMBER-LISTP))
 (113 113 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (108 108 (:REWRITE SYMBOLP-OF-CAR-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP))
 (92 92 (:TYPE-PRESCRIPTION ALISTP))
 (92 55 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (92 55 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (84 84 (:REWRITE ACL2S::DEF=>NAT-LIST))
 (84 42 (:REWRITE ACL2S::CDR-BOOLEAN-LISTP-SIG))
 (80 80 (:TYPE-PRESCRIPTION O-P))
 (78 78 (:REWRITE REDUCE-INTEGERP-+))
 (78 78 (:REWRITE INTEGERP-MINUS-X))
 (78 78 (:META META-INTEGERP-CORRECT))
 (72 36 (:REWRITE SYMBOLP-OF-CAAR-WHEN-SYMBOL-SYMBOL-ALISTP))
 (72 36 (:REWRITE DEFDATA::PROPER-SYMBOL-LISTP-IS-SYMBOL-LIST))
 (60 60 (:REWRITE THE-FLOOR-BELOW))
 (60 60 (:REWRITE THE-FLOOR-ABOVE))
 (60 60 (:REWRITE SIMPLIFY-SUMS-<))
 (60 60 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (60 60 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (60 60 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (60 60 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (60 60 (:REWRITE INTEGERP-<-CONSTANT))
 (60 60 (:REWRITE DEFAULT-LESS-THAN-2))
 (60 60 (:REWRITE DEFAULT-LESS-THAN-1))
 (60 60 (:REWRITE CONSTANT-<-INTEGERP))
 (60 60 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (60 60 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (60 60 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (60 60 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (60 60 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (60 60 (:REWRITE |(< c (- x))|))
 (60 60 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (60 60 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (60 60 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (60 60 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (60 60 (:REWRITE |(< (/ x) (/ y))|))
 (60 60 (:REWRITE |(< (- x) c)|))
 (60 60 (:REWRITE |(< (- x) (- y))|))
 (56 55 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (55 55 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (55 55 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (55 55 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (55 55 (:REWRITE |(equal c (/ x))|))
 (55 55 (:REWRITE |(equal c (- x))|))
 (55 55 (:REWRITE |(equal (/ x) c)|))
 (55 55 (:REWRITE |(equal (/ x) (/ y))|))
 (55 55 (:REWRITE |(equal (- x) c)|))
 (55 55 (:REWRITE |(equal (- x) (- y))|))
 (54 54 (:TYPE-PRESCRIPTION LEGAL-CONSTANTP))
 (54 54 (:REWRITE ACL2S::DEF=>BOOLEAN-LIST))
 (48 24 (:REWRITE ACL2S::CDR-SYMBOL-LISTP-SIG))
 (48 24 (:REWRITE ACL2S::CDR-STRING-LISTP-SIG))
 (48 24 (:REWRITE ACL2S::CDR-RATIONAL-LISTP-SIG))
 (48 24 (:REWRITE ACL2S::CDR-PROPER-SYMBOL-LISTP-SIG))
 (48 24 (:REWRITE ACL2S::CDR-POS-LISTP-SIG))
 (48 24 (:REWRITE ACL2S::CDR-L-STR-ALLP-SIG))
 (48 24 (:REWRITE ACL2S::CDR-KEYWORD-LISTP-SIG))
 (48 24 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (48 24 (:REWRITE ACL2S::CDR-COMPLEX-RATIONAL-LISTP-SIG))
 (48 24 (:REWRITE ACL2S::CDR-ATOM-LISTP-SIG))
 (48 24 (:REWRITE ACL2S::CDR-ACL2-NUMBER-LISTP-SIG))
 (44 44 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (42 42 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (42 42 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (42 42 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (42 42 (:REWRITE |(< (/ x) 0)|))
 (42 42 (:REWRITE |(< (* x y) 0)|))
 (39 12 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (37 37 (:REWRITE ACL2S::DEF=>TRUE-LIST-LIST))
 (36 36 (:TYPE-PRESCRIPTION DEFDATA::PROPER-SYMBOL-LISTP))
 (36 36 (:REWRITE DEFAULT-SYMBOL-PACKAGE-NAME))
 (36 36 (:REWRITE ACL2S::DEF=>SYMBOL-LIST))
 (36 36 (:REWRITE ACL2S::DEF=>STRING-LIST))
 (36 36 (:REWRITE ACL2S::DEF=>RATIONAL-LIST))
 (36 36 (:REWRITE ACL2S::DEF=>PROPER-SYMBOL-LIST))
 (36 36 (:REWRITE ACL2S::DEF=>POS-LIST))
 (36 36 (:REWRITE ACL2S::DEF=>L-STR-ALL))
 (36 36 (:REWRITE ACL2S::DEF=>KEYWORD-LIST))
 (36 36 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (36 36 (:REWRITE ACL2S::DEF=>COMPLEX-RATIONAL-LIST))
 (36 36 (:REWRITE ACL2S::DEF=>ATOM-LIST))
 (36 36 (:REWRITE ACL2S::DEF=>ACL2-NUMBER-LIST))
 (36 18 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (27 3 (:REWRITE ACL2S::CDR-ALISTOF-ALISTP-SIG))
 (26 26 (:REWRITE TRUE-LISTP-WHEN-THEOREM-SYMBOL-LISTP))
 (26 26 (:REWRITE TRUE-LISTP-WHEN-TERMFN-LISTP))
 (26 26 (:REWRITE TRUE-LISTP-WHEN-MACRO-SYMBOL-LISTP))
 (26 26 (:REWRITE TRUE-LISTP-WHEN-LAMBDA-LISTP))
 (26 26 (:REWRITE TRUE-LISTP-WHEN-FUNCTION-SYMBOL-LISTP))
 (18 18 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (18 18 (:TYPE-PRESCRIPTION SET::EMPTYP-TYPE))
 (18 18 (:TYPE-PRESCRIPTION BOOLEANP))
 (18 18 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (18 18 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (18 18 (:REWRITE REDUCE-RATIONALP-+))
 (18 18 (:REWRITE REDUCE-RATIONALP-*))
 (18 18 (:REWRITE RATIONALP-X))
 (18 18 (:REWRITE RATIONALP-MINUS-X))
 (18 18 (:REWRITE SET::IN-SET))
 (18 18 (:REWRITE ACL2-NUMBERP-X))
 (18 18 (:REWRITE |(< 0 (/ x))|))
 (18 18 (:REWRITE |(< 0 (* x y))|))
 (18 18 (:META META-RATIONALP-CORRECT))
 (18 3 (:REWRITE ALISTP-OF-CDR))
 (12 12 (:REWRITE ACL2S::DEF=>ALIST))
 (12 12 (:REWRITE ALISTP-WHEN-ATOM))
 (9 9 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (6 6 (:REWRITE O-P-DEF-O-FINP-1))
 )
(ACL2S::EVENS-TRUE-LISTP-SIG
 (10627 22 (:REWRITE ACL2S::CDR-TRUE-LISTP-SIG))
 (3742 63 (:DEFINITION NAT-LISTP))
 (2633 56 (:REWRITE DEFDATA::NAT-LISTP--TRUE-LISTP))
 (2201 56 (:REWRITE ACL2S::TRUE-LIST-LISTP-IMPLIES-TLP))
 (2123 22 (:DEFINITION TRUE-LIST-LISTP))
 (2079 63 (:DEFINITION NATP))
 (1443 56 (:REWRITE ACL2S::NAT-LISTP-IMPLIES-TLP))
 (1415 56 (:REWRITE ACL2S::POS-LISTP-IMPLIES-TLP))
 (1342 106 (:REWRITE ACL2S::CDR-NAT-LISTP-SIG))
 (1321 56 (:REWRITE ACL2S::PROPER-SYMBOL-LISTP-IMPLIES-TLP))
 (1275 56 (:REWRITE ACL2S::BOOLEAN-LISTP-IMPLIES-TLP))
 (1257 22 (:DEFINITION ACL2S::POS-LISTP))
 (1187 56 (:REWRITE ACL2S::L-STR-ALLP-IMPLIES-TLP))
 (1163 22 (:DEFINITION ACL2S::PROPER-SYMBOL-LISTP))
 (1135 56 (:REWRITE ACL2S::KEYWORD-LISTP-IMPLIES-TLP))
 (1117 28 (:DEFINITION BOOLEAN-LISTP))
 (1029 22 (:DEFINITION ACL2S::L-STR-ALLP))
 (977 22 (:DEFINITION ACL2S::KEYWORD-LISTP))
 (880 44 (:DEFINITION KEYWORDP))
 (793 56 (:REWRITE ACL2S::ATOM-LISTP-IMPLIES-TLP))
 (704 22 (:DEFINITION POSP))
 (660 330 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (657 56 (:REWRITE ACL2S::SYMBOL-LISTP-IMPLIES-TLP))
 (653 56 (:REWRITE ACL2S::RATIONAL-LISTP-IMPLIES-TLP))
 (635 22 (:DEFINITION ATOM-LISTP))
 (597 56 (:REWRITE ACL2S::INTEGER-LISTP-IMPLIES-TLP))
 (591 591 (:REWRITE DEFAULT-CDR))
 (584 584 (:REWRITE DEFAULT-CAR))
 (584 584 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (572 22 (:DEFINITION ACL2S::PROPER-SYMBOLP))
 (541 56 (:REWRITE ACL2S::ACL2-NUMBER-LISTP-IMPLIES-TLP))
 (513 56 (:REWRITE ACL2S::STRING-LISTP-IMPLIES-TLP))
 (513 56 (:REWRITE ACL2S::COMPLEX-RATIONAL-LISTP-IMPLIES-TLP))
 (506 22 (:DEFINITION ACL2S::STR-ALLP))
 (495 22 (:DEFINITION RATIONAL-LISTP))
 (467 22 (:DEFINITION SYMBOL-LISTP))
 (439 22 (:DEFINITION INTEGER-LISTP))
 (428 428 (:TYPE-PRESCRIPTION NAT-LISTP))
 (383 22 (:DEFINITION ACL2-NUMBER-LISTP))
 (364 364 (:TYPE-PRESCRIPTION STRINGP-SYMBOL-PACKAGE-NAME))
 (355 22 (:DEFINITION STRING-LISTP))
 (355 22 (:DEFINITION ACL2S::COMPLEX-RATIONAL-LISTP))
 (330 330 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (330 330 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (330 330 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (330 330 (:REWRITE CONSP-BY-LEN))
 (290 290 (:TYPE-PRESCRIPTION BOOLEAN-LISTP))
 (228 228 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (176 56 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (170 170 (:TYPE-PRESCRIPTION TRUE-LIST-LISTP))
 (170 170 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (170 170 (:TYPE-PRESCRIPTION STRING-LISTP))
 (170 170 (:TYPE-PRESCRIPTION RATIONAL-LISTP))
 (170 170 (:TYPE-PRESCRIPTION ACL2S::PROPER-SYMBOL-LISTP))
 (170 170 (:TYPE-PRESCRIPTION ACL2S::POS-LISTP))
 (170 170 (:TYPE-PRESCRIPTION ACL2S::L-STR-ALLP))
 (170 170 (:TYPE-PRESCRIPTION ACL2S::KEYWORD-LISTP))
 (170 170 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (170 170 (:TYPE-PRESCRIPTION ACL2S::COMPLEX-RATIONAL-LISTP))
 (170 170 (:TYPE-PRESCRIPTION ATOM-LISTP))
 (170 170 (:TYPE-PRESCRIPTION ACL2-NUMBER-LISTP))
 (168 168 (:REWRITE SYMBOLP-OF-CAR-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP))
 (156 78 (:REWRITE ACL2S::CDR-BOOLEAN-LISTP-SIG))
 (148 91 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (148 91 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (139 139 (:REWRITE REDUCE-INTEGERP-+))
 (139 139 (:REWRITE INTEGERP-MINUS-X))
 (139 139 (:META META-INTEGERP-CORRECT))
 (136 68 (:REWRITE O-P-O-INFP-CAR))
 (136 68 (:REWRITE CONSP-OF-CAR-WHEN-ALISTP))
 (126 126 (:REWRITE ACL2S::DEF=>NAT-LIST))
 (121 56 (:REWRITE TRUE-LISTP-WHEN-ATOM))
 (111 111 (:REWRITE THE-FLOOR-BELOW))
 (111 111 (:REWRITE THE-FLOOR-ABOVE))
 (111 111 (:REWRITE SIMPLIFY-SUMS-<))
 (111 111 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (111 111 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (111 111 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (111 111 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (111 111 (:REWRITE INTEGERP-<-CONSTANT))
 (111 111 (:REWRITE DEFAULT-LESS-THAN-2))
 (111 111 (:REWRITE DEFAULT-LESS-THAN-1))
 (111 111 (:REWRITE CONSTANT-<-INTEGERP))
 (111 111 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (111 111 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (111 111 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (111 111 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (111 111 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (111 111 (:REWRITE |(< c (- x))|))
 (111 111 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (111 111 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (111 111 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (111 111 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (111 111 (:REWRITE |(< (/ x) (/ y))|))
 (111 111 (:REWRITE |(< (- x) c)|))
 (111 111 (:REWRITE |(< (- x) (- y))|))
 (92 91 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (91 91 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (91 91 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (91 91 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (91 91 (:REWRITE |(equal c (/ x))|))
 (91 91 (:REWRITE |(equal c (- x))|))
 (91 91 (:REWRITE |(equal (/ x) c)|))
 (91 91 (:REWRITE |(equal (/ x) (/ y))|))
 (91 91 (:REWRITE |(equal (- x) c)|))
 (91 91 (:REWRITE |(equal (- x) (- y))|))
 (88 44 (:REWRITE DEFDATA::PROPER-SYMBOL-LISTP-IS-SYMBOL-LIST))
 (84 84 (:TYPE-PRESCRIPTION LEGAL-CONSTANTP))
 (84 84 (:REWRITE ACL2S::DEF=>BOOLEAN-LIST))
 (83 83 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (83 83 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (83 83 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (83 83 (:REWRITE |(< (/ x) 0)|))
 (83 83 (:REWRITE |(< (* x y) 0)|))
 (76 38 (:REWRITE ACL2S::CDR-TRUE-LIST-LISTP-SIG))
 (76 38 (:REWRITE ACL2S::CDR-SYMBOL-LISTP-SIG))
 (76 38 (:REWRITE ACL2S::CDR-STRING-LISTP-SIG))
 (76 38 (:REWRITE ACL2S::CDR-RATIONAL-LISTP-SIG))
 (76 38 (:REWRITE ACL2S::CDR-PROPER-SYMBOL-LISTP-SIG))
 (76 38 (:REWRITE ACL2S::CDR-POS-LISTP-SIG))
 (76 38 (:REWRITE ACL2S::CDR-L-STR-ALLP-SIG))
 (76 38 (:REWRITE ACL2S::CDR-KEYWORD-LISTP-SIG))
 (76 38 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (76 38 (:REWRITE ACL2S::CDR-COMPLEX-RATIONAL-LISTP-SIG))
 (76 38 (:REWRITE ACL2S::CDR-ATOM-LISTP-SIG))
 (76 38 (:REWRITE ACL2S::CDR-ACL2-NUMBER-LISTP-SIG))
 (72 72 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (68 68 (:TYPE-PRESCRIPTION O-P))
 (68 68 (:TYPE-PRESCRIPTION ALISTP))
 (56 56 (:REWRITE TRUE-LISTP-WHEN-THEOREM-SYMBOL-LISTP))
 (56 56 (:REWRITE TRUE-LISTP-WHEN-TERMFN-LISTP))
 (56 56 (:REWRITE TRUE-LISTP-WHEN-MACRO-SYMBOL-LISTP))
 (56 56 (:REWRITE TRUE-LISTP-WHEN-LAMBDA-LISTP))
 (56 56 (:REWRITE TRUE-LISTP-WHEN-FUNCTION-SYMBOL-LISTP))
 (56 56 (:REWRITE DEFAULT-SYMBOL-PACKAGE-NAME))
 (48 48 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (44 44 (:TYPE-PRESCRIPTION DEFDATA::PROPER-SYMBOL-LISTP))
 (44 44 (:REWRITE ACL2S::DEF=>TRUE-LIST-LIST))
 (44 44 (:REWRITE ACL2S::DEF=>SYMBOL-LIST))
 (44 44 (:REWRITE ACL2S::DEF=>STRING-LIST))
 (44 44 (:REWRITE ACL2S::DEF=>RATIONAL-LIST))
 (44 44 (:REWRITE ACL2S::DEF=>PROPER-SYMBOL-LIST))
 (44 44 (:REWRITE ACL2S::DEF=>POS-LIST))
 (44 44 (:REWRITE ACL2S::DEF=>L-STR-ALL))
 (44 44 (:REWRITE ACL2S::DEF=>KEYWORD-LIST))
 (44 44 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (44 44 (:REWRITE ACL2S::DEF=>COMPLEX-RATIONAL-LIST))
 (44 44 (:REWRITE ACL2S::DEF=>ATOM-LIST))
 (44 44 (:REWRITE ACL2S::DEF=>ACL2-NUMBER-LIST))
 (32 16 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (28 28 (:TYPE-PRESCRIPTION BOOLEANP))
 (28 28 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (28 28 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (28 28 (:REWRITE REDUCE-RATIONALP-+))
 (28 28 (:REWRITE REDUCE-RATIONALP-*))
 (28 28 (:REWRITE RATIONALP-X))
 (28 28 (:REWRITE RATIONALP-MINUS-X))
 (28 28 (:REWRITE ACL2-NUMBERP-X))
 (28 28 (:REWRITE |(< 0 (/ x))|))
 (28 28 (:REWRITE |(< 0 (* x y))|))
 (28 28 (:META META-RATIONALP-CORRECT))
 (16 16 (:TYPE-PRESCRIPTION SET::EMPTYP-TYPE))
 (16 16 (:REWRITE SET::IN-SET))
 )
(ACL2S::EVENS-ATOM-LISTP-SIG
 (98 10 (:REWRITE ACL2S::CDR-ATOM-LISTP-SIG))
 (90 5 (:REWRITE CONSP-OF-CAR-WHEN-ALISTP))
 (35 11 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (27 3 (:REWRITE ACL2S::CDR-ALISTOF-ALISTP-SIG))
 (22 22 (:TYPE-PRESCRIPTION ALISTP))
 (22 11 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (20 5 (:REWRITE O-P-O-INFP-CAR))
 (18 3 (:REWRITE ALISTP-OF-CDR))
 (16 16 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (16 16 (:REWRITE ACL2S::DEF=>ATOM-LIST))
 (11 11 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (11 11 (:REWRITE ACL2S::DEF=>ALIST))
 (11 11 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (11 11 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (11 11 (:REWRITE CONSP-BY-LEN))
 (11 11 (:REWRITE ALISTP-WHEN-ATOM))
 (10 10 (:TYPE-PRESCRIPTION O-P))
 (8 8 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (5 5 (:REWRITE O-P-DEF-O-FINP-1))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (1 1 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE |(equal c (/ x))|))
 (1 1 (:REWRITE |(equal c (- x))|))
 (1 1 (:REWRITE |(equal (/ x) c)|))
 (1 1 (:REWRITE |(equal (/ x) (/ y))|))
 (1 1 (:REWRITE |(equal (- x) c)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ACL2S::EVENS-STRING-LISTP-SIG
 (64 10 (:REWRITE ACL2S::CDR-STRING-LISTP-SIG))
 (16 16 (:REWRITE ACL2S::DEF=>STRING-LIST))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (1 1 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE |(equal c (/ x))|))
 (1 1 (:REWRITE |(equal c (- x))|))
 (1 1 (:REWRITE |(equal (/ x) c)|))
 (1 1 (:REWRITE |(equal (/ x) (/ y))|))
 (1 1 (:REWRITE |(equal (- x) c)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ACL2S::EVENS-STANDARD-CHAR-LISTP-SIG
 (73 10 (:REWRITE ACL2S::CDR-STANDARD-CHAR-LISTP-SIG))
 (16 16 (:REWRITE ACL2S::DEF=>STANDARD-CHAR-LIST))
 (14 14 (:REWRITE DEFAULT-CAR))
 (14 14 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (3 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (3 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (3 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (1 1 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE |(equal c (/ x))|))
 (1 1 (:REWRITE |(equal c (- x))|))
 (1 1 (:REWRITE |(equal (/ x) c)|))
 (1 1 (:REWRITE |(equal (/ x) (/ y))|))
 (1 1 (:REWRITE |(equal (- x) c)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ACL2S::EVENS-CHARACTER-LISTP-SIG
 (304 10 (:REWRITE ACL2S::CDR-CHARACTER-LISTP-SIG))
 (148 16 (:REWRITE STR::CHARACTER-LISTP-WHEN-OCT-DIGIT-CHAR-LIST*P))
 (148 16 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LIST*P))
 (116 16 (:REWRITE STR::CHARACTER-LISTP-WHEN-DEC-DIGIT-CHAR-LIST*P))
 (32 32 (:REWRITE STR::OCT-DIGIT-CHAR-LIST*P-WHEN-SUBSETP-EQUAL))
 (32 32 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-SUBSETP-EQUAL))
 (32 16 (:REWRITE STR::OCT-DIGIT-CHAR-LIST*P-WHEN-OCT-DIGIT-CHAR-LISTP))
 (32 16 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-HEX-DIGIT-CHAR-LISTP))
 (32 16 (:REWRITE STR::DEC-DIGIT-CHAR-LIST*P-WHEN-DEC-DIGIT-CHAR-LISTP))
 (20 10 (:REWRITE STR::OCT-DIGIT-CHAR-LIST*P-OF-CDR-WHEN-OCT-DIGIT-CHAR-LIST*P))
 (20 10 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-OF-CDR-WHEN-HEX-DIGIT-CHAR-LIST*P))
 (20 10 (:REWRITE STR::DEC-DIGIT-CHAR-LIST*P-OF-CDR-WHEN-DEC-DIGIT-CHAR-LIST*P))
 (16 16 (:REWRITE STR::OCT-DIGIT-CHAR-LIST*P-WHEN-NOT-CONSP))
 (16 16 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-NOT-CONSP))
 (16 16 (:REWRITE STR::DEC-DIGIT-CHAR-LIST*P-WHEN-NOT-CONSP))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (1 1 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE |(equal c (/ x))|))
 (1 1 (:REWRITE |(equal c (- x))|))
 (1 1 (:REWRITE |(equal (/ x) c)|))
 (1 1 (:REWRITE |(equal (/ x) (/ y))|))
 (1 1 (:REWRITE |(equal (- x) c)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ACL2S::EVENS-PROPER-SYMBOL-LISTP-SIG
 (67 10 (:REWRITE ACL2S::CDR-PROPER-SYMBOL-LISTP-SIG))
 (16 16 (:REWRITE ACL2S::DEF=>PROPER-SYMBOL-LIST))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 )
(ACL2S::EVENS-KEYWORD-LISTP-SIG
 (67 10 (:REWRITE ACL2S::CDR-KEYWORD-LISTP-SIG))
 (16 16 (:REWRITE ACL2S::DEF=>KEYWORD-LIST))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 )
(ACL2S::EVENS-SYMBOL-LISTP-SIG
 (96 10 (:REWRITE ACL2S::CDR-SYMBOL-LISTP-SIG))
 (48 16 (:REWRITE DEFDATA::PROPER-SYMBOL-LISTP-IS-SYMBOL-LIST))
 (32 32 (:TYPE-PRESCRIPTION DEFDATA::PROPER-SYMBOL-LISTP))
 (16 16 (:REWRITE ACL2S::DEF=>SYMBOL-LIST))
 (12 12 (:REWRITE SYMBOLP-OF-CAR-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (1 1 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE |(equal c (/ x))|))
 (1 1 (:REWRITE |(equal c (- x))|))
 (1 1 (:REWRITE |(equal (/ x) c)|))
 (1 1 (:REWRITE |(equal (/ x) (/ y))|))
 (1 1 (:REWRITE |(equal (- x) c)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ACL2S::EVENS-BOOLEAN-LISTP-SIG
 (158 23 (:REWRITE ACL2S::CDR-BOOLEAN-LISTP-SIG))
 (63 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (54 6 (:REWRITE ACL2-NUMBERP-X))
 (35 35 (:REWRITE ACL2S::DEF=>BOOLEAN-LIST))
 (24 6 (:REWRITE RATIONALP-X))
 (16 16 (:REWRITE DEFAULT-CDR))
 (16 16 (:REWRITE DEFAULT-CAR))
 (16 16 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (14 7 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (9 7 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (9 7 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (7 7 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (7 7 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (7 7 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (7 7 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (7 7 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (7 7 (:REWRITE CONSP-BY-LEN))
 (7 7 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (7 7 (:REWRITE |(equal c (/ x))|))
 (7 7 (:REWRITE |(equal c (- x))|))
 (7 7 (:REWRITE |(equal (/ x) c)|))
 (7 7 (:REWRITE |(equal (/ x) (/ y))|))
 (7 7 (:REWRITE |(equal (- x) c)|))
 (7 7 (:REWRITE |(equal (- x) (- y))|))
 (6 6 (:REWRITE REDUCE-RATIONALP-+))
 (6 6 (:REWRITE REDUCE-RATIONALP-*))
 (6 6 (:REWRITE REDUCE-INTEGERP-+))
 (6 6 (:REWRITE RATIONALP-MINUS-X))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (6 6 (:META META-RATIONALP-CORRECT))
 (6 6 (:META META-INTEGERP-CORRECT))
 (4 4 (:REWRITE CONSP-OF-CDR-BY-LEN))
 )
(ACL2S::EVENS-ACL2-NUMBER-LISTP-SIG
 (73 10 (:REWRITE ACL2S::CDR-ACL2-NUMBER-LISTP-SIG))
 (54 6 (:REWRITE ACL2-NUMBERP-X))
 (24 6 (:REWRITE RATIONALP-X))
 (16 16 (:REWRITE ACL2S::DEF=>ACL2-NUMBER-LIST))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE REDUCE-RATIONALP-+))
 (6 6 (:REWRITE REDUCE-RATIONALP-*))
 (6 6 (:REWRITE REDUCE-INTEGERP-+))
 (6 6 (:REWRITE RATIONALP-MINUS-X))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (6 6 (:META META-RATIONALP-CORRECT))
 (6 6 (:META META-INTEGERP-CORRECT))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (1 1 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE |(equal c (/ x))|))
 (1 1 (:REWRITE |(equal c (- x))|))
 (1 1 (:REWRITE |(equal (/ x) c)|))
 (1 1 (:REWRITE |(equal (/ x) (/ y))|))
 (1 1 (:REWRITE |(equal (- x) c)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ACL2S::EVENS-COMPLEX-RATIONAL-LISTP-SIG
 (64 10 (:REWRITE ACL2S::CDR-COMPLEX-RATIONAL-LISTP-SIG))
 (16 16 (:REWRITE ACL2S::DEF=>COMPLEX-RATIONAL-LIST))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 )
(ACL2S::EVENS-RATIONAL-LISTP-SIG
 (72 10 (:REWRITE ACL2S::CDR-RATIONAL-LISTP-SIG))
 (24 6 (:REWRITE RATIONALP-X))
 (16 16 (:REWRITE ACL2S::DEF=>RATIONAL-LIST))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE REDUCE-RATIONALP-+))
 (6 6 (:REWRITE REDUCE-RATIONALP-*))
 (6 6 (:REWRITE REDUCE-INTEGERP-+))
 (6 6 (:REWRITE RATIONALP-MINUS-X))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (6 6 (:META META-RATIONALP-CORRECT))
 (6 6 (:META META-INTEGERP-CORRECT))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (1 1 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE |(equal c (/ x))|))
 (1 1 (:REWRITE |(equal c (- x))|))
 (1 1 (:REWRITE |(equal (/ x) c)|))
 (1 1 (:REWRITE |(equal (/ x) (/ y))|))
 (1 1 (:REWRITE |(equal (- x) c)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ACL2S::EVENS-INTEGER-LISTP-SIG
 (67 10 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (16 16 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE REDUCE-INTEGERP-+))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (6 6 (:META META-INTEGERP-CORRECT))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (1 1 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE |(equal c (/ x))|))
 (1 1 (:REWRITE |(equal c (- x))|))
 (1 1 (:REWRITE |(equal (/ x) c)|))
 (1 1 (:REWRITE |(equal (/ x) (/ y))|))
 (1 1 (:REWRITE |(equal (- x) c)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ACL2S::EVENS-POS-LISTP-SIG
 (65 10 (:REWRITE ACL2S::CDR-POS-LISTP-SIG))
 (16 16 (:REWRITE ACL2S::DEF=>POS-LIST))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 )
(ACL2S::EVENS-NAT-LISTP-SIG
 (65 10 (:REWRITE ACL2S::CDR-NAT-LISTP-SIG))
 (16 16 (:REWRITE ACL2S::DEF=>NAT-LIST))
 (12 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (6 6 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6 6 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (1 1 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE |(equal c (/ x))|))
 (1 1 (:REWRITE |(equal c (- x))|))
 (1 1 (:REWRITE |(equal (/ x) c)|))
 (1 1 (:REWRITE |(equal (/ x) (/ y))|))
 (1 1 (:REWRITE |(equal (- x) c)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ACL2S::EVENS-L-STR-ALLP-GENRULE-SIG)
(ACL2S::EVENS-TRUE-LIST-LISTP-GENRULE-SIG)
(ACL2S::EVENS-TRUE-LISTP-GENRULE-SIG)
(ACL2S::EVENS-ATOM-LISTP-GENRULE-SIG)
(ACL2S::EVENS-STRING-LISTP-GENRULE-SIG)
(ACL2S::EVENS-STANDARD-CHAR-LISTP-GENRULE-SIG)
(ACL2S::EVENS-CHARACTER-LISTP-GENRULE-SIG)
(ACL2S::EVENS-PROPER-SYMBOL-LISTP-GENRULE-SIG)
(ACL2S::EVENS-KEYWORD-LISTP-GENRULE-SIG)
(ACL2S::EVENS-SYMBOL-LISTP-GENRULE-SIG)
(ACL2S::EVENS-BOOLEAN-LISTP-GENRULE-SIG)
(ACL2S::EVENS-ACL2-NUMBER-LISTP-GENRULE-SIG)
(ACL2S::EVENS-COMPLEX-RATIONAL-LISTP-GENRULE-SIG)
(ACL2S::EVENS-RATIONAL-LISTP-GENRULE-SIG)
(ACL2S::EVENS-INTEGER-LISTP-GENRULE-SIG)
(ACL2S::EVENS-POS-LISTP-GENRULE-SIG)
(ACL2S::EVENS-NAT-LISTP-GENRULE-SIG)
(ACL2S::ODDS-POLYMORPHIC-SIG)
(ACL2S::ODDS-L-STR-ALLP-SIG)
(ACL2S::ODDS-TRUE-LIST-LISTP-SIG)
(ACL2S::ODDS-TRUE-LISTP-SIG)
(ACL2S::ODDS-ATOM-LISTP-SIG)
(ACL2S::ODDS-STRING-LISTP-SIG)
(ACL2S::ODDS-STANDARD-CHAR-LISTP-SIG)
(ACL2S::ODDS-CHARACTER-LISTP-SIG)
(ACL2S::ODDS-PROPER-SYMBOL-LISTP-SIG)
(ACL2S::ODDS-KEYWORD-LISTP-SIG)
(ACL2S::ODDS-SYMBOL-LISTP-SIG)
(ACL2S::ODDS-BOOLEAN-LISTP-SIG)
(ACL2S::ODDS-ACL2-NUMBER-LISTP-SIG)
(ACL2S::ODDS-COMPLEX-RATIONAL-LISTP-SIG)
(ACL2S::ODDS-RATIONAL-LISTP-SIG)
(ACL2S::ODDS-INTEGER-LISTP-SIG)
(ACL2S::ODDS-POS-LISTP-SIG)
(ACL2S::ODDS-NAT-LISTP-SIG)
(ACL2S::ODDS-L-STR-ALLP-GENRULE-SIG)
(ACL2S::ODDS-TRUE-LIST-LISTP-GENRULE-SIG)
(ACL2S::ODDS-TRUE-LISTP-GENRULE-SIG)
(ACL2S::ODDS-ATOM-LISTP-GENRULE-SIG)
(ACL2S::ODDS-STRING-LISTP-GENRULE-SIG)
(ACL2S::ODDS-STANDARD-CHAR-LISTP-GENRULE-SIG)
(ACL2S::ODDS-CHARACTER-LISTP-GENRULE-SIG)
(ACL2S::ODDS-PROPER-SYMBOL-LISTP-GENRULE-SIG)
(ACL2S::ODDS-KEYWORD-LISTP-GENRULE-SIG)
(ACL2S::ODDS-SYMBOL-LISTP-GENRULE-SIG)
(ACL2S::ODDS-BOOLEAN-LISTP-GENRULE-SIG)
(ACL2S::ODDS-ACL2-NUMBER-LISTP-GENRULE-SIG)
(ACL2S::ODDS-COMPLEX-RATIONAL-LISTP-GENRULE-SIG)
(ACL2S::ODDS-RATIONAL-LISTP-GENRULE-SIG)
(ACL2S::ODDS-INTEGER-LISTP-GENRULE-SIG)
(ACL2S::ODDS-POS-LISTP-GENRULE-SIG)
(ACL2S::ODDS-NAT-LISTP-GENRULE-SIG)
(ACL2S::MSORT-CONTRACT
 (69 3 (:DEFINITION ACL2S::MERGE2-DEFINITION-RULE))
 (62 15 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (39 39 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (35 32 (:REWRITE DEFAULT-CDR))
 (20 3 (:DEFINITION EVENS))
 (19 19 (:REWRITE DEFAULT-CAR))
 (19 19 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (12 12 (:REWRITE REDUCE-INTEGERP-+))
 (12 12 (:REWRITE INTEGERP-MINUS-X))
 (12 12 (:META META-INTEGERP-CORRECT))
 (9 9 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (9 9 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (9 9 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (9 9 (:REWRITE CONSP-BY-LEN))
 (6 6 (:TYPE-PRESCRIPTION EVENS))
 (1 1 (:REWRITE ACL2S::EVENS-INTEGER-LISTP-SIG))
 )
(ACL2S::MSORT-CONTRACT-TP)
(ACL2S::MSORT-CONTRACT-GENRULE)
(ACL2S::MSORT)
(ACL2S::MSORT-INDUCTION-SCHEME)
(ACL2S::MSORT-DEFINITION-RULE)
(ACL2S::MERGE2-NO-DUPS-CONTRACT
 (113 113 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (70 70 (:REWRITE DEFAULT-CAR))
 (70 70 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (58 2 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (58 2 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (58 2 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (58 2 (:REWRITE |(< x (/ y)) with (< 0 y)|))
 (43 43 (:REWRITE DEFAULT-CDR))
 (34 16 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (30 30 (:REWRITE REDUCE-INTEGERP-+))
 (30 30 (:REWRITE INTEGERP-MINUS-X))
 (30 30 (:META META-INTEGERP-CORRECT))
 (28 28 (:REWRITE THE-FLOOR-BELOW))
 (28 28 (:REWRITE THE-FLOOR-ABOVE))
 (28 28 (:REWRITE DEFAULT-LESS-THAN-2))
 (28 28 (:REWRITE DEFAULT-LESS-THAN-1))
 (23 23 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (23 23 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (23 23 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (23 23 (:REWRITE CONSP-BY-LEN))
 (19 3 (:REWRITE ACL2-NUMBERP-X))
 (17 16 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (17 12 (:REWRITE O-INFP->NEQ-0))
 (16 16 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (16 16 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (16 16 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (16 16 (:REWRITE DEFAULT-TIMES-2))
 (16 16 (:REWRITE DEFAULT-TIMES-1))
 (16 16 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (16 16 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (16 16 (:REWRITE |(equal c (/ x))|))
 (16 16 (:REWRITE |(equal (/ x) (/ y))|))
 (16 16 (:REWRITE |(equal (- x) (- y))|))
 (15 15 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (14 14 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (14 14 (:REWRITE |(equal c (- x))|))
 (14 14 (:REWRITE |(equal (- x) c)|))
 (13 13 (:REWRITE SIMPLIFY-SUMS-<))
 (13 13 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (13 13 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (13 13 (:REWRITE INTEGERP-<-CONSTANT))
 (13 13 (:REWRITE CONSTANT-<-INTEGERP))
 (13 13 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (13 13 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (13 13 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (13 13 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (13 13 (:REWRITE |(< c (- x))|))
 (13 13 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (13 13 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (13 13 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (13 13 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (13 13 (:REWRITE |(< (/ x) (/ y))|))
 (13 13 (:REWRITE |(< (- x) c)|))
 (13 13 (:REWRITE |(< (- x) (- y))|))
 (8 2 (:REWRITE RATIONALP-X))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (6 6 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (6 6 (:REWRITE |(< 0 (/ x))|))
 (6 6 (:REWRITE |(< 0 (* x y))|))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (4 4 (:REWRITE |(< (/ x) 0)|))
 (4 4 (:REWRITE |(< (* x y) 0)|))
 (3 3 (:TYPE-PRESCRIPTION O-FINP))
 (3 1 (:REWRITE O-FIRST-EXPT-O-INFP))
 (2 2 (:REWRITE REDUCE-RATIONALP-+))
 (2 2 (:REWRITE REDUCE-RATIONALP-*))
 (2 2 (:REWRITE RATIONALP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-DIVIDE))
 (2 2 (:REWRITE |(not (equal x (/ y)))|))
 (2 2 (:REWRITE |(equal x (/ y))|))
 (2 2 (:META META-RATIONALP-CORRECT))
 (2 1 (:REWRITE O-FIRST-EXPT-DEF-O-FINP))
 )
(ACL2S::MERGE2-NO-DUPS-CONTRACT-TP)
(ACL2S::MERGE2-NO-DUPS-CONTRACT-GENRULE)
(ACL2S::MERGE2-NO-DUPS)
(ACL2S::MERGE2-NO-DUPS-INDUCTION-SCHEME)
(ACL2S::MERGE2-NO-DUPS-DEFINITION-RULE)
(ACL2S::MSORT-NO-DUPS-CONTRACT
 (69 3 (:DEFINITION ACL2S::MERGE2-NO-DUPS-DEFINITION-RULE))
 (62 15 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (39 39 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (35 32 (:REWRITE DEFAULT-CDR))
 (20 3 (:DEFINITION EVENS))
 (19 19 (:REWRITE DEFAULT-CAR))
 (19 19 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (12 12 (:REWRITE REDUCE-INTEGERP-+))
 (12 12 (:REWRITE INTEGERP-MINUS-X))
 (12 12 (:META META-INTEGERP-CORRECT))
 (9 9 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (9 9 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (9 9 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (9 9 (:REWRITE CONSP-BY-LEN))
 (6 6 (:TYPE-PRESCRIPTION EVENS))
 (1 1 (:REWRITE ACL2S::EVENS-INTEGER-LISTP-SIG))
 )
(ACL2S::MSORT-NO-DUPS-CONTRACT-TP)
(ACL2S::MSORT-NO-DUPS-CONTRACT-GENRULE)
(ACL2S::MSORT-NO-DUPS)
(ACL2S::MSORT-NO-DUPS-INDUCTION-SCHEME)
(ACL2S::MSORT-NO-DUPS-DEFINITION-RULE)
(ACL2S::MERGE2-LEN
 (8161 2775 (:REWRITE DEFAULT-PLUS-2))
 (4146 2775 (:REWRITE DEFAULT-PLUS-1))
 (2568 2568 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2568 2568 (:REWRITE NORMALIZE-ADDENDS))
 (2556 284 (:REWRITE ACL2-NUMBERP-X))
 (1761 1761 (:REWRITE DEFAULT-CDR))
 (1479 1479 (:REWRITE DEFAULT-CAR))
 (1479 1479 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (1143 1143 (:REWRITE FOLD-CONSTS-IN-+))
 (1143 1143 (:REWRITE |(+ c (+ d x))|))
 (1136 284 (:REWRITE RATIONALP-X))
 (506 506 (:REWRITE THE-FLOOR-BELOW))
 (506 506 (:REWRITE THE-FLOOR-ABOVE))
 (364 364 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (363 363 (:REWRITE SIMPLIFY-SUMS-<))
 (363 363 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (363 363 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (363 363 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (363 363 (:REWRITE INTEGERP-<-CONSTANT))
 (363 363 (:REWRITE CONSTANT-<-INTEGERP))
 (363 363 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (363 363 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (363 363 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (363 363 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (363 363 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (363 363 (:REWRITE |(< c (- x))|))
 (363 363 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (363 363 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (363 363 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (363 363 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (363 363 (:REWRITE |(< (/ x) (/ y))|))
 (363 363 (:REWRITE |(< (- x) c)|))
 (363 363 (:REWRITE |(< (- x) (- y))|))
 (306 306 (:REWRITE REDUCE-INTEGERP-+))
 (306 306 (:REWRITE INTEGERP-MINUS-X))
 (306 306 (:META META-INTEGERP-CORRECT))
 (284 284 (:REWRITE REDUCE-RATIONALP-+))
 (284 284 (:REWRITE REDUCE-RATIONALP-*))
 (284 284 (:REWRITE RATIONALP-MINUS-X))
 (284 284 (:META META-RATIONALP-CORRECT))
 (203 203 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (203 203 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (203 203 (:REWRITE |(< (/ x) 0)|))
 (203 203 (:REWRITE |(< (* x y) 0)|))
 (172 172 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (172 172 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (172 172 (:LINEAR LEN-WHEN-PREFIXP))
 (148 148 (:REWRITE DEFAULT-MINUS))
 (148 148 (:LINEAR CONS-SIZE-WHEN-MEMBER))
 (148 148 (:LINEAR ACL2S-SIZE-WHEN-MEMBER))
 (148 148 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (130 26 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (86 86 (:LINEAR INDEX-OF-<-LEN))
 (86 86 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
 (84 84 (:REWRITE DEFAULT-RATIONAL-NUMERATOR))
 (74 20 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (74 20 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (74 20 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (62 62 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (55 55 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (55 55 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (55 55 (:REWRITE |(< 0 (/ x))|))
 (55 55 (:REWRITE |(< 0 (* x y))|))
 (22 22 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (22 22 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (22 22 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (22 22 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (22 22 (:REWRITE CONSP-BY-LEN))
 (20 20 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (20 20 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (20 20 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (20 20 (:REWRITE |(equal c (/ x))|))
 (20 20 (:REWRITE |(equal c (- x))|))
 (20 20 (:REWRITE |(equal (/ x) c)|))
 (20 20 (:REWRITE |(equal (/ x) (/ y))|))
 (20 20 (:REWRITE |(equal (- x) c)|))
 (20 20 (:REWRITE |(equal (- x) (- y))|))
 (19 19 (:REWRITE |(equal (+ (- c) x) y)|))
 (4 4 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 2 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 )
(ACL2S::EXPAND-EVENS
 (4804 11 (:REWRITE ACL2S::CDR-TRUE-LISTP-SIG))
 (1897 31 (:DEFINITION NAT-LISTP))
 (1254 31 (:REWRITE DEFDATA::NAT-LISTP--TRUE-LISTP))
 (1253 31 (:REWRITE ACL2S::TRUE-LIST-LISTP-IMPLIES-TLP))
 (1217 12 (:DEFINITION TRUE-LIST-LISTP))
 (1023 31 (:DEFINITION NATP))
 (813 31 (:REWRITE ACL2S::NAT-LISTP-IMPLIES-TLP))
 (797 31 (:REWRITE ACL2S::POS-LISTP-IMPLIES-TLP))
 (745 31 (:REWRITE ACL2S::PROPER-SYMBOL-LISTP-IMPLIES-TLP))
 (738 31 (:REWRITE ACL2S::BOOLEAN-LISTP-IMPLIES-TLP))
 (715 12 (:DEFINITION ACL2S::POS-LISTP))
 (669 31 (:REWRITE ACL2S::L-STR-ALLP-IMPLIES-TLP))
 (663 12 (:DEFINITION ACL2S::PROPER-SYMBOL-LISTP))
 (656 16 (:DEFINITION BOOLEAN-LISTP))
 (637 31 (:REWRITE ACL2S::KEYWORD-LISTP-IMPLIES-TLP))
 (587 12 (:DEFINITION ACL2S::L-STR-ALLP))
 (555 12 (:DEFINITION ACL2S::KEYWORD-LISTP))
 (521 51 (:REWRITE ACL2S::CDR-NAT-LISTP-SIG))
 (480 24 (:DEFINITION KEYWORDP))
 (441 31 (:REWRITE ACL2S::ATOM-LISTP-IMPLIES-TLP))
 (384 12 (:DEFINITION POSP))
 (380 191 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (361 31 (:REWRITE ACL2S::SYMBOL-LISTP-IMPLIES-TLP))
 (361 31 (:REWRITE ACL2S::RATIONAL-LISTP-IMPLIES-TLP))
 (359 12 (:DEFINITION ATOM-LISTP))
 (345 343 (:REWRITE DEFAULT-CDR))
 (337 337 (:REWRITE DEFAULT-CAR))
 (337 337 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (329 31 (:REWRITE ACL2S::INTEGER-LISTP-IMPLIES-TLP))
 (312 12 (:DEFINITION ACL2S::PROPER-SYMBOLP))
 (297 31 (:REWRITE ACL2S::ACL2-NUMBER-LISTP-IMPLIES-TLP))
 (281 31 (:REWRITE ACL2S::STRING-LISTP-IMPLIES-TLP))
 (281 31 (:REWRITE ACL2S::COMPLEX-RATIONAL-LISTP-IMPLIES-TLP))
 (279 12 (:DEFINITION RATIONAL-LISTP))
 (276 12 (:DEFINITION ACL2S::STR-ALLP))
 (263 12 (:DEFINITION SYMBOL-LISTP))
 (247 12 (:DEFINITION INTEGER-LISTP))
 (215 12 (:DEFINITION ACL2-NUMBER-LISTP))
 (214 214 (:TYPE-PRESCRIPTION NAT-LISTP))
 (208 208 (:TYPE-PRESCRIPTION STRINGP-SYMBOL-PACKAGE-NAME))
 (199 12 (:DEFINITION STRING-LISTP))
 (199 12 (:DEFINITION ACL2S::COMPLEX-RATIONAL-LISTP))
 (187 187 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (187 187 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (187 187 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (187 187 (:REWRITE CONSP-BY-LEN))
 (163 163 (:TYPE-PRESCRIPTION BOOLEAN-LISTP))
 (115 115 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (96 96 (:REWRITE SYMBOLP-OF-CAR-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP))
 (94 31 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (91 91 (:TYPE-PRESCRIPTION TRUE-LIST-LISTP))
 (91 91 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (91 91 (:TYPE-PRESCRIPTION STRING-LISTP))
 (91 91 (:TYPE-PRESCRIPTION RATIONAL-LISTP))
 (91 91 (:TYPE-PRESCRIPTION ACL2S::PROPER-SYMBOL-LISTP))
 (91 91 (:TYPE-PRESCRIPTION ACL2S::POS-LISTP))
 (91 91 (:TYPE-PRESCRIPTION ACL2S::L-STR-ALLP))
 (91 91 (:TYPE-PRESCRIPTION ACL2S::KEYWORD-LISTP))
 (91 91 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (91 91 (:TYPE-PRESCRIPTION ACL2S::COMPLEX-RATIONAL-LISTP))
 (91 91 (:TYPE-PRESCRIPTION ATOM-LISTP))
 (91 91 (:TYPE-PRESCRIPTION ACL2-NUMBER-LISTP))
 (88 44 (:REWRITE ACL2S::CDR-BOOLEAN-LISTP-SIG))
 (84 52 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (84 52 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (78 39 (:REWRITE O-P-O-INFP-CAR))
 (78 39 (:REWRITE CONSP-OF-CAR-WHEN-ALISTP))
 (74 74 (:REWRITE REDUCE-INTEGERP-+))
 (74 74 (:REWRITE INTEGERP-MINUS-X))
 (74 74 (:META META-INTEGERP-CORRECT))
 (62 62 (:REWRITE ACL2S::DEF=>NAT-LIST))
 (59 31 (:REWRITE TRUE-LISTP-WHEN-ATOM))
 (58 58 (:REWRITE THE-FLOOR-BELOW))
 (58 58 (:REWRITE THE-FLOOR-ABOVE))
 (58 58 (:REWRITE SIMPLIFY-SUMS-<))
 (58 58 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (58 58 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (58 58 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (58 58 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (58 58 (:REWRITE INTEGERP-<-CONSTANT))
 (58 58 (:REWRITE DEFAULT-LESS-THAN-2))
 (58 58 (:REWRITE DEFAULT-LESS-THAN-1))
 (58 58 (:REWRITE CONSTANT-<-INTEGERP))
 (58 58 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (58 58 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (58 58 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (58 58 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (58 58 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (58 58 (:REWRITE |(< c (- x))|))
 (58 58 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (58 58 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (58 58 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (58 58 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (58 58 (:REWRITE |(< (/ x) (/ y))|))
 (58 58 (:REWRITE |(< (- x) c)|))
 (58 58 (:REWRITE |(< (- x) (- y))|))
 (52 52 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (52 52 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (52 52 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (52 52 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (52 52 (:REWRITE |(equal c (/ x))|))
 (52 52 (:REWRITE |(equal c (- x))|))
 (52 52 (:REWRITE |(equal (/ x) c)|))
 (52 52 (:REWRITE |(equal (/ x) (/ y))|))
 (52 52 (:REWRITE |(equal (- x) c)|))
 (52 52 (:REWRITE |(equal (- x) (- y))|))
 (48 48 (:TYPE-PRESCRIPTION LEGAL-CONSTANTP))
 (48 48 (:REWRITE ACL2S::DEF=>BOOLEAN-LIST))
 (48 24 (:REWRITE DEFDATA::PROPER-SYMBOL-LISTP-IS-SYMBOL-LIST))
 (42 42 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (42 42 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (42 42 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (42 42 (:REWRITE |(< (/ x) 0)|))
 (42 42 (:REWRITE |(< (* x y) 0)|))
 (40 20 (:REWRITE ACL2S::CDR-TRUE-LIST-LISTP-SIG))
 (40 20 (:REWRITE ACL2S::CDR-SYMBOL-LISTP-SIG))
 (40 20 (:REWRITE ACL2S::CDR-STRING-LISTP-SIG))
 (40 20 (:REWRITE ACL2S::CDR-RATIONAL-LISTP-SIG))
 (40 20 (:REWRITE ACL2S::CDR-PROPER-SYMBOL-LISTP-SIG))
 (40 20 (:REWRITE ACL2S::CDR-POS-LISTP-SIG))
 (40 20 (:REWRITE ACL2S::CDR-L-STR-ALLP-SIG))
 (40 20 (:REWRITE ACL2S::CDR-KEYWORD-LISTP-SIG))
 (40 20 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (40 20 (:REWRITE ACL2S::CDR-COMPLEX-RATIONAL-LISTP-SIG))
 (40 20 (:REWRITE ACL2S::CDR-ATOM-LISTP-SIG))
 (40 20 (:REWRITE ACL2S::CDR-ACL2-NUMBER-LISTP-SIG))
 (39 39 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (39 39 (:TYPE-PRESCRIPTION O-P))
 (39 39 (:TYPE-PRESCRIPTION ALISTP))
 (32 32 (:REWRITE DEFAULT-SYMBOL-PACKAGE-NAME))
 (31 31 (:REWRITE TRUE-LISTP-WHEN-THEOREM-SYMBOL-LISTP))
 (31 31 (:REWRITE TRUE-LISTP-WHEN-TERMFN-LISTP))
 (31 31 (:REWRITE TRUE-LISTP-WHEN-MACRO-SYMBOL-LISTP))
 (31 31 (:REWRITE TRUE-LISTP-WHEN-LAMBDA-LISTP))
 (31 31 (:REWRITE TRUE-LISTP-WHEN-FUNCTION-SYMBOL-LISTP))
 (24 24 (:TYPE-PRESCRIPTION DEFDATA::PROPER-SYMBOL-LISTP))
 (24 24 (:REWRITE ACL2S::DEF=>TRUE-LIST-LIST))
 (24 24 (:REWRITE ACL2S::DEF=>SYMBOL-LIST))
 (24 24 (:REWRITE ACL2S::DEF=>STRING-LIST))
 (24 24 (:REWRITE ACL2S::DEF=>RATIONAL-LIST))
 (24 24 (:REWRITE ACL2S::DEF=>PROPER-SYMBOL-LIST))
 (24 24 (:REWRITE ACL2S::DEF=>POS-LIST))
 (24 24 (:REWRITE ACL2S::DEF=>L-STR-ALL))
 (24 24 (:REWRITE ACL2S::DEF=>KEYWORD-LIST))
 (24 24 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (24 24 (:REWRITE ACL2S::DEF=>COMPLEX-RATIONAL-LIST))
 (24 24 (:REWRITE ACL2S::DEF=>ATOM-LIST))
 (24 24 (:REWRITE ACL2S::DEF=>ACL2-NUMBER-LIST))
 (16 16 (:TYPE-PRESCRIPTION BOOLEANP))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (16 16 (:REWRITE REDUCE-RATIONALP-+))
 (16 16 (:REWRITE REDUCE-RATIONALP-*))
 (16 16 (:REWRITE RATIONALP-X))
 (16 16 (:REWRITE RATIONALP-MINUS-X))
 (16 16 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (16 16 (:REWRITE ACL2-NUMBERP-X))
 (16 16 (:REWRITE |(< 0 (/ x))|))
 (16 16 (:REWRITE |(< 0 (* x y))|))
 (16 16 (:META META-RATIONALP-CORRECT))
 (16 8 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (8 8 (:TYPE-PRESCRIPTION SET::EMPTYP-TYPE))
 (8 8 (:REWRITE SET::IN-SET))
 )
(ACL2S::EVENS-LEN
 (56688 118 (:REWRITE ACL2S::CDR-TRUE-LISTP-SIG))
 (19461 333 (:DEFINITION NAT-LISTP))
 (14069 283 (:REWRITE DEFDATA::NAT-LISTP--TRUE-LISTP))
 (13918 4848 (:REWRITE DEFAULT-PLUS-2))
 (11826 258 (:DEFINITION INTEGER-ABS))
 (11136 174 (:DEFINITION LENGTH))
 (10989 333 (:DEFINITION NATP))
 (10980 283 (:REWRITE ACL2S::TRUE-LIST-LISTP-IMPLIES-TLP))
 (10552 111 (:DEFINITION TRUE-LIST-LISTP))
 (9106 4848 (:REWRITE DEFAULT-PLUS-1))
 (8882 7755 (:REWRITE DEFAULT-CDR))
 (7691 561 (:REWRITE ACL2S::CDR-NAT-LISTP-SIG))
 (7150 283 (:REWRITE ACL2S::NAT-LISTP-IMPLIES-TLP))
 (7134 522 (:REWRITE STR::CONSP-OF-EXPLODE))
 (7013 283 (:REWRITE ACL2S::POS-LISTP-IMPLIES-TLP))
 (6545 283 (:REWRITE ACL2S::PROPER-SYMBOL-LISTP-IMPLIES-TLP))
 (6319 283 (:REWRITE ACL2S::BOOLEAN-LISTP-IMPLIES-TLP))
 (6189 111 (:DEFINITION ACL2S::POS-LISTP))
 (5886 283 (:REWRITE ACL2S::L-STR-ALLP-IMPLIES-TLP))
 (5721 111 (:DEFINITION ACL2S::PROPER-SYMBOL-LISTP))
 (5643 283 (:REWRITE ACL2S::KEYWORD-LISTP-IMPLIES-TLP))
 (5495 139 (:DEFINITION BOOLEAN-LISTP))
 (5220 174 (:REWRITE NUMERATOR-NEGATIVE))
 (5063 5047 (:REWRITE DEFAULT-CAR))
 (5062 111 (:DEFINITION ACL2S::L-STR-ALLP))
 (5047 5047 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (4819 111 (:DEFINITION ACL2S::KEYWORD-LISTP))
 (4499 4499 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (4499 4499 (:REWRITE NORMALIZE-ADDENDS))
 (4440 222 (:DEFINITION KEYWORDP))
 (3972 283 (:REWRITE ACL2S::ATOM-LISTP-IMPLIES-TLP))
 (3552 111 (:DEFINITION POSP))
 (3318 283 (:REWRITE ACL2S::SYMBOL-LISTP-IMPLIES-TLP))
 (3287 283 (:REWRITE ACL2S::RATIONAL-LISTP-IMPLIES-TLP))
 (3220 661 (:REWRITE CONSP-OF-CAR-WHEN-ALISTP))
 (3148 111 (:DEFINITION ATOM-LISTP))
 (3013 283 (:REWRITE ACL2S::INTEGER-LISTP-IMPLIES-TLP))
 (2940 84 (:REWRITE |(+ (if a b c) x)|))
 (2886 111 (:DEFINITION ACL2S::PROPER-SYMBOLP))
 (2739 283 (:REWRITE ACL2S::ACL2-NUMBER-LISTP-IMPLIES-TLP))
 (2602 283 (:REWRITE ACL2S::STRING-LISTP-IMPLIES-TLP))
 (2602 283 (:REWRITE ACL2S::COMPLEX-RATIONAL-LISTP-IMPLIES-TLP))
 (2553 111 (:DEFINITION ACL2S::STR-ALLP))
 (2463 111 (:DEFINITION RATIONAL-LISTP))
 (2324 111 (:DEFINITION SYMBOL-LISTP))
 (2245 2245 (:TYPE-PRESCRIPTION NAT-LISTP))
 (2189 111 (:DEFINITION INTEGER-LISTP))
 (2074 2074 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (2074 2074 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (2074 2074 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (2074 2074 (:REWRITE CONSP-BY-LEN))
 (1915 111 (:DEFINITION ACL2-NUMBER-LISTP))
 (1870 1000 (:REWRITE DEFAULT-LESS-THAN-1))
 (1841 1841 (:REWRITE FOLD-CONSTS-IN-+))
 (1830 661 (:REWRITE O-P-O-INFP-CAR))
 (1781 1781 (:TYPE-PRESCRIPTION STRINGP-SYMBOL-PACKAGE-NAME))
 (1778 111 (:DEFINITION STRING-LISTP))
 (1778 111 (:DEFINITION ACL2S::COMPLEX-RATIONAL-LISTP))
 (1566 1566 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (1444 1444 (:TYPE-PRESCRIPTION BOOLEAN-LISTP))
 (1284 974 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1284 974 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (1257 1257 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (1128 258 (:REWRITE DEFAULT-MINUS))
 (1112 278 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (1053 1053 (:REWRITE REDUCE-INTEGERP-+))
 (1053 1053 (:REWRITE INTEGERP-MINUS-X))
 (1053 1053 (:META META-INTEGERP-CORRECT))
 (1026 1026 (:TYPE-PRESCRIPTION NUMERATOR-ZERO))
 (1026 1026 (:TYPE-PRESCRIPTION NUMERATOR-POSITIVE . 2))
 (1026 1026 (:TYPE-PRESCRIPTION NUMERATOR-POSITIVE . 1))
 (1026 1026 (:TYPE-PRESCRIPTION NUMERATOR-NEGATIVE . 2))
 (1026 1026 (:TYPE-PRESCRIPTION NUMERATOR-NEGATIVE . 1))
 (1010 974 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1000 1000 (:REWRITE THE-FLOOR-BELOW))
 (1000 1000 (:REWRITE THE-FLOOR-ABOVE))
 (1000 1000 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (1000 1000 (:REWRITE DEFAULT-LESS-THAN-2))
 (975 975 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (974 974 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (974 974 (:REWRITE |(equal c (/ x))|))
 (974 974 (:REWRITE |(equal c (- x))|))
 (974 974 (:REWRITE |(equal (/ x) c)|))
 (974 974 (:REWRITE |(equal (/ x) (/ y))|))
 (974 974 (:REWRITE |(equal (- x) c)|))
 (974 974 (:REWRITE |(equal (- x) (- y))|))
 (906 283 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (891 891 (:TYPE-PRESCRIPTION ALISTP))
 (864 864 (:TYPE-PRESCRIPTION TRUE-LIST-LISTP))
 (864 864 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (864 864 (:TYPE-PRESCRIPTION STRING-LISTP))
 (864 864 (:TYPE-PRESCRIPTION RATIONAL-LISTP))
 (864 864 (:TYPE-PRESCRIPTION ACL2S::PROPER-SYMBOL-LISTP))
 (864 864 (:TYPE-PRESCRIPTION ACL2S::POS-LISTP))
 (864 864 (:TYPE-PRESCRIPTION ACL2S::L-STR-ALLP))
 (864 864 (:TYPE-PRESCRIPTION ACL2S::KEYWORD-LISTP))
 (864 864 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (864 864 (:TYPE-PRESCRIPTION ACL2S::COMPLEX-RATIONAL-LISTP))
 (864 864 (:TYPE-PRESCRIPTION ATOM-LISTP))
 (864 864 (:TYPE-PRESCRIPTION ACL2-NUMBER-LISTP))
 (863 863 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (833 311 (:REWRITE RATIONALP-X))
 (826 826 (:REWRITE SIMPLIFY-SUMS-<))
 (826 826 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (826 826 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (826 826 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (826 826 (:REWRITE INTEGERP-<-CONSTANT))
 (826 826 (:REWRITE CONSTANT-<-INTEGERP))
 (826 826 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (826 826 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (826 826 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (826 826 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (826 826 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (826 826 (:REWRITE |(< c (- x))|))
 (826 826 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (826 826 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (826 826 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (826 826 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (826 826 (:REWRITE |(< (/ x) (/ y))|))
 (826 826 (:REWRITE |(< (- x) c)|))
 (826 826 (:REWRITE |(< (- x) (- y))|))
 (822 822 (:REWRITE SYMBOLP-OF-CAR-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP))
 (774 387 (:REWRITE ACL2S::CDR-BOOLEAN-LISTP-SIG))
 (689 689 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (689 689 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (689 689 (:REWRITE |(< (/ x) 0)|))
 (689 689 (:REWRITE |(< (* x y) 0)|))
 (664 664 (:REWRITE ACL2S::DEF=>NAT-LIST))
 (660 283 (:REWRITE TRUE-LISTP-WHEN-ATOM))
 (556 556 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (444 174 (:REWRITE INTEGERP==>NUMERATOR-=-X))
 (442 221 (:REWRITE DEFDATA::PROPER-SYMBOL-LISTP-IS-SYMBOL-LIST))
 (415 415 (:REWRITE ACL2S::DEF=>BOOLEAN-LIST))
 (411 411 (:TYPE-PRESCRIPTION LEGAL-CONSTANTP))
 (386 193 (:REWRITE ACL2S::CDR-TRUE-LIST-LISTP-SIG))
 (386 193 (:REWRITE ACL2S::CDR-SYMBOL-LISTP-SIG))
 (386 193 (:REWRITE ACL2S::CDR-STRING-LISTP-SIG))
 (386 193 (:REWRITE ACL2S::CDR-RATIONAL-LISTP-SIG))
 (386 193 (:REWRITE ACL2S::CDR-PROPER-SYMBOL-LISTP-SIG))
 (386 193 (:REWRITE ACL2S::CDR-POS-LISTP-SIG))
 (386 193 (:REWRITE ACL2S::CDR-L-STR-ALLP-SIG))
 (386 193 (:REWRITE ACL2S::CDR-KEYWORD-LISTP-SIG))
 (386 193 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (386 193 (:REWRITE ACL2S::CDR-COMPLEX-RATIONAL-LISTP-SIG))
 (386 193 (:REWRITE ACL2S::CDR-ATOM-LISTP-SIG))
 (386 193 (:REWRITE ACL2S::CDR-ACL2-NUMBER-LISTP-SIG))
 (368 368 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (348 174 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (311 311 (:REWRITE REDUCE-RATIONALP-+))
 (311 311 (:REWRITE REDUCE-RATIONALP-*))
 (311 311 (:REWRITE RATIONALP-MINUS-X))
 (311 311 (:META META-RATIONALP-CORRECT))
 (306 306 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (283 283 (:REWRITE TRUE-LISTP-WHEN-THEOREM-SYMBOL-LISTP))
 (283 283 (:REWRITE TRUE-LISTP-WHEN-TERMFN-LISTP))
 (283 283 (:REWRITE TRUE-LISTP-WHEN-MACRO-SYMBOL-LISTP))
 (283 283 (:REWRITE TRUE-LISTP-WHEN-LAMBDA-LISTP))
 (283 283 (:REWRITE TRUE-LISTP-WHEN-FUNCTION-SYMBOL-LISTP))
 (278 278 (:REWRITE O-P-DEF-O-FINP-1))
 (278 278 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (278 278 (:REWRITE ACL2S::DEF=>ALIST))
 (278 278 (:REWRITE ALISTP-WHEN-ATOM))
 (274 274 (:REWRITE DEFAULT-SYMBOL-PACKAGE-NAME))
 (258 258 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (258 258 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (258 258 (:LINEAR LEN-WHEN-PREFIXP))
 (252 252 (:LINEAR CONS-SIZE-WHEN-MEMBER))
 (252 252 (:LINEAR ACL2S-SIZE-WHEN-MEMBER))
 (252 252 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (225 54 (:LINEAR CGEN::ACL2-COUNT-EVENS-STRONG))
 (221 221 (:TYPE-PRESCRIPTION DEFDATA::PROPER-SYMBOL-LISTP))
 (221 221 (:REWRITE ACL2S::DEF=>TRUE-LIST-LIST))
 (221 221 (:REWRITE ACL2S::DEF=>SYMBOL-LIST))
 (221 221 (:REWRITE ACL2S::DEF=>STRING-LIST))
 (221 221 (:REWRITE ACL2S::DEF=>RATIONAL-LIST))
 (221 221 (:REWRITE ACL2S::DEF=>PROPER-SYMBOL-LIST))
 (221 221 (:REWRITE ACL2S::DEF=>POS-LIST))
 (221 221 (:REWRITE ACL2S::DEF=>L-STR-ALL))
 (221 221 (:REWRITE ACL2S::DEF=>KEYWORD-LIST))
 (221 221 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (221 221 (:REWRITE ACL2S::DEF=>COMPLEX-RATIONAL-LIST))
 (221 221 (:REWRITE ACL2S::DEF=>ATOM-LIST))
 (221 221 (:REWRITE ACL2S::DEF=>ACL2-NUMBER-LIST))
 (186 54 (:LINEAR ACL2S-SIZE-EVENS-STRONG))
 (174 174 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (174 174 (:REWRITE DEFAULT-RATIONAL-NUMERATOR))
 (170 85 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (137 137 (:TYPE-PRESCRIPTION BOOLEANP))
 (137 137 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (137 137 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (137 137 (:REWRITE ACL2-NUMBERP-X))
 (137 137 (:REWRITE |(< 0 (/ x))|))
 (137 137 (:REWRITE |(< 0 (* x y))|))
 (129 129 (:LINEAR INDEX-OF-<-LEN))
 (129 129 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
 (127 54 (:LINEAR CONS-SIZE-EVENS-STRONG))
 (127 54 (:LINEAR ACL2-COUNT-EVENS-STRONG))
 (85 85 (:TYPE-PRESCRIPTION SET::EMPTYP-TYPE))
 (85 85 (:REWRITE SET::IN-SET))
 (84 84 (:REWRITE INTEGERP==>DENOMINATOR-=-1))
 (84 84 (:REWRITE DEFAULT-REALPART))
 (84 84 (:REWRITE DEFAULT-RATIONAL-DENOMINATOR))
 (84 84 (:REWRITE DEFAULT-IMAGPART))
 (54 54 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (24 24 (:REWRITE |arith (+ c (+ d x))|))
 (12 12 (:REWRITE |(equal (+ (- c) x) y)|))
 )
(ACL2S::MSORT-LEN
 (12866 74 (:DEFINITION ACL2S::MERGE2-DEFINITION-RULE))
 (10824 464 (:REWRITE DEFAULT-LESS-THAN-2))
 (8984 390 (:REWRITE DEFAULT-LESS-THAN-1))
 (3996 444 (:REWRITE ACL2-NUMBERP-X))
 (3404 1171 (:REWRITE DEFAULT-PLUS-2))
 (1863 1171 (:REWRITE DEFAULT-PLUS-1))
 (1776 444 (:REWRITE RATIONALP-X))
 (1742 1605 (:REWRITE DEFAULT-CDR))
 (1094 1094 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1094 1094 (:REWRITE NORMALIZE-ADDENDS))
 (988 988 (:REWRITE DEFAULT-CAR))
 (988 988 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (470 470 (:REWRITE FOLD-CONSTS-IN-+))
 (470 470 (:REWRITE |(+ c (+ d x))|))
 (464 464 (:REWRITE THE-FLOOR-BELOW))
 (464 464 (:REWRITE THE-FLOOR-ABOVE))
 (458 458 (:REWRITE REDUCE-INTEGERP-+))
 (458 458 (:REWRITE INTEGERP-MINUS-X))
 (458 458 (:META META-INTEGERP-CORRECT))
 (444 444 (:REWRITE REDUCE-RATIONALP-+))
 (444 444 (:REWRITE REDUCE-RATIONALP-*))
 (444 444 (:REWRITE RATIONALP-MINUS-X))
 (444 444 (:META META-RATIONALP-CORRECT))
 (242 242 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (242 242 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (240 240 (:REWRITE SIMPLIFY-SUMS-<))
 (240 240 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (240 240 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (240 240 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (240 240 (:REWRITE INTEGERP-<-CONSTANT))
 (240 240 (:REWRITE CONSTANT-<-INTEGERP))
 (240 240 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (240 240 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (240 240 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (240 240 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (240 240 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (240 240 (:REWRITE |(< c (- x))|))
 (240 240 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (240 240 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (240 240 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (240 240 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (240 240 (:REWRITE |(< (/ x) (/ y))|))
 (240 240 (:REWRITE |(< (- x) c)|))
 (240 240 (:REWRITE |(< (- x) (- y))|))
 (148 148 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (148 148 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (148 148 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (148 148 (:REWRITE CONSP-BY-LEN))
 (122 27 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (111 30 (:REWRITE ACL2S::EVENS-INTEGER-LISTP-SIG))
 (92 92 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (92 92 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (92 92 (:REWRITE |(< (/ x) 0)|))
 (92 92 (:REWRITE |(< (* x y) 0)|))
 (82 82 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (82 82 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (82 82 (:LINEAR LEN-WHEN-PREFIXP))
 (74 74 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (74 74 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (74 74 (:REWRITE |(< 0 (/ x))|))
 (74 74 (:REWRITE |(< 0 (* x y))|))
 (70 70 (:LINEAR CONS-SIZE-WHEN-MEMBER))
 (70 70 (:LINEAR ACL2S-SIZE-WHEN-MEMBER))
 (70 70 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (58 58 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (52 52 (:TYPE-PRESCRIPTION NUMERATOR-ZERO))
 (41 41 (:LINEAR INDEX-OF-<-LEN))
 (41 41 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
 (28 18 (:REWRITE DEFAULT-MINUS))
 (28 9 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (28 9 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (28 9 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (9 9 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (9 9 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (9 9 (:REWRITE DEFAULT-RATIONAL-NUMERATOR))
 (9 9 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (9 9 (:REWRITE |(equal c (/ x))|))
 (9 9 (:REWRITE |(equal c (- x))|))
 (9 9 (:REWRITE |(equal (/ x) c)|))
 (9 9 (:REWRITE |(equal (/ x) (/ y))|))
 (9 9 (:REWRITE |(equal (- x) c)|))
 (9 9 (:REWRITE |(equal (- x) (- y))|))
 (7 1 (:REWRITE ACL2S::L-STR-ALLP-IMPLIES-TLP))
 (6 1 (:REWRITE ACL2S::TRUE-LIST-LISTP-IMPLIES-TLP))
 (6 1 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (4 1 (:DEFINITION ACL2S::L-STR-ALLP))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (3 1 (:DEFINITION TRUE-LIST-LISTP))
 (2 2 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (2 2 (:REWRITE ACL2S::DEF=>ATOM-LIST))
 (2 1 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (2 1 (:REWRITE ACL2S::CDR-ATOM-LISTP-SIG))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LIST-LISTP))
 (1 1 (:TYPE-PRESCRIPTION ACL2S::L-STR-ALLP))
 (1 1 (:TYPE-PRESCRIPTION SET::EMPTYP-TYPE))
 (1 1 (:REWRITE TRUE-LISTP-WHEN-THEOREM-SYMBOL-LISTP))
 (1 1 (:REWRITE TRUE-LISTP-WHEN-TERMFN-LISTP))
 (1 1 (:REWRITE TRUE-LISTP-WHEN-MACRO-SYMBOL-LISTP))
 (1 1 (:REWRITE TRUE-LISTP-WHEN-LAMBDA-LISTP))
 (1 1 (:REWRITE TRUE-LISTP-WHEN-FUNCTION-SYMBOL-LISTP))
 (1 1 (:REWRITE TRUE-LISTP-WHEN-ATOM))
 (1 1 (:REWRITE INTEGERP==>DENOMINATOR-=-1))
 (1 1 (:REWRITE SET::IN-SET))
 (1 1 (:REWRITE DEFAULT-RATIONAL-DENOMINATOR))
 (1 1 (:REWRITE ACL2S::DEF=>TRUE-LIST-LIST))
 (1 1 (:REWRITE ACL2S::DEF=>L-STR-ALL))
 (1 1 (:REWRITE |(equal (+ (- c) x) y)|))
 (1 1 (:DEFINITION ACL2S::STR-ALLP))
 )
(ACL2S::MERGE2-NO-DUPS-LEN
 (10733 3697 (:REWRITE DEFAULT-PLUS-2))
 (5671 735 (:REWRITE ACL2-NUMBERP-X))
 (5304 3697 (:REWRITE DEFAULT-PLUS-1))
 (3280 3280 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2596 2596 (:REWRITE DEFAULT-CDR))
 (2468 617 (:REWRITE RATIONALP-X))
 (2324 2324 (:REWRITE DEFAULT-CAR))
 (2324 2324 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (1394 1394 (:REWRITE FOLD-CONSTS-IN-+))
 (1234 163 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (893 893 (:REWRITE THE-FLOOR-BELOW))
 (893 893 (:REWRITE THE-FLOOR-ABOVE))
 (645 645 (:REWRITE REDUCE-INTEGERP-+))
 (645 645 (:REWRITE INTEGERP-MINUS-X))
 (645 645 (:META META-INTEGERP-CORRECT))
 (617 617 (:REWRITE REDUCE-RATIONALP-+))
 (617 617 (:REWRITE REDUCE-RATIONALP-*))
 (617 617 (:REWRITE RATIONALP-MINUS-X))
 (617 617 (:META META-RATIONALP-CORRECT))
 (616 616 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (615 615 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (606 606 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (606 606 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (606 606 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (606 606 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (606 606 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (606 606 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (606 606 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (606 606 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (606 606 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (606 606 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (606 606 (:REWRITE |(< (/ x) (/ y))|))
 (606 606 (:REWRITE |(< (- x) (- y))|))
 (601 601 (:REWRITE INTEGERP-<-CONSTANT))
 (601 601 (:REWRITE CONSTANT-<-INTEGERP))
 (601 601 (:REWRITE |(< c (- x))|))
 (601 601 (:REWRITE |(< (- x) c)|))
 (323 323 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (323 323 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (323 323 (:REWRITE |(< (/ x) 0)|))
 (323 323 (:REWRITE |(< (* x y) 0)|))
 (281 163 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (214 214 (:REWRITE DEFAULT-MINUS))
 (210 42 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (203 7 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (203 7 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (203 7 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (203 7 (:REWRITE |(< x (/ y)) with (< 0 y)|))
 (163 163 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (163 163 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (163 163 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (163 163 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (163 163 (:REWRITE |(equal c (/ x))|))
 (163 163 (:REWRITE |(equal (/ x) (/ y))|))
 (163 163 (:REWRITE |(equal (- x) (- y))|))
 (156 156 (:REWRITE |(equal c (- x))|))
 (156 156 (:REWRITE |(equal (- x) c)|))
 (150 150 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (150 150 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (150 150 (:LINEAR LEN-WHEN-PREFIXP))
 (146 146 (:LINEAR CONS-SIZE-WHEN-MEMBER))
 (146 146 (:LINEAR ACL2S-SIZE-WHEN-MEMBER))
 (146 146 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (122 122 (:REWRITE DEFAULT-RATIONAL-NUMERATOR))
 (115 115 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (115 115 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (115 115 (:REWRITE |(< 0 (* x y))|))
 (94 94 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (75 75 (:LINEAR INDEX-OF-<-LEN))
 (75 75 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
 (56 56 (:REWRITE DEFAULT-TIMES-2))
 (56 56 (:REWRITE DEFAULT-TIMES-1))
 (40 40 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (38 33 (:REWRITE O-INFP->NEQ-0))
 (34 34 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (34 34 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (34 34 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (34 34 (:REWRITE CONSP-BY-LEN))
 (30 30 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-<2))
 (28 28 (:REWRITE |(< (+ c/d x) y)|))
 (28 28 (:REWRITE |(< (+ (- c) x) y)|))
 (20 20 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-<1))
 (18 18 (:REWRITE |(< y (+ (- c) x))|))
 (18 18 (:REWRITE |(< x (+ c/d y))|))
 (12 12 (:REWRITE DEFAULT-DIVIDE))
 (8 8 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (8 4 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (7 7 (:REWRITE |(not (equal x (/ y)))|))
 (7 7 (:REWRITE |(equal x (/ y))|))
 (3 3 (:TYPE-PRESCRIPTION O-FINP))
 (3 1 (:REWRITE O-FIRST-EXPT-O-INFP))
 (2 2 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (2 1 (:REWRITE O-FIRST-EXPT-DEF-O-FINP))
 )
(ACL2S::MSORT-NO-DUPS-LEN
 (39952 194 (:DEFINITION ACL2S::MERGE2-NO-DUPS-DEFINITION-RULE))
 (28515 1303 (:REWRITE DEFAULT-LESS-THAN-2))
 (23675 1109 (:REWRITE DEFAULT-LESS-THAN-1))
 (14706 45 (:REWRITE LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (12416 1552 (:REWRITE ACL2-NUMBERP-X))
 (10964 15 (:REWRITE SUBLISTP-WHEN-PREFIXP))
 (6796 2359 (:REWRITE DEFAULT-PLUS-2))
 (5432 1358 (:REWRITE RATIONALP-X))
 (4971 60 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (4922 4394 (:REWRITE DEFAULT-CDR))
 (3712 60 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (3712 60 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (3530 2359 (:REWRITE DEFAULT-PLUS-1))
 (3530 15 (:REWRITE SUBLISTP-WHEN-ATOM-LEFT))
 (3375 60 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (2889 2866 (:REWRITE DEFAULT-CAR))
 (2866 2866 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (2197 2197 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2197 2197 (:REWRITE NORMALIZE-ADDENDS))
 (1940 194 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1383 1383 (:REWRITE REDUCE-INTEGERP-+))
 (1383 1383 (:REWRITE INTEGERP-MINUS-X))
 (1383 1383 (:META META-INTEGERP-CORRECT))
 (1358 1358 (:REWRITE REDUCE-RATIONALP-+))
 (1358 1358 (:REWRITE REDUCE-RATIONALP-*))
 (1358 1358 (:REWRITE RATIONALP-MINUS-X))
 (1358 1358 (:META META-RATIONALP-CORRECT))
 (1303 1303 (:REWRITE THE-FLOOR-BELOW))
 (1303 1303 (:REWRITE THE-FLOOR-ABOVE))
 (926 926 (:REWRITE FOLD-CONSTS-IN-+))
 (926 926 (:REWRITE |(+ c (+ d x))|))
 (823 719 (:REWRITE SIMPLIFY-SUMS-<))
 (823 719 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (798 721 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (721 721 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (719 719 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (719 719 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (719 719 (:REWRITE INTEGERP-<-CONSTANT))
 (719 719 (:REWRITE CONSTANT-<-INTEGERP))
 (719 719 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (719 719 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (719 719 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (719 719 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (719 719 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (719 719 (:REWRITE |(< c (- x))|))
 (719 719 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (719 719 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (719 719 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (719 719 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (719 719 (:REWRITE |(< (/ x) (/ y))|))
 (719 719 (:REWRITE |(< (- x) c)|))
 (719 719 (:REWRITE |(< (- x) (- y))|))
 (536 146 (:REWRITE ACL2S::EVENS-INTEGER-LISTP-SIG))
 (388 194 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (375 45 (:REWRITE LEN-WHEN-PREFIXP))
 (341 341 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (341 341 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (341 341 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (341 341 (:REWRITE CONSP-BY-LEN))
 (334 79 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (314 314 (:TYPE-PRESCRIPTION ACL2S::MSORT-NO-DUPS-CONTRACT-TP))
 (279 279 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (279 279 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (279 279 (:REWRITE |(< (/ x) 0)|))
 (279 279 (:REWRITE |(< (* x y) 0)|))
 (194 194 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (194 194 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (194 194 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (194 194 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (194 194 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (194 194 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (194 194 (:REWRITE |(equal c (/ x))|))
 (194 194 (:REWRITE |(equal c (- x))|))
 (194 194 (:REWRITE |(equal (/ x) c)|))
 (194 194 (:REWRITE |(equal (/ x) (/ y))|))
 (194 194 (:REWRITE |(equal (- x) c)|))
 (194 194 (:REWRITE |(equal (- x) (- y))|))
 (194 194 (:REWRITE |(< 0 (/ x))|))
 (194 194 (:REWRITE |(< 0 (* x y))|))
 (192 192 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (192 192 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (192 192 (:LINEAR LEN-WHEN-PREFIXP))
 (165 165 (:TYPE-PRESCRIPTION PREFIXP))
 (152 15 (:REWRITE SUBLISTP-WHEN-ATOM-RIGHT))
 (151 151 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (140 140 (:LINEAR CONS-SIZE-WHEN-MEMBER))
 (140 140 (:LINEAR ACL2S-SIZE-WHEN-MEMBER))
 (140 140 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (96 96 (:LINEAR INDEX-OF-<-LEN))
 (96 96 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
 (95 85 (:REWRITE DEFAULT-MINUS))
 (60 60 (:TYPE-PRESCRIPTION SUBLISTP))
 (60 60 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (60 60 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (60 60 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (60 60 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (52 52 (:TYPE-PRESCRIPTION NUMERATOR-ZERO))
 (43 43 (:REWRITE DEFAULT-RATIONAL-NUMERATOR))
 (40 40 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (31 11 (:REWRITE ACL2S::CONS-INTEGER-LISTP-SIG))
 (16 16 (:REWRITE |arith (+ c (+ d x))|))
 (15 15 (:REWRITE SUBLISTP-COMPLETE))
 (11 11 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (7 7 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-<2))
 (7 7 (:REWRITE |(< (+ c/d x) y)|))
 (7 7 (:REWRITE |(< (+ (- c) x) y)|))
 (1 1 (:REWRITE INTEGERP==>DENOMINATOR-=-1))
 (1 1 (:REWRITE DEFAULT-RATIONAL-DENOMINATOR))
 )
(ACL2S::INSERT-CONTRACT
 (24 24 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (14 14 (:REWRITE DEFAULT-CAR))
 (14 14 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (12 12 (:REWRITE REDUCE-INTEGERP-+))
 (12 12 (:REWRITE INTEGERP-MINUS-X))
 (12 12 (:META META-INTEGERP-CORRECT))
 (9 9 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (5 5 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (5 5 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (5 5 (:REWRITE CONSP-BY-LEN))
 (4 4 (:REWRITE THE-FLOOR-BELOW))
 (4 4 (:REWRITE THE-FLOOR-ABOVE))
 (4 4 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (4 4 (:REWRITE DEFAULT-LESS-THAN-2))
 (4 4 (:REWRITE DEFAULT-LESS-THAN-1))
 (3 3 (:REWRITE SIMPLIFY-SUMS-<))
 (3 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3 3 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (3 3 (:REWRITE INTEGERP-<-CONSTANT))
 (3 3 (:REWRITE CONSTANT-<-INTEGERP))
 (3 3 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (3 3 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (3 3 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (3 3 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (3 3 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (3 3 (:REWRITE |(< c (- x))|))
 (3 3 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (3 3 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (3 3 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (3 3 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (3 3 (:REWRITE |(< (/ x) (/ y))|))
 (3 3 (:REWRITE |(< (- x) c)|))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 (1 1 (:REWRITE CONSP-OF-CDR-BY-LEN))
 )
(ACL2S::INSERT-CONTRACT-TP)
(ACL2S::INSERT-CONTRACT-GENRULE)
(ACL2S::INSERT)
(ACL2S::INSERT-INDUCTION-SCHEME)
(ACL2S::INSERT-DEFINITION-RULE)
(ACL2S::INSERT-NO-DUPS-CONTRACT
 (58 2 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (58 2 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (58 2 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (58 2 (:REWRITE |(< x (/ y)) with (< 0 y)|))
 (34 34 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (31 31 (:REWRITE DEFAULT-CAR))
 (31 31 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (28 28 (:REWRITE THE-FLOOR-BELOW))
 (28 28 (:REWRITE THE-FLOOR-ABOVE))
 (28 28 (:REWRITE DEFAULT-LESS-THAN-2))
 (28 28 (:REWRITE DEFAULT-LESS-THAN-1))
 (16 16 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (16 16 (:REWRITE DEFAULT-TIMES-2))
 (16 16 (:REWRITE DEFAULT-TIMES-1))
 (15 15 (:REWRITE DEFAULT-CDR))
 (15 15 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (14 14 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (14 14 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (14 14 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (14 14 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (14 14 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (14 14 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (14 14 (:REWRITE |(equal c (/ x))|))
 (14 14 (:REWRITE |(equal (/ x) (/ y))|))
 (14 14 (:REWRITE |(equal (- x) (- y))|))
 (13 13 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (13 13 (:REWRITE SIMPLIFY-SUMS-<))
 (13 13 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (13 13 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (13 13 (:REWRITE REDUCE-INTEGERP-+))
 (13 13 (:REWRITE INTEGERP-MINUS-X))
 (13 13 (:REWRITE INTEGERP-<-CONSTANT))
 (13 13 (:REWRITE CONSTANT-<-INTEGERP))
 (13 13 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (13 13 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (13 13 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (13 13 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (13 13 (:REWRITE |(< c (- x))|))
 (13 13 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (13 13 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (13 13 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (13 13 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (13 13 (:REWRITE |(< (/ x) (/ y))|))
 (13 13 (:REWRITE |(< (- x) c)|))
 (13 13 (:REWRITE |(< (- x) (- y))|))
 (13 13 (:META META-INTEGERP-CORRECT))
 (12 12 (:REWRITE |(equal c (- x))|))
 (12 12 (:REWRITE |(equal (- x) c)|))
 (11 11 (:REWRITE O-INFP->NEQ-0))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (6 6 (:REWRITE |(< 0 (/ x))|))
 (6 6 (:REWRITE |(< 0 (* x y))|))
 (5 5 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (5 5 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (5 5 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (5 5 (:REWRITE CONSP-BY-LEN))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (4 4 (:REWRITE |(< (/ x) 0)|))
 (4 4 (:REWRITE |(< (* x y) 0)|))
 (2 2 (:REWRITE DEFAULT-DIVIDE))
 (2 2 (:REWRITE |(not (equal x (/ y)))|))
 (2 2 (:REWRITE |(equal x (/ y))|))
 (1 1 (:REWRITE CONSP-OF-CDR-BY-LEN))
 )
(ACL2S::INSERT-NO-DUPS-CONTRACT-TP)
(ACL2S::INSERT-NO-DUPS-CONTRACT-GENRULE)
(ACL2S::INSERT-NO-DUPS)
(ACL2S::INSERT-NO-DUPS-INDUCTION-SCHEME)
(ACL2S::INSERT-NO-DUPS-DEFINITION-RULE)
(ACL2S::ISORT-CONTRACT
 (83 1 (:DEFINITION ACL2S::INSERT-DEFINITION-RULE))
 (73 3 (:REWRITE DEFAULT-LESS-THAN-1))
 (36 8 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (20 20 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (18 2 (:REWRITE ACL2-NUMBERP-X))
 (11 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (10 10 (:REWRITE DEFAULT-CAR))
 (10 10 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (8 8 (:REWRITE REDUCE-INTEGERP-+))
 (8 8 (:REWRITE INTEGERP-MINUS-X))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 8 (:META META-INTEGERP-CORRECT))
 (8 2 (:REWRITE RATIONALP-X))
 (5 5 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (5 5 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (5 5 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (5 5 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE THE-FLOOR-BELOW))
 (3 3 (:REWRITE THE-FLOOR-ABOVE))
 (3 3 (:REWRITE DEFAULT-LESS-THAN-2))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (2 2 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (2 2 (:REWRITE REDUCE-RATIONALP-+))
 (2 2 (:REWRITE REDUCE-RATIONALP-*))
 (2 2 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (2 2 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (2 2 (:REWRITE RATIONALP-MINUS-X))
 (2 2 (:REWRITE INTEGERP-<-CONSTANT))
 (2 2 (:REWRITE CONSTANT-<-INTEGERP))
 (2 2 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (2 2 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (2 2 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (2 2 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (2 2 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (2 2 (:REWRITE |(< c (- x))|))
 (2 2 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (2 2 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (2 2 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (2 2 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (2 2 (:REWRITE |(< (/ x) (/ y))|))
 (2 2 (:REWRITE |(< (- x) c)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-RATIONALP-CORRECT))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (1 1 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (1 1 (:REWRITE |(< 0 (/ x))|))
 (1 1 (:REWRITE |(< 0 (* x y))|))
 )
(ACL2S::ISORT-CONTRACT-TP)
(ACL2S::ISORT-CONTRACT-GENRULE)
(ACL2S::ISORT)
(ACL2S::ISORT-INDUCTION-SCHEME)
(ACL2S::ISORT-DEFINITION-RULE)
(ACL2S::ISORT-NO-DUPS-CONTRACT
 (106 1 (:DEFINITION ACL2S::INSERT-NO-DUPS-DEFINITION-RULE))
 (73 3 (:REWRITE DEFAULT-LESS-THAN-2))
 (36 8 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (28 4 (:REWRITE ACL2-NUMBERP-X))
 (20 20 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (12 3 (:REWRITE RATIONALP-X))
 (11 11 (:REWRITE DEFAULT-CAR))
 (11 11 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (11 6 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (10 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (9 9 (:REWRITE REDUCE-INTEGERP-+))
 (9 9 (:REWRITE INTEGERP-MINUS-X))
 (9 9 (:META META-INTEGERP-CORRECT))
 (8 8 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (5 5 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (5 5 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (5 5 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE THE-FLOOR-BELOW))
 (3 3 (:REWRITE THE-FLOOR-ABOVE))
 (3 3 (:REWRITE REDUCE-RATIONALP-+))
 (3 3 (:REWRITE REDUCE-RATIONALP-*))
 (3 3 (:REWRITE RATIONALP-MINUS-X))
 (3 3 (:META META-RATIONALP-CORRECT))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (2 2 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (2 2 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (2 2 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (2 2 (:REWRITE INTEGERP-<-CONSTANT))
 (2 2 (:REWRITE DEFAULT-LESS-THAN-1))
 (2 2 (:REWRITE CONSTANT-<-INTEGERP))
 (2 2 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (2 2 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (2 2 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (2 2 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (2 2 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (2 2 (:REWRITE |(< c (- x))|))
 (2 2 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (2 2 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (2 2 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (2 2 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (2 2 (:REWRITE |(< (/ x) (/ y))|))
 (2 2 (:REWRITE |(< (- x) c)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (1 1 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (1 1 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE |(equal c (/ x))|))
 (1 1 (:REWRITE |(equal c (- x))|))
 (1 1 (:REWRITE |(equal (/ x) c)|))
 (1 1 (:REWRITE |(equal (/ x) (/ y))|))
 (1 1 (:REWRITE |(equal (- x) c)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< (/ x) 0)|))
 (1 1 (:REWRITE |(< (* x y) 0)|))
 )
(ACL2S::ISORT-NO-DUPS-CONTRACT-TP)
(ACL2S::ISORT-NO-DUPS-CONTRACT-GENRULE)
(ACL2S::ISORT-NO-DUPS)
(ACL2S::ISORT-NO-DUPS-INDUCTION-SCHEME)
(ACL2S::ISORT-NO-DUPS-DEFINITION-RULE)
(ACL2S::INSERT-LEN
 (2361 82 (:REWRITE LEN-WHEN-ATOM))
 (923 320 (:REWRITE DEFAULT-PLUS-2))
 (764 37 (:DEFINITION ACL2-COUNT))
 (720 80 (:REWRITE ACL2-NUMBERP-X))
 (479 320 (:REWRITE DEFAULT-PLUS-1))
 (320 80 (:REWRITE RATIONALP-X))
 (305 305 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (305 305 (:REWRITE NORMALIZE-ADDENDS))
 (243 243 (:REWRITE DEFAULT-CDR))
 (211 211 (:REWRITE DEFAULT-CAR))
 (211 211 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (128 128 (:REWRITE THE-FLOOR-BELOW))
 (128 128 (:REWRITE THE-FLOOR-ABOVE))
 (128 128 (:REWRITE DEFAULT-LESS-THAN-2))
 (126 126 (:REWRITE FOLD-CONSTS-IN-+))
 (93 93 (:REWRITE REDUCE-INTEGERP-+))
 (93 93 (:REWRITE INTEGERP-MINUS-X))
 (93 93 (:META META-INTEGERP-CORRECT))
 (88 88 (:REWRITE SIMPLIFY-SUMS-<))
 (88 88 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (88 88 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (88 88 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (88 88 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (88 88 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (88 88 (:REWRITE INTEGERP-<-CONSTANT))
 (88 88 (:REWRITE CONSTANT-<-INTEGERP))
 (88 88 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (88 88 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (88 88 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (88 88 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (88 88 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (88 88 (:REWRITE |(< c (- x))|))
 (88 88 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (88 88 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (88 88 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (88 88 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (88 88 (:REWRITE |(< (/ x) (/ y))|))
 (88 88 (:REWRITE |(< (- x) c)|))
 (88 88 (:REWRITE |(< (- x) (- y))|))
 (80 80 (:REWRITE REDUCE-RATIONALP-+))
 (80 80 (:REWRITE REDUCE-RATIONALP-*))
 (80 80 (:REWRITE RATIONALP-MINUS-X))
 (80 80 (:META META-RATIONALP-CORRECT))
 (68 68 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (68 68 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (68 68 (:LINEAR LEN-WHEN-PREFIXP))
 (44 44 (:LINEAR CONS-SIZE-WHEN-MEMBER))
 (44 44 (:LINEAR ACL2S-SIZE-WHEN-MEMBER))
 (44 44 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (40 40 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (40 40 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (40 40 (:REWRITE |(< 0 (/ x))|))
 (40 40 (:REWRITE |(< 0 (* x y))|))
 (34 34 (:LINEAR INDEX-OF-<-LEN))
 (34 34 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
 (21 7 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (21 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (21 7 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (20 4 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (15 15 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (14 14 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (9 9 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (9 9 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (9 9 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (9 9 (:REWRITE CONSP-BY-LEN))
 (7 7 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (7 7 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (7 7 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (7 7 (:REWRITE |(equal c (/ x))|))
 (7 7 (:REWRITE |(equal c (- x))|))
 (7 7 (:REWRITE |(equal (/ x) c)|))
 (7 7 (:REWRITE |(equal (/ x) (/ y))|))
 (7 7 (:REWRITE |(equal (- x) c)|))
 (7 7 (:REWRITE |(equal (- x) (- y))|))
 (7 7 (:REWRITE |(equal (+ (- c) x) y)|))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (6 6 (:REWRITE DEFAULT-MINUS))
 (6 6 (:REWRITE |(< (/ x) 0)|))
 (6 6 (:REWRITE |(< (* x y) 0)|))
 (4 4 (:REWRITE DEFAULT-RATIONAL-NUMERATOR))
 (1 1 (:REWRITE CONSP-OF-CDR-BY-LEN))
 )
(ACL2S::ISORT-LEN
 (552 24 (:DEFINITION ACL2S-SIZE))
 (504 180 (:REWRITE DEFAULT-PLUS-2))
 (456 24 (:DEFINITION CONS-SIZE))
 (456 24 (:DEFINITION ACL2-COUNT))
 (371 69 (:REWRITE LEN-WHEN-ATOM))
 (276 180 (:REWRITE DEFAULT-PLUS-1))
 (223 36 (:DEFINITION ACL2S::INSERT-DEFINITION-RULE))
 (182 182 (:REWRITE DEFAULT-CDR))
 (180 180 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (180 180 (:REWRITE NORMALIZE-ADDENDS))
 (127 18 (:LINEAR ACL2S::ACL2S-SIZE-CONSP))
 (116 116 (:REWRITE DEFAULT-CAR))
 (116 116 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (73 3 (:REWRITE DEFAULT-LESS-THAN-1))
 (72 72 (:REWRITE FOLD-CONSTS-IN-+))
 (72 72 (:REWRITE |(+ c (+ d x))|))
 (54 54 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (54 54 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (54 54 (:LINEAR LEN-WHEN-PREFIXP))
 (42 42 (:REWRITE REDUCE-INTEGERP-+))
 (42 42 (:REWRITE INTEGERP-MINUS-X))
 (42 42 (:META META-INTEGERP-CORRECT))
 (36 36 (:LINEAR CONS-SIZE-WHEN-MEMBER))
 (36 36 (:LINEAR ACL2S-SIZE-WHEN-MEMBER))
 (36 36 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (27 27 (:LINEAR INDEX-OF-<-LEN))
 (27 27 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
 (20 4 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (18 2 (:REWRITE ACL2-NUMBERP-X))
 (15 5 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (15 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (15 5 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (14 14 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (11 11 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (8 2 (:REWRITE RATIONALP-X))
 (7 7 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (7 7 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (7 7 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (7 7 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (7 7 (:REWRITE CONSP-BY-LEN))
 (5 5 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (5 5 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (5 5 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (5 5 (:REWRITE |(equal c (/ x))|))
 (5 5 (:REWRITE |(equal c (- x))|))
 (5 5 (:REWRITE |(equal (/ x) c)|))
 (5 5 (:REWRITE |(equal (/ x) (/ y))|))
 (5 5 (:REWRITE |(equal (- x) c)|))
 (5 5 (:REWRITE |(equal (- x) (- y))|))
 (4 4 (:REWRITE |arith (+ c (+ d x))|))
 (3 3 (:REWRITE THE-FLOOR-BELOW))
 (3 3 (:REWRITE THE-FLOOR-ABOVE))
 (3 3 (:REWRITE DEFAULT-LESS-THAN-2))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (2 2 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (2 2 (:REWRITE REDUCE-RATIONALP-+))
 (2 2 (:REWRITE REDUCE-RATIONALP-*))
 (2 2 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (2 2 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (2 2 (:REWRITE RATIONALP-MINUS-X))
 (2 2 (:REWRITE INTEGERP-<-CONSTANT))
 (2 2 (:REWRITE CONSTANT-<-INTEGERP))
 (2 2 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (2 2 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (2 2 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (2 2 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (2 2 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (2 2 (:REWRITE |(< c (- x))|))
 (2 2 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (2 2 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (2 2 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (2 2 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (2 2 (:REWRITE |(< (/ x) (/ y))|))
 (2 2 (:REWRITE |(< (- x) c)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-RATIONALP-CORRECT))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (1 1 (:REWRITE |(< 0 (/ x))|))
 (1 1 (:REWRITE |(< 0 (* x y))|))
 )
(ACL2S::INSERT-NO-DUPS-LEN
 (3517 91 (:REWRITE LEN-WHEN-ATOM))
 (1051 375 (:REWRITE DEFAULT-PLUS-2))
 (840 41 (:DEFINITION ACL2-COUNT))
 (756 108 (:REWRITE ACL2-NUMBERP-X))
 (684 36 (:DEFINITION CONS-SIZE))
 (580 375 (:REWRITE DEFAULT-PLUS-1))
 (336 336 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (324 81 (:REWRITE RATIONALP-X))
 (304 61 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (282 282 (:REWRITE DEFAULT-CAR))
 (282 282 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (246 246 (:REWRITE DEFAULT-CDR))
 (231 1 (:LINEAR ACL2S-SIZE-CAR-CDR-LINEAR))
 (203 7 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (203 7 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (203 7 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (203 7 (:REWRITE |(< x (/ y)) with (< 0 y)|))
 (197 1 (:LINEAR ACL2-COUNT-CAR-CDR-LINEAR))
 (183 183 (:REWRITE THE-FLOOR-BELOW))
 (183 183 (:REWRITE THE-FLOOR-ABOVE))
 (165 156 (:REWRITE DEFAULT-LESS-THAN-1))
 (135 135 (:REWRITE FOLD-CONSTS-IN-+))
 (129 129 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (128 128 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (118 118 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (118 118 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (118 118 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (118 118 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (118 118 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (118 118 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (118 118 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (118 118 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (118 118 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (118 118 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (118 118 (:REWRITE |(< (/ x) (/ y))|))
 (118 118 (:REWRITE |(< (- x) (- y))|))
 (113 113 (:REWRITE INTEGERP-<-CONSTANT))
 (113 113 (:REWRITE CONSTANT-<-INTEGERP))
 (113 113 (:REWRITE |(< c (- x))|))
 (113 113 (:REWRITE |(< (- x) c)|))
 (97 97 (:REWRITE REDUCE-INTEGERP-+))
 (97 97 (:REWRITE INTEGERP-MINUS-X))
 (97 97 (:META META-INTEGERP-CORRECT))
 (88 61 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (81 81 (:REWRITE REDUCE-RATIONALP-+))
 (81 81 (:REWRITE REDUCE-RATIONALP-*))
 (81 81 (:REWRITE RATIONALP-MINUS-X))
 (81 81 (:META META-RATIONALP-CORRECT))
 (61 61 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (61 61 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (61 61 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (61 61 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (61 61 (:REWRITE |(equal c (/ x))|))
 (61 61 (:REWRITE |(equal (/ x) (/ y))|))
 (61 61 (:REWRITE |(equal (- x) (- y))|))
 (56 56 (:REWRITE DEFAULT-TIMES-2))
 (56 56 (:REWRITE DEFAULT-TIMES-1))
 (54 54 (:REWRITE |(equal c (- x))|))
 (54 54 (:REWRITE |(equal (- x) c)|))
 (46 46 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (46 46 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (46 46 (:REWRITE |(< (/ x) 0)|))
 (46 46 (:REWRITE |(< (* x y) 0)|))
 (33 33 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (26 26 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (26 26 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (26 26 (:REWRITE O-INFP->NEQ-0))
 (26 26 (:REWRITE |(< 0 (* x y))|))
 (26 26 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (26 26 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (26 26 (:LINEAR LEN-WHEN-PREFIXP))
 (22 22 (:LINEAR CONS-SIZE-WHEN-MEMBER))
 (22 22 (:LINEAR ACL2S-SIZE-WHEN-MEMBER))
 (22 22 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (21 21 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (20 4 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (13 13 (:LINEAR INDEX-OF-<-LEN))
 (13 13 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
 (12 12 (:REWRITE DEFAULT-DIVIDE))
 (12 6 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (9 9 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-<2))
 (8 8 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (8 8 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (8 8 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (8 8 (:REWRITE CONSP-BY-LEN))
 (7 7 (:REWRITE |(not (equal x (/ y)))|))
 (7 7 (:REWRITE |(equal x (/ y))|))
 (6 6 (:REWRITE |(< (+ c/d x) y)|))
 (6 6 (:REWRITE |(< (+ (- c) x) y)|))
 (5 5 (:REWRITE DEFAULT-MINUS))
 (4 4 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-<1))
 (3 3 (:REWRITE DEFAULT-RATIONAL-NUMERATOR))
 (2 2 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (1 1 (:REWRITE |(< y (+ (- c) x))|))
 (1 1 (:REWRITE |(< x (+ c/d y))|))
 )
(ACL2S::ISORT-NO-DUPS-LEN
 (1875 15 (:REWRITE LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (1788 5 (:REWRITE SUBLISTP-WHEN-PREFIXP))
 (1579 20 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (876 310 (:REWRITE DEFAULT-PLUS-2))
 (700 37 (:DEFINITION CONS-SIZE))
 (471 310 (:REWRITE DEFAULT-PLUS-1))
 (470 20 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (308 308 (:REWRITE DEFAULT-CDR))
 (306 306 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (306 306 (:REWRITE NORMALIZE-ADDENDS))
 (224 32 (:REWRITE ACL2-NUMBERP-X))
 (200 200 (:REWRITE DEFAULT-CAR))
 (200 200 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (125 15 (:REWRITE LEN-WHEN-PREFIXP))
 (122 122 (:REWRITE FOLD-CONSTS-IN-+))
 (122 122 (:REWRITE |(+ c (+ d x))|))
 (96 24 (:REWRITE RATIONALP-X))
 (80 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (77 20 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (77 20 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (73 73 (:REWRITE REDUCE-INTEGERP-+))
 (73 73 (:REWRITE INTEGERP-MINUS-X))
 (73 73 (:META META-INTEGERP-CORRECT))
 (66 34 (:REWRITE SIMPLIFY-SUMS-<))
 (66 34 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (56 5 (:REWRITE SUBLISTP-WHEN-ATOM-LEFT))
 (55 55 (:TYPE-PRESCRIPTION PREFIXP))
 (50 34 (:REWRITE DEFAULT-LESS-THAN-1))
 (42 42 (:REWRITE THE-FLOOR-BELOW))
 (42 42 (:REWRITE THE-FLOOR-ABOVE))
 (41 34 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (36 36 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (36 36 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (36 36 (:LINEAR LEN-WHEN-PREFIXP))
 (34 34 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (34 34 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (34 34 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (34 34 (:REWRITE INTEGERP-<-CONSTANT))
 (34 34 (:REWRITE CONSTANT-<-INTEGERP))
 (34 34 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (34 34 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (34 34 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (34 34 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (34 34 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (34 34 (:REWRITE |(< c (- x))|))
 (34 34 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (34 34 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (34 34 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (34 34 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (34 34 (:REWRITE |(< (/ x) (/ y))|))
 (34 34 (:REWRITE |(< (- x) c)|))
 (34 34 (:REWRITE |(< (- x) (- y))|))
 (26 26 (:LINEAR CONS-SIZE-WHEN-MEMBER))
 (26 26 (:LINEAR ACL2S-SIZE-WHEN-MEMBER))
 (26 26 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (24 24 (:REWRITE REDUCE-RATIONALP-+))
 (24 24 (:REWRITE REDUCE-RATIONALP-*))
 (24 24 (:REWRITE RATIONALP-MINUS-X))
 (24 24 (:META META-RATIONALP-CORRECT))
 (20 20 (:TYPE-PRESCRIPTION SUBLISTP))
 (20 20 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (20 20 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (20 20 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (20 20 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (20 4 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (18 18 (:LINEAR INDEX-OF-<-LEN))
 (18 18 (:LINEAR STR::COUNT-LEADING-CHARSET-LEN))
 (16 8 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (15 15 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (11 5 (:REWRITE SUBLISTP-WHEN-ATOM-RIGHT))
 (10 10 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (10 10 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (10 10 (:REWRITE |(< (/ x) 0)|))
 (10 10 (:REWRITE |(< (* x y) 0)|))
 (8 8 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (8 8 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (8 8 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (8 8 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (8 8 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (8 8 (:REWRITE CONSP-BY-LEN))
 (8 8 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (8 8 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (8 8 (:REWRITE |(equal c (/ x))|))
 (8 8 (:REWRITE |(equal c (- x))|))
 (8 8 (:REWRITE |(equal (/ x) c)|))
 (8 8 (:REWRITE |(equal (/ x) (/ y))|))
 (8 8 (:REWRITE |(equal (- x) c)|))
 (8 8 (:REWRITE |(equal (- x) (- y))|))
 (5 5 (:REWRITE SUBLISTP-COMPLETE))
 (2 2 (:REWRITE DEFAULT-MINUS))
 (1 1 (:REWRITE DEFAULT-RATIONAL-NUMERATOR))
 (1 1 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (1 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-<2))
 (1 1 (:REWRITE |(< (+ c/d x) y)|))
 (1 1 (:REWRITE |(< (+ (- c) x) y)|))
 )
(ACL2S::REM-DUPS-SORTED-CONTRACT
 (41 41 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (27 27 (:REWRITE DEFAULT-CDR))
 (26 26 (:REWRITE DEFAULT-CAR))
 (26 26 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (20 4 (:REWRITE ACL2-NUMBERP-X))
 (20 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (15 15 (:REWRITE REDUCE-INTEGERP-+))
 (15 15 (:REWRITE INTEGERP-MINUS-X))
 (15 15 (:META META-INTEGERP-CORRECT))
 (8 2 (:REWRITE RATIONALP-X))
 (7 7 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (7 7 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (7 7 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (7 7 (:REWRITE CONSP-BY-LEN))
 (4 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 2 (:REWRITE REDUCE-RATIONALP-+))
 (2 2 (:REWRITE REDUCE-RATIONALP-*))
 (2 2 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (2 2 (:REWRITE RATIONALP-MINUS-X))
 (2 2 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (2 2 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (2 2 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (2 2 (:REWRITE |(equal c (/ x))|))
 (2 2 (:REWRITE |(equal c (- x))|))
 (2 2 (:REWRITE |(equal (/ x) c)|))
 (2 2 (:REWRITE |(equal (/ x) (/ y))|))
 (2 2 (:REWRITE |(equal (- x) c)|))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:META META-RATIONALP-CORRECT))
 )
(ACL2S::REM-DUPS-SORTED-CONTRACT-TP)
(ACL2S::REM-DUPS-SORTED-CONTRACT-GENRULE)
(ACL2S::REM-DUPS-SORTED)
(ACL2S::REM-DUPS-SORTED-INDUCTION-SCHEME)
(ACL2S::REM-DUPS-SORTED-DEFINITION-RULE)
(ACL2S::FILL-IN-LIST-CONTRACT
 (52 52 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (45 9 (:REWRITE |(+ c (+ d x))|))
 (36 36 (:REWRITE DEFAULT-PLUS-2))
 (36 36 (:REWRITE DEFAULT-PLUS-1))
 (31 31 (:REWRITE REDUCE-INTEGERP-+))
 (31 31 (:REWRITE INTEGERP-MINUS-X))
 (31 31 (:META META-INTEGERP-CORRECT))
 (27 27 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (27 27 (:REWRITE NORMALIZE-ADDENDS))
 (24 24 (:REWRITE DEFAULT-CAR))
 (24 24 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (19 19 (:REWRITE DEFAULT-CDR))
 (14 14 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (14 14 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (14 14 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (14 14 (:REWRITE CONSP-BY-LEN))
 (9 9 (:REWRITE THE-FLOOR-BELOW))
 (9 9 (:REWRITE THE-FLOOR-ABOVE))
 (9 9 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (9 9 (:REWRITE DEFAULT-LESS-THAN-2))
 (9 9 (:REWRITE DEFAULT-LESS-THAN-1))
 (8 8 (:REWRITE SIMPLIFY-SUMS-<))
 (8 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (8 8 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (8 8 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (8 8 (:REWRITE INTEGERP-<-CONSTANT))
 (8 8 (:REWRITE CONSTANT-<-INTEGERP))
 (8 8 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (8 8 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (8 8 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (8 8 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (8 8 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (8 8 (:REWRITE |(< c (- x))|))
 (8 8 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (8 8 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (8 8 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (8 8 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (8 8 (:REWRITE |(< (/ x) (/ y))|))
 (8 8 (:REWRITE |(< (- x) c)|))
 (8 8 (:REWRITE |(< (- x) (- y))|))
 (7 7 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (7 7 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (7 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (7 7 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (7 7 (:REWRITE O-INFP->NEQ-0))
 (7 7 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (7 7 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (7 7 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (7 7 (:REWRITE |(equal c (/ x))|))
 (7 7 (:REWRITE |(equal c (- x))|))
 (7 7 (:REWRITE |(equal (/ x) c)|))
 (7 7 (:REWRITE |(equal (/ x) (/ y))|))
 (7 7 (:REWRITE |(equal (- x) c)|))
 (7 7 (:REWRITE |(equal (- x) (- y))|))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (5 5 (:REWRITE |(< (/ x) 0)|))
 (5 5 (:REWRITE |(< (* x y) 0)|))
 (3 3 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-<2))
 (3 3 (:REWRITE |(equal (+ (- c) x) y)|))
 (3 3 (:REWRITE |(< (+ c/d x) y)|))
 (3 3 (:REWRITE |(< (+ (- c) x) y)|))
 (1 1 (:REWRITE CONSP-OF-CDR-BY-LEN))
 )
(ACL2S::FILL-IN-LIST-CONTRACT-TP)
(ACL2S::FILL-IN-LIST-CONTRACT-GENRULE)
(ACL2S::FILL-IN-LIST)
(ACL2S::FILL-IN-LIST-INDUCTION-SCHEME)
(ACL2S::FILL-IN-LIST-DEFINITION-RULE)
(ACL2S::MAKE-UNIQUE-ORDERED-CONTRACT
 (484 1 (:DEFINITION ACL2S::FILL-IN-LIST-DEFINITION-RULE))
 (446 2 (:DEFINITION ACL2S::MSORT-NO-DUPS-DEFINITION-RULE))
 (410 2 (:DEFINITION ACL2S::MERGE2-NO-DUPS-DEFINITION-RULE))
 (365 15 (:REWRITE DEFAULT-LESS-THAN-2))
 (273 1 (:DEFINITION NATP))
 (267 1 (:LINEAR ACL2S::MSORT-NO-DUPS-LEN))
 (244 12 (:REWRITE DEFAULT-LESS-THAN-1))
 (146 18 (:REWRITE ACL2-NUMBERP-X))
 (65 4 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (64 16 (:REWRITE RATIONALP-X))
 (64 4 (:DEFINITION LEN))
 (51 51 (:TYPE-PRESCRIPTION LEN))
 (42 25 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (40 25 (:REWRITE DEFAULT-PLUS-2))
 (40 8 (:REWRITE LEN-WHEN-ATOM))
 (38 2 (:DEFINITION INTEGER-LISTP))
 (33 31 (:REWRITE DEFAULT-CDR))
 (32 25 (:REWRITE DEFAULT-PLUS-1))
 (24 4 (:DEFINITION EVENS))
 (24 1 (:REWRITE |(+ y (+ x z))|))
 (23 23 (:REWRITE DEFAULT-CAR))
 (23 23 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (23 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (22 7 (:REWRITE |(+ c (+ d x))|))
 (19 19 (:REWRITE REDUCE-INTEGERP-+))
 (19 19 (:REWRITE INTEGERP-MINUS-X))
 (19 19 (:META META-INTEGERP-CORRECT))
 (18 9 (:REWRITE NORMALIZE-ADDENDS))
 (18 2 (:DEFINITION ODDS))
 (16 16 (:REWRITE REDUCE-RATIONALP-+))
 (16 16 (:REWRITE REDUCE-RATIONALP-*))
 (16 16 (:REWRITE RATIONALP-MINUS-X))
 (16 16 (:META META-RATIONALP-CORRECT))
 (15 15 (:REWRITE THE-FLOOR-BELOW))
 (15 15 (:REWRITE THE-FLOOR-ABOVE))
 (13 13 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (13 13 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (13 13 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (13 13 (:REWRITE CONSP-BY-LEN))
 (12 2 (:REWRITE |(+ y x)|))
 (10 2 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (9 7 (:REWRITE |(+ 0 x)|))
 (8 8 (:REWRITE SIMPLIFY-SUMS-<))
 (8 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (8 8 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (8 8 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (8 8 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (8 8 (:REWRITE INTEGERP-<-CONSTANT))
 (8 8 (:REWRITE CONSTANT-<-INTEGERP))
 (8 8 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (8 8 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (8 8 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (8 8 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (8 8 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (8 8 (:REWRITE |(< c (- x))|))
 (8 8 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (8 8 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (8 8 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (8 8 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (8 8 (:REWRITE |(< (/ x) (/ y))|))
 (8 8 (:REWRITE |(< (- x) c)|))
 (8 8 (:REWRITE |(< (- x) (- y))|))
 (7 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 6 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (5 5 (:TYPE-PRESCRIPTION ACL2S::MSORT-NO-DUPS-CONTRACT-TP))
 (4 4 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (4 4 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (4 2 (:DEFINITION FIX))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE |(equal c (/ x))|))
 (3 3 (:REWRITE |(equal c (- x))|))
 (3 3 (:REWRITE |(equal (/ x) c)|))
 (3 3 (:REWRITE |(equal (/ x) (/ y))|))
 (3 3 (:REWRITE |(equal (- x) c)|))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (3 3 (:REWRITE |(< (/ x) 0)|))
 (3 3 (:REWRITE |(< (* x y) 0)|))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 2 (:REWRITE |(< 0 (/ x))|))
 (2 2 (:REWRITE |(< 0 (* x y))|))
 (2 1 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (2 1 (:REWRITE DEFAULT-MINUS))
 (2 1 (:REWRITE BUBBLE-DOWN-+-MATCH-1))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE |(+ x (- x))|))
 )
(ACL2S::MAKE-UNIQUE-ORDERED-CONTRACT-TP)
(ACL2S::MAKE-UNIQUE-ORDERED-CONTRACT-GENRULE)
(ACL2S::MAKE-UNIQUE-ORDERED
 (669 3 (:DEFINITION ACL2S::MSORT-NO-DUPS-DEFINITION-RULE))
 (615 3 (:DEFINITION ACL2S::MERGE2-NO-DUPS-DEFINITION-RULE))
 (439 19 (:REWRITE DEFAULT-LESS-THAN-2))
 (366 16 (:REWRITE DEFAULT-LESS-THAN-1))
 (253 8 (:REWRITE LEN-WHEN-ATOM))
 (192 24 (:REWRITE ACL2-NUMBERP-X))
 (84 21 (:REWRITE RATIONALP-X))
 (54 4 (:DEFINITION LEN))
 (45 42 (:REWRITE DEFAULT-CDR))
 (36 6 (:DEFINITION EVENS))
 (30 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (29 29 (:REWRITE DEFAULT-CAR))
 (29 29 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (27 3 (:DEFINITION ODDS))
 (25 25 (:REWRITE REDUCE-INTEGERP-+))
 (25 25 (:REWRITE INTEGERP-MINUS-X))
 (25 25 (:META META-INTEGERP-CORRECT))
 (21 21 (:REWRITE REDUCE-RATIONALP-+))
 (21 21 (:REWRITE REDUCE-RATIONALP-*))
 (21 21 (:REWRITE RATIONALP-MINUS-X))
 (21 21 (:META META-RATIONALP-CORRECT))
 (19 19 (:REWRITE THE-FLOOR-BELOW))
 (19 19 (:REWRITE THE-FLOOR-ABOVE))
 (12 10 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (11 10 (:REWRITE |(< (- x) c)|))
 (11 10 (:REWRITE |(< (- x) (- y))|))
 (11 6 (:REWRITE DEFAULT-PLUS-2))
 (10 10 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (10 10 (:REWRITE SIMPLIFY-SUMS-<))
 (10 10 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (10 10 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (10 10 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (10 10 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (10 10 (:REWRITE INTEGERP-<-CONSTANT))
 (10 10 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (10 10 (:REWRITE CONSTANT-<-INTEGERP))
 (10 10 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (10 10 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (10 10 (:REWRITE CONSP-BY-LEN))
 (10 10 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (10 10 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (10 10 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (10 10 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (10 10 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (10 10 (:REWRITE |(< c (- x))|))
 (10 10 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (10 10 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (10 10 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (10 10 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (10 10 (:REWRITE |(< (/ x) (/ y))|))
 (7 6 (:REWRITE DEFAULT-PLUS-1))
 (6 6 (:TYPE-PRESCRIPTION ACL2S::MSORT-NO-DUPS-CONTRACT-TP))
 (6 6 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (6 6 (:REWRITE NORMALIZE-ADDENDS))
 (6 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (4 4 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (4 4 (:REWRITE |(< (/ x) 0)|))
 (4 4 (:REWRITE |(< (* x y) 0)|))
 (4 2 (:REWRITE DEFAULT-MINUS))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (3 3 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (3 3 (:REWRITE |(equal c (/ x))|))
 (3 3 (:REWRITE |(equal c (- x))|))
 (3 3 (:REWRITE |(equal (/ x) c)|))
 (3 3 (:REWRITE |(equal (/ x) (/ y))|))
 (3 3 (:REWRITE |(equal (- x) c)|))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (3 3 (:REWRITE |(< 0 (/ x))|))
 (3 3 (:REWRITE |(< 0 (* x y))|))
 (1 1 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (1 1 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-<2))
 (1 1 (:REWRITE |(< (+ c/d x) y)|))
 (1 1 (:REWRITE |(< (+ (- c) x) y)|))
 )
(ACL2S::MAKE-UNIQUE-ORDERED-DEFINITION-RULE)
(ACL2S::MAKE-NONDEC-CONTRACT
 (193 1 (:DEFINITION ACL2S::MSORT-DEFINITION-RULE))
 (175 1 (:DEFINITION ACL2S::MERGE2-DEFINITION-RULE))
 (146 6 (:REWRITE DEFAULT-LESS-THAN-2))
 (121 5 (:REWRITE DEFAULT-LESS-THAN-1))
 (54 6 (:REWRITE ACL2-NUMBERP-X))
 (38 2 (:DEFINITION INTEGER-LISTP))
 (24 6 (:REWRITE RATIONALP-X))
 (12 11 (:REWRITE DEFAULT-CDR))
 (12 7 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (12 2 (:DEFINITION EVENS))
 (10 2 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (9 1 (:DEFINITION ODDS))
 (8 8 (:REWRITE REDUCE-INTEGERP-+))
 (8 8 (:REWRITE INTEGERP-MINUS-X))
 (8 8 (:REWRITE DEFAULT-CAR))
 (8 8 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (8 8 (:META META-INTEGERP-CORRECT))
 (6 6 (:REWRITE THE-FLOOR-BELOW))
 (6 6 (:REWRITE THE-FLOOR-ABOVE))
 (6 6 (:REWRITE REDUCE-RATIONALP-+))
 (6 6 (:REWRITE REDUCE-RATIONALP-*))
 (6 6 (:REWRITE RATIONALP-MINUS-X))
 (6 6 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (6 6 (:META META-RATIONALP-CORRECT))
 (4 4 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (4 4 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (4 4 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (4 4 (:REWRITE CONSP-BY-LEN))
 (3 3 (:REWRITE SIMPLIFY-SUMS-<))
 (3 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (3 3 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (3 3 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (3 3 (:REWRITE INTEGERP-<-CONSTANT))
 (3 3 (:REWRITE CONSTANT-<-INTEGERP))
 (3 3 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (3 3 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (3 3 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (3 3 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (3 3 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (3 3 (:REWRITE |(< c (- x))|))
 (3 3 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (3 3 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (3 3 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (3 3 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (3 3 (:REWRITE |(< (/ x) (/ y))|))
 (3 3 (:REWRITE |(< (- x) c)|))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:TYPE-PRESCRIPTION ACL2S::MSORT-CONTRACT-TP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (1 1 (:REWRITE |(< 0 (/ x))|))
 (1 1 (:REWRITE |(< 0 (* x y))|))
 (1 1 (:REWRITE |(< (/ x) 0)|))
 (1 1 (:REWRITE |(< (* x y) 0)|))
 )
(ACL2S::MAKE-NONDEC-CONTRACT-TP)
(ACL2S::MAKE-NONDEC-CONTRACT-GENRULE)
(ACL2S::MAKE-NONDEC)
(ACL2S::MAKE-NONDEC-DEFINITION-RULE)
(ACL2S::MAKE-UNIQUE-DECREASING-CONTRACT
 (484 1 (:DEFINITION ACL2S::FILL-IN-LIST-DEFINITION-RULE))
 (446 2 (:DEFINITION ACL2S::MSORT-NO-DUPS-DEFINITION-RULE))
 (410 2 (:DEFINITION ACL2S::MERGE2-NO-DUPS-DEFINITION-RULE))
 (365 15 (:REWRITE DEFAULT-LESS-THAN-2))
 (273 1 (:DEFINITION NATP))
 (267 1 (:LINEAR ACL2S::MSORT-NO-DUPS-LEN))
 (244 12 (:REWRITE DEFAULT-LESS-THAN-1))
 (146 18 (:REWRITE ACL2-NUMBERP-X))
 (65 32 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (65 4 (:REWRITE ACL2S::ACL2S-PREFER-POSITIVE-ADDENDS-EQUAL))
 (64 16 (:REWRITE RATIONALP-X))
 (64 4 (:DEFINITION LEN))
 (51 51 (:TYPE-PRESCRIPTION LEN))
 (44 2 (:DEFINITION INTEGER-LISTP))
 (44 1 (:DEFINITION REV))
 (40 25 (:REWRITE DEFAULT-PLUS-2))
 (40 8 (:REWRITE LEN-WHEN-ATOM))
 (36 34 (:REWRITE DEFAULT-CDR))
 (32 25 (:REWRITE DEFAULT-PLUS-1))
 (25 25 (:REWRITE DEFAULT-CAR))
 (25 25 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (24 4 (:DEFINITION EVENS))
 (24 1 (:REWRITE |(+ y (+ x z))|))
 (23 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (22 7 (:REWRITE |(+ c (+ d x))|))
 (19 19 (:REWRITE REDUCE-INTEGERP-+))
 (19 19 (:REWRITE INTEGERP-MINUS-X))
 (19 19 (:META META-INTEGERP-CORRECT))
 (18 9 (:REWRITE NORMALIZE-ADDENDS))
 (18 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (18 2 (:DEFINITION ODDS))
 (17 17 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (17 17 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (17 17 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (17 17 (:REWRITE CONSP-BY-LEN))
 (16 16 (:REWRITE REDUCE-RATIONALP-+))
 (16 16 (:REWRITE REDUCE-RATIONALP-*))
 (16 16 (:REWRITE RATIONALP-MINUS-X))
 (16 16 (:META META-RATIONALP-CORRECT))
 (15 15 (:REWRITE THE-FLOOR-BELOW))
 (15 15 (:REWRITE THE-FLOOR-ABOVE))
 (15 2 (:REWRITE REV-WHEN-NOT-CONSP))
 (13 2 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (12 2 (:REWRITE |(+ y x)|))
 (12 1 (:DEFINITION BINARY-APPEND))
 (9 7 (:REWRITE |(+ 0 x)|))
 (8 8 (:REWRITE SIMPLIFY-SUMS-<))
 (8 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (8 8 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (8 8 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (8 8 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (8 8 (:REWRITE INTEGERP-<-CONSTANT))
 (8 8 (:REWRITE CONSTANT-<-INTEGERP))
 (8 8 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (8 8 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (8 8 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (8 8 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (8 8 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (8 8 (:REWRITE |(< c (- x))|))
 (8 8 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (8 8 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (8 8 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (8 8 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (8 8 (:REWRITE |(< (/ x) (/ y))|))
 (8 8 (:REWRITE |(< (- x) c)|))
 (8 8 (:REWRITE |(< (- x) (- y))|))
 (8 6 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (8 1 (:REWRITE REV-UNDER-IFF))
 (7 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5 5 (:TYPE-PRESCRIPTION ACL2S::MSORT-NO-DUPS-CONTRACT-TP))
 (4 4 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (4 4 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (4 4 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (4 2 (:DEFINITION FIX))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE |(equal c (/ x))|))
 (3 3 (:REWRITE |(equal c (- x))|))
 (3 3 (:REWRITE |(equal (/ x) c)|))
 (3 3 (:REWRITE |(equal (/ x) (/ y))|))
 (3 3 (:REWRITE |(equal (- x) c)|))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (3 3 (:REWRITE |(< (/ x) 0)|))
 (3 3 (:REWRITE |(< (* x y) 0)|))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE |(< 0 (/ x))|))
 (2 2 (:REWRITE |(< 0 (* x y))|))
 (2 1 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (2 1 (:REWRITE DEFAULT-MINUS))
 (2 1 (:REWRITE BUBBLE-DOWN-+-MATCH-1))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE |(+ x (- x))|))
 )
(ACL2S::MAKE-UNIQUE-DECREASING-CONTRACT-TP)
(ACL2S::MAKE-UNIQUE-DECREASING-CONTRACT-GENRULE)
(ACL2S::MAKE-UNIQUE-DECREASING)
(ACL2S::MAKE-UNIQUE-DECREASING-DEFINITION-RULE)
(ACL2S::MAKE-NONINC-CONTRACT
 (193 1 (:DEFINITION ACL2S::MSORT-DEFINITION-RULE))
 (175 1 (:DEFINITION ACL2S::MERGE2-DEFINITION-RULE))
 (146 6 (:REWRITE DEFAULT-LESS-THAN-2))
 (121 5 (:REWRITE DEFAULT-LESS-THAN-1))
 (54 6 (:REWRITE ACL2-NUMBERP-X))
 (44 2 (:DEFINITION INTEGER-LISTP))
 (44 1 (:DEFINITION REV))
 (35 14 (:REWRITE CONSP-UNDER-IFF-WHEN-TRUE-LISTP))
 (24 6 (:REWRITE RATIONALP-X))
 (18 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (15 14 (:REWRITE DEFAULT-CDR))
 (15 2 (:REWRITE REV-WHEN-NOT-CONSP))
 (13 2 (:REWRITE ACL2S::CDR-INTEGER-LISTP-SIG))
 (12 2 (:DEFINITION EVENS))
 (12 1 (:DEFINITION BINARY-APPEND))
 (10 10 (:REWRITE DEFAULT-CAR))
 (10 10 (:REWRITE CAR-WHEN-ALL-EQUALP))
 (9 1 (:DEFINITION ODDS))
 (8 8 (:REWRITE REDUCE-INTEGERP-+))
 (8 8 (:REWRITE INTEGERP-MINUS-X))
 (8 8 (:REWRITE FIELD-NOT-EMPTY-IMPLIES-RECORD-NOT-EMPTY1))
 (8 8 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (8 8 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (8 8 (:REWRITE CONSP-BY-LEN))
 (8 8 (:META META-INTEGERP-CORRECT))
 (8 6 (:REWRITE ACL2S::DEF=>INTEGER-LIST))
 (8 1 (:REWRITE REV-UNDER-IFF))
 (6 6 (:REWRITE THE-FLOOR-BELOW))
 (6 6 (:REWRITE THE-FLOOR-ABOVE))
 (6 6 (:REWRITE REDUCE-RATIONALP-+))
 (6 6 (:REWRITE REDUCE-RATIONALP-*))
 (6 6 (:REWRITE RATIONALP-MINUS-X))
 (6 6 (:META META-RATIONALP-CORRECT))
 (3 3 (:REWRITE SIMPLIFY-SUMS-<))
 (3 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (3 3 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (3 3 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (3 3 (:REWRITE INTEGERP-<-CONSTANT))
 (3 3 (:REWRITE CONSTANT-<-INTEGERP))
 (3 3 (:REWRITE ACL2S::ACL2S-REDUCE-ADDITIVE-CONSTANT-<))
 (3 3 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (3 3 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (3 3 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (3 3 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (3 3 (:REWRITE |(< c (- x))|))
 (3 3 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (3 3 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (3 3 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (3 3 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (3 3 (:REWRITE |(< (/ x) (/ y))|))
 (3 3 (:REWRITE |(< (- x) c)|))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:TYPE-PRESCRIPTION ACL2S::MSORT-CONTRACT-TP))
 (2 2 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (1 1 (:REWRITE |(< 0 (/ x))|))
 (1 1 (:REWRITE |(< 0 (* x y))|))
 (1 1 (:REWRITE |(< (/ x) 0)|))
 (1 1 (:REWRITE |(< (* x y) 0)|))
 )
(ACL2S::MAKE-NONINC-CONTRACT-TP)
(ACL2S::MAKE-NONINC-CONTRACT-GENRULE)
(ACL2S::MAKE-NONINC)
(ACL2S::MAKE-NONINC-DEFINITION-RULE)