(ADE::DELETE-TO-EQ
 (2 2 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::ALISTP-DELETE-TO-EQ
 (25 25 (:REWRITE DEFAULT-CAR))
 (12 12 (:REWRITE DEFAULT-CDR))
 )
(ADE::UPDATE-ALIST
 (2 2 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::SYMBOL-ALISTP-UPDATE-ALIST
 (52 50 (:REWRITE DEFAULT-CAR))
 (13 12 (:REWRITE DEFAULT-CDR))
 )
(ADE::CONSP-OF-ASSOC-UPDATE-ALIST-LEMMA
 (137 124 (:REWRITE DEFAULT-CAR))
 (49 46 (:REWRITE DEFAULT-CDR))
 )
(ADE::STRIP-CARS-UPDATE-ALIST
 (36 35 (:REWRITE DEFAULT-CAR))
 (13 12 (:REWRITE DEFAULT-CDR))
 )
(ADE::UPDATE-ALIST-DIFF-KEYS
 (149 139 (:REWRITE DEFAULT-CAR))
 (78 72 (:REWRITE DEFAULT-CDR))
 )
(ADE::NFIX-OF-NAT
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 )
(ADE::LEN-0-IS-ATOM
 (9 5 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE DEFAULT-CDR))
 )
(ADE::POS-LEN=>CONS)
(ADE::OPEN-LEN
 (10 5 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE DEFAULT-+-1))
 )
(ADE::OPEN-NTH
 (11 5 (:REWRITE ZP-OPEN))
 (8 8 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-+-1))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 )
(ADE::LEFT-ASSOCIATIVITY-OF-APPEND
 (45 18 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (24 18 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (18 18 (:TYPE-PRESCRIPTION TRUE-LISTP))
 )
(ADE::NTH-APPEND-<-LEN
 (180 90 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (90 90 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (90 90 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (26 9 (:REWRITE DEFAULT-CDR))
 (24 17 (:REWRITE DEFAULT-<-2))
 (19 13 (:REWRITE DEFAULT-+-2))
 (18 18 (:REWRITE DEFAULT-CAR))
 (17 17 (:REWRITE DEFAULT-<-1))
 (13 13 (:REWRITE DEFAULT-+-1))
 (10 10 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (10 10 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (8 8 (:REWRITE ZP-OPEN))
 (6 2 (:REWRITE CAR-OF-APPEND))
 (4 4 (:REWRITE CONSP-OF-APPEND))
 (2 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::NTH-APPEND->=-LEN
 (95 61 (:REWRITE DEFAULT-+-2))
 (72 52 (:REWRITE DEFAULT-CDR))
 (61 61 (:REWRITE DEFAULT-+-1))
 (30 30 (:REWRITE DEFAULT-CAR))
 (22 11 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (20 14 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (14 14 (:REWRITE DEFAULT-<-1))
 (11 11 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (11 11 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (8 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::SYMBOL-LISTP-APPEND
 (30 13 (:REWRITE DEFAULT-CDR))
 (21 19 (:REWRITE DEFAULT-CAR))
 (9 3 (:REWRITE CAR-OF-APPEND))
 (6 6 (:REWRITE CONSP-OF-APPEND))
 (5 5 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (3 3 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::SYMBOL-LISTP-REMOVE-DUPLICATES-EQ
 (102 6 (:DEFINITION MEMBER-EQUAL))
 (98 14 (:REWRITE SUBSETP-CAR-MEMBER))
 (30 29 (:REWRITE DEFAULT-CAR))
 (27 26 (:REWRITE DEFAULT-CDR))
 (18 18 (:REWRITE SUBSETP-TRANS2))
 (18 18 (:REWRITE SUBSETP-TRANS))
 (16 16 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (16 16 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (14 14 (:REWRITE SUBSETP-MEMBER . 4))
 (14 14 (:REWRITE INTERSECTP-MEMBER . 3))
 (14 14 (:REWRITE INTERSECTP-MEMBER . 2))
 (14 2 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (13 13 (:REWRITE SUBSETP-MEMBER . 2))
 (12 12 (:REWRITE MEMBER-WHEN-ATOM))
 )
(ADE::TRUE-LISTP-UNION-LEMMA
 (70 10 (:REWRITE SUBSETP-CAR-MEMBER))
 (68 4 (:DEFINITION MEMBER-EQUAL))
 (19 19 (:REWRITE DEFAULT-CDR))
 (13 13 (:REWRITE DEFAULT-CAR))
 (12 12 (:REWRITE SUBSETP-TRANS2))
 (12 12 (:REWRITE SUBSETP-TRANS))
 (10 10 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (10 10 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (10 10 (:REWRITE SUBSETP-MEMBER . 4))
 (10 10 (:REWRITE INTERSECTP-MEMBER . 3))
 (10 10 (:REWRITE INTERSECTP-MEMBER . 2))
 (9 9 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE MEMBER-WHEN-ATOM))
 )
(ADE::MEMBER-APPEND
 (6 3 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (3 3 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (3 3 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (3 3 (:REWRITE SUBSETP-TRANS2))
 (3 3 (:REWRITE SUBSETP-TRANS))
 (2 2 (:REWRITE SUBSETP-MEMBER . 4))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 3))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 2))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 )
(ADE::NOT-MEMBER-APPEND
 (98 6 (:REWRITE SUBSETP-APPEND1))
 (84 2 (:DEFINITION MEMBER-EQUAL))
 (76 5 (:REWRITE SUBSETP-MEMBER . 1))
 (47 27 (:REWRITE SUBSETP-TRANS2))
 (27 27 (:REWRITE SUBSETP-TRANS))
 (21 21 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (21 21 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (14 2 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (7 7 (:REWRITE SUBSETP-MEMBER . 4))
 (7 7 (:REWRITE INTERSECTP-MEMBER . 3))
 (7 7 (:REWRITE INTERSECTP-MEMBER . 2))
 (6 3 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (5 5 (:REWRITE SUBSETP-MEMBER . 2))
 (5 1 (:DEFINITION BINARY-APPEND))
 (4 4 (:REWRITE MEMBER-WHEN-ATOM))
 (3 3 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (3 3 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (2 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (1 1 (:REWRITE ADE::MEMBER-APPEND))
 )
(ADE::NOT-MEMBER=>NOT-EQUAL-NTH
 (40 4 (:DEFINITION MEMBER-EQUAL))
 (20 20 (:REWRITE DEFAULT-CAR))
 (11 11 (:REWRITE ZP-OPEN))
 (10 10 (:REWRITE SUBSETP-MEMBER . 4))
 (10 10 (:REWRITE SUBSETP-MEMBER . 3))
 (10 10 (:REWRITE SUBSETP-MEMBER . 2))
 (10 10 (:REWRITE INTERSECTP-MEMBER . 3))
 (10 10 (:REWRITE INTERSECTP-MEMBER . 2))
 (10 10 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE DEFAULT-+-2))
 (6 6 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 )
(ADE::SUBSETP=>MEMBER-NTH
 (104 9 (:DEFINITION MEMBER-EQUAL))
 (101 19 (:REWRITE SUBSETP-MEMBER . 2))
 (21 13 (:REWRITE DEFAULT-<-1))
 (19 13 (:REWRITE DEFAULT-<-2))
 (17 12 (:REWRITE SUBSETP-TRANS2))
 (16 16 (:REWRITE DEFAULT-CDR))
 (15 9 (:REWRITE DEFAULT-+-2))
 (14 14 (:REWRITE DEFAULT-CAR))
 (12 12 (:REWRITE SUBSETP-TRANS))
 (11 11 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (9 9 (:REWRITE DEFAULT-+-1))
 (8 8 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (7 7 (:REWRITE SUBSETP-MEMBER . 4))
 (7 7 (:REWRITE SUBSETP-MEMBER . 3))
 (7 7 (:REWRITE INTERSECTP-MEMBER . 3))
 (7 7 (:REWRITE INTERSECTP-MEMBER . 2))
 (6 6 (:REWRITE ZP-OPEN))
 (6 6 (:REWRITE MEMBER-WHEN-ATOM))
 )
(ADE::MEMBER-OF-TRUE-LIST-LIST-IS-TRUE-LIST
 (14 14 (:REWRITE DEFAULT-CAR))
 (14 8 (:REWRITE SUBSETP-MEMBER . 3))
 (14 7 (:DEFINITION TRUE-LISTP))
 (11 11 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE SUBSETP-MEMBER . 4))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (8 8 (:REWRITE INTERSECTP-MEMBER . 3))
 (8 8 (:REWRITE INTERSECTP-MEMBER . 2))
 (2 2 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 )
(ADE::ALISTP-PAIRLIS$
 (11 10 (:REWRITE DEFAULT-CAR))
 (9 8 (:REWRITE DEFAULT-CDR))
 )
(ADE::LEN-PAIRLIS$
 (14 7 (:REWRITE DEFAULT-+-2))
 (11 10 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE DEFAULT-CAR))
 )
(ADE::SYMBOL-ALISTP-PAIRLIS$
 (24 22 (:REWRITE DEFAULT-CAR))
 (11 10 (:REWRITE DEFAULT-CDR))
 )
(ADE::PAIRLIS$-APPEND
 (121 48 (:REWRITE DEFAULT-CDR))
 (81 64 (:REWRITE DEFAULT-CAR))
 (30 30 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (24 8 (:REWRITE CAR-OF-APPEND))
 (20 10 (:REWRITE DEFAULT-+-2))
 (12 12 (:REWRITE CONSP-OF-APPEND))
 (10 10 (:REWRITE DEFAULT-+-1))
 (8 8 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::PAIRLIS$-OF-TAKE
 (120 6 (:REWRITE CONSP-OF-TAKE))
 (90 23 (:REWRITE DEFAULT-CDR))
 (89 22 (:REWRITE DEFAULT-CAR))
 (80 10 (:REWRITE ZP-OPEN))
 (35 19 (:REWRITE DEFAULT-<-2))
 (30 3 (:REWRITE CAR-OF-TAKE))
 (22 19 (:REWRITE DEFAULT-<-1))
 (16 10 (:REWRITE DEFAULT-+-2))
 (14 14 (:TYPE-PRESCRIPTION TAKE))
 (10 10 (:REWRITE DEFAULT-+-1))
 (6 3 (:REWRITE ADE::NFIX-OF-NAT))
 (3 3 (:TYPE-PRESCRIPTION NFIX))
 )
(ADE::ALISTP-APPEND
 (30 13 (:REWRITE DEFAULT-CDR))
 (21 19 (:REWRITE DEFAULT-CAR))
 (9 3 (:REWRITE CAR-OF-APPEND))
 (6 6 (:REWRITE CONSP-OF-APPEND))
 (5 5 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (3 3 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::ALISTP-APPEND-TWO-PAIRLIS$)
(ADE::SYMBOL-ALISTP-APPEND
 (52 48 (:REWRITE DEFAULT-CAR))
 (30 13 (:REWRITE DEFAULT-CDR))
 (18 6 (:REWRITE CAR-OF-APPEND))
 (6 6 (:REWRITE CONSP-OF-APPEND))
 (5 5 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (3 3 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::SYMBOL-ALISTP-APPEND-TWO-PAIRLIS$)
(ADE::STRIP-CARS-OF-SYMBOL-ALIST-IS-SYMBOL-LIST
 (25 23 (:REWRITE DEFAULT-CAR))
 (12 10 (:REWRITE DEFAULT-CDR))
 )
(ADE::STRIP-CARS-PAIRLIS$
 (15 14 (:REWRITE DEFAULT-CAR))
 (12 11 (:REWRITE DEFAULT-CDR))
 )
(ADE::STRIP-CDRS-PAIRLIS$
 (28 25 (:REWRITE DEFAULT-CDR))
 (20 17 (:REWRITE DEFAULT-CAR))
 (20 10 (:REWRITE DEFAULT-+-2))
 (10 10 (:REWRITE DEFAULT-+-1))
 )
(ADE::LEN-STRIP-CARS
 (14 7 (:REWRITE DEFAULT-+-2))
 (9 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE DEFAULT-CAR))
 )
(ADE::DISJOINT)
(ADE::DISJOINT-ATOM
 (30 6 (:REWRITE SUBSETP-CAR-MEMBER))
 (6 6 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (6 6 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (6 6 (:REWRITE SUBSETP-TRANS2))
 (6 6 (:REWRITE SUBSETP-TRANS))
 (6 6 (:REWRITE SUBSETP-MEMBER . 4))
 (6 6 (:REWRITE SUBSETP-MEMBER . 3))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 (6 6 (:REWRITE INTERSECTP-MEMBER . 3))
 (6 6 (:REWRITE INTERSECTP-MEMBER . 2))
 (6 6 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE DEFAULT-CDR))
 )
(ADE::DISJOINT-CONS
 (420 51 (:REWRITE SUBSETP-CAR-MEMBER))
 (83 83 (:REWRITE SUBSETP-MEMBER . 2))
 (82 82 (:REWRITE SUBSETP-MEMBER . 4))
 (82 82 (:REWRITE INTERSECTP-MEMBER . 3))
 (82 82 (:REWRITE INTERSECTP-MEMBER . 2))
 (75 75 (:REWRITE SUBSETP-TRANS2))
 (75 75 (:REWRITE SUBSETP-TRANS))
 (71 71 (:REWRITE DEFAULT-CAR))
 (66 66 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (66 66 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (60 2 (:REWRITE SUBSETP-OF-CONS))
 (55 55 (:REWRITE DEFAULT-CDR))
 (20 20 (:TYPE-PRESCRIPTION ATOM))
 (14 2 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 )
(ADE::DISJOINT-APPEND
 (4412 246 (:DEFINITION MEMBER-EQUAL))
 (3779 492 (:REWRITE SUBSETP-CAR-MEMBER))
 (1200 25 (:REWRITE ADE::MEMBER-APPEND))
 (925 25 (:REWRITE ADE::NOT-MEMBER-APPEND))
 (892 446 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (757 582 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (599 599 (:REWRITE SUBSETP-TRANS2))
 (599 599 (:REWRITE SUBSETP-TRANS))
 (582 582 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (573 447 (:REWRITE DEFAULT-CDR))
 (520 520 (:REWRITE SUBSETP-MEMBER . 2))
 (455 455 (:REWRITE DEFAULT-CAR))
 (446 446 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (446 446 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (434 434 (:REWRITE SUBSETP-MEMBER . 4))
 (434 434 (:REWRITE INTERSECTP-MEMBER . 3))
 (434 434 (:REWRITE INTERSECTP-MEMBER . 2))
 (392 392 (:REWRITE MEMBER-WHEN-ATOM))
 (350 25 (:REWRITE SUBSETP-OF-APPEND-WHEN-SUBSET-OF-EITHER))
 (315 45 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (227 227 (:TYPE-PRESCRIPTION ATOM))
 (18 18 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::DISJOINT=>NOT-MEMBER-NTH
 (177 10 (:DEFINITION MEMBER-EQUAL))
 (105 15 (:REWRITE SUBSETP-CAR-MEMBER))
 (70 7 (:REWRITE ADE::SUBSETP=>MEMBER-NTH))
 (27 27 (:REWRITE SUBSETP-TRANS2))
 (27 27 (:REWRITE SUBSETP-TRANS))
 (25 25 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (25 25 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (22 22 (:REWRITE SUBSETP-MEMBER . 4))
 (22 22 (:REWRITE INTERSECTP-MEMBER . 3))
 (22 22 (:REWRITE INTERSECTP-MEMBER . 2))
 (21 13 (:REWRITE DEFAULT-<-1))
 (21 3 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (20 20 (:REWRITE SUBSETP-MEMBER . 2))
 (20 20 (:REWRITE SUBSETP-MEMBER . 1))
 (20 20 (:REWRITE MEMBER-WHEN-ATOM))
 (20 20 (:REWRITE DEFAULT-CAR))
 (19 13 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE DEFAULT-CDR))
 (15 9 (:REWRITE DEFAULT-+-2))
 (12 12 (:DEFINITION ATOM))
 (9 9 (:REWRITE DEFAULT-+-1))
 (8 8 (:TYPE-PRESCRIPTION ATOM))
 (8 8 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 6 (:REWRITE ZP-OPEN))
 )
(ADE::DISJOINT-COMMUTATIVE
 (364 21 (:DEFINITION MEMBER-EQUAL))
 (329 43 (:REWRITE SUBSETP-CAR-MEMBER))
 (51 51 (:REWRITE SUBSETP-TRANS2))
 (51 51 (:REWRITE SUBSETP-TRANS))
 (47 47 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (47 47 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (46 46 (:REWRITE SUBSETP-MEMBER . 4))
 (46 46 (:REWRITE INTERSECTP-MEMBER . 3))
 (46 46 (:REWRITE INTERSECTP-MEMBER . 2))
 (44 44 (:REWRITE DEFAULT-CAR))
 (43 43 (:REWRITE SUBSETP-MEMBER . 2))
 (42 42 (:REWRITE MEMBER-WHEN-ATOM))
 (41 41 (:REWRITE DEFAULT-CDR))
 (28 4 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (27 27 (:TYPE-PRESCRIPTION ATOM))
 )
(ADE::OPEN-TAKE
 (10 4 (:REWRITE ZP-OPEN))
 (7 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (5 5 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 )
(ADE::TAKE-OF-LEN-IS-ITSELF
 (5 1 (:DEFINITION LEN))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 1 (:REWRITE DEFAULT-+-2))
 (2 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::APPEND-TAKE-LEMMA
 (136 98 (:REWRITE DEFAULT-CDR))
 (125 74 (:REWRITE DEFAULT-<-2))
 (114 72 (:REWRITE DEFAULT-+-2))
 (102 5 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (74 74 (:REWRITE DEFAULT-<-1))
 (72 72 (:REWRITE DEFAULT-+-1))
 (57 57 (:REWRITE DEFAULT-CAR))
 )
(ADE::OPEN-NTHCDR
 (10 10 (:REWRITE DEFAULT-+-2))
 (10 10 (:REWRITE DEFAULT-+-1))
 (10 4 (:REWRITE ZP-OPEN))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (5 5 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 )
(ADE::NTHCDR-0
 (22 11 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (11 11 (:TYPE-PRESCRIPTION TRUE-LISTP))
 )
(ADE::NTHCDR-OF-POS-CONST-IDX
 (10 10 (:REWRITE DEFAULT-+-2))
 (10 10 (:REWRITE DEFAULT-+-1))
 (8 2 (:REWRITE ZP-OPEN))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (5 5 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 )
(ADE::LEN-NTHCDR
 (106 60 (:REWRITE DEFAULT-+-2))
 (64 60 (:REWRITE DEFAULT-+-1))
 (29 18 (:REWRITE DEFAULT-<-1))
 (28 14 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (25 25 (:REWRITE DEFAULT-CDR))
 (20 18 (:REWRITE DEFAULT-<-2))
 (14 14 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (7 7 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 6 (:REWRITE ZP-OPEN))
 (6 6 (:REWRITE FOLD-CONSTS-IN-+))
 (5 1 (:REWRITE ADE::NFIX-OF-NAT))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 1 (:DEFINITION NATP))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::CAR-NTHCDR
 (47 14 (:REWRITE DEFAULT-CAR))
 (32 32 (:REWRITE DEFAULT-+-2))
 (32 32 (:REWRITE DEFAULT-+-1))
 (32 14 (:REWRITE ZP-OPEN))
 (18 6 (:REWRITE FOLD-CONSTS-IN-+))
 (6 6 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE DEFAULT-<-1))
 )
(ADE::CDR-NTHCDR
 (36 36 (:REWRITE DEFAULT-+-2))
 (36 36 (:REWRITE DEFAULT-+-1))
 (15 12 (:REWRITE ZP-OPEN))
 (10 10 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE DEFAULT-<-1))
 (6 2 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::NTHCDR-CONS
 (10 10 (:REWRITE DEFAULT-+-2))
 (10 10 (:REWRITE DEFAULT-+-1))
 (8 2 (:REWRITE ZP-OPEN))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 )
(ADE::NTHCDR-CDR
 (24 8 (:REWRITE COMMUTATIVITY-OF-+))
 (16 16 (:REWRITE DEFAULT-+-2))
 (16 16 (:REWRITE DEFAULT-+-1))
 (10 10 (:REWRITE ZP-OPEN))
 )
(ADE::APPEND-TAKE-NTHCDR
 (342 114 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (29 23 (:REWRITE DEFAULT-+-2))
 (28 16 (:REWRITE DEFAULT-CDR))
 (24 18 (:REWRITE DEFAULT-<-1))
 (23 23 (:REWRITE DEFAULT-+-1))
 (21 18 (:REWRITE DEFAULT-<-2))
 (7 7 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(ADE::NOT-MEMBER-TAKE-LEMMA
 (87 8 (:REWRITE SUBSETP-MEMBER . 1))
 (28 4 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (25 17 (:REWRITE DEFAULT-<-1))
 (18 17 (:REWRITE DEFAULT-<-2))
 (14 11 (:REWRITE DEFAULT-CDR))
 (13 7 (:REWRITE DEFAULT-+-2))
 (12 4 (:DEFINITION NFIX))
 (12 4 (:DEFINITION NATP))
 (10 10 (:REWRITE ZP-OPEN))
 (10 3 (:REWRITE MEMBER-WHEN-ATOM))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 1 (:DEFINITION TAKE))
 (5 5 (:REWRITE SUBSETP-TRANS2))
 (5 5 (:REWRITE SUBSETP-TRANS))
 (5 5 (:REWRITE SUBSETP-MEMBER . 4))
 (5 5 (:REWRITE INTERSECTP-MEMBER . 3))
 (5 5 (:REWRITE INTERSECTP-MEMBER . 2))
 (5 1 (:REWRITE SUBSETP-CAR-MEMBER))
 (4 4 (:TYPE-PRESCRIPTION ZP))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE SUBSETP-REFL))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(ADE::NOT-MEMBER-NTHCDR-LEMMA
 (126 63 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (99 21 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (63 63 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (33 21 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (23 23 (:REWRITE SUBSETP-TRANS2))
 (23 23 (:REWRITE SUBSETP-TRANS))
 (21 3 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (17 17 (:REWRITE SUBSETP-MEMBER . 4))
 (17 17 (:REWRITE INTERSECTP-MEMBER . 3))
 (17 17 (:REWRITE INTERSECTP-MEMBER . 2))
 (15 15 (:REWRITE SUBSETP-MEMBER . 2))
 (9 9 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE DEFAULT-CDR))
 (6 2 (:REWRITE COMMUTATIVITY-OF-+))
 (5 5 (:REWRITE ZP-OPEN))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 )
(ADE::NTHCDR-APPEND
 (280 280 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (91 68 (:REWRITE DEFAULT-+-2))
 (68 68 (:REWRITE DEFAULT-+-1))
 (59 38 (:REWRITE DEFAULT-CDR))
 (13 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE DEFAULT-CAR))
 (9 9 (:REWRITE DEFAULT-<-1))
 (8 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:REWRITE CONSP-OF-APPEND))
 (3 3 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::TRUE-LIST-LISTP-NTHCDR
 (24 12 (:DEFINITION TRUE-LISTP))
 (22 22 (:REWRITE DEFAULT-CDR))
 (16 16 (:REWRITE DEFAULT-+-2))
 (16 16 (:REWRITE DEFAULT-+-1))
 (14 8 (:REWRITE ZP-OPEN))
 (13 13 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 )
(ADE::NTHCDR-OF-NTHCDR
 (68 68 (:REWRITE DEFAULT-+-2))
 (68 68 (:REWRITE DEFAULT-+-1))
 (63 27 (:REWRITE DEFAULT-CDR))
 (38 26 (:REWRITE ZP-OPEN))
 (31 25 (:REWRITE DEFAULT-<-1))
 (25 25 (:REWRITE DEFAULT-<-2))
 (10 8 (:REWRITE FOLD-CONSTS-IN-+))
 (10 2 (:REWRITE ADE::NFIX-OF-NAT))
 (6 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 2 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::NTHCDR-PLUS
 (24 2 (:DEFINITION NTHCDR))
 (8 2 (:REWRITE ZP-OPEN))
 (8 2 (:REWRITE COMMUTATIVITY-OF-+))
 (6 6 (:REWRITE DEFAULT-+-2))
 (6 6 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::SUBSETP-CONS
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 )
(ADE::SUBSETP-IDENTITY)
(ADE::SUBSETP-TAKE
 (15 3 (:DEFINITION LEN))
 (10 7 (:REWRITE DEFAULT-<-1))
 (10 2 (:REWRITE ADE::NFIX-OF-NAT))
 (10 1 (:DEFINITION MEMBER-EQUAL))
 (8 7 (:REWRITE DEFAULT-<-2))
 (8 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (7 4 (:REWRITE DEFAULT-+-2))
 (6 2 (:DEFINITION NATP))
 (6 1 (:DEFINITION TAKE))
 (5 5 (:REWRITE DEFAULT-CDR))
 (5 1 (:REWRITE CONSP-OF-TAKE))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE ZP-OPEN))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE SUBSETP-MEMBER . 4))
 (2 2 (:REWRITE SUBSETP-MEMBER . 3))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:REWRITE MEMBER-WHEN-ATOM))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 3))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 2))
 (2 2 (:REWRITE DEFAULT-CAR))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(ADE::SUBSETP-NTHCDR
 (24 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (21 3 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (6 2 (:REWRITE COMMUTATIVITY-OF-+))
 (4 4 (:REWRITE ZP-OPEN))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (3 3 (:REWRITE DEFAULT-CDR))
 )
(ADE::SUBSETP-TRANSITIVITY
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2 2 (:REWRITE SUBSETP-TRANS))
 )
(ADE::SUBSETP-TRANSITIVITY-TAKE-NTHCDR
 (126 9 (:DEFINITION TAKE))
 (72 42 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (51 15 (:REWRITE DEFAULT-CDR))
 (50 35 (:REWRITE DEFAULT-+-2))
 (46 10 (:REWRITE DEFAULT-CAR))
 (41 35 (:REWRITE DEFAULT-+-1))
 (40 5 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (31 19 (:REWRITE DEFAULT-<-1))
 (30 30 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (28 28 (:REWRITE ZP-OPEN))
 (23 2 (:REWRITE ADE::SUBSETP-TAKE))
 (21 19 (:REWRITE DEFAULT-<-2))
 (14 14 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (10 2 (:REWRITE ADE::NFIX-OF-NAT))
 (10 1 (:DEFINITION MEMBER-EQUAL))
 (7 7 (:REWRITE SUBSETP-TRANS2))
 (7 7 (:REWRITE SUBSETP-TRANS))
 (6 2 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE SUBSETP-MEMBER . 4))
 (2 2 (:REWRITE SUBSETP-MEMBER . 3))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:REWRITE MEMBER-WHEN-ATOM))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 3))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 2))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(ADE::DISJOINT-TAKE
 (275 99 (:DEFINITION ATOM))
 (186 10 (:DEFINITION MEMBER-EQUAL))
 (139 25 (:REWRITE CONSP-OF-TAKE))
 (132 20 (:REWRITE SUBSETP-CAR-MEMBER))
 (96 42 (:REWRITE ZP-OPEN))
 (68 68 (:TYPE-PRESCRIPTION TAKE))
 (58 45 (:REWRITE DEFAULT-<-1))
 (53 34 (:REWRITE DEFAULT-+-2))
 (48 45 (:REWRITE DEFAULT-<-2))
 (46 46 (:TYPE-PRESCRIPTION ATOM))
 (39 39 (:REWRITE DEFAULT-CDR))
 (34 34 (:REWRITE DEFAULT-+-1))
 (32 32 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (23 23 (:REWRITE DEFAULT-CAR))
 (20 20 (:REWRITE SUBSETP-MEMBER . 4))
 (20 20 (:REWRITE SUBSETP-MEMBER . 3))
 (20 20 (:REWRITE SUBSETP-MEMBER . 2))
 (20 20 (:REWRITE SUBSETP-MEMBER . 1))
 (20 20 (:REWRITE MEMBER-WHEN-ATOM))
 (20 20 (:REWRITE INTERSECTP-MEMBER . 3))
 (20 20 (:REWRITE INTERSECTP-MEMBER . 2))
 (16 16 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (16 16 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (16 16 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (16 16 (:REWRITE SUBSETP-TRANS2))
 (16 16 (:REWRITE SUBSETP-TRANS))
 (12 4 (:REWRITE FOLD-CONSTS-IN-+))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(ADE::DISJOINT-NTHCDR
 (160 76 (:DEFINITION ATOM))
 (154 77 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (77 77 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (38 38 (:TYPE-PRESCRIPTION ATOM))
 (21 12 (:REWRITE ZP-OPEN))
 (17 17 (:REWRITE DEFAULT-+-2))
 (17 17 (:REWRITE DEFAULT-+-1))
 (9 3 (:REWRITE FOLD-CONSTS-IN-+))
 (3 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 )
(ADE::NO-DUPLICATESP-TAKE-LEMMA
 (275 10 (:DEFINITION MEMBER-EQUAL))
 (190 19 (:REWRITE SUBSETP-CAR-MEMBER))
 (129 19 (:REWRITE SUBSETP-MEMBER . 3))
 (62 3 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (58 2 (:REWRITE SUBSETP-OF-TAKE))
 (56 40 (:REWRITE DEFAULT-<-1))
 (51 12 (:REWRITE CONSP-OF-TAKE))
 (50 36 (:REWRITE DEFAULT-CDR))
 (46 24 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (42 40 (:REWRITE DEFAULT-<-2))
 (40 24 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (40 18 (:REWRITE MEMBER-WHEN-ATOM))
 (32 14 (:REWRITE ZP-OPEN))
 (25 25 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (25 24 (:REWRITE DEFAULT-CAR))
 (24 24 (:REWRITE SUBSETP-TRANS2))
 (24 24 (:REWRITE SUBSETP-TRANS))
 (22 22 (:REWRITE SUBSETP-MEMBER . 2))
 (22 14 (:REWRITE DEFAULT-+-2))
 (20 4 (:REWRITE CAR-OF-TAKE))
 (19 19 (:REWRITE SUBSETP-MEMBER . 4))
 (19 19 (:REWRITE INTERSECTP-MEMBER . 3))
 (19 19 (:REWRITE INTERSECTP-MEMBER . 2))
 (15 3 (:REWRITE SECOND-OF-TAKE))
 (14 14 (:REWRITE DEFAULT-+-1))
 (8 1 (:REWRITE ADE::NOT-MEMBER-TAKE-LEMMA))
 (6 2 (:DEFINITION NFIX))
 (6 2 (:DEFINITION NATP))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(ADE::NO-DUPLICATESP-NTHCDR-LEMMA
 (216 12 (:DEFINITION MEMBER-EQUAL))
 (200 25 (:REWRITE SUBSETP-CAR-MEMBER))
 (35 35 (:REWRITE DEFAULT-CDR))
 (26 26 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (25 25 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (25 25 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (25 25 (:REWRITE SUBSETP-TRANS2))
 (25 25 (:REWRITE SUBSETP-TRANS))
 (25 25 (:REWRITE SUBSETP-MEMBER . 4))
 (25 25 (:REWRITE INTERSECTP-MEMBER . 3))
 (25 25 (:REWRITE INTERSECTP-MEMBER . 2))
 (25 25 (:REWRITE DEFAULT-CAR))
 (24 24 (:REWRITE SUBSETP-MEMBER . 2))
 (24 24 (:REWRITE SUBSETP-MEMBER . 1))
 (24 24 (:REWRITE MEMBER-WHEN-ATOM))
 (6 2 (:REWRITE COMMUTATIVITY-OF-+))
 (5 5 (:REWRITE ZP-OPEN))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 )
(ADE::DISJOINT-TAKE-NTHCDR-SAME-LIST
 (251 47 (:DEFINITION ATOM))
 (183 10 (:REWRITE ADE::DISJOINT-TAKE))
 (132 66 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (108 6 (:DEFINITION MEMBER-EQUAL))
 (105 14 (:REWRITE SUBSETP-CAR-MEMBER))
 (91 17 (:REWRITE CONSP-OF-TAKE))
 (66 66 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (63 39 (:REWRITE ZP-OPEN))
 (48 48 (:TYPE-PRESCRIPTION TAKE))
 (28 28 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (25 25 (:REWRITE DEFAULT-CDR))
 (22 16 (:REWRITE SUBSETP-MEMBER . 3))
 (20 20 (:TYPE-PRESCRIPTION ATOM))
 (20 20 (:REWRITE DEFAULT-+-2))
 (20 20 (:REWRITE DEFAULT-+-1))
 (16 16 (:REWRITE SUBSETP-MEMBER . 4))
 (16 16 (:REWRITE INTERSECTP-MEMBER . 3))
 (16 16 (:REWRITE INTERSECTP-MEMBER . 2))
 (16 16 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE DEFAULT-<-1))
 (15 15 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (14 14 (:REWRITE SUBSETP-MEMBER . 2))
 (14 14 (:REWRITE SUBSETP-MEMBER . 1))
 (13 13 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (13 13 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (13 13 (:REWRITE SUBSETP-TRANS2))
 (13 13 (:REWRITE SUBSETP-TRANS))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE ADE::SUBSETP-IDENTITY))
 (2 2 (:DEFINITION LEN))
 )
(ADE::DISJOINT-NTHCDR-TAKE-OF-DISJOINT-LISTS
 (8 2 (:REWRITE ADE::DISJOINT-ATOM))
 (8 1 (:DEFINITION NTHCDR))
 (6 1 (:DEFINITION TAKE))
 (5 4 (:REWRITE DEFAULT-+-2))
 (5 1 (:DEFINITION LEN))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 4 (:DEFINITION ATOM))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 1 (:REWRITE COMMUTATIVITY-OF-+))
 (2 2 (:TYPE-PRESCRIPTION ATOM))
 (2 2 (:REWRITE ZP-OPEN))
 (2 1 (:REWRITE DEFAULT-<-2))
 (2 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1 1 (:REWRITE DEFAULT-CAR))
 )
(ADE::TREE-SIZE)
(ADE::TREE-SIZE-ATOM)
(ADE::NOT-EQUAL-TREE-SIZE-TREE-0)
(ADE::TREE-SIZE-1-CROCK
 (9 9 (:REWRITE ADE::TREE-SIZE-ATOM))
 (8 4 (:REWRITE DEFAULT-+-2))
 (8 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-CAR))
 )
(ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS
 (35 7 (:DEFINITION LEN))
 (32 16 (:REWRITE DEFAULT-+-2))
 (25 16 (:REWRITE DEFAULT-+-1))
 (15 15 (:REWRITE DEFAULT-CDR))
 (6 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 )
(ADE::TREE-SIZE-LEMMAS
 (46 22 (:REWRITE DEFAULT-+-2))
 (45 22 (:REWRITE DEFAULT-+-1))
 (30 30 (:REWRITE ADE::TREE-SIZE-ATOM))
 (14 14 (:REWRITE DEFAULT-CDR))
 (14 14 (:REWRITE DEFAULT-CAR))
 (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::MAKE-LIST-APPEND-TREE-CROCK
 (22 22 (:TYPE-PRESCRIPTION ADE::TREE-SIZE))
 (20 9 (:REWRITE DEFAULT-+-2))
 (16 9 (:REWRITE DEFAULT-+-1))
 (16 2 (:DEFINITION MAKE-LIST-AC))
 (15 15 (:REWRITE ADE::TREE-SIZE-ATOM))
 (7 7 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(ADE::TFIRSTN)
(ADE::TRESTN)
(ADE::TREE-HEIGHT)
(ADE::MAKE-TREE
 (812 812 (:TYPE-PRESCRIPTION NOT-INTEGERP-4B))
 (812 812 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (812 812 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (812 812 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (400 32 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (280 32 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (280 32 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (280 32 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (211 68 (:REWRITE DEFAULT-PLUS-2))
 (160 32 (:TYPE-PRESCRIPTION FLOOR-ZERO . 4))
 (160 32 (:TYPE-PRESCRIPTION FLOOR-ZERO . 3))
 (160 32 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (160 32 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (160 32 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 2))
 (160 32 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (160 32 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (160 32 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (160 32 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (160 32 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (152 152 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (152 152 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (152 152 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (124 68 (:REWRITE DEFAULT-PLUS-1))
 (123 47 (:REWRITE DEFAULT-LESS-THAN-1))
 (106 106 (:TYPE-PRESCRIPTION NUMERATOR-ZERO))
 (60 60 (:REWRITE DEFAULT-TIMES-2))
 (60 60 (:REWRITE DEFAULT-TIMES-1))
 (52 47 (:REWRITE DEFAULT-LESS-THAN-2))
 (47 47 (:REWRITE THE-FLOOR-BELOW))
 (47 47 (:REWRITE THE-FLOOR-ABOVE))
 (43 36 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (43 36 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (40 40 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (37 32 (:REWRITE |(< (- x) (- y))|))
 (36 36 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (35 14 (:REWRITE DEFAULT-MINUS))
 (33 3 (:REWRITE DEFAULT-FLOOR-RATIO))
 (32 32 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (32 32 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (32 32 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (32 32 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (32 32 (:REWRITE |(< c (- x))|))
 (32 32 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (32 32 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (32 32 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (32 32 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (32 32 (:REWRITE |(< (/ x) (/ y))|))
 (31 31 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (31 31 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (31 31 (:REWRITE INTEGERP-<-CONSTANT))
 (31 31 (:REWRITE CONSTANT-<-INTEGERP))
 (23 23 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (21 21 (:REWRITE |(< (/ x) 0)|))
 (21 21 (:REWRITE |(< (* x y) 0)|))
 (17 12 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (16 16 (:REWRITE |(< (+ c/d x) y)|))
 (16 16 (:REWRITE |(< (+ (- c) x) y)|))
 (14 14 (:TYPE-PRESCRIPTION ABS))
 (14 14 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (10 10 (:REWRITE REDUCE-INTEGERP-+))
 (10 10 (:REWRITE INTEGERP-MINUS-X))
 (10 10 (:META META-INTEGERP-CORRECT))
 (10 2 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 1))
 (7 7 (:REWRITE |(* (- x) y)|))
 (6 6 (:REWRITE ZP-OPEN))
 (6 6 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 6 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (6 6 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (6 6 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (6 6 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (6 6 (:REWRITE |(equal c (/ x))|))
 (6 6 (:REWRITE |(equal c (- x))|))
 (6 6 (:REWRITE |(equal (/ x) c)|))
 (6 6 (:REWRITE |(equal (/ x) (/ y))|))
 (6 6 (:REWRITE |(equal (- x) c)|))
 (6 6 (:REWRITE |(equal (- x) (- y))|))
 (5 5 (:REWRITE |(< (* x y) 0) rationalp (* x y)|))
 (4 4 (:REWRITE |(< 0 (* x y))|))
 (3 3 (:REWRITE DEFAULT-FLOOR-2))
 (3 3 (:REWRITE DEFAULT-FLOOR-1))
 (3 3 (:REWRITE |(floor x 2)| . 2))
 (3 3 (:REWRITE |(< y (+ (- c) x))|))
 (3 3 (:REWRITE |(< x (+ c/d y))|))
 (2 2 (:REWRITE INTEGERP==>NUMERATOR-=-X))
 (2 2 (:REWRITE INTEGERP==>DENOMINATOR-=-1))
 (2 2 (:REWRITE DEFAULT-RATIONAL-NUMERATOR))
 (2 2 (:REWRITE DEFAULT-RATIONAL-DENOMINATOR))
 (2 2 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (2 2 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (2 2 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (2 2 (:REWRITE |(< 0 (/ x))|))
 (2 2 (:REWRITE |(< (/ x) y) with (< x 0)|))
 (1 1 (:TYPE-PRESCRIPTION NOT-INTEGERP-4D))
 (1 1 (:TYPE-PRESCRIPTION NOT-INTEGERP-3D))
 (1 1 (:TYPE-PRESCRIPTION NOT-INTEGERP-2D))
 (1 1 (:TYPE-PRESCRIPTION NOT-INTEGERP-1D))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 )
(ADE::TREE-SIZE-MAKE-TREE
 (1022 1022 (:TYPE-PRESCRIPTION NOT-INTEGERP-4B))
 (1022 1022 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (1022 1022 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (1022 1022 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (488 40 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (344 40 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (344 40 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (317 37 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (200 40 (:TYPE-PRESCRIPTION FLOOR-ZERO . 4))
 (200 40 (:TYPE-PRESCRIPTION FLOOR-ZERO . 3))
 (200 40 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (200 40 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (200 40 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (200 40 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (200 40 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (200 40 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (197 63 (:REWRITE DEFAULT-PLUS-2))
 (185 37 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (138 14 (:REWRITE DEFAULT-FLOOR-RATIO))
 (128 2 (:REWRITE |(+ x (if a b c))|))
 (114 114 (:TYPE-PRESCRIPTION NOT-INTEGERP-4A))
 (114 114 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (114 114 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (114 114 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (100 100 (:REWRITE DEFAULT-TIMES-2))
 (100 100 (:REWRITE DEFAULT-TIMES-1))
 (87 63 (:REWRITE DEFAULT-PLUS-1))
 (76 76 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (56 24 (:REWRITE ADE::TREE-SIZE-ATOM))
 (54 2 (:REWRITE |(- (if a b c))|))
 (52 2 (:LINEAR LINEAR-FLOOR-BOUNDS-3))
 (44 2 (:LINEAR LINEAR-FLOOR-BOUNDS-2))
 (30 30 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (22 14 (:REWRITE DEFAULT-MINUS))
 (20 12 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (20 12 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (20 12 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (20 4 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 1))
 (14 14 (:REWRITE REDUCE-INTEGERP-+))
 (14 14 (:REWRITE INTEGERP-MINUS-X))
 (14 14 (:REWRITE DEFAULT-FLOOR-2))
 (14 14 (:REWRITE DEFAULT-FLOOR-1))
 (14 14 (:REWRITE |(floor x 2)| . 2))
 (14 14 (:META META-INTEGERP-CORRECT))
 (12 12 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (12 12 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (12 12 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (12 12 (:REWRITE |(equal c (/ x))|))
 (12 12 (:REWRITE |(equal c (- x))|))
 (12 12 (:REWRITE |(equal (/ x) c)|))
 (12 12 (:REWRITE |(equal (/ x) (/ y))|))
 (12 12 (:REWRITE |(equal (- x) c)|))
 (12 12 (:REWRITE |(equal (- x) (- y))|))
 (10 10 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (10 8 (:REWRITE DEFAULT-CDR))
 (10 8 (:REWRITE DEFAULT-CAR))
 (8 8 (:REWRITE |(* (- x) y)|))
 (4 4 (:REWRITE ZP-OPEN))
 (3 3 (:REWRITE |(equal (+ (- c) x) y)|))
 )
(ADE::CONSP-MAKE-TREE
 (1602 1602 (:TYPE-PRESCRIPTION NOT-INTEGERP-4B))
 (1602 1602 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (1602 1602 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (1602 1602 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (875 71 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (615 71 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (615 71 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (606 70 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (452 108 (:REWRITE DEFAULT-PLUS-2))
 (355 71 (:TYPE-PRESCRIPTION FLOOR-ZERO . 4))
 (355 71 (:TYPE-PRESCRIPTION FLOOR-ZERO . 3))
 (355 71 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (355 71 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (355 71 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (355 71 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (355 71 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (355 71 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (350 70 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (256 4 (:REWRITE |(+ x (if a b c))|))
 (231 25 (:REWRITE DEFAULT-FLOOR-RATIO))
 (210 210 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (210 210 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (210 210 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (158 158 (:REWRITE DEFAULT-TIMES-2))
 (158 158 (:REWRITE DEFAULT-TIMES-1))
 (131 131 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (129 108 (:REWRITE DEFAULT-PLUS-1))
 (108 4 (:REWRITE |(- (if a b c))|))
 (100 25 (:REWRITE |(* y x)|))
 (70 38 (:REWRITE DEFAULT-MINUS))
 (54 6 (:REWRITE ACL2-NUMBERP-X))
 (49 49 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (37 31 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (36 36 (:REWRITE THE-FLOOR-BELOW))
 (36 36 (:REWRITE THE-FLOOR-ABOVE))
 (36 36 (:REWRITE DEFAULT-LESS-THAN-2))
 (35 31 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (35 31 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (31 31 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (31 31 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (31 31 (:REWRITE INTEGERP-<-CONSTANT))
 (31 31 (:REWRITE CONSTANT-<-INTEGERP))
 (31 31 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (31 31 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (31 31 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (31 31 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (31 31 (:REWRITE |(< c (- x))|))
 (31 31 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (31 31 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (31 31 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (31 31 (:REWRITE |(< (/ x) (/ y))|))
 (31 31 (:REWRITE |(< (- x) c)|))
 (31 31 (:REWRITE |(< (- x) (- y))|))
 (30 30 (:REWRITE SIMPLIFY-SUMS-<))
 (30 30 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (30 30 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (30 6 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 1))
 (25 25 (:REWRITE REDUCE-INTEGERP-+))
 (25 25 (:REWRITE INTEGERP-MINUS-X))
 (25 25 (:REWRITE DEFAULT-FLOOR-2))
 (25 25 (:REWRITE DEFAULT-FLOOR-1))
 (25 25 (:REWRITE |(floor x 2)| . 2))
 (25 25 (:META META-INTEGERP-CORRECT))
 (24 6 (:REWRITE RATIONALP-X))
 (21 21 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (21 21 (:REWRITE |(* (- x) y)|))
 (10 10 (:REWRITE |(< (/ x) 0)|))
 (10 10 (:REWRITE |(< (* x y) 0)|))
 (9 9 (:REWRITE |(< (+ c/d x) y)|))
 (9 9 (:REWRITE |(< (+ (- c) x) y)|))
 (8 8 (:TYPE-PRESCRIPTION ABS))
 (7 7 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (6 6 (:REWRITE REDUCE-RATIONALP-+))
 (6 6 (:REWRITE REDUCE-RATIONALP-*))
 (6 6 (:REWRITE RATIONALP-MINUS-X))
 (6 6 (:META META-RATIONALP-CORRECT))
 (5 5 (:REWRITE ZP-OPEN))
 (4 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (4 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (4 4 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (4 4 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (4 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (4 4 (:REWRITE |(equal c (/ x))|))
 (4 4 (:REWRITE |(equal c (- x))|))
 (4 4 (:REWRITE |(equal (/ x) c)|))
 (4 4 (:REWRITE |(equal (/ x) (/ y))|))
 (4 4 (:REWRITE |(equal (- x) c)|))
 (4 4 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< (* x y) 0) rationalp (* x y)|))
 )
(ADE::APPEND-REC
 (2 1 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (1 1 (:TYPE-PRESCRIPTION BINARY-APPEND))
 )
(ADE::PREPEND-REC
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 1 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (2 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION BINARY-APPEND))
 )
(ADE::TRUE-LIST-LISTP-PREPEND-REC
 (17 16 (:REWRITE DEFAULT-CDR))
 (14 7 (:DEFINITION TRUE-LISTP))
 (12 3 (:DEFINITION BINARY-APPEND))
 (11 10 (:REWRITE DEFAULT-CAR))
 (6 6 (:REWRITE APPEND-WHEN-NOT-CONSP))
 )
(ADE::MEMBER-APPEND-PREPEND-REC
 (152 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (131 21 (:REWRITE ACL2-NUMBERP-X))
 (108 54 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (55 7 (:REWRITE RATIONALP-X))
 (54 54 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (54 54 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (54 16 (:REWRITE SUBSETP-MEMBER . 3))
 (44 11 (:DEFINITION BINARY-APPEND))
 (42 8 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (42 8 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (23 23 (:REWRITE DEFAULT-CAR))
 (22 22 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (18 18 (:REWRITE DEFAULT-CDR))
 (16 16 (:REWRITE SUBSETP-MEMBER . 4))
 (16 16 (:REWRITE SUBSETP-MEMBER . 2))
 (16 16 (:REWRITE INTERSECTP-MEMBER . 3))
 (16 16 (:REWRITE INTERSECTP-MEMBER . 2))
 (11 1 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (10 4 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (8 8 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (8 8 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (8 8 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (8 8 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (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))|))
 (7 7 (:REWRITE REDUCE-RATIONALP-+))
 (7 7 (:REWRITE REDUCE-RATIONALP-*))
 (7 7 (:REWRITE REDUCE-INTEGERP-+))
 (7 7 (:REWRITE RATIONALP-MINUS-X))
 (7 7 (:REWRITE INTEGERP-MINUS-X))
 (7 7 (:META META-RATIONALP-CORRECT))
 (7 7 (:META META-INTEGERP-CORRECT))
 (7 4 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )
(ADE::SUBSETP-PREPEND-REC
 (200 17 (:REWRITE SUBSETP-TRANS2))
 (139 2 (:DEFINITION MEMBER-EQUAL))
 (47 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (40 6 (:REWRITE ACL2-NUMBERP-X))
 (34 17 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (32 8 (:DEFINITION BINARY-APPEND))
 (29 17 (:REWRITE SUBSETP-TRANS))
 (26 14 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (18 18 (:REWRITE DEFAULT-CDR))
 (18 18 (:REWRITE DEFAULT-CAR))
 (17 17 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (17 17 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (17 2 (:REWRITE RATIONALP-X))
 (16 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (13 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (13 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:REWRITE REDUCE-RATIONALP-+))
 (2 2 (:REWRITE REDUCE-RATIONALP-*))
 (2 2 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (2 2 (:REWRITE RATIONALP-MINUS-X))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (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))
 (2 2 (:META META-INTEGERP-CORRECT))
 )
(ADE::PREPEND-REC-OF-APPEND
 (65 34 (:REWRITE DEFAULT-CDR))
 (44 41 (:REWRITE DEFAULT-CAR))
 (15 15 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (12 4 (:REWRITE CAR-OF-APPEND))
 (8 8 (:REWRITE CONSP-OF-APPEND))
 (6 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (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))|))
 )
(ADE::PREPEND-REC-OF-PREPEND-REC
 (60 15 (:DEFINITION BINARY-APPEND))
 (30 30 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (26 25 (:REWRITE DEFAULT-CAR))
 (24 23 (:REWRITE DEFAULT-CDR))
 (6 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (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))|))
 )
(ADE::BOOL->BIT$INLINE)
(ADE::CONS-REC)
(ADE::MEMBER-CONS-CONS-REC
 (54 16 (:REWRITE SUBSETP-MEMBER . 3))
 (44 12 (:REWRITE ACL2-NUMBERP-X))
 (44 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (16 16 (:REWRITE SUBSETP-MEMBER . 4))
 (16 16 (:REWRITE SUBSETP-MEMBER . 2))
 (16 16 (:REWRITE INTERSECTP-MEMBER . 3))
 (16 16 (:REWRITE INTERSECTP-MEMBER . 2))
 (16 4 (:REWRITE RATIONALP-X))
 (12 12 (:REWRITE DEFAULT-CAR))
 (12 8 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (12 8 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (11 1 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (10 4 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (8 8 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (8 8 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (8 8 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (8 8 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (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))|))
 (7 7 (:REWRITE DEFAULT-CDR))
 (7 4 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 (4 4 (:REWRITE REDUCE-RATIONALP-+))
 (4 4 (:REWRITE REDUCE-RATIONALP-*))
 (4 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE RATIONALP-MINUS-X))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:META META-RATIONALP-CORRECT))
 (4 4 (:META META-INTEGERP-CORRECT))
 )
(ADE::INTERLEAVE
 (1260 24 (:DEFINITION INTEGER-ABS))
 (794 320 (:REWRITE DEFAULT-PLUS-2))
 (700 320 (:REWRITE DEFAULT-PLUS-1))
 (420 12 (:REWRITE |(+ (if a b c) x)|))
 (372 12 (:REWRITE NUMERATOR-NEGATIVE))
 (194 194 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (120 12 (:DEFINITION LENGTH))
 (116 44 (:REWRITE DEFAULT-LESS-THAN-1))
 (108 108 (:TYPE-PRESCRIPTION NUMERATOR-ZERO))
 (108 108 (:TYPE-PRESCRIPTION NUMERATOR-POSITIVE . 2))
 (108 108 (:TYPE-PRESCRIPTION NUMERATOR-POSITIVE . 1))
 (108 108 (:TYPE-PRESCRIPTION NUMERATOR-NEGATIVE . 2))
 (108 108 (:TYPE-PRESCRIPTION NUMERATOR-NEGATIVE . 1))
 (84 24 (:REWRITE DEFAULT-MINUS))
 (84 12 (:DEFINITION LEN))
 (70 70 (:REWRITE DEFAULT-CDR))
 (68 68 (:REWRITE FOLD-CONSTS-IN-+))
 (56 44 (:REWRITE DEFAULT-LESS-THAN-2))
 (56 32 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (56 32 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (48 48 (:REWRITE DEFAULT-CAR))
 (48 12 (:REWRITE RATIONALP-X))
 (44 44 (:REWRITE THE-FLOOR-BELOW))
 (44 44 (:REWRITE THE-FLOOR-ABOVE))
 (44 44 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (44 44 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (44 44 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (44 44 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (44 44 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (44 44 (:REWRITE INTEGERP-<-CONSTANT))
 (44 44 (:REWRITE CONSTANT-<-INTEGERP))
 (44 44 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (44 44 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (44 44 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (44 44 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (44 44 (:REWRITE |(< c (- x))|))
 (44 44 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (44 44 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (44 44 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (44 44 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (44 44 (:REWRITE |(< (/ x) (/ y))|))
 (44 44 (:REWRITE |(< (- x) c)|))
 (44 44 (:REWRITE |(< (- x) (- y))|))
 (36 36 (:REWRITE |(< (/ x) 0)|))
 (36 36 (:REWRITE |(< (* x y) 0)|))
 (24 24 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (24 24 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (24 24 (:REWRITE REDUCE-INTEGERP-+))
 (24 24 (:REWRITE INTEGERP-MINUS-X))
 (24 24 (:META META-INTEGERP-CORRECT))
 (16 8 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (12 12 (:TYPE-PRESCRIPTION LEN))
 (12 12 (:REWRITE REDUCE-RATIONALP-+))
 (12 12 (:REWRITE REDUCE-RATIONALP-*))
 (12 12 (:REWRITE RATIONALP-MINUS-X))
 (12 12 (:REWRITE INTEGERP==>NUMERATOR-=-X))
 (12 12 (:REWRITE INTEGERP==>DENOMINATOR-=-1))
 (12 12 (:REWRITE DEFAULT-REALPART))
 (12 12 (:REWRITE DEFAULT-RATIONAL-NUMERATOR))
 (12 12 (:REWRITE DEFAULT-RATIONAL-DENOMINATOR))
 (12 12 (:REWRITE DEFAULT-IMAGPART))
 (12 12 (:REWRITE DEFAULT-COERCE-2))
 (12 12 (:REWRITE DEFAULT-COERCE-1))
 (12 12 (:META META-RATIONALP-CORRECT))
 (8 8 (:REWRITE |(< y (+ (- c) x))|))
 (8 8 (:REWRITE |(< x (+ c/d y))|))
 (8 8 (:REWRITE |(< (+ c/d x) y)|))
 (8 8 (:REWRITE |(< (+ (- c) x) y)|))
 (8 8 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 )
(ADE::CONSP-INTERLEAVE
 (424 52 (:DEFINITION BINARY-APPEND))
 (315 315 (:REWRITE DEFAULT-CDR))
 (302 302 (:REWRITE DEFAULT-CAR))
 (260 104 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (228 12 (:REWRITE COMMUTATIVITY-OF-APPEND-UNDER-SET-EQUIV))
 (224 56 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (24 24 (:REWRITE CDR-CONS))
 (24 24 (:REWRITE CAR-CONS))
 )
(ADE::TRUE-LIST-LISTP-INTERLEAVE
 (1292 614 (:REWRITE DEFAULT-CDR))
 (898 484 (:REWRITE DEFAULT-CAR))
 (456 76 (:DEFINITION BINARY-APPEND))
 (240 48 (:REWRITE CONSP-OF-APPEND))
 (192 24 (:REWRITE CAR-OF-APPEND))
 (96 24 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::SUBSETP-PREPEND-REC-INTERLEAVE-1
 (8005 198 (:DEFINITION MEMBER-EQUAL))
 (6265 3143 (:REWRITE DEFAULT-CDR))
 (5400 3124 (:REWRITE DEFAULT-CAR))
 (3108 44 (:REWRITE ADE::NOT-MEMBER-APPEND))
 (2631 283 (:REWRITE SUBSETP-MEMBER . 3))
 (2504 642 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1908 426 (:REWRITE SUBSETP-MEMBER . 1))
 (1848 462 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (1804 640 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (724 670 (:REWRITE SUBSETP-TRANS))
 (692 66 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (518 426 (:REWRITE SUBSETP-MEMBER . 2))
 (285 204 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (283 283 (:REWRITE SUBSETP-MEMBER . 4))
 (283 283 (:REWRITE INTERSECTP-MEMBER . 3))
 (283 283 (:REWRITE INTERSECTP-MEMBER . 2))
 (277 204 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (277 204 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (204 204 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (204 204 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (204 204 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (204 204 (:REWRITE |(equal c (/ x))|))
 (204 204 (:REWRITE |(equal c (- x))|))
 (204 204 (:REWRITE |(equal (/ x) c)|))
 (204 204 (:REWRITE |(equal (/ x) (/ y))|))
 (204 204 (:REWRITE |(equal (- x) c)|))
 (204 204 (:REWRITE |(equal (- x) (- y))|))
 (22 2 (:REWRITE ADE::MEMBER-APPEND-PREPEND-REC))
 (12 2 (:REWRITE SUBSETP-CAR-MEMBER))
 (11 3 (:REWRITE ACL2-NUMBERP-X))
 (4 1 (:REWRITE RATIONALP-X))
 (1 1 (:REWRITE REDUCE-RATIONALP-+))
 (1 1 (:REWRITE REDUCE-RATIONALP-*))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE RATIONALP-MINUS-X))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:META META-RATIONALP-CORRECT))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::SUBSETP-PREPEND-REC-INTERLEAVE-2
 (8275 202 (:DEFINITION MEMBER-EQUAL))
 (6297 3159 (:REWRITE DEFAULT-CDR))
 (5430 3138 (:REWRITE DEFAULT-CAR))
 (3108 44 (:REWRITE ADE::NOT-MEMBER-APPEND))
 (2715 291 (:REWRITE SUBSETP-MEMBER . 3))
 (2562 656 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2028 434 (:REWRITE SUBSETP-MEMBER . 1))
 (1864 466 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (1862 654 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (738 684 (:REWRITE SUBSETP-TRANS))
 (716 68 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (526 434 (:REWRITE SUBSETP-MEMBER . 2))
 (291 291 (:REWRITE SUBSETP-MEMBER . 4))
 (291 291 (:REWRITE INTERSECTP-MEMBER . 3))
 (291 291 (:REWRITE INTERSECTP-MEMBER . 2))
 (289 208 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (281 208 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (281 208 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (208 208 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (208 208 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (208 208 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (208 208 (:REWRITE |(equal c (/ x))|))
 (208 208 (:REWRITE |(equal c (- x))|))
 (208 208 (:REWRITE |(equal (/ x) c)|))
 (208 208 (:REWRITE |(equal (/ x) (/ y))|))
 (208 208 (:REWRITE |(equal (- x) c)|))
 (208 208 (:REWRITE |(equal (- x) (- y))|))
 (22 2 (:REWRITE ADE::MEMBER-APPEND-PREPEND-REC))
 (12 2 (:REWRITE SUBSETP-CAR-MEMBER))
 (11 3 (:REWRITE ACL2-NUMBERP-X))
 (4 1 (:REWRITE RATIONALP-X))
 (1 1 (:REWRITE REDUCE-RATIONALP-+))
 (1 1 (:REWRITE REDUCE-RATIONALP-*))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE RATIONALP-MINUS-X))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:META META-RATIONALP-CORRECT))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::MEMBER-APPEND-INTERLEAVE-1
 (180 4 (:DEFINITION ADE::INTERLEAVE))
 (72 8 (:DEFINITION ADE::CONS-REC))
 (58 28 (:REWRITE DEFAULT-CDR))
 (56 8 (:DEFINITION BINARY-APPEND))
 (49 1 (:DEFINITION MEMBER-EQUAL))
 (48 28 (:REWRITE DEFAULT-CAR))
 (38 38 (:TYPE-PRESCRIPTION ADE::CONS-REC))
 (38 2 (:REWRITE COMMUTATIVITY-OF-APPEND-UNDER-SET-EQUIV))
 (34 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (24 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (24 1 (:DEFINITION ADE::PREPEND-REC))
 (11 3 (:REWRITE ACL2-NUMBERP-X))
 (10 2 (:REWRITE MEMBER-WHEN-ATOM))
 (10 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 2 (:REWRITE CAR-OF-APPEND))
 (4 4 (:REWRITE CONSP-OF-APPEND))
 (4 2 (:DEFINITION TRUE-LISTP))
 (4 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4 1 (:REWRITE RATIONALP-X))
 (3 3 (:REWRITE SUBSETP-MEMBER . 4))
 (3 3 (:REWRITE SUBSETP-MEMBER . 3))
 (3 3 (:REWRITE INTERSECTP-MEMBER . 3))
 (3 3 (:REWRITE INTERSECTP-MEMBER . 2))
 (3 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 (1 1 (:REWRITE REDUCE-RATIONALP-+))
 (1 1 (:REWRITE REDUCE-RATIONALP-*))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE RATIONALP-MINUS-X))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (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 (:META META-RATIONALP-CORRECT))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::MEMBER-APPEND-INTERLEAVE-2
 (184 4 (:DEFINITION ADE::INTERLEAVE))
 (72 8 (:DEFINITION ADE::CONS-REC))
 (58 28 (:REWRITE DEFAULT-CDR))
 (56 8 (:DEFINITION BINARY-APPEND))
 (49 1 (:DEFINITION MEMBER-EQUAL))
 (48 28 (:REWRITE DEFAULT-CAR))
 (38 38 (:TYPE-PRESCRIPTION ADE::CONS-REC))
 (34 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (24 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (24 1 (:DEFINITION ADE::PREPEND-REC))
 (11 3 (:REWRITE ACL2-NUMBERP-X))
 (10 2 (:REWRITE MEMBER-WHEN-ATOM))
 (10 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 6 (:REWRITE CONSP-OF-APPEND))
 (6 2 (:REWRITE CAR-OF-APPEND))
 (4 2 (:DEFINITION TRUE-LISTP))
 (4 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4 1 (:REWRITE RATIONALP-X))
 (3 3 (:REWRITE SUBSETP-MEMBER . 4))
 (3 3 (:REWRITE SUBSETP-MEMBER . 3))
 (3 3 (:REWRITE INTERSECTP-MEMBER . 3))
 (3 3 (:REWRITE INTERSECTP-MEMBER . 2))
 (3 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 (1 1 (:REWRITE REDUCE-RATIONALP-+))
 (1 1 (:REWRITE REDUCE-RATIONALP-*))
 (1 1 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (1 1 (:REWRITE RATIONALP-MINUS-X))
 (1 1 (:REWRITE ADE::MEMBER-APPEND-INTERLEAVE-1))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (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 (:META META-RATIONALP-CORRECT))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::SUBSETP-PREPEND-REC-INTERLEAVE-CONS-1
 (494 14 (:DEFINITION ADE::INTERLEAVE))
 (376 18 (:DEFINITION ADE::PREPEND-REC))
 (252 28 (:DEFINITION ADE::CONS-REC))
 (228 36 (:DEFINITION BINARY-APPEND))
 (206 114 (:REWRITE DEFAULT-CDR))
 (198 114 (:REWRITE DEFAULT-CAR))
 (196 196 (:TYPE-PRESCRIPTION ADE::INTERLEAVE))
 (196 196 (:TYPE-PRESCRIPTION ADE::CONSP-INTERLEAVE))
 (70 70 (:TYPE-PRESCRIPTION ADE::CONS-REC))
 (16 4 (:REWRITE CAR-OF-APPEND))
 (12 3 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (12 3 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (8 4 (:DEFINITION TRUE-LISTP))
 (6 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (4 4 (:REWRITE CAR-CONS))
 (3 3 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (3 3 (:REWRITE SUBSETP-TRANS2))
 (3 3 (:REWRITE SUBSETP-TRANS))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (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))|))
 )
(ADE::SUBSETP-PREPEND-REC-INTERLEAVE-CONS-2
 (502 14 (:DEFINITION ADE::INTERLEAVE))
 (376 18 (:DEFINITION ADE::PREPEND-REC))
 (252 28 (:DEFINITION ADE::CONS-REC))
 (228 36 (:DEFINITION BINARY-APPEND))
 (206 114 (:REWRITE DEFAULT-CDR))
 (198 114 (:REWRITE DEFAULT-CAR))
 (196 196 (:TYPE-PRESCRIPTION ADE::INTERLEAVE))
 (196 196 (:TYPE-PRESCRIPTION ADE::CONSP-INTERLEAVE))
 (70 70 (:TYPE-PRESCRIPTION ADE::CONS-REC))
 (16 4 (:REWRITE CAR-OF-APPEND))
 (12 3 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (12 3 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (8 4 (:DEFINITION TRUE-LISTP))
 (6 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (4 4 (:REWRITE CAR-CONS))
 (3 3 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (3 3 (:REWRITE SUBSETP-TRANS2))
 (3 3 (:REWRITE SUBSETP-TRANS))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (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))|))
 )
(ADE::INTERLEAVE-OF
 (1785 34 (:DEFINITION INTEGER-ABS))
 (1214 440 (:REWRITE DEFAULT-PLUS-2))
 (1009 440 (:REWRITE DEFAULT-PLUS-1))
 (595 17 (:REWRITE |(+ (if a b c) x)|))
 (527 17 (:REWRITE NUMERATOR-NEGATIVE))
 (236 236 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (170 17 (:DEFINITION LENGTH))
 (162 62 (:REWRITE DEFAULT-LESS-THAN-1))
 (153 153 (:TYPE-PRESCRIPTION NUMERATOR-ZERO))
 (153 153 (:TYPE-PRESCRIPTION NUMERATOR-POSITIVE . 2))
 (153 153 (:TYPE-PRESCRIPTION NUMERATOR-POSITIVE . 1))
 (153 153 (:TYPE-PRESCRIPTION NUMERATOR-NEGATIVE . 2))
 (153 153 (:TYPE-PRESCRIPTION NUMERATOR-NEGATIVE . 1))
 (119 34 (:REWRITE DEFAULT-MINUS))
 (119 17 (:DEFINITION LEN))
 (99 99 (:REWRITE FOLD-CONSTS-IN-+))
 (88 62 (:REWRITE DEFAULT-LESS-THAN-2))
 (86 45 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (86 45 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (84 21 (:REWRITE RATIONALP-X))
 (72 72 (:REWRITE DEFAULT-CDR))
 (62 62 (:REWRITE THE-FLOOR-BELOW))
 (62 62 (:REWRITE THE-FLOOR-ABOVE))
 (62 62 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (62 62 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (62 62 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (62 62 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (62 62 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (62 62 (:REWRITE INTEGERP-<-CONSTANT))
 (62 62 (:REWRITE CONSTANT-<-INTEGERP))
 (62 62 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (62 62 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (62 62 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (62 62 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (62 62 (:REWRITE |(< c (- x))|))
 (62 62 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (62 62 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (62 62 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (62 62 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (62 62 (:REWRITE |(< (/ x) (/ y))|))
 (62 62 (:REWRITE |(< (- x) c)|))
 (62 62 (:REWRITE |(< (- x) (- y))|))
 (53 53 (:REWRITE DEFAULT-CAR))
 (51 51 (:REWRITE |(< (/ x) 0)|))
 (51 51 (:REWRITE |(< (* x y) 0)|))
 (44 12 (:REWRITE ACL2-NUMBERP-X))
 (40 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (38 38 (:REWRITE REDUCE-INTEGERP-+))
 (38 38 (:REWRITE INTEGERP-MINUS-X))
 (38 38 (:META META-INTEGERP-CORRECT))
 (34 34 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (34 34 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (32 16 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (21 21 (:REWRITE REDUCE-RATIONALP-+))
 (21 21 (:REWRITE REDUCE-RATIONALP-*))
 (21 21 (:REWRITE RATIONALP-MINUS-X))
 (21 21 (:META META-RATIONALP-CORRECT))
 (17 17 (:TYPE-PRESCRIPTION LEN))
 (17 17 (:REWRITE INTEGERP==>NUMERATOR-=-X))
 (17 17 (:REWRITE INTEGERP==>DENOMINATOR-=-1))
 (17 17 (:REWRITE DEFAULT-REALPART))
 (17 17 (:REWRITE DEFAULT-RATIONAL-NUMERATOR))
 (17 17 (:REWRITE DEFAULT-RATIONAL-DENOMINATOR))
 (17 17 (:REWRITE DEFAULT-IMAGPART))
 (17 17 (:REWRITE DEFAULT-COERCE-2))
 (17 17 (:REWRITE DEFAULT-COERCE-1))
 (11 11 (:REWRITE |(< y (+ (- c) x))|))
 (11 11 (:REWRITE |(< x (+ c/d y))|))
 (8 8 (:REWRITE |(< (+ c/d x) y)|))
 (8 8 (:REWRITE |(< (+ (- c) x) y)|))
 (8 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (8 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (4 4 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (4 4 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (4 4 (:REWRITE |(equal c (/ x))|))
 (4 4 (:REWRITE |(equal c (- x))|))
 (4 4 (:REWRITE |(equal (/ x) c)|))
 (4 4 (:REWRITE |(equal (/ x) (/ y))|))
 (4 4 (:REWRITE |(equal (- x) c)|))
 (4 4 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::INTERLEAVE-OF-LIST-FIX
 (352 96 (:REWRITE ACL2-NUMBERP-X))
 (352 56 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (145 31 (:DEFINITION TRUE-LISTP))
 (140 140 (:REWRITE DEFAULT-CAR))
 (128 32 (:REWRITE RATIONALP-X))
 (112 112 (:REWRITE DEFAULT-CDR))
 (100 56 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (88 56 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (64 32 (:REWRITE DEFAULT-PLUS-2))
 (56 56 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (56 56 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (56 56 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (56 56 (:REWRITE |(equal c (/ x))|))
 (56 56 (:REWRITE |(equal c (- x))|))
 (56 56 (:REWRITE |(equal (/ x) c)|))
 (56 56 (:REWRITE |(equal (/ x) (/ y))|))
 (56 56 (:REWRITE |(equal (- x) c)|))
 (56 56 (:REWRITE |(equal (- x) (- y))|))
 (32 32 (:REWRITE REDUCE-RATIONALP-+))
 (32 32 (:REWRITE REDUCE-RATIONALP-*))
 (32 32 (:REWRITE REDUCE-INTEGERP-+))
 (32 32 (:REWRITE RATIONALP-MINUS-X))
 (32 32 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (32 32 (:REWRITE NORMALIZE-ADDENDS))
 (32 32 (:REWRITE INTEGERP-MINUS-X))
 (32 32 (:REWRITE DEFAULT-PLUS-1))
 (32 32 (:META META-RATIONALP-CORRECT))
 (32 32 (:META META-INTEGERP-CORRECT))
 (21 21 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (14 14 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (14 14 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::INTERLEAVE-OF-APPEND-1
 (891 243 (:REWRITE ACL2-NUMBERP-X))
 (879 118 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (521 349 (:REWRITE DEFAULT-CDR))
 (457 425 (:REWRITE DEFAULT-CAR))
 (334 6 (:REWRITE EQUAL-OF-APPEND-AND-APPEND-SAME-ARG2))
 (324 81 (:REWRITE RATIONALP-X))
 (231 118 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (229 118 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (152 6 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (118 118 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (118 118 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (118 118 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (118 118 (:REWRITE |(equal c (/ x))|))
 (118 118 (:REWRITE |(equal c (- x))|))
 (118 118 (:REWRITE |(equal (/ x) c)|))
 (118 118 (:REWRITE |(equal (/ x) (/ y))|))
 (118 118 (:REWRITE |(equal (- x) c)|))
 (118 118 (:REWRITE |(equal (- x) (- y))|))
 (94 10 (:DEFINITION LEN))
 (81 81 (:REWRITE REDUCE-RATIONALP-+))
 (81 81 (:REWRITE REDUCE-RATIONALP-*))
 (81 81 (:REWRITE REDUCE-INTEGERP-+))
 (81 81 (:REWRITE RATIONALP-MINUS-X))
 (81 81 (:REWRITE INTEGERP-MINUS-X))
 (81 81 (:META META-RATIONALP-CORRECT))
 (81 81 (:META META-INTEGERP-CORRECT))
 (38 38 (:TYPE-PRESCRIPTION LEN))
 (30 30 (:REWRITE |(equal x (if a b c))|))
 (30 30 (:REWRITE |(equal (if a b c) x)|))
 (28 14 (:REWRITE DEFAULT-PLUS-2))
 (24 24 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 (14 14 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (14 14 (:REWRITE NORMALIZE-ADDENDS))
 (14 14 (:REWRITE DEFAULT-PLUS-1))
 (6 6 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::INTERLEAVE-OF-APPEND-2
 (836 228 (:REWRITE ACL2-NUMBERP-X))
 (835 117 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (477 283 (:REWRITE DEFAULT-CDR))
 (403 377 (:REWRITE DEFAULT-CAR))
 (338 6 (:REWRITE EQUAL-OF-APPEND-AND-APPEND-SAME-ARG2))
 (304 76 (:REWRITE RATIONALP-X))
 (227 117 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (223 117 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (166 6 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (117 117 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (117 117 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (117 117 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (117 117 (:REWRITE |(equal c (/ x))|))
 (117 117 (:REWRITE |(equal c (- x))|))
 (117 117 (:REWRITE |(equal (/ x) c)|))
 (117 117 (:REWRITE |(equal (/ x) (/ y))|))
 (117 117 (:REWRITE |(equal (- x) c)|))
 (117 117 (:REWRITE |(equal (- x) (- y))|))
 (76 76 (:REWRITE REDUCE-RATIONALP-+))
 (76 76 (:REWRITE REDUCE-RATIONALP-*))
 (76 76 (:REWRITE REDUCE-INTEGERP-+))
 (76 76 (:REWRITE RATIONALP-MINUS-X))
 (76 76 (:REWRITE INTEGERP-MINUS-X))
 (76 76 (:META META-RATIONALP-CORRECT))
 (76 76 (:META META-INTEGERP-CORRECT))
 (68 8 (:DEFINITION LEN))
 (46 46 (:TYPE-PRESCRIPTION LEN))
 (30 30 (:REWRITE |(equal x (if a b c))|))
 (30 30 (:REWRITE |(equal (if a b c) x)|))
 (24 24 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 (20 10 (:REWRITE DEFAULT-PLUS-2))
 (10 10 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (10 10 (:REWRITE NORMALIZE-ADDENDS))
 (10 10 (:REWRITE DEFAULT-PLUS-1))
 (6 6 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::LEN-1-LISTP)
(ADE::LEN-1-TRUE-LISTP)
(ADE::LEN-1-TRUE-LISTP=>TRUE-LISTP)
(ADE::PAIRLIS$-STRIP-CARS
 (122 121 (:REWRITE DEFAULT-CDR))
 (88 87 (:REWRITE DEFAULT-CAR))
 (73 39 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (73 39 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (65 33 (:REWRITE DEFAULT-PLUS-2))
 (48 39 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (40 40 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (39 39 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (39 39 (:REWRITE |(equal c (/ x))|))
 (39 39 (:REWRITE |(equal c (- x))|))
 (39 39 (:REWRITE |(equal (/ x) c)|))
 (39 39 (:REWRITE |(equal (/ x) (/ y))|))
 (39 39 (:REWRITE |(equal (- x) c)|))
 (39 39 (:REWRITE |(equal (- x) (- y))|))
 (33 33 (:REWRITE DEFAULT-PLUS-1))
 (30 30 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (30 30 (:REWRITE NORMALIZE-ADDENDS))
 (14 14 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (1 1 (:REWRITE |(equal (+ (- c) x) y)|))
 )
(ADE::LEN-1-TRUE-LISTP-PAIRLIS$-WITH-NIL
 (31 29 (:REWRITE DEFAULT-CDR))
 (20 20 (:TYPE-PRESCRIPTION LEN))
 (18 16 (:REWRITE DEFAULT-CAR))
 (8 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (8 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (8 4 (:REWRITE DEFAULT-PLUS-2))
 (4 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (4 4 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (4 4 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (4 4 (:REWRITE NORMALIZE-ADDENDS))
 (4 4 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (4 4 (:REWRITE DEFAULT-PLUS-1))
 (4 4 (:REWRITE |(equal c (/ x))|))
 (4 4 (:REWRITE |(equal c (- x))|))
 (4 4 (:REWRITE |(equal (/ x) c)|))
 (4 4 (:REWRITE |(equal (/ x) (/ y))|))
 (4 4 (:REWRITE |(equal (- x) c)|))
 (4 4 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::POSITION1)
(ADE::MEMBER==>POSITION1
 (66 18 (:REWRITE ACL2-NUMBERP-X))
 (60 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (24 6 (:REWRITE RATIONALP-X))
 (14 7 (:REWRITE SUBSETP-MEMBER . 3))
 (12 12 (:REWRITE DEFAULT-CAR))
 (12 6 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (12 6 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (7 7 (:REWRITE SUBSETP-MEMBER . 4))
 (7 7 (:REWRITE SUBSETP-MEMBER . 2))
 (7 7 (:REWRITE SUBSETP-MEMBER . 1))
 (7 7 (:REWRITE INTERSECTP-MEMBER . 3))
 (7 7 (:REWRITE INTERSECTP-MEMBER . 2))
 (6 6 (:REWRITE REDUCE-RATIONALP-+))
 (6 6 (:REWRITE REDUCE-RATIONALP-*))
 (6 6 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (6 6 (:REWRITE REDUCE-INTEGERP-+))
 (6 6 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (6 6 (:REWRITE RATIONALP-MINUS-X))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (6 6 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (6 6 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE |(equal c (/ x))|))
 (6 6 (:REWRITE |(equal c (- x))|))
 (6 6 (:REWRITE |(equal (/ x) c)|))
 (6 6 (:REWRITE |(equal (/ x) (/ y))|))
 (6 6 (:REWRITE |(equal (- x) c)|))
 (6 6 (:REWRITE |(equal (- x) (- y))|))
 (6 6 (:META META-RATIONALP-CORRECT))
 (6 6 (:META META-INTEGERP-CORRECT))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-PLUS-2))
 (3 3 (:REWRITE DEFAULT-PLUS-1))
 (2 2 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 )
(ADE::POSITION1-OF-APPEND
 (1047 233 (:REWRITE ACL2-NUMBERP-X))
 (810 73 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (407 86 (:REWRITE RATIONALP-X))
 (223 41 (:REWRITE SUBSETP-MEMBER . 3))
 (178 73 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (178 73 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (157 96 (:REWRITE DEFAULT-CDR))
 (156 78 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (147 83 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (94 88 (:REWRITE DEFAULT-CAR))
 (86 86 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (86 86 (:REWRITE REDUCE-RATIONALP-+))
 (86 86 (:REWRITE REDUCE-RATIONALP-*))
 (86 86 (:REWRITE REDUCE-INTEGERP-+))
 (86 86 (:REWRITE RATIONALP-MINUS-X))
 (86 86 (:REWRITE INTEGERP-MINUS-X))
 (86 86 (:META META-RATIONALP-CORRECT))
 (86 86 (:META META-INTEGERP-CORRECT))
 (85 85 (:REWRITE SUBSETP-MEMBER . 2))
 (83 83 (:REWRITE SUBSETP-TRANS2))
 (83 83 (:REWRITE SUBSETP-TRANS))
 (82 82 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (78 78 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (78 78 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (73 73 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (73 73 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (73 73 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (73 73 (:REWRITE |(equal c (/ x))|))
 (73 73 (:REWRITE |(equal c (- x))|))
 (73 73 (:REWRITE |(equal (/ x) c)|))
 (73 73 (:REWRITE |(equal (/ x) (/ y))|))
 (73 73 (:REWRITE |(equal (- x) c)|))
 (73 73 (:REWRITE |(equal (- x) (- y))|))
 (56 7 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (47 41 (:REWRITE DEFAULT-PLUS-1))
 (41 41 (:REWRITE SUBSETP-MEMBER . 4))
 (41 41 (:REWRITE INTERSECTP-MEMBER . 3))
 (41 41 (:REWRITE INTERSECTP-MEMBER . 2))
 (39 39 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (39 39 (:REWRITE NORMALIZE-ADDENDS))
 (21 7 (:REWRITE CAR-OF-APPEND))
 (14 14 (:REWRITE CONSP-OF-APPEND))
 (14 14 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (7 7 (:REWRITE |(equal x (if a b c))|))
 (4 4 (:REWRITE |(equal (+ (- c) x) y)|))
 )
(ADE::REMOVE-LST)
(ADE::TV-GUARD)
(ADE::TV-GUARD-MAKE-TREE
 (27600 12 (:REWRITE ADE::CONSP-MAKE-TREE))
 (19770 73 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (14055 5 (:DEFINITION NATP))
 (10485 87 (:REWRITE THE-FLOOR-BELOW))
 (9921 5 (:REWRITE DEFAULT-CDR))
 (9921 5 (:REWRITE DEFAULT-CAR))
 (8507 17 (:LINEAR LINEAR-FLOOR-BOUNDS-1))
 (4687 4687 (:TYPE-PRESCRIPTION NOT-INTEGERP-4B))
 (4687 4687 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (4687 4687 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (4687 4687 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (3422 106 (:REWRITE DEFAULT-PLUS-2))
 (3366 106 (:REWRITE DEFAULT-PLUS-1))
 (3267 31 (:REWRITE |(+ y x)|))
 (3172 244 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (2910 34 (:REWRITE NORMALIZE-ADDENDS))
 (2434 8 (:REWRITE |(+ y (+ x z))|))
 (2214 84 (:REWRITE THE-FLOOR-ABOVE))
 (2196 244 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (2196 244 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (1409 25 (:DEFINITION FIX))
 (1220 244 (:TYPE-PRESCRIPTION FLOOR-ZERO . 4))
 (1220 244 (:TYPE-PRESCRIPTION FLOOR-ZERO . 3))
 (1220 244 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (1220 244 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (1220 244 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 2))
 (1220 244 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (1220 244 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (1220 244 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (1220 244 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (1156 17 (:REWRITE FLOOR-ZERO . 3))
 (928 16 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (927 103 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (921 76 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (901 17 (:REWRITE CANCEL-FLOOR-+))
 (617 81 (:REWRITE DEFAULT-LESS-THAN-1))
 (552 138 (:REWRITE |(* y x)|))
 (532 76 (:REWRITE |(< (- x) c)|))
 (532 76 (:REWRITE |(< (- x) (- y))|))
 (515 103 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (515 103 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 2))
 (510 17 (:REWRITE FLOOR-ZERO . 4))
 (510 17 (:REWRITE FLOOR-X-Y-=-1 . 2))
 (502 111 (:REWRITE INTEGERP-MINUS-X))
 (495 495 (:TYPE-PRESCRIPTION NOT-INTEGERP-4A))
 (495 495 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (495 495 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (495 495 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (389 369 (:REWRITE DEFAULT-TIMES-2))
 (374 17 (:REWRITE FLOOR-=-X/Y . 3))
 (374 17 (:REWRITE FLOOR-=-X/Y . 2))
 (369 369 (:REWRITE DEFAULT-TIMES-1))
 (352 67 (:REWRITE SIMPLIFY-SUMS-<))
 (327 21 (:REWRITE |(floor x 2)| . 2))
 (324 15 (:REWRITE |(+ 0 x)|))
 (321 81 (:REWRITE DEFAULT-LESS-THAN-2))
 (293 38 (:REWRITE |(* (- x) y)|))
 (291 6 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (291 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (291 6 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (260 10 (:LINEAR LINEAR-FLOOR-BOUNDS-3))
 (231 21 (:REWRITE DEFAULT-FLOOR-RATIO))
 (220 10 (:LINEAR LINEAR-FLOOR-BOUNDS-2))
 (203 203 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (186 42 (:REWRITE DEFAULT-MINUS))
 (173 81 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (173 38 (:REWRITE |(- (* c x))|))
 (128 2 (:REWRITE |(+ x (if a b c))|))
 (117 21 (:REWRITE |(floor x 2)| . 1))
 (97 79 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (94 94 (:REWRITE REDUCE-INTEGERP-+))
 (94 94 (:META META-INTEGERP-CORRECT))
 (85 17 (:REWRITE FLOOR-ZERO . 5))
 (85 17 (:REWRITE FLOOR-ZERO . 2))
 (85 17 (:REWRITE FLOOR-X-Y-=-1 . 3))
 (85 17 (:REWRITE FLOOR-X-Y-=--1 . 3))
 (85 17 (:REWRITE FLOOR-X-Y-=--1 . 2))
 (85 17 (:REWRITE FLOOR-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (85 17 (:REWRITE FLOOR-CANCEL-*-CONST))
 (85 17 (:REWRITE |(floor (* x (/ y)) z) not rewriting-goal-literal|))
 (79 79 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (76 76 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (76 76 (:REWRITE INTEGERP-<-CONSTANT))
 (76 76 (:REWRITE CONSTANT-<-INTEGERP))
 (76 76 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (76 76 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (76 76 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (76 76 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (76 76 (:REWRITE |(< c (- x))|))
 (76 76 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (76 76 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (76 76 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (76 76 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (76 76 (:REWRITE |(< (/ x) (/ y))|))
 (54 2 (:REWRITE |(- (if a b c))|))
 (44 16 (:REWRITE BUBBLE-DOWN-+-MATCH-1))
 (38 38 (:TYPE-PRESCRIPTION ABS))
 (30 2 (:REWRITE |(- (+ x y))|))
 (21 21 (:REWRITE DEFAULT-FLOOR-2))
 (21 21 (:REWRITE DEFAULT-FLOOR-1))
 (21 3 (:REWRITE |(* y (* x z))|))
 (19 19 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (18 18 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (17 17 (:REWRITE FLOOR-CANCEL-*-REWRITING-GOAL-LITERAL))
 (17 17 (:REWRITE |(floor x (- y))| . 2))
 (17 17 (:REWRITE |(floor x (- y))| . 1))
 (17 17 (:REWRITE |(floor x (* y (/ z))) rewriting-goal-literal|))
 (17 17 (:REWRITE |(floor x (* y (/ z))) not rewriting-goal-literal|))
 (17 17 (:REWRITE |(floor (- x) y)| . 2))
 (17 17 (:REWRITE |(floor (- x) y)| . 1))
 (17 17 (:REWRITE |(floor (* x (/ y)) z) rewriting-goal-literal|))
 (17 17 (:REWRITE |(< (* (/ x) y) 1) with (< x 0)|))
 (17 17 (:REWRITE |(< (* (/ x) y) 1) with (< 0 x)|))
 (16 4 (:REWRITE |(+ x (* c x))|))
 (12 12 (:REWRITE |(+ x (- x))|))
 (6 6 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (6 6 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (6 6 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (6 6 (:REWRITE |(equal c (/ x))|))
 (6 6 (:REWRITE |(equal c (- x))|))
 (6 6 (:REWRITE |(equal (/ x) c)|))
 (6 6 (:REWRITE |(equal (/ x) (/ y))|))
 (6 6 (:REWRITE |(equal (- x) c)|))
 (6 6 (:REWRITE |(equal (- x) (- y))|))
 (6 6 (:REWRITE |(< (+ c/d x) y)|))
 (6 6 (:REWRITE |(< (+ (- c) x) y)|))
 (6 6 (:REWRITE |(* a (/ a))|))
 (5 5 (:REWRITE |(< (/ x) 0)|))
 (5 5 (:REWRITE |(< (* x y) 0)|))
 (4 4 (:REWRITE ZP-OPEN))
 (3 3 (:REWRITE |(equal (+ (- c) x) y)|))
 (3 3 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (3 3 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (3 3 (:REWRITE |(< y (+ (- c) x))|))
 (3 3 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (3 3 (:REWRITE |(< x (/ y)) with (< 0 y)|))
 (3 3 (:REWRITE |(< x (+ c/d y))|))
 (3 3 (:REWRITE |(< 0 (* x y))|))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (2 2 (:REWRITE |(* a (/ a) b)|))
 )