(MAKE-CHARACTER-LIST-MAKES-CHARACTER-LIST
 (17 15 (:REWRITE DEFAULT-CAR))
 (12 10 (:REWRITE DEFAULT-CDR))
 )
(LEN-OF-APPEND
 (48 24 (:REWRITE DEFAULT-+-2))
 (31 24 (:REWRITE DEFAULT-+-1))
 (20 10 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (18 15 (:REWRITE DEFAULT-CDR))
 (10 10 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (10 10 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (3 3 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(CONSP-OF-APPEND
 (224 112 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (112 112 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (112 112 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (6 6 (:REWRITE DEFAULT-CAR))
 (5 5 (:REWRITE DEFAULT-CDR))
 )
(LEN-OF-MAKE-CHARACTER-LIST
 (42 38 (:REWRITE DEFAULT-CDR))
 (42 21 (:REWRITE DEFAULT-+-2))
 (21 21 (:REWRITE DEFAULT-+-1))
 (17 17 (:REWRITE DEFAULT-CAR))
 )
(LEN-OF-REVAPPEND
 (54 26 (:REWRITE DEFAULT-+-2))
 (34 26 (:REWRITE DEFAULT-+-1))
 (21 15 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE FOLD-CONSTS-IN-+))
 (3 3 (:REWRITE DEFAULT-CAR))
 )
(LEN-OF-TAKE
 (14 10 (:REWRITE DEFAULT-+-2))
 (10 10 (:REWRITE DEFAULT-+-1))
 (9 8 (:REWRITE DEFAULT-CDR))
 (6 5 (:REWRITE DEFAULT-<-1))
 (5 5 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE ZP-OPEN))
 (4 4 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(NTHCDR-OF-APPEND
 (1282 1282 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (198 143 (:REWRITE DEFAULT-+-2))
 (164 86 (:REWRITE DEFAULT-CDR))
 (148 143 (:REWRITE DEFAULT-+-1))
 (75 52 (:REWRITE DEFAULT-<-1))
 (58 52 (:REWRITE DEFAULT-<-2))
 (40 40 (:REWRITE DEFAULT-CAR))
 (22 11 (:REWRITE DEFAULT-UNARY-MINUS))
 (14 14 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (9 9 (:REWRITE CONSP-OF-APPEND))
 )
(TAKE-OF-BINARY-APPEND-1
 (28 11 (:REWRITE DEFAULT-CAR))
 (26 9 (:REWRITE DEFAULT-CDR))
 (20 10 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (18 12 (:REWRITE DEFAULT-+-2))
 (16 10 (:REWRITE DEFAULT-<-1))
 (12 12 (:REWRITE DEFAULT-+-1))
 (10 10 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (10 10 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (10 10 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE ZP-OPEN))
 (4 4 (:REWRITE CONSP-OF-APPEND))
 )
(BY-SLICE-YOU-MEAN-THE-WHOLE-CAKE-1
 (22 22 (:REWRITE DEFAULT-CDR))
 (18 18 (:REWRITE DEFAULT-CAR))
 (13 7 (:REWRITE DEFAULT-+-2))
 (8 1 (:REWRITE ZP-OPEN))
 (7 7 (:REWRITE DEFAULT-+-1))
 (3 3 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (2 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(TAKE-OF-LEN-FREE
 (32 4 (:REWRITE ZP-OPEN))
 (16 10 (:REWRITE DEFAULT-+-2))
 (12 12 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-+-1))
 (9 9 (:REWRITE DEFAULT-CAR))
 (8 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 )
(ASSOC-AFTER-REMOVE1-ASSOC
 (74 74 (:REWRITE DEFAULT-CAR))
 (25 25 (:REWRITE DEFAULT-CDR))
 )
(ASSOC-AFTER-REMOVE-ASSOC
 (96 92 (:REWRITE DEFAULT-CDR))
 )
(CHARACTER-LISTP-OF-REVAPPEND
 (80 10 (:REWRITE CHARACTER-LISTP-REVAPPEND))
 (63 49 (:REWRITE DEFAULT-CDR))
 (60 45 (:REWRITE DEFAULT-CAR))
 (50 10 (:DEFINITION TRUE-LISTP))
 )
(CHARACTER-LISTP-OF-TAKE
 (208 25 (:REWRITE TAKE-OF-LEN-FREE))
 (74 44 (:REWRITE DEFAULT-+-2))
 (52 50 (:REWRITE DEFAULT-CDR))
 (44 44 (:REWRITE DEFAULT-+-1))
 (43 30 (:REWRITE DEFAULT-<-1))
 (40 37 (:REWRITE DEFAULT-CAR))
 (30 30 (:REWRITE DEFAULT-<-2))
 (15 9 (:REWRITE ZP-OPEN))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(CHARACTER-LISTP-OF-NTHCDR
 (16 16 (:REWRITE DEFAULT-+-2))
 (16 16 (:REWRITE DEFAULT-+-1))
 (14 8 (:REWRITE ZP-OPEN))
 (13 13 (:REWRITE DEFAULT-CAR))
 (10 10 (:REWRITE DEFAULT-CDR))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 )
(STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP
 (16 16 (:REWRITE DEFAULT-CAR))
 (8 8 (:REWRITE DEFAULT-CDR))
 )
(MAKE-CHARACTER-LIST-OF-BINARY-APPEND
 (914 55 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
 (692 56 (:DEFINITION CHARACTER-LISTP))
 (263 105 (:REWRITE DEFAULT-CDR))
 (262 262 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (228 106 (:REWRITE DEFAULT-CAR))
 (216 216 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (72 9 (:REWRITE CHARACTER-LISTP-APPEND))
 (51 51 (:REWRITE CONSP-OF-APPEND))
 (45 9 (:DEFINITION TRUE-LISTP))
 )
(LEN-OF-NTHCDR
 (135 93 (:REWRITE DEFAULT-+-2))
 (98 93 (:REWRITE DEFAULT-+-1))
 (30 12 (:REWRITE ZP-OPEN))
 (29 22 (:REWRITE DEFAULT-<-1))
 (27 15 (:REWRITE FOLD-CONSTS-IN-+))
 (22 22 (:REWRITE DEFAULT-<-2))
 (14 14 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(CONSP-OF-NTHCDR
 (190 95 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (95 95 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (70 44 (:REWRITE DEFAULT-+-2))
 (48 44 (:REWRITE DEFAULT-+-1))
 (34 24 (:REWRITE DEFAULT-<-2))
 (30 24 (:REWRITE DEFAULT-<-1))
 (29 29 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE ZP-OPEN))
 (3 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(REVAPPEND-OF-BINARY-APPEND-1
 (489 489 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (33 24 (:REWRITE DEFAULT-CAR))
 (32 23 (:REWRITE DEFAULT-CDR))
 )
(BINARY-APPEND-FIRST-N-AC-NTHCDR
 (53 3 (:REWRITE BY-SLICE-YOU-MEAN-THE-WHOLE-CAKE-1))
 (47 32 (:REWRITE DEFAULT-+-2))
 (35 35 (:REWRITE DEFAULT-CDR))
 (32 32 (:REWRITE DEFAULT-+-1))
 (11 11 (:REWRITE DEFAULT-CAR))
 (11 7 (:REWRITE DEFAULT-<-1))
 (10 4 (:REWRITE ZP-OPEN))
 (9 3 (:REWRITE FOLD-CONSTS-IN-+))
 (8 7 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(NTH-OF-APPEND
 (99 46 (:REWRITE DEFAULT-CAR))
 (93 61 (:REWRITE DEFAULT-+-2))
 (65 61 (:REWRITE DEFAULT-+-1))
 (49 36 (:REWRITE DEFAULT-CDR))
 (40 28 (:REWRITE DEFAULT-<-2))
 (28 28 (:REWRITE DEFAULT-<-1))
 (12 7 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(ASSOCIATIVITY-OF-APPEND
 (1556 628 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (830 628 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (628 628 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (58 20 (:REWRITE DEFAULT-CAR))
 (54 16 (:REWRITE DEFAULT-CDR))
 (15 15 (:REWRITE CONSP-OF-APPEND))
 )
(MEMBER-OF-A-NAT-LIST
 (24 24 (:REWRITE DEFAULT-CAR))
 (12 10 (:REWRITE DEFAULT-<-1))
 (10 10 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(UPDATE-NTH-OF-BOOLEAN-LIST
 (56 28 (:REWRITE DEFAULT-CAR))
 (50 22 (:REWRITE DEFAULT-CDR))
 (9 6 (:REWRITE ZP-OPEN))
 (6 6 (:REWRITE DEFAULT-+-2))
 (6 6 (:REWRITE DEFAULT-+-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(NAT-LISTP-OF-BINARY-APPEND
 (188 94 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (101 44 (:REWRITE DEFAULT-CAR))
 (95 38 (:REWRITE DEFAULT-CDR))
 (94 94 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (94 94 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (27 27 (:REWRITE DEFAULT-<-2))
 (27 27 (:REWRITE DEFAULT-<-1))
 (21 21 (:REWRITE CONSP-OF-APPEND))
 )
(EQLABLE-LISTP-IF-NAT-LISTP
 (11 11 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 )
(MEMBER-OF-BINARY-APPEND
 (108 54 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (98 44 (:REWRITE DEFAULT-CAR))
 (82 31 (:REWRITE DEFAULT-CDR))
 (54 54 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (54 54 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (18 18 (:REWRITE CONSP-OF-APPEND))
 )
(NO-DUPLICATESP-OF-APPEND
 (220 130 (:REWRITE DEFAULT-CDR))
 (200 100 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (184 106 (:REWRITE DEFAULT-CAR))
 (100 100 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (100 100 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (27 27 (:REWRITE CONSP-OF-APPEND))
 )
(INTERSECTP-OF-APPEND-1
 (84 84 (:REWRITE DEFAULT-CAR))
 (69 69 (:REWRITE DEFAULT-CDR))
 (30 10 (:DEFINITION BINARY-APPEND))
 )
(INTERSECTP-OF-APPEND-2
 (141 76 (:REWRITE DEFAULT-CAR))
 (128 64 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (126 64 (:REWRITE DEFAULT-CDR))
 (64 64 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (64 64 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (24 24 (:REWRITE CONSP-OF-APPEND))
 )
(INTERSECTP-IS-COMMUTATIVE
 (158 158 (:REWRITE DEFAULT-CAR))
 (109 109 (:REWRITE DEFAULT-CDR))
 )
(SUBSETP-APPEND1
 (126 68 (:REWRITE DEFAULT-CAR))
 (120 60 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (113 58 (:REWRITE DEFAULT-CDR))
 (60 60 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (60 60 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (21 21 (:REWRITE CONSP-OF-APPEND))
 )
(SUBSETP-APPEND2
 (155 128 (:REWRITE DEFAULT-CAR))
 (138 69 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (107 92 (:REWRITE DEFAULT-CDR))
 (69 69 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (69 69 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (36 12 (:REWRITE MEMBER-OF-BINARY-APPEND))
 )
(SUBSETP-APPEND3
 (167 152 (:REWRITE DEFAULT-CAR))
 (113 98 (:REWRITE DEFAULT-CDR))
 (84 12 (:REWRITE MEMBER-OF-BINARY-APPEND))
 (50 25 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (25 25 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (25 25 (:TYPE-PRESCRIPTION BINARY-APPEND))
 )
(SUBSETP-TRANS
 (116 116 (:REWRITE DEFAULT-CAR))
 (89 89 (:REWRITE DEFAULT-CDR))
 )
(SUBSETP-MEMBER
 (28 28 (:REWRITE DEFAULT-CAR))
 (16 16 (:REWRITE DEFAULT-CDR))
 (9 9 (:REWRITE SUBSETP-TRANS))
 )
(SUBSETP-TRANS2
 (60 2 (:DEFINITION SUBSETP-EQUAL))
 (32 6 (:REWRITE SUBSETP-MEMBER . 4))
 (32 4 (:DEFINITION MEMBER-EQUAL))
 (18 8 (:REWRITE SUBSETP-MEMBER . 2))
 (12 12 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (6 6 (:REWRITE SUBSETP-MEMBER . 3))
 (6 6 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE DEFAULT-CAR))
 )
(NTH-OF-REVAPPEND
 (323 237 (:REWRITE DEFAULT-+-2))
 (245 237 (:REWRITE DEFAULT-+-1))
 (234 207 (:REWRITE DEFAULT-CDR))
 (165 108 (:REWRITE DEFAULT-CAR))
 (106 81 (:REWRITE DEFAULT-<-2))
 (87 81 (:REWRITE DEFAULT-<-1))
 (32 23 (:REWRITE DEFAULT-UNARY-MINUS))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(TRUE-LISTP-OF-MAKE-LIST-AC
 (13 11 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE ZP-OPEN))
 (2 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 )
(LEN-OF-MAKE-LIST-AC
 (72 40 (:REWRITE DEFAULT-+-2))
 (44 40 (:REWRITE DEFAULT-+-1))
 (25 19 (:REWRITE DEFAULT-CDR))
 (7 6 (:REWRITE DEFAULT-<-1))
 (6 6 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE ZP-OPEN))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(CONSP-OF-MAKE-LIST-AC
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(BOOLEAN-LISTP-OF-MAKE-LIST-AC
 (76 20 (:REWRITE DEFAULT-CDR))
 (54 20 (:REWRITE DEFAULT-CAR))
 (36 8 (:REWRITE CONSP-OF-MAKE-LIST-AC))
 (18 18 (:REWRITE ZP-OPEN))
 (2 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 )
(BOOLEANP-OF-CAR-MAKE-LIST
 (39 17 (:REWRITE DEFAULT-CAR))
 (24 13 (:REWRITE DEFAULT-+-2))
 (16 16 (:REWRITE DEFAULT-CDR))
 (16 13 (:REWRITE DEFAULT-+-1))
 (10 10 (:REWRITE ZP-OPEN))
 (10 2 (:REWRITE CONSP-OF-MAKE-LIST-AC))
 (8 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(CAR-OF-MAKE-LIST
 (44 10 (:REWRITE DEFAULT-CAR))
 (7 3 (:REWRITE CONSP-OF-MAKE-LIST-AC))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(CDR-OF-MAKE-LIST
 (49 12 (:REWRITE DEFAULT-CDR))
 (38 38 (:REWRITE DEFAULT-+-2))
 (38 38 (:REWRITE DEFAULT-+-1))
 (12 12 (:REWRITE DEFAULT-<-2))
 (12 12 (:REWRITE DEFAULT-<-1))
 (7 3 (:REWRITE CONSP-OF-MAKE-LIST-AC))
 )
(MEMBER-EQUAL-NTH
 (39 17 (:REWRITE SUBSETP-MEMBER . 1))
 (31 31 (:REWRITE DEFAULT-CAR))
 (31 21 (:REWRITE DEFAULT-<-2))
 (26 15 (:REWRITE DEFAULT-+-2))
 (23 21 (:REWRITE DEFAULT-<-1))
 (20 1 (:DEFINITION SUBSETP-EQUAL))
 (17 17 (:REWRITE SUBSETP-MEMBER . 2))
 (15 15 (:REWRITE SUBSETP-MEMBER . 4))
 (15 15 (:REWRITE SUBSETP-MEMBER . 3))
 (15 15 (:REWRITE DEFAULT-CDR))
 (15 15 (:REWRITE DEFAULT-+-1))
 (8 8 (:REWRITE ZP-OPEN))
 (5 5 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(MAKE-CHARACTER-LIST-OF-REVAPPEND
 (642 58 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
 (445 66 (:DEFINITION CHARACTER-LISTP))
 (298 298 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (151 125 (:REWRITE DEFAULT-CAR))
 (139 113 (:REWRITE DEFAULT-CDR))
 (132 6 (:REWRITE CHARACTER-LISTP-OF-REVAPPEND))
 (18 6 (:DEFINITION TRUE-LIST-FIX))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 )
(TAKE-OF-MAKE-CHARACTER-LIST
 (721 63 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
 (500 77 (:DEFINITION CHARACTER-LISTP))
 (483 35 (:REWRITE TAKE-OF-LEN-FREE))
 (378 378 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (208 183 (:REWRITE DEFAULT-CDR))
 (166 147 (:REWRITE DEFAULT-CAR))
 (130 15 (:REWRITE CHARACTER-LISTP-OF-TAKE))
 (128 80 (:REWRITE DEFAULT-+-2))
 (80 80 (:REWRITE DEFAULT-+-1))
 (48 8 (:REWRITE LEN-OF-MAKE-CHARACTER-LIST))
 (41 17 (:REWRITE ZP-OPEN))
 (24 16 (:REWRITE DEFAULT-<-1))
 (24 8 (:REWRITE FOLD-CONSTS-IN-+))
 (19 16 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(REVAPPEND-OF-TRUE-LIST-FIX
 (41 32 (:REWRITE DEFAULT-CAR))
 (39 30 (:REWRITE DEFAULT-CDR))
 )
(APPEND-OF-TRUE-LIST-FIX
 (199 199 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (11 10 (:REWRITE DEFAULT-CAR))
 (9 8 (:REWRITE DEFAULT-CDR))
 )
(BOOLEAN-LISTP-OF-REVAPPEND
 (92 68 (:REWRITE DEFAULT-CAR))
 (88 64 (:REWRITE DEFAULT-CDR))
 )
(BOOLEAN-LISTP-OF-FIRST-N-AC
 (103 12 (:REWRITE BY-SLICE-YOU-MEAN-THE-WHOLE-CAKE-1))
 (76 76 (:REWRITE DEFAULT-CAR))
 (72 72 (:REWRITE DEFAULT-CDR))
 (56 56 (:TYPE-PRESCRIPTION LEN))
 (44 8 (:DEFINITION LEN))
 (28 28 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 (24 15 (:REWRITE DEFAULT-+-2))
 (23 7 (:DEFINITION REVAPPEND))
 (15 15 (:REWRITE DEFAULT-+-1))
 (9 6 (:REWRITE ZP-OPEN))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(CONSP-OF-TAKE
 (141 11 (:REWRITE TAKE-OF-LEN-FREE))
 (79 79 (:TYPE-PRESCRIPTION LEN))
 (64 12 (:DEFINITION LEN))
 (31 18 (:REWRITE DEFAULT-+-2))
 (18 18 (:REWRITE DEFAULT-+-1))
 (17 17 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(NTH-OF-MAKE-LIST-AC
 (108 101 (:REWRITE DEFAULT-+-2))
 (107 101 (:REWRITE DEFAULT-+-1))
 (85 83 (:REWRITE DEFAULT-<-1))
 (83 83 (:REWRITE DEFAULT-<-2))
 (28 28 (:REWRITE DEFAULT-CAR))
 (21 21 (:REWRITE DEFAULT-CDR))
 (19 19 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (13 13 (:REWRITE DEFAULT-UNARY-MINUS))
 (1 1 (:REWRITE NTH-ADD1))
 )
(NTH-OF-NTHCDR
 (242 197 (:REWRITE DEFAULT-+-2))
 (225 45 (:DEFINITION LEN))
 (197 197 (:REWRITE DEFAULT-+-1))
 (147 127 (:REWRITE DEFAULT-<-2))
 (132 127 (:REWRITE DEFAULT-<-1))
 (120 51 (:REWRITE ZP-OPEN))
 (69 27 (:REWRITE FOLD-CONSTS-IN-+))
 (5 5 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(INTERSECT-WITH-SUBSET
 (1152 336 (:REWRITE SUBSETP-TRANS2))
 (1117 336 (:REWRITE SUBSETP-TRANS))
 (485 485 (:REWRITE DEFAULT-CAR))
 (459 238 (:REWRITE SUBSETP-MEMBER . 3))
 (414 414 (:REWRITE DEFAULT-CDR))
 (238 238 (:REWRITE SUBSETP-MEMBER . 4))
 )
(UPDATE-NTH-OF-MAKE-LIST
 (81 81 (:REWRITE DEFAULT-+-2))
 (81 81 (:REWRITE DEFAULT-+-1))
 (70 31 (:REWRITE DEFAULT-CDR))
 (60 21 (:REWRITE DEFAULT-CAR))
 (42 42 (:REWRITE DEFAULT-<-2))
 (42 42 (:REWRITE DEFAULT-<-1))
 (7 7 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(NTHCDR-OF-UPDATE-NTH
 (775 241 (:REWRITE DEFAULT-CDR))
 (555 37 (:REWRITE CONSP-OF-NTHCDR))
 (410 356 (:REWRITE DEFAULT-+-2))
 (356 356 (:REWRITE DEFAULT-+-1))
 (290 44 (:REWRITE DEFAULT-CAR))
 (226 189 (:REWRITE DEFAULT-<-2))
 (192 189 (:REWRITE DEFAULT-<-1))
 (185 185 (:TYPE-PRESCRIPTION LEN))
 (185 37 (:DEFINITION LEN))
 (20 20 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (17 17 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(UPDATE-NTH-OF-UPDATE-NTH-1
 (413 130 (:REWRITE DEFAULT-CAR))
 (106 103 (:REWRITE DEFAULT-+-2))
 (103 103 (:REWRITE DEFAULT-+-1))
 (90 36 (:REWRITE ZP-OPEN))
 (54 18 (:REWRITE FOLD-CONSTS-IN-+))
 (41 40 (:REWRITE DEFAULT-<-1))
 (40 40 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(UPDATE-NTH-OF-UPDATE-NTH-2
 (73 22 (:REWRITE DEFAULT-CDR))
 (60 15 (:REWRITE DEFAULT-CAR))
 (8 8 (:REWRITE ZP-OPEN))
 (7 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE UPDATE-NTH-OF-UPDATE-NTH-1))
 )
(NAT-LISTP-OF-REMOVE
 (29 28 (:REWRITE DEFAULT-CAR))
 (20 19 (:REWRITE DEFAULT-CDR))
 (11 11 (:REWRITE DEFAULT-<-2))
 (11 11 (:REWRITE DEFAULT-<-1))
 )
(SUBSETP-OF-REMOVE
 (976 182 (:REWRITE SUBSETP-TRANS))
 (870 182 (:REWRITE SUBSETP-TRANS2))
 (495 249 (:REWRITE SUBSETP-MEMBER . 1))
 (310 309 (:REWRITE DEFAULT-CAR))
 (255 254 (:REWRITE DEFAULT-CDR))
 (101 101 (:REWRITE SUBSETP-MEMBER . 4))
 (101 101 (:REWRITE SUBSETP-MEMBER . 3))
 (71 71 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (71 71 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (71 71 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (71 71 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 )
(MEMBER-OF-REMOVE
 (1831 73 (:DEFINITION SUBSETP-EQUAL))
 (330 313 (:REWRITE DEFAULT-CDR))
 (310 291 (:REWRITE DEFAULT-CAR))
 (181 181 (:REWRITE SUBSETP-MEMBER . 2))
 (141 141 (:REWRITE SUBSETP-TRANS2))
 (141 141 (:REWRITE SUBSETP-TRANS))
 (51 51 (:REWRITE SUBSETP-MEMBER . 4))
 )
(ASSOC-AFTER-PUT-ASSOC
 (229 165 (:REWRITE DEFAULT-CAR))
 (81 67 (:REWRITE DEFAULT-CDR))
 )
(NTHCDR-OF-CDR
 (38 26 (:REWRITE DEFAULT-+-2))
 (28 28 (:TYPE-PRESCRIPTION LEN))
 (26 26 (:REWRITE DEFAULT-+-1))
 (21 7 (:REWRITE COMMUTATIVITY-OF-+))
 (13 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE ZP-OPEN))
 (9 9 (:REWRITE DEFAULT-<-1))
 )
(CONSP-OF-CDR-OF-NTHCDR
 (162 108 (:REWRITE DEFAULT-+-2))
 (108 108 (:REWRITE DEFAULT-+-1))
 (81 27 (:REWRITE COMMUTATIVITY-OF-+))
 (71 56 (:REWRITE DEFAULT-<-2))
 (58 56 (:REWRITE DEFAULT-<-1))
 (27 27 (:REWRITE ZP-OPEN))
 (24 6 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(UPDATE-NTH-OF-NTH
 (33 20 (:REWRITE DEFAULT-+-2))
 (27 18 (:REWRITE DEFAULT-<-2))
 (24 24 (:REWRITE DEFAULT-CDR))
 (20 20 (:REWRITE DEFAULT-+-1))
 (20 18 (:REWRITE DEFAULT-<-1))
 (12 12 (:REWRITE DEFAULT-CAR))
 (8 8 (:REWRITE ZP-OPEN))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(CHARACTER-LISTP-OF-MAKE-LIST-AC
 (34 34 (:REWRITE DEFAULT-+-2))
 (34 34 (:REWRITE DEFAULT-+-1))
 (23 23 (:REWRITE DEFAULT-CAR))
 (22 22 (:REWRITE DEFAULT-CDR))
 (14 14 (:REWRITE DEFAULT-<-2))
 (14 14 (:REWRITE DEFAULT-<-1))
 (14 6 (:REWRITE CONSP-OF-MAKE-LIST-AC))
 )
(STRING-LISTP-OF-APPEND
 (124 62 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (100 43 (:REWRITE DEFAULT-CAR))
 (95 38 (:REWRITE DEFAULT-CDR))
 (62 62 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (62 62 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (21 21 (:REWRITE CONSP-OF-APPEND))
 )
(TRUE-LISTP-WHEN-STRING-LIST
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 2 (:DEFINITION TRUE-LISTP))
 (3 3 (:REWRITE DEFAULT-CAR))
 )
(BINARY-APPEND-TAKE-NTHCDR
 (390 130 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (71 7 (:REWRITE TAKE-OF-LEN-FREE))
 (67 21 (:REWRITE DEFAULT-CDR))
 (47 32 (:REWRITE DEFAULT-+-2))
 (32 32 (:REWRITE DEFAULT-+-1))
 (28 2 (:REWRITE CONSP-OF-NTHCDR))
 (21 12 (:REWRITE ZP-OPEN))
 (20 14 (:REWRITE DEFAULT-<-1))
 (20 9 (:REWRITE CONSP-OF-TAKE))
 (19 14 (:REWRITE DEFAULT-<-2))
 (17 7 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (6 2 (:DEFINITION NFIX))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(TRUE-LIST-FIX-WHEN-TRUE-LISTP
 (55 6 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (39 7 (:DEFINITION STRING-LISTP))
 (28 28 (:TYPE-PRESCRIPTION STRING-LISTP))
 (12 12 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-CAR))
 )
(TRUE-LIST-FIX-OF-COERCE
 (2 2 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE DEFAULT-COERCE-1))
 )
(LEN-OF-TRUE-LIST-FIX
 (166 6 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (118 13 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (95 7 (:DEFINITION TRUE-LISTP))
 (81 14 (:DEFINITION STRING-LISTP))
 (63 63 (:TYPE-PRESCRIPTION STRING-LISTP))
 (30 29 (:REWRITE DEFAULT-CDR))
 (28 28 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (17 17 (:REWRITE DEFAULT-CAR))
 (14 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-+-1))
 )
(NTH-OF-MAKE-CHARACTER-LIST
 (800 91 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
 (577 103 (:DEFINITION CHARACTER-LISTP))
 (442 442 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (231 221 (:REWRITE DEFAULT-CAR))
 (184 178 (:REWRITE DEFAULT-CDR))
 (90 54 (:REWRITE DEFAULT-+-2))
 (70 45 (:REWRITE DEFAULT-<-2))
 (54 54 (:REWRITE DEFAULT-+-1))
 (45 45 (:REWRITE DEFAULT-<-1))
 (45 5 (:REWRITE CHARACTERP-NTH))
 (10 10 (:REWRITE ZP-OPEN))
 )
(NTH-OF-FIRST-N-AC
 (759 519 (:REWRITE DEFAULT-+-2))
 (613 66 (:REWRITE BY-SLICE-YOU-MEAN-THE-WHOLE-CAKE-1))
 (539 519 (:REWRITE DEFAULT-+-1))
 (234 182 (:REWRITE DEFAULT-<-2))
 (191 182 (:REWRITE DEFAULT-<-1))
 (55 38 (:REWRITE DEFAULT-UNARY-MINUS))
 (9 9 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(NTH-OF-TAKE
 (273 24 (:REWRITE TAKE-OF-LEN-FREE))
 (140 24 (:DEFINITION LEN))
 (138 138 (:TYPE-PRESCRIPTION LEN))
 (83 54 (:REWRITE DEFAULT-+-2))
 (54 54 (:REWRITE DEFAULT-+-1))
 (30 30 (:REWRITE DEFAULT-<-2))
 (30 30 (:REWRITE DEFAULT-<-1))
 (17 14 (:REWRITE ZP-OPEN))
 (9 3 (:REWRITE FOLD-CONSTS-IN-+))
 )
(NTHCDR-OF-NIL
 (6 2 (:REWRITE COMMUTATIVITY-OF-+))
 (4 4 (:REWRITE ZP-OPEN))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 )
(NTHCDR-WHEN->=-N-LEN-L
 (149 15 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (114 48 (:REWRITE DEFAULT-CDR))
 (106 17 (:DEFINITION STRING-LISTP))
 (79 79 (:TYPE-PRESCRIPTION STRING-LISTP))
 (62 3 (:REWRITE CONSP-OF-NTHCDR))
 (57 40 (:REWRITE DEFAULT-+-2))
 (40 40 (:REWRITE DEFAULT-+-1))
 (37 27 (:REWRITE DEFAULT-<-2))
 (27 27 (:REWRITE DEFAULT-<-1))
 (19 19 (:REWRITE DEFAULT-CAR))
 (18 9 (:REWRITE ZP-OPEN))
 (9 3 (:REWRITE FOLD-CONSTS-IN-+))
 )
(REVAPPEND-OF-REVAPPEND
 (574 287 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (287 287 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (24 18 (:REWRITE DEFAULT-CAR))
 (21 15 (:REWRITE DEFAULT-CDR))
 )
(CHARACTER-LISTP-OF-MEMBER
 (21 21 (:REWRITE DEFAULT-CAR))
 (11 11 (:REWRITE DEFAULT-CDR))
 (9 9 (:REWRITE SUBSETP-MEMBER . 4))
 (9 9 (:REWRITE SUBSETP-MEMBER . 3))
 )
(TRUE-LISTP-OF-MEMBER
 (163 15 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (121 17 (:DEFINITION STRING-LISTP))
 (75 75 (:TYPE-PRESCRIPTION STRING-LISTP))
 (29 29 (:REWRITE DEFAULT-CDR))
 (27 27 (:REWRITE DEFAULT-CAR))
 (13 13 (:REWRITE SUBSETP-MEMBER . 4))
 (13 13 (:REWRITE SUBSETP-MEMBER . 3))
 )
(LEN-OF-MEMBER
 (22 11 (:REWRITE DEFAULT-+-2))
 (11 11 (:REWRITE DEFAULT-+-1))
 (10 5 (:REWRITE DEFAULT-<-2))
 (10 5 (:REWRITE DEFAULT-<-1))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE SUBSETP-MEMBER . 4))
 (7 7 (:REWRITE SUBSETP-MEMBER . 3))
 (6 6 (:REWRITE DEFAULT-CAR))
 )
(LEN-OF-REMOVE1-ASSOC
 (41 21 (:REWRITE DEFAULT-+-2))
 (25 25 (:REWRITE DEFAULT-CAR))
 (21 21 (:REWRITE DEFAULT-+-1))
 (16 16 (:REWRITE DEFAULT-CDR))
 )
(LEN-OF-REMOVE1-EQUAL
 (77 39 (:REWRITE DEFAULT-+-2))
 (72 72 (:REWRITE DEFAULT-CDR))
 (70 17 (:REWRITE SUBSETP-MEMBER . 3))
 (70 3 (:DEFINITION SUBSETP-EQUAL))
 (46 24 (:REWRITE SUBSETP-MEMBER . 1))
 (43 43 (:REWRITE DEFAULT-CAR))
 (39 39 (:REWRITE DEFAULT-+-1))
 (24 24 (:REWRITE SUBSETP-MEMBER . 2))
 (17 17 (:REWRITE SUBSETP-MEMBER . 4))
 (12 12 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (6 6 (:REWRITE SUBSETP-TRANS2))
 (6 6 (:REWRITE SUBSETP-TRANS))
 )
(ASSOC-OF-REMOVE1-ASSOC
 (61 61 (:REWRITE DEFAULT-CAR))
 (17 17 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE ASSOC-AFTER-REMOVE1-ASSOC))
 )
(ASSOC-EQUAL-OF-REMOVE1-EQUAL
 (53 53 (:REWRITE DEFAULT-CAR))
 (17 17 (:REWRITE DEFAULT-CDR))
 )
(ASSOC-OF-CAR-WHEN-MEMBER
 (113 113 (:REWRITE DEFAULT-CAR))
 (69 16 (:REWRITE SUBSETP-MEMBER . 3))
 (50 2 (:DEFINITION SUBSETP-EQUAL))
 (21 21 (:REWRITE SUBSETP-MEMBER . 2))
 (21 21 (:REWRITE SUBSETP-MEMBER . 1))
 (19 19 (:REWRITE DEFAULT-CDR))
 (16 16 (:REWRITE SUBSETP-MEMBER . 4))
 (7 7 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )
(CAR-OF-NTHCDR
 (319 33 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (265 17 (:DEFINITION TRUE-LISTP))
 (225 37 (:DEFINITION STRING-LISTP))
 (170 53 (:REWRITE DEFAULT-CAR))
 (169 169 (:TYPE-PRESCRIPTION STRING-LISTP))
 (117 6 (:REWRITE CONSP-OF-NTHCDR))
 (72 12 (:DEFINITION LEN))
 (68 53 (:REWRITE DEFAULT-+-2))
 (53 53 (:REWRITE DEFAULT-+-1))
 (48 3 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (35 26 (:REWRITE DEFAULT-<-2))
 (26 26 (:REWRITE DEFAULT-<-1))
 )
(STRINGP-OF-NTH
 (42 31 (:REWRITE DEFAULT-<-2))
 (40 24 (:REWRITE DEFAULT-+-2))
 (31 31 (:REWRITE DEFAULT-<-1))
 (30 30 (:REWRITE DEFAULT-CAR))
 (26 26 (:REWRITE DEFAULT-CDR))
 (24 24 (:REWRITE DEFAULT-+-1))
 (7 7 (:REWRITE ZP-OPEN))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(STRING-LISTP-OF-UPDATE-NTH
 (149 117 (:REWRITE DEFAULT-CDR))
 (104 70 (:REWRITE DEFAULT-CAR))
 (73 44 (:REWRITE DEFAULT-+-2))
 (69 44 (:REWRITE DEFAULT-<-1))
 (45 44 (:REWRITE DEFAULT-<-2))
 (44 44 (:REWRITE DEFAULT-+-1))
 (14 8 (:REWRITE ZP-OPEN))
 (8 8 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(REVAPPEND-OF-BINARY-APPEND-2
 (240 120 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (120 120 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (58 19 (:REWRITE DEFAULT-CAR))
 (56 17 (:REWRITE DEFAULT-CDR))
 (9 9 (:REWRITE CONSP-OF-APPEND))
 )
(ADD-PAIR-OF-ADD-PAIR-1
 (124 88 (:REWRITE DEFAULT-CAR))
 (70 14 (:REWRITE SYMBOL<-ASYMMETRIC))
 (39 30 (:REWRITE SYMBOL<-TRICHOTOMY))
 (39 26 (:REWRITE DEFAULT-CDR))
 (36 30 (:REWRITE SYMBOL<-TRANSITIVE))
 )
(PRINC$-OF-PRINC$
 (54 51 (:REWRITE DEFAULT-CAR))
 (51 45 (:REWRITE DEFAULT-CDR))
 (48 3 (:DEFINITION ADD-PAIR))
 (40 8 (:DEFINITION ASSOC-EQUAL))
 (20 10 (:DEFINITION NTH))
 (15 3 (:REWRITE SYMBOL<-ASYMMETRIC))
 (14 10 (:REWRITE DEFAULT-COERCE-1))
 (12 4 (:DEFINITION REVAPPEND))
 (11 11 (:REWRITE DEFAULT-COERCE-2))
 (9 9 (:TYPE-PRESCRIPTION SYMBOL<))
 (9 3 (:DEFINITION UPDATE-NTH))
 (6 6 (:REWRITE SYMBOL<-TRICHOTOMY))
 (6 6 (:REWRITE SYMBOL<-TRANSITIVE))
 (6 3 (:TYPE-PRESCRIPTION TRUE-LISTP-REVAPPEND-TYPE-PRESCRIPTION))
 (6 2 (:DEFINITION BINARY-APPEND))
 (6 1 (:REWRITE DEFAULT-COERCE-3))
 (3 3 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (3 3 (:TYPE-PRESCRIPTION REVAPPEND))
 (1 1 (:REWRITE CONSP-OF-APPEND))
 )
(PAINFUL-DEBUGGING-LEMMA-1)
(PAINFUL-DEBUGGING-LEMMA-2)
(PAINFUL-DEBUGGING-LEMMA-3)
(PAINFUL-DEBUGGING-LEMMA-4
 (8 8 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 4 (:REWRITE DEFAULT-<-2))
 (6 4 (:REWRITE DEFAULT-<-1))
 (4 2 (:REWRITE DEFAULT-+-2))
 (4 2 (:REWRITE DEFAULT-+-1))
 )
(PAINFUL-DEBUGGING-LEMMA-5)
(PAINFUL-DEBUGGING-LEMMA-6
 (3 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(PAINFUL-DEBUGGING-LEMMA-7
 (14 9 (:REWRITE DEFAULT-*-2))
 (9 9 (:REWRITE DEFAULT-*-1))
 (9 5 (:REWRITE DEFAULT-<-2))
 (8 4 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE ZP-OPEN))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE DEFAULT-CDR))
 )
(PAINFUL-DEBUGGING-LEMMA-12
 (1 1 (:REWRITE DEFAULT-UNARY-MINUS))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(PAINFUL-DEBUGGING-LEMMA-13)
(INTEGERP-OF-NTH-WHEN-INTEGER-LISTP
 (42 31 (:REWRITE DEFAULT-<-2))
 (40 24 (:REWRITE DEFAULT-+-2))
 (31 31 (:REWRITE DEFAULT-<-1))
 (30 30 (:REWRITE DEFAULT-CAR))
 (26 26 (:REWRITE DEFAULT-CDR))
 (24 24 (:REWRITE DEFAULT-+-1))
 (7 7 (:REWRITE ZP-OPEN))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(TRUE-LIST-LISTP-OF-APPEND
 (843 89 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (595 45 (:DEFINITION TRUE-LISTP))
 (581 90 (:DEFINITION STRING-LISTP))
 (440 440 (:TYPE-PRESCRIPTION STRING-LISTP))
 (430 15 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (232 175 (:REWRITE DEFAULT-CDR))
 (216 108 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (191 134 (:REWRITE DEFAULT-CAR))
 (108 108 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (21 21 (:REWRITE CONSP-OF-APPEND))
 )
(RATIONALP-OF-NTH-WHEN-RATIONAL-LISTP
 (42 31 (:REWRITE DEFAULT-<-2))
 (40 24 (:REWRITE DEFAULT-+-2))
 (31 31 (:REWRITE DEFAULT-<-1))
 (30 30 (:REWRITE DEFAULT-CAR))
 (26 26 (:REWRITE DEFAULT-CDR))
 (24 24 (:REWRITE DEFAULT-+-1))
 (7 7 (:REWRITE ZP-OPEN))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(MEMBER-OF-REMOVE1-ASSOC
 (498 27 (:DEFINITION SUBSETP-EQUAL))
 (382 19 (:REWRITE SUBSETP-MEMBER . 3))
 (276 67 (:REWRITE SUBSETP-MEMBER . 1))
 (122 122 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (78 78 (:REWRITE DEFAULT-CAR))
 (67 67 (:REWRITE SUBSETP-MEMBER . 2))
 (59 59 (:REWRITE DEFAULT-CDR))
 (53 53 (:REWRITE SUBSETP-TRANS2))
 (53 53 (:REWRITE SUBSETP-TRANS))
 (19 19 (:REWRITE SUBSETP-MEMBER . 4))
 )
(ACL2-COUNT-OF-TRUE-LIST-FIX
 (170 10 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (118 13 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (113 50 (:REWRITE DEFAULT-+-2))
 (95 7 (:DEFINITION TRUE-LISTP))
 (81 14 (:DEFINITION STRING-LISTP))
 (72 50 (:REWRITE DEFAULT-+-1))
 (63 63 (:TYPE-PRESCRIPTION STRING-LISTP))
 (48 2 (:LINEAR ACL2-COUNT-CAR-CDR-LINEAR))
 (37 36 (:REWRITE DEFAULT-CDR))
 (28 28 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (28 27 (:REWRITE DEFAULT-CAR))
 (28 17 (:REWRITE DEFAULT-<-1))
 (25 17 (:REWRITE DEFAULT-<-2))
 (19 19 (:REWRITE FOLD-CONSTS-IN-+))
 (15 3 (:DEFINITION LEN))
 (6 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:REWRITE DEFAULT-NUMERATOR))
 (3 3 (:REWRITE DEFAULT-DENOMINATOR))
 (3 3 (:REWRITE DEFAULT-COERCE-2))
 (3 3 (:REWRITE DEFAULT-COERCE-1))
 (2 2 (:REWRITE DEFAULT-REALPART))
 (2 2 (:REWRITE DEFAULT-IMAGPART))
 )
(UPDATE-NTH-OF-REVAPPEND
 (526 208 (:REWRITE DEFAULT-CAR))
 (325 235 (:REWRITE DEFAULT-+-2))
 (241 235 (:REWRITE DEFAULT-+-1))
 (111 86 (:REWRITE DEFAULT-<-2))
 (94 86 (:REWRITE DEFAULT-<-1))
 (35 25 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(TRUE-LISTP-OF-UPDATE-NTH
 (439 26 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (357 36 (:DEFINITION STRING-LISTP))
 (171 171 (:TYPE-PRESCRIPTION STRING-LISTP))
 (110 80 (:REWRITE DEFAULT-CDR))
 (63 42 (:REWRITE DEFAULT-CAR))
 (53 7 (:REWRITE STRING-LISTP-OF-UPDATE-NTH))
 (36 21 (:REWRITE DEFAULT-+-2))
 (21 21 (:REWRITE DEFAULT-+-1))
 (20 15 (:REWRITE DEFAULT-<-2))
 (15 15 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE ZP-OPEN))
 (3 3 (:REWRITE CAR-CONS))
 )
(NTHCDR-OF-NTHCDR
 (5802 128 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (3884 201 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (3285 204 (:DEFINITION STRING-LISTP))
 (3265 101 (:DEFINITION TRUE-LISTP))
 (1404 88 (:REWRITE CONSP-OF-NTHCDR))
 (1098 84 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (1049 1049 (:TYPE-PRESCRIPTION STRING-LISTP))
 (860 172 (:DEFINITION LEN))
 (704 704 (:TYPE-PRESCRIPTION LEN))
 (618 432 (:REWRITE DEFAULT-+-2))
 (579 205 (:REWRITE DEFAULT-CAR))
 (525 426 (:REWRITE DEFAULT-<-2))
 (446 432 (:REWRITE DEFAULT-+-1))
 (435 426 (:REWRITE DEFAULT-<-1))
 (259 7 (:REWRITE LEN-OF-NTHCDR))
 (212 68 (:REWRITE ZP-OPEN))
 (176 14 (:REWRITE CAR-OF-NTHCDR))
 (162 14 (:DEFINITION NTH))
 (56 14 (:REWRITE STRINGP-OF-NTH))
 (28 7 (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+))
 (14 14 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1 1 (:REWRITE CAR-CONS))
 )
(ACL2-COUNT-OF-MEMBER
 (143 62 (:REWRITE DEFAULT-+-2))
 (96 4 (:LINEAR ACL2-COUNT-CAR-CDR-LINEAR))
 (90 62 (:REWRITE DEFAULT-+-1))
 (35 20 (:REWRITE DEFAULT-<-1))
 (31 20 (:REWRITE DEFAULT-<-2))
 (25 25 (:REWRITE FOLD-CONSTS-IN-+))
 (19 19 (:REWRITE DEFAULT-CDR))
 (19 19 (:REWRITE DEFAULT-CAR))
 (15 3 (:DEFINITION LEN))
 (14 14 (:REWRITE SUBSETP-MEMBER . 4))
 (14 14 (:REWRITE SUBSETP-MEMBER . 3))
 (6 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:REWRITE DEFAULT-NUMERATOR))
 (3 3 (:REWRITE DEFAULT-DENOMINATOR))
 (3 3 (:REWRITE DEFAULT-COERCE-2))
 (3 3 (:REWRITE DEFAULT-COERCE-1))
 (2 2 (:REWRITE DEFAULT-REALPART))
 (2 2 (:REWRITE DEFAULT-IMAGPART))
 )
(STRING-LISTP-OF-RESIZE-LIST
 (22 20 (:REWRITE DEFAULT-CDR))
 (21 19 (:REWRITE DEFAULT-CAR))
 (14 14 (:REWRITE DEFAULT-+-2))
 (14 14 (:REWRITE DEFAULT-+-1))
 (11 11 (:REWRITE DEFAULT-<-2))
 (11 11 (:REWRITE DEFAULT-<-1))
 (9 3 (:REWRITE FOLD-CONSTS-IN-+))
 )
(UPDATE-NTH-OF-FIRST-N-AC
 (2091 144 (:REWRITE BY-SLICE-YOU-MEAN-THE-WHOLE-CAKE-1))
 (969 641 (:REWRITE DEFAULT-+-2))
 (791 597 (:REWRITE DEFAULT-CDR))
 (648 641 (:REWRITE DEFAULT-+-1))
 (568 99 (:DEFINITION REVAPPEND))
 (417 294 (:REWRITE DEFAULT-CAR))
 (286 9 (:REWRITE LEN-UPDATE-NTH))
 (243 191 (:REWRITE DEFAULT-<-2))
 (217 191 (:REWRITE DEFAULT-<-1))
 (95 9 (:DEFINITION MAX))
 (74 74 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (70 20 (:TYPE-PRESCRIPTION MAX))
 (39 25 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FIRST-N-AC-OF-UPDATE-NTH
 (770 39 (:REWRITE BY-SLICE-YOU-MEAN-THE-WHOLE-CAKE-1))
 (334 192 (:REWRITE DEFAULT-+-2))
 (207 192 (:REWRITE DEFAULT-+-1))
 (201 141 (:REWRITE DEFAULT-CDR))
 (161 7 (:REWRITE LEN-UPDATE-NTH))
 (99 57 (:REWRITE DEFAULT-CAR))
 (99 28 (:DEFINITION REVAPPEND))
 (84 65 (:REWRITE DEFAULT-<-1))
 (72 65 (:REWRITE DEFAULT-<-2))
 (49 24 (:REWRITE ZP-OPEN))
 (49 7 (:DEFINITION MAX))
 (20 20 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (6 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(TAKE-OF-UPDATE-NTH
 (1623 104 (:REWRITE TAKE-OF-LEN-FREE))
 (879 130 (:DEFINITION LEN))
 (770 770 (:TYPE-PRESCRIPTION LEN))
 (418 249 (:REWRITE DEFAULT-+-2))
 (249 249 (:REWRITE DEFAULT-+-1))
 (110 5 (:REWRITE LEN-UPDATE-NTH))
 (99 66 (:REWRITE DEFAULT-CAR))
 (64 57 (:REWRITE DEFAULT-<-1))
 (57 57 (:REWRITE DEFAULT-<-2))
 (56 16 (:REWRITE FOLD-CONSTS-IN-+))
 (35 5 (:DEFINITION MAX))
 (26 26 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (23 23 (:REWRITE ZP-OPEN))
 (23 11 (:REWRITE CONSP-OF-TAKE))
 (9 9 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (8 4 (:REWRITE UNICITY-OF-0))
 (6 3 (:TYPE-PRESCRIPTION MAX))
 (4 4 (:DEFINITION FIX))
 )
(LEMMA
 (127 4 (:REWRITE BY-SLICE-YOU-MEAN-THE-WHOLE-CAKE-1))
 (116 12 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (105 87 (:REWRITE DEFAULT-CDR))
 (100 51 (:REWRITE DEFAULT-+-2))
 (83 14 (:DEFINITION STRING-LISTP))
 (60 60 (:TYPE-PRESCRIPTION STRING-LISTP))
 (56 38 (:REWRITE DEFAULT-CAR))
 (51 51 (:REWRITE DEFAULT-+-1))
 (5 5 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE ZP-OPEN))
 )
(REMEMBER-THAT-TIME-WITH-UPDATE-NTH
 (401 43 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (392 281 (:REWRITE DEFAULT-CDR))
 (299 188 (:REWRITE DEFAULT-+-2))
 (278 47 (:DEFINITION STRING-LISTP))
 (266 155 (:REWRITE DEFAULT-CAR))
 (219 24 (:REWRITE TAKE-OF-LEN-FREE))
 (211 211 (:TYPE-PRESCRIPTION STRING-LISTP))
 (188 188 (:REWRITE DEFAULT-+-1))
 (184 19 (:REWRITE BY-SLICE-YOU-MEAN-THE-WHOLE-CAKE-1))
 (135 45 (:REWRITE ZP-OPEN))
 (90 30 (:REWRITE CONSP-OF-TAKE))
 (67 58 (:REWRITE DEFAULT-<-1))
 (58 58 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(TAKE-OF-NTHCDR
 (1812 134 (:REWRITE TAKE-OF-LEN-FREE))
 (1477 154 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1139 799 (:REWRITE DEFAULT-+-2))
 (1065 48 (:REWRITE CONSP-OF-NTHCDR))
 (1059 171 (:DEFINITION STRING-LISTP))
 (860 715 (:REWRITE DEFAULT-<-2))
 (804 799 (:REWRITE DEFAULT-+-1))
 (764 764 (:TYPE-PRESCRIPTION STRING-LISTP))
 (725 715 (:REWRITE DEFAULT-<-1))
 (704 60 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (112 20 (:REWRITE CONSP-OF-TAKE))
 (108 4 (:REWRITE LEN-OF-NTHCDR))
 (32 4 (:REWRITE CAR-OF-NTHCDR))
 (28 4 (:DEFINITION NTH))
 (8 8 (:REWRITE CAR-CONS))
 (7 1 (:REWRITE DISTRIBUTIVITY-OF-MINUS-OVER-+))
 (6 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 5 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(PUT-ASSOC-EQUAL-WITHOUT-CHANGE)
(MEMBER-EQUAL-OF-REMOVE1-EQUAL
 (1582 74 (:DEFINITION SUBSETP-EQUAL))
 (1010 188 (:REWRITE SUBSETP-MEMBER . 1))
 (989 48 (:REWRITE SUBSETP-MEMBER . 3))
 (340 340 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (256 256 (:REWRITE DEFAULT-CAR))
 (254 254 (:REWRITE DEFAULT-CDR))
 (188 188 (:REWRITE SUBSETP-MEMBER . 2))
 (148 148 (:REWRITE SUBSETP-TRANS2))
 (148 148 (:REWRITE SUBSETP-TRANS))
 (48 48 (:REWRITE SUBSETP-MEMBER . 4))
 )
(MEMBER-OF-INTERSECTION$
 (4390 730 (:REWRITE SUBSETP-MEMBER . 1))
 (826 803 (:REWRITE DEFAULT-CAR))
 (804 782 (:REWRITE DEFAULT-CDR))
 (730 730 (:REWRITE SUBSETP-MEMBER . 2))
 (566 566 (:REWRITE SUBSETP-TRANS2))
 (566 566 (:REWRITE SUBSETP-TRANS))
 (282 282 (:REWRITE SUBSETP-MEMBER . 4))
 )
(NTH-OF-INTERSECTION$
 (68 4 (:DEFINITION INTERSECTION-EQUAL))
 (67 7 (:DEFINITION MEMBER-EQUAL))
 (53 15 (:REWRITE SUBSETP-MEMBER . 1))
 (33 2 (:DEFINITION SUBSETP-EQUAL))
 (24 3 (:DEFINITION NTH))
 (20 20 (:REWRITE DEFAULT-CDR))
 (20 20 (:REWRITE DEFAULT-CAR))
 (15 15 (:REWRITE SUBSETP-MEMBER . 2))
 (12 12 (:REWRITE SUBSETP-MEMBER . 4))
 (12 12 (:REWRITE SUBSETP-MEMBER . 3))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (6 6 (:TYPE-PRESCRIPTION INTERSECTION-EQUAL))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 (3 3 (:REWRITE ZP-OPEN))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 )
(MEMBER-OF-STRIP-CARS-OF-REMOVE-ASSOC
 (2490 90 (:DEFINITION SUBSETP-EQUAL))
 (1846 67 (:REWRITE SUBSETP-MEMBER . 3))
 (1201 238 (:REWRITE SUBSETP-MEMBER . 1))
 (528 493 (:REWRITE DEFAULT-CAR))
 (404 404 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (327 300 (:REWRITE DEFAULT-CDR))
 (238 238 (:REWRITE SUBSETP-MEMBER . 2))
 (176 176 (:REWRITE SUBSETP-TRANS2))
 (176 176 (:REWRITE SUBSETP-TRANS))
 (67 67 (:REWRITE SUBSETP-MEMBER . 4))
 )
(NO-DUPLICATESP-OF-STRIP-CARS-OF-REMOVE-ASSOC
 (102 96 (:REWRITE DEFAULT-CAR))
 (83 72 (:REWRITE DEFAULT-CDR))
 (73 36 (:REWRITE SUBSETP-MEMBER . 3))
 (38 38 (:REWRITE SUBSETP-MEMBER . 2))
 (38 38 (:REWRITE SUBSETP-MEMBER . 1))
 (36 36 (:REWRITE SUBSETP-MEMBER . 4))
 (29 2 (:DEFINITION SUBSETP-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )
(TAKE-FEWER-OF-TAKE-MORE
 (396 39 (:REWRITE TAKE-OF-LEN-FREE))
 (199 199 (:TYPE-PRESCRIPTION LEN))
 (172 29 (:DEFINITION LEN))
 (74 44 (:REWRITE DEFAULT-+-2))
 (66 43 (:REWRITE DEFAULT-CDR))
 (44 44 (:REWRITE DEFAULT-+-1))
 (38 16 (:REWRITE DEFAULT-CAR))
 (30 6 (:REWRITE CONSP-OF-TAKE))
 (27 27 (:REWRITE ZP-OPEN))
 (20 5 (:REWRITE LEN-OF-TAKE))
 (19 16 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE DEFAULT-<-1))
 (5 1 (:REWRITE FOLD-CONSTS-IN-+))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (2 1 (:REWRITE UNICITY-OF-0))
 (1 1 (:DEFINITION FIX))
 )
(LEN-OF-REMOVE-WHEN-NO-DUPLICATESP
 (99 97 (:REWRITE DEFAULT-CDR))
 (77 39 (:REWRITE DEFAULT-+-2))
 (67 45 (:REWRITE SUBSETP-MEMBER . 1))
 (63 63 (:REWRITE DEFAULT-CAR))
 (56 41 (:REWRITE SUBSETP-MEMBER . 3))
 (45 45 (:REWRITE SUBSETP-MEMBER . 2))
 (41 41 (:REWRITE SUBSETP-MEMBER . 4))
 (39 39 (:REWRITE DEFAULT-+-1))
 (32 2 (:DEFINITION SUBSETP-EQUAL))
 (6 6 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (3 3 (:REWRITE SUBSETP-TRANS2))
 (3 3 (:REWRITE SUBSETP-TRANS))
 )
(NO-DUPLICATESP-OF-REMOVE
 (57 24 (:REWRITE SUBSETP-MEMBER . 3))
 (47 45 (:REWRITE DEFAULT-CDR))
 (44 43 (:REWRITE DEFAULT-CAR))
 (26 26 (:REWRITE SUBSETP-MEMBER . 2))
 (26 26 (:REWRITE SUBSETP-MEMBER . 1))
 (25 2 (:DEFINITION SUBSETP-EQUAL))
 (24 24 (:REWRITE SUBSETP-MEMBER . 4))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )
(DEC-DEC-INDUCT
 (3 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE ZP-OPEN))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(TAKE-OF-MAKE-LIST-AC-LEMMA-1
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(TAKE-OF-MAKE-LIST-AC
 (253 12 (:REWRITE TAKE-OF-LEN-FREE))
 (156 7 (:REWRITE LEN-OF-MAKE-LIST-AC))
 (98 73 (:REWRITE DEFAULT-+-2))
 (92 92 (:TYPE-PRESCRIPTION LEN))
 (82 73 (:REWRITE DEFAULT-+-1))
 (72 9 (:REWRITE COMMUTATIVITY-OF-+))
 (62 10 (:DEFINITION LEN))
 (53 17 (:REWRITE ZP-OPEN))
 (48 4 (:REWRITE COMMUTATIVITY-2-OF-+))
 (41 19 (:REWRITE FOLD-CONSTS-IN-+))
 (34 34 (:REWRITE DEFAULT-<-2))
 (34 34 (:REWRITE DEFAULT-<-1))
 (12 12 (:REWRITE DEFAULT-CDR))
 (4 4 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(STRINGP-OF-APPEND
 (224 112 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (112 112 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (112 112 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (6 6 (:REWRITE DEFAULT-CAR))
 (5 5 (:REWRITE DEFAULT-CDR))
 )
(REMOVE-ASSOC-OF-PUT-ASSOC
 (503 432 (:REWRITE DEFAULT-CAR))
 (410 55 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (301 59 (:DEFINITION ASSOC-EQUAL))
 (236 204 (:REWRITE DEFAULT-CDR))
 (84 14 (:REWRITE ASSOC-AFTER-REMOVE-ASSOC))
 (41 4 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (25 3 (:DEFINITION MEMBER-EQUAL))
 (15 15 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 )
(LAST-OF-MEMBER
 (131 30 (:REWRITE SUBSETP-MEMBER . 3))
 (87 5 (:DEFINITION SUBSETP-EQUAL))
 (82 65 (:REWRITE DEFAULT-CDR))
 (43 38 (:REWRITE DEFAULT-CAR))
 (30 30 (:REWRITE SUBSETP-MEMBER . 4))
 (24 24 (:REWRITE SUBSETP-MEMBER . 2))
 (24 24 (:REWRITE SUBSETP-MEMBER . 1))
 (18 18 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (9 9 (:REWRITE SUBSETP-TRANS2))
 (9 9 (:REWRITE SUBSETP-TRANS))
 )
(INTEGERP-OF-CAR-OF-LAST-WHEN-INTEGER-LISTP
 (18 10 (:REWRITE DEFAULT-CAR))
 (12 12 (:REWRITE DEFAULT-CDR))
 )
(NON-NEGATIVITY-OF-CAR-OF-LAST-WHEN-NAT-LISTP
 (36 10 (:REWRITE DEFAULT-<-1))
 (18 10 (:REWRITE DEFAULT-CAR))
 (15 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (11 11 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-<-2))
 )
(LEN-OF-PUT-ASSOC-EQUAL
 (157 157 (:REWRITE DEFAULT-CAR))
 (150 25 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (132 118 (:REWRITE DEFAULT-CDR))
 (114 57 (:REWRITE DEFAULT-+-2))
 (57 57 (:REWRITE DEFAULT-+-1))
 (52 4 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (32 4 (:DEFINITION MEMBER-EQUAL))
 (20 20 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 )
(REMOVE-ASSOC-WHEN-ABSENT-1
 (218 8 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (154 17 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (123 9 (:DEFINITION TRUE-LISTP))
 (105 18 (:DEFINITION STRING-LISTP))
 (83 83 (:TYPE-PRESCRIPTION STRING-LISTP))
 (49 49 (:REWRITE DEFAULT-CAR))
 (39 39 (:REWRITE DEFAULT-CDR))
 (38 38 (:TYPE-PRESCRIPTION TRUE-LISTP))
 )
(REMOVE-ASSOC-WHEN-ABSENT-2
 (90 5 (:DEFINITION REMOVE-ASSOC-EQUAL))
 (80 16 (:DEFINITION ASSOC-EQUAL))
 (63 63 (:REWRITE DEFAULT-CAR))
 (26 26 (:REWRITE DEFAULT-CDR))
 )
(REMOVE-ASSOC-OF-REMOVE-ASSOC
 (593 583 (:REWRITE DEFAULT-CAR))
 (327 25 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (253 247 (:REWRITE DEFAULT-CDR))
 (206 24 (:DEFINITION MEMBER-EQUAL))
 (168 25 (:REWRITE ASSOC-AFTER-REMOVE-ASSOC))
 (120 120 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (57 19 (:REWRITE REMOVE-ASSOC-WHEN-ABSENT-2))
 (48 48 (:REWRITE SUBSETP-MEMBER . 2))
 (48 48 (:REWRITE SUBSETP-MEMBER . 1))
 (19 4 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (9 3 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (3 3 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (3 3 (:TYPE-PRESCRIPTION STRING-LISTP))
 (3 3 (:DEFINITION TRUE-LISTP))
 (3 3 (:DEFINITION STRING-LISTP))
 )
(LEN-OF-REMOVE-ASSOC-1
 (91 7 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (79 79 (:REWRITE DEFAULT-CAR))
 (56 7 (:DEFINITION MEMBER-EQUAL))
 (44 43 (:REWRITE DEFAULT-CDR))
 (35 35 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (24 12 (:REWRITE DEFAULT-+-2))
 (14 14 (:REWRITE SUBSETP-MEMBER . 2))
 (14 14 (:REWRITE SUBSETP-MEMBER . 1))
 (12 12 (:REWRITE DEFAULT-+-1))
 (12 6 (:REWRITE DEFAULT-<-2))
 (12 6 (:REWRITE DEFAULT-<-1))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(LEN-OF-REMOVE-ASSOC-2
 (257 257 (:REWRITE DEFAULT-CAR))
 (164 163 (:REWRITE DEFAULT-CDR))
 (116 59 (:REWRITE DEFAULT-+-2))
 (104 4 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (72 8 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (59 59 (:REWRITE DEFAULT-+-1))
 (58 2 (:DEFINITION TRUE-LIST-FIX))
 (56 4 (:DEFINITION TRUE-LISTP))
 (48 8 (:DEFINITION STRING-LISTP))
 (40 40 (:TYPE-PRESCRIPTION STRING-LISTP))
 (24 12 (:REWRITE DEFAULT-<-1))
 (22 12 (:REWRITE DEFAULT-<-2))
 (20 20 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (13 1 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (8 1 (:DEFINITION MEMBER-EQUAL))
 (5 5 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 )
(MEMBER-OF-STRIP-CARS
 (130 5 (:DEFINITION SUBSETP-EQUAL))
 (106 18 (:REWRITE SUBSETP-MEMBER . 3))
 (81 28 (:REWRITE SUBSETP-MEMBER . 1))
 (80 76 (:REWRITE DEFAULT-CAR))
 (30 27 (:REWRITE DEFAULT-CDR))
 (28 28 (:REWRITE SUBSETP-MEMBER . 2))
 (22 22 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (18 18 (:REWRITE SUBSETP-MEMBER . 4))
 (10 10 (:REWRITE SUBSETP-TRANS2))
 (10 10 (:REWRITE SUBSETP-TRANS))
 )
(LEN-OF-REMOVE-ASSOC-WHEN-NO-DUPLICATESP-STRIP-CARS
 (416 16 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (360 354 (:REWRITE DEFAULT-CAR))
 (289 263 (:REWRITE DEFAULT-CDR))
 (288 32 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (272 139 (:REWRITE DEFAULT-+-2))
 (232 8 (:DEFINITION TRUE-LIST-FIX))
 (224 16 (:DEFINITION TRUE-LISTP))
 (192 32 (:DEFINITION STRING-LISTP))
 (170 22 (:DEFINITION MEMBER-EQUAL))
 (160 160 (:TYPE-PRESCRIPTION STRING-LISTP))
 (139 139 (:REWRITE DEFAULT-+-1))
 (80 80 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (78 6 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (44 44 (:REWRITE SUBSETP-MEMBER . 2))
 (44 44 (:REWRITE SUBSETP-MEMBER . 1))
 (32 32 (:REWRITE SUBSETP-MEMBER . 4))
 (32 32 (:REWRITE SUBSETP-MEMBER . 3))
 )
(STRIP-CARS-OF-REMOVE-ASSOC
 (126 122 (:REWRITE DEFAULT-CAR))
 (91 7 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (59 56 (:REWRITE DEFAULT-CDR))
 (56 7 (:DEFINITION MEMBER-EQUAL))
 (35 35 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (14 14 (:REWRITE SUBSETP-MEMBER . 2))
 (14 14 (:REWRITE SUBSETP-MEMBER . 1))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(STRIP-CARS-OF-PUT-ASSOC
 (71 14 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (68 53 (:REWRITE DEFAULT-CDR))
 )
(REMOVE-WHEN-ABSENT
 (166 6 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (118 13 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (95 7 (:DEFINITION TRUE-LISTP))
 (81 14 (:DEFINITION STRING-LISTP))
 (63 63 (:TYPE-PRESCRIPTION STRING-LISTP))
 (31 31 (:REWRITE DEFAULT-CDR))
 (31 9 (:REWRITE SUBSETP-MEMBER . 1))
 (29 29 (:REWRITE DEFAULT-CAR))
 (28 28 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (20 1 (:DEFINITION SUBSETP-EQUAL))
 (9 9 (:REWRITE SUBSETP-MEMBER . 2))
 (7 7 (:REWRITE SUBSETP-MEMBER . 4))
 (7 7 (:REWRITE SUBSETP-MEMBER . 3))
 (5 5 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 )
(INTERSECTP-WHEN-MEMBER
 (2666 762 (:REWRITE SUBSETP-MEMBER . 1))
 (889 873 (:REWRITE DEFAULT-CAR))
 (807 796 (:REWRITE DEFAULT-CDR))
 (762 762 (:REWRITE SUBSETP-MEMBER . 2))
 (635 635 (:REWRITE SUBSETP-TRANS2))
 (635 635 (:REWRITE SUBSETP-TRANS))
 (542 17 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (395 40 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (330 20 (:DEFINITION TRUE-LISTP))
 (285 285 (:REWRITE SUBSETP-MEMBER . 4))
 (280 45 (:DEFINITION STRING-LISTP))
 (210 210 (:TYPE-PRESCRIPTION STRING-LISTP))
 (177 18 (:REWRITE MEMBER-OF-REMOVE))
 (131 83 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (90 90 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (90 90 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (90 90 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (90 90 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (85 85 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (83 83 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (83 83 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (83 83 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (83 83 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (81 81 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 )
(CONSP-OF-ASSOC-EQUAL-OF-APPEND
 (198 99 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (101 32 (:REWRITE DEFAULT-CDR))
 (99 99 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (99 99 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (27 27 (:REWRITE CONSP-OF-APPEND))
 )
(CONSP-OF-ASSOC-OF-REMOVE
 (82 81 (:REWRITE DEFAULT-CAR))
 (44 43 (:REWRITE DEFAULT-CDR))
 (38 38 (:REWRITE SUBSETP-MEMBER . 4))
 (38 38 (:REWRITE SUBSETP-MEMBER . 3))
 (38 38 (:REWRITE SUBSETP-MEMBER . 2))
 (38 38 (:REWRITE SUBSETP-MEMBER . 1))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(STRIP-CARS-OF-APPEND
 (105 37 (:REWRITE DEFAULT-CAR))
 (51 19 (:REWRITE DEFAULT-CDR))
 (35 35 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (12 12 (:REWRITE CONSP-OF-APPEND))
 )
(REMOVE-OF-APPEND
 (657 9 (:REWRITE MEMBER-OF-BINARY-APPEND))
 (519 150 (:REWRITE SUBSETP-MEMBER . 3))
 (297 18 (:DEFINITION SUBSETP-EQUAL))
 (240 146 (:REWRITE DEFAULT-CDR))
 (218 160 (:REWRITE DEFAULT-CAR))
 (177 177 (:REWRITE SUBSETP-MEMBER . 2))
 (177 177 (:REWRITE SUBSETP-MEMBER . 1))
 (150 150 (:REWRITE SUBSETP-MEMBER . 4))
 (116 116 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (90 90 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (36 36 (:REWRITE SUBSETP-TRANS2))
 (36 36 (:REWRITE SUBSETP-TRANS))
 (24 24 (:REWRITE CONSP-OF-APPEND))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(REMOVE-OF-STRIP-CARS-OF-REMOVE
 (135 135 (:REWRITE SUBSETP-MEMBER . 4))
 (135 135 (:REWRITE SUBSETP-MEMBER . 3))
 (135 135 (:REWRITE SUBSETP-MEMBER . 2))
 (135 135 (:REWRITE SUBSETP-MEMBER . 1))
 (129 121 (:REWRITE DEFAULT-CDR))
 (23 23 (:REWRITE MEMBER-OF-STRIP-CARS))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(ASSOC-OF-APPEND-1
 (138 69 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (78 30 (:REWRITE DEFAULT-CDR))
 (69 69 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (69 69 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (18 18 (:REWRITE CONSP-OF-APPEND))
 )
(ASSOC-OF-APPEND-2
 (106 53 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (53 53 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (53 53 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (35 16 (:REWRITE DEFAULT-CDR))
 (12 12 (:REWRITE CONSP-OF-APPEND))
 (4 4 (:REWRITE ASSOC-OF-APPEND-1))
 (3 3 (:REWRITE CONSP-OF-ASSOC-EQUAL-OF-APPEND))
 )
(LEMMA-1
 (5 5 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DEFAULT-CAR))
 )
(LEMMA-2
 (60 12 (:DEFINITION ASSOC-EQUAL))
 (45 45 (:REWRITE DEFAULT-CAR))
 (36 3 (:DEFINITION PUT-ASSOC-EQUAL))
 (22 22 (:REWRITE DEFAULT-CDR))
 )
(PUT-ASSOC-EQUAL-MATCH
 (606 528 (:REWRITE DEFAULT-CDR))
 (355 31 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (216 27 (:DEFINITION MEMBER-EQUAL))
 (135 135 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (54 54 (:REWRITE SUBSETP-MEMBER . 2))
 (54 54 (:REWRITE SUBSETP-MEMBER . 1))
 )
(ASSOC-OF-REMOVE
 (238 204 (:TYPE-PRESCRIPTION CONSP-OF-ASSOC-OF-REMOVE))
 (111 108 (:REWRITE DEFAULT-CAR))
 (55 54 (:REWRITE DEFAULT-CDR))
 (43 43 (:REWRITE SUBSETP-MEMBER . 4))
 (43 43 (:REWRITE SUBSETP-MEMBER . 3))
 (43 43 (:REWRITE SUBSETP-MEMBER . 2))
 (43 43 (:REWRITE SUBSETP-MEMBER . 1))
 (34 34 (:TYPE-PRESCRIPTION NULL))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(MEMBER-OF-CAR-OF-NTH-IN-STRIP-CARS
 (204 199 (:REWRITE DEFAULT-CDR))
 (178 102 (:REWRITE DEFAULT-+-2))
 (160 97 (:REWRITE SUBSETP-MEMBER . 1))
 (153 104 (:REWRITE DEFAULT-<-2))
 (116 104 (:REWRITE DEFAULT-<-1))
 (102 102 (:REWRITE DEFAULT-+-1))
 (97 97 (:REWRITE SUBSETP-MEMBER . 2))
 (83 83 (:REWRITE SUBSETP-MEMBER . 4))
 (83 83 (:REWRITE SUBSETP-MEMBER . 3))
 (59 12 (:DEFINITION ASSOC-EQUAL))
 (58 2 (:DEFINITION SUBSETP-EQUAL))
 (27 27 (:REWRITE ZP-OPEN))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (12 2 (:DEFINITION ALISTP))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )
(ASSOC-OF-CAR-OF-NTH
 (1364 1349 (:REWRITE DEFAULT-CAR))
 (992 962 (:REWRITE DEFAULT-CDR))
 (470 270 (:REWRITE SUBSETP-MEMBER . 1))
 (415 313 (:REWRITE DEFAULT-+-2))
 (313 313 (:REWRITE DEFAULT-+-1))
 (299 23 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (270 270 (:REWRITE SUBSETP-MEMBER . 2))
 (220 220 (:REWRITE SUBSETP-MEMBER . 4))
 (220 220 (:REWRITE SUBSETP-MEMBER . 3))
 (220 184 (:REWRITE DEFAULT-<-2))
 (202 184 (:REWRITE DEFAULT-<-1))
 (180 8 (:DEFINITION SUBSETP-EQUAL))
 (52 52 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (40 40 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (16 16 (:REWRITE SUBSETP-TRANS2))
 (16 16 (:REWRITE SUBSETP-TRANS))
 )
(CONSP-OF-NTH-WHEN-ALISTP
 (19 12 (:REWRITE DEFAULT-<-2))
 (18 11 (:REWRITE DEFAULT-+-2))
 (16 16 (:REWRITE DEFAULT-CAR))
 (12 12 (:REWRITE DEFAULT-<-1))
 (11 11 (:REWRITE DEFAULT-+-1))
 (9 9 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE ZP-OPEN))
 )
(MEMBER-EQUAL-OF-STRIP-CARS-OF-PUT-ASSOC
 (2028 78 (:DEFINITION SUBSETP-EQUAL))
 (1141 175 (:REWRITE SUBSETP-MEMBER . 1))
 (746 617 (:REWRITE DEFAULT-CAR))
 (400 81 (:DEFINITION ASSOC-EQUAL))
 (360 312 (:REWRITE DEFAULT-CDR))
 (208 3 (:REWRITE SUBSETP-APPEND1))
 (196 31 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (195 153 (:REWRITE SUBSETP-TRANS2))
 (189 175 (:REWRITE SUBSETP-MEMBER . 2))
 (152 152 (:REWRITE SUBSETP-TRANS))
 (83 8 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (82 82 (:REWRITE SUBSETP-MEMBER . 4))
 (42 26 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (30 6 (:DEFINITION BINARY-APPEND))
 (26 26 (:TYPE-PRESCRIPTION BINARY-APPEND))
 )
(NO-DUPLICATESP-OF-STRIP-CARS-OF-PUT-ASSOC
 (697 652 (:REWRITE DEFAULT-CAR))
 (496 446 (:REWRITE DEFAULT-CDR))
 (383 78 (:DEFINITION ASSOC-EQUAL))
 (290 152 (:REWRITE SUBSETP-MEMBER . 3))
 (214 17 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (185 185 (:REWRITE SUBSETP-MEMBER . 2))
 (173 23 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (152 152 (:REWRITE SUBSETP-MEMBER . 4))
 (113 6 (:DEFINITION SUBSETP-EQUAL))
 (100 20 (:DEFINITION BINARY-APPEND))
 (61 1 (:REWRITE SUBSETP-APPEND1))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (28 28 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (23 11 (:REWRITE SUBSETP-TRANS2))
 (11 11 (:REWRITE SUBSETP-TRANS))
 )
(NTH-WHEN->=-N-LEN-L
 (37 21 (:REWRITE DEFAULT-+-2))
 (21 21 (:REWRITE DEFAULT-+-1))
 (20 15 (:REWRITE DEFAULT-<-2))
 (17 15 (:REWRITE DEFAULT-<-1))
 (14 14 (:REWRITE DEFAULT-CDR))
 (9 9 (:REWRITE DEFAULT-CAR))
 (5 5 (:REWRITE ZP-OPEN))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(STRIP-CARS-OF-REMOVE1-ASSOC
 (53 50 (:REWRITE DEFAULT-CAR))
 (24 22 (:REWRITE DEFAULT-CDR))
 )
(INTERSECTP-EQUAL-OF-STRIP-CARS-OF-REMOVE-EQUAL
 (67047 695 (:DEFINITION SUBSETP-EQUAL))
 (39337 305 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (10979 8337 (:REWRITE SUBSETP-MEMBER . 1))
 (10522 10249 (:REWRITE DEFAULT-CAR))
 (10496 6539 (:REWRITE SUBSETP-MEMBER . 3))
 (8440 8206 (:REWRITE DEFAULT-CDR))
 (8337 8337 (:REWRITE SUBSETP-MEMBER . 2))
 (6539 6539 (:REWRITE SUBSETP-MEMBER . 4))
 (3902 242 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1625 273 (:DEFINITION ASSOC-EQUAL))
 (1557 1557 (:REWRITE SUBSETP-TRANS2))
 (1557 1557 (:REWRITE SUBSETP-TRANS))
 (1316 305 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (1155 129 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (769 129 (:DEFINITION STRING-LISTP))
 (713 305 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (705 65 (:DEFINITION TRUE-LISTP))
 (641 641 (:TYPE-PRESCRIPTION STRING-LISTP))
 (354 354 (:REWRITE REMOVE-OF-STRIP-CARS-OF-REMOVE))
 (305 305 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (305 305 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (305 305 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (305 305 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (305 305 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (305 305 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (305 305 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (305 305 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (130 130 (:REWRITE ASSOC-OF-REMOVE))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 )
(INTERSECTP-OF-REMOVE
 (24 2 (:DEFINITION SUBSETP-EQUAL))
 (19 3 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (19 3 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 2 (:DEFINITION MEMBER-EQUAL))
 (3 3 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (3 3 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (3 3 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (3 3 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (3 3 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (3 3 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (3 3 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(REMOVE-OF-REMOVE
 (450 25 (:REWRITE MEMBER-OF-REMOVE))
 (258 258 (:REWRITE SUBSETP-MEMBER . 4))
 (258 258 (:REWRITE SUBSETP-MEMBER . 3))
 (258 258 (:REWRITE SUBSETP-MEMBER . 2))
 (258 258 (:REWRITE SUBSETP-MEMBER . 1))
 (247 239 (:REWRITE DEFAULT-CAR))
 (229 223 (:REWRITE DEFAULT-CDR))
 (7 2 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(REMOVE1-ASSOC-OF-APPEND
 (1200 1200 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (600 355 (:REWRITE DEFAULT-CDR))
 (557 61 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (441 31 (:DEFINITION TRUE-LISTP))
 (377 63 (:DEFINITION STRING-LISTP))
 (305 305 (:TYPE-PRESCRIPTION STRING-LISTP))
 (68 68 (:REWRITE CONSP-OF-APPEND))
 )
(REMOVE1-ASSOC-WHEN-ABSENT
 (485 53 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (385 27 (:DEFINITION TRUE-LISTP))
 (329 55 (:DEFINITION STRING-LISTP))
 (265 265 (:TYPE-PRESCRIPTION STRING-LISTP))
 (228 228 (:REWRITE DEFAULT-CAR))
 (176 176 (:REWRITE DEFAULT-CDR))
 (78 6 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (48 6 (:DEFINITION MEMBER-EQUAL))
 (30 30 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (12 12 (:REWRITE SUBSETP-MEMBER . 2))
 (12 12 (:REWRITE SUBSETP-MEMBER . 1))
 )
(PUT-ASSOC-OF-PUT-ASSOC-1
 (160 24 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (128 103 (:REWRITE DEFAULT-CAR))
 (114 19 (:DEFINITION ASSOC-EQUAL))
 (61 46 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE ASSOC-AFTER-PUT-ASSOC))
 )
(PUT-ASSOC-OF-PUT-ASSOC-2
 (1816 213 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (1499 1204 (:REWRITE DEFAULT-CAR))
 (702 558 (:REWRITE DEFAULT-CDR))
 (344 79 (:REWRITE ASSOC-AFTER-PUT-ASSOC))
 (130 10 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (84 9 (:DEFINITION MEMBER-EQUAL))
 (45 45 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (18 18 (:REWRITE SUBSETP-MEMBER . 2))
 (18 18 (:REWRITE SUBSETP-MEMBER . 1))
 )
(PUT-ASSOC-OF-APPEND
 (387 39 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (250 120 (:REWRITE DEFAULT-CDR))
 (104 14 (:REWRITE ASSOC-OF-APPEND-1))
 (24 24 (:REWRITE CONSP-OF-APPEND))
 )
(PUT-ASSOC-OF-REMOVE
 (348 44 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (254 221 (:REWRITE DEFAULT-CDR))
 (237 46 (:DEFINITION ASSOC-EQUAL))
 (152 152 (:REWRITE SUBSETP-MEMBER . 2))
 (152 152 (:REWRITE SUBSETP-MEMBER . 1))
 (146 146 (:REWRITE SUBSETP-MEMBER . 4))
 (146 146 (:REWRITE SUBSETP-MEMBER . 3))
 (84 14 (:REWRITE ASSOC-OF-REMOVE))
 (41 4 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (13 13 (:TYPE-PRESCRIPTION CONSP-OF-ASSOC-OF-REMOVE))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(MEMBER-OF-PUT-ASSOC
 (3295 104 (:DEFINITION SUBSETP-EQUAL))
 (2050 302 (:REWRITE SUBSETP-MEMBER . 1))
 (1830 62 (:REWRITE SUBSETP-MEMBER . 3))
 (732 86 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (567 471 (:REWRITE DEFAULT-CDR))
 (472 472 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (388 77 (:DEFINITION ASSOC-EQUAL))
 (302 302 (:REWRITE SUBSETP-MEMBER . 2))
 (258 22 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (208 208 (:REWRITE SUBSETP-TRANS2))
 (208 208 (:REWRITE SUBSETP-TRANS))
 (62 62 (:REWRITE SUBSETP-MEMBER . 4))
 )
(CONSP-OF-REMOVE-ASSOC-1
 (207 17 (:REWRITE REMOVE-ASSOC-WHEN-ABSENT-1))
 (117 117 (:REWRITE DEFAULT-CAR))
 (91 7 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (56 7 (:DEFINITION MEMBER-EQUAL))
 (42 42 (:REWRITE DEFAULT-CDR))
 (35 35 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (14 14 (:REWRITE SUBSETP-MEMBER . 2))
 (14 14 (:REWRITE SUBSETP-MEMBER . 1))
 )
(ASSOC-OF-TRUE-LIST-FIX
 (192 7 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (136 15 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (109 8 (:DEFINITION TRUE-LISTP))
 (93 16 (:DEFINITION STRING-LISTP))
 (73 73 (:TYPE-PRESCRIPTION STRING-LISTP))
 (55 52 (:REWRITE DEFAULT-CAR))
 (33 33 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (33 32 (:REWRITE DEFAULT-CDR))
 )
(STRIP-CARS-OF-TRUE-LIST-FIX
 (166 6 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (118 13 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (95 7 (:DEFINITION TRUE-LISTP))
 (81 14 (:DEFINITION STRING-LISTP))
 (63 63 (:TYPE-PRESCRIPTION STRING-LISTP))
 (32 31 (:REWRITE DEFAULT-CAR))
 (30 29 (:REWRITE DEFAULT-CDR))
 (28 28 (:TYPE-PRESCRIPTION TRUE-LISTP))
 )
(REMOVE-ASSOC-OF-TRUE-LIST-FIX
 (229 9 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (200 194 (:REWRITE DEFAULT-CAR))
 (172 14 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (164 18 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (134 10 (:DEFINITION TRUE-LISTP))
 (114 20 (:DEFINITION STRING-LISTP))
 (107 104 (:REWRITE DEFAULT-CDR))
 (106 13 (:DEFINITION MEMBER-EQUAL))
 (86 86 (:TYPE-PRESCRIPTION STRING-LISTP))
 (65 65 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (42 7 (:REWRITE ASSOC-OF-TRUE-LIST-FIX))
 (36 36 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (26 26 (:REWRITE SUBSETP-MEMBER . 2))
 (26 26 (:REWRITE SUBSETP-MEMBER . 1))
 )
(PUT-ASSOC-EQUAL-OF-TRUE-LIST-FIX
 (417 39 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (372 20 (:DEFINITION TRUE-LISTP))
 (304 41 (:DEFINITION STRING-LISTP))
 (191 191 (:TYPE-PRESCRIPTION STRING-LISTP))
 (160 142 (:REWRITE DEFAULT-CAR))
 (129 19 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (122 101 (:REWRITE DEFAULT-CDR))
 (105 21 (:DEFINITION ASSOC-EQUAL))
 (87 87 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (36 6 (:REWRITE ASSOC-OF-TRUE-LIST-FIX))
 )
(LEN-WHEN-CONSP
 (9 5 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE DEFAULT-CDR))
 (2 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(SUBSETP-OF-STRIP-CARS-OF-PUT-ASSOC
 (837 49 (:REWRITE MEMBER-OF-STRIP-CARS))
 (574 38 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (454 392 (:REWRITE DEFAULT-CAR))
 (361 138 (:REWRITE SUBSETP-TRANS))
 (290 158 (:REWRITE SUBSETP-MEMBER . 1))
 (285 58 (:DEFINITION ASSOC-EQUAL))
 (245 222 (:REWRITE DEFAULT-CDR))
 (66 11 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (59 59 (:REWRITE SUBSETP-MEMBER . 4))
 (59 59 (:REWRITE SUBSETP-MEMBER . 3))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (10 5 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (10 2 (:DEFINITION BINARY-APPEND))
 (5 5 (:TYPE-PRESCRIPTION BINARY-APPEND))
 )
(POSITION-EQUAL-AC-OF-NTHCDR
 (1244 688 (:TYPE-PRESCRIPTION NATP-POSITION-EQUAL-AC))
 (710 74 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (642 321 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (586 38 (:DEFINITION TRUE-LISTP))
 (538 8 (:DEFINITION SUBSETP-EQUAL))
 (535 535 (:TYPE-PRESCRIPTION NATP))
 (498 82 (:DEFINITION STRING-LISTP))
 (479 479 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (423 79 (:DEFINITION LEN))
 (411 39 (:REWRITE TAKE-OF-LEN-FREE))
 (378 378 (:TYPE-PRESCRIPTION STRING-LISTP))
 (312 41 (:REWRITE SUBSETP-MEMBER . 1))
 (234 18 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (216 13 (:REWRITE CONSP-OF-NTHCDR))
 (146 4 (:REWRITE CAR-OF-NTHCDR))
 (136 117 (:REWRITE DEFAULT-<-2))
 (120 8 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (117 117 (:REWRITE DEFAULT-<-1))
 (107 47 (:REWRITE ZP-OPEN))
 (106 41 (:REWRITE CONSP-OF-TAKE))
 (90 4 (:DEFINITION NTH))
 (70 29 (:REWRITE FOLD-CONSTS-IN-+))
 (59 59 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (41 41 (:REWRITE SUBSETP-MEMBER . 2))
 (28 28 (:REWRITE SUBSETP-MEMBER . 4))
 (16 16 (:REWRITE SUBSETP-TRANS2))
 (16 16 (:REWRITE SUBSETP-TRANS))
 (10 10 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(POSITION-EQUAL-AC-OF-+
 (678 339 (:TYPE-PRESCRIPTION NATP-POSITION-EQUAL-AC))
 (339 339 (:TYPE-PRESCRIPTION NATP))
 (174 34 (:REWRITE DEFAULT-+-2))
 (105 45 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (70 3 (:DEFINITION SUBSETP-EQUAL))
 (69 16 (:REWRITE SUBSETP-MEMBER . 3))
 (45 23 (:REWRITE SUBSETP-MEMBER . 1))
 (36 36 (:REWRITE DEFAULT-CAR))
 (28 28 (:REWRITE DEFAULT-CDR))
 (23 23 (:REWRITE SUBSETP-MEMBER . 2))
 (16 16 (:REWRITE SUBSETP-MEMBER . 4))
 (13 11 (:REWRITE FOLD-CONSTS-IN-+))
 (12 12 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (6 6 (:REWRITE SUBSETP-TRANS2))
 (6 6 (:REWRITE SUBSETP-TRANS))
 )
(POSITION-EQUAL-AC-WHEN-MEMBER
 (204 102 (:TYPE-PRESCRIPTION NATP-POSITION-EQUAL-AC))
 (66 13 (:REWRITE SUBSETP-MEMBER . 3))
 (50 2 (:DEFINITION SUBSETP-EQUAL))
 (48 20 (:REWRITE DEFAULT-<-1))
 (47 27 (:REWRITE DEFAULT-+-2))
 (30 20 (:REWRITE DEFAULT-<-2))
 (27 27 (:REWRITE DEFAULT-+-1))
 (25 25 (:REWRITE DEFAULT-CAR))
 (21 21 (:REWRITE DEFAULT-CDR))
 (18 18 (:REWRITE SUBSETP-MEMBER . 2))
 (18 18 (:REWRITE SUBSETP-MEMBER . 1))
 (16 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (13 13 (:REWRITE SUBSETP-MEMBER . 4))
 (7 7 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (7 7 (:REWRITE FOLD-CONSTS-IN-+))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 (4 2 (:TYPE-PRESCRIPTION POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(NTH-OF-POSITION-EQUAL-AC
 (339 105 (:REWRITE DEFAULT-+-2))
 (258 129 (:TYPE-PRESCRIPTION NATP-POSITION-EQUAL-AC))
 (165 41 (:REWRITE SUBSETP-MEMBER . 1))
 (154 105 (:REWRITE DEFAULT-+-1))
 (150 10 (:DEFINITION SUBSETP-EQUAL))
 (139 49 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (113 17 (:DEFINITION NFIX))
 (102 102 (:REWRITE DEFAULT-CDR))
 (90 57 (:REWRITE DEFAULT-<-1))
 (83 83 (:REWRITE DEFAULT-CAR))
 (80 57 (:REWRITE DEFAULT-<-2))
 (79 26 (:REWRITE SUBSETP-MEMBER . 3))
 (47 47 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (41 41 (:REWRITE SUBSETP-MEMBER . 2))
 (31 25 (:REWRITE FOLD-CONSTS-IN-+))
 (30 10 (:DEFINITION NATP))
 (26 26 (:REWRITE SUBSETP-MEMBER . 4))
 (20 20 (:REWRITE SUBSETP-TRANS2))
 (20 20 (:REWRITE SUBSETP-TRANS))
 )
(POSITION-EQUAL-AC-OF-NTH
 (469 28 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (348 174 (:TYPE-PRESCRIPTION NATP-POSITION-EQUAL-AC))
 (232 136 (:REWRITE DEFAULT-+-2))
 (216 216 (:REWRITE DEFAULT-CDR))
 (212 80 (:REWRITE SUBSETP-MEMBER . 3))
 (178 178 (:TYPE-PRESCRIPTION NATP))
 (144 144 (:REWRITE DEFAULT-CAR))
 (103 78 (:REWRITE DEFAULT-<-2))
 (100 8 (:DEFINITION SUBSETP-EQUAL))
 (96 96 (:REWRITE SUBSETP-MEMBER . 2))
 (96 96 (:REWRITE SUBSETP-MEMBER . 1))
 (80 80 (:REWRITE SUBSETP-MEMBER . 4))
 (78 78 (:REWRITE DEFAULT-<-1))
 (56 56 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (40 40 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (16 16 (:REWRITE SUBSETP-TRANS2))
 (16 16 (:REWRITE SUBSETP-TRANS))
 (12 4 (:DEFINITION NATP))
 )
(POSITION-EQUAL-AC-OF-TAKE
 (1458 729 (:TYPE-PRESCRIPTION NATP-POSITION-EQUAL-AC))
 (746 43 (:REWRITE SUBSETP-MEMBER . 3))
 (460 269 (:REWRITE DEFAULT-CDR))
 (257 253 (:REWRITE DEFAULT-+-1))
 (134 121 (:REWRITE DEFAULT-<-1))
 (133 133 (:REWRITE SUBSETP-MEMBER . 2))
 (129 43 (:REWRITE FOLD-CONSTS-IN-+))
 (121 121 (:REWRITE DEFAULT-<-2))
 (100 100 (:REWRITE SUBSETP-TRANS2))
 (100 100 (:REWRITE SUBSETP-TRANS))
 (44 35 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (43 43 (:REWRITE SUBSETP-MEMBER . 4))
 (12 4 (:DEFINITION NATP))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(POSITION-EQUAL-AC-WHEN-MEMBER-OF-TAKE
 (1582 817 (:TYPE-PRESCRIPTION NATP-POSITION-EQUAL-AC))
 (991 64 (:REWRITE TAKE-OF-LEN-FREE))
 (777 777 (:TYPE-PRESCRIPTION NATP))
 (530 219 (:REWRITE CONSP-OF-TAKE))
 (515 38 (:REWRITE SUBSETP-MEMBER . 3))
 (476 270 (:REWRITE DEFAULT-CDR))
 (466 190 (:REWRITE DEFAULT-+-2))
 (342 60 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (226 226 (:REWRITE SUBSETP-MEMBER . 2))
 (224 143 (:REWRITE ZP-OPEN))
 (166 166 (:REWRITE SUBSETP-TRANS2))
 (166 166 (:REWRITE SUBSETP-TRANS))
 (105 94 (:REWRITE DEFAULT-<-1))
 (38 38 (:REWRITE SUBSETP-MEMBER . 4))
 (36 12 (:DEFINITION NATP))
 )
(POSITION-OF-NTHCDR
 (471 44 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (457 10 (:DEFINITION SUBSETP-EQUAL))
 (380 10 (:REWRITE TAKE-OF-LEN-FREE))
 (280 12 (:REWRITE SUBSETP-MEMBER . 3))
 (258 4 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (245 25 (:REWRITE SUBSETP-MEMBER . 1))
 (204 39 (:DEFINITION POSITION-EQUAL-AC))
 (160 32 (:DEFINITION LEN))
 (155 155 (:TYPE-PRESCRIPTION LEN))
 (154 100 (:REWRITE DEFAULT-+-2))
 (113 101 (:REWRITE DEFAULT-CDR))
 (106 100 (:REWRITE DEFAULT-+-1))
 (80 68 (:REWRITE DEFAULT-CAR))
 (54 6 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (52 26 (:TYPE-PRESCRIPTION NATP-POSITION-EQUAL-AC))
 (42 42 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (36 6 (:DEFINITION STRING-LISTP))
 (34 34 (:TYPE-PRESCRIPTION TAKE))
 (33 3 (:DEFINITION TRUE-LISTP))
 (30 30 (:TYPE-PRESCRIPTION STRING-LISTP))
 (26 12 (:REWRITE CONSP-OF-TAKE))
 (25 25 (:REWRITE SUBSETP-MEMBER . 2))
 (18 18 (:REWRITE SUBSETP-TRANS2))
 (18 18 (:REWRITE SUBSETP-TRANS))
 (18 14 (:REWRITE DEFAULT-<-2))
 (14 14 (:REWRITE DEFAULT-<-1))
 (12 12 (:REWRITE SUBSETP-MEMBER . 4))
 (12 12 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER-OF-TAKE))
 (9 9 (:REWRITE ZP-OPEN))
 (6 2 (:DEFINITION NATP))
 (4 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:TYPE-PRESCRIPTION ZP))
 )
(POSITION-WHEN-MEMBER
 (24 8 (:DEFINITION POSITION-EQUAL-AC))
 (15 3 (:DEFINITION LEN))
 (12 12 (:REWRITE DEFAULT-CDR))
 (10 5 (:REWRITE DEFAULT-+-2))
 (9 9 (:REWRITE DEFAULT-CAR))
 (8 4 (:TYPE-PRESCRIPTION POSITION-WHEN-MEMBER))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (5 5 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE SUBSETP-MEMBER . 4))
 (4 4 (:REWRITE SUBSETP-MEMBER . 3))
 (3 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 (2 2 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE DEFAULT-COERCE-1))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER-OF-TAKE))
 )
(NTH-OF-POSITION-EQUAL
 (158 2 (:DEFINITION NTH))
 (99 11 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (61 5 (:LINEAR POSITION-WHEN-MEMBER))
 (40 24 (:REWRITE DEFAULT-+-2))
 (38 7 (:REWRITE SUBSETP-MEMBER . 1))
 (32 32 (:REWRITE DEFAULT-CDR))
 (27 24 (:REWRITE DEFAULT-+-1))
 (25 2 (:DEFINITION SUBSETP-EQUAL))
 (23 4 (:DEFINITION NFIX))
 (22 22 (:REWRITE DEFAULT-CAR))
 (16 10 (:REWRITE DEFAULT-<-2))
 (16 2 (:REWRITE ZP-OPEN))
 (13 10 (:REWRITE DEFAULT-<-1))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (7 7 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:TYPE-PRESCRIPTION NATP-POSITION-AC))
 (5 5 (:REWRITE SUBSETP-MEMBER . 4))
 (5 5 (:REWRITE SUBSETP-MEMBER . 3))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 (3 3 (:REWRITE DEFAULT-COERCE-2))
 (3 3 (:REWRITE DEFAULT-COERCE-1))
 (3 3 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER-OF-TAKE))
 )
(POSITION-EQUAL-OF-NTH
 (164 82 (:TYPE-PRESCRIPTION POSITION-WHEN-MEMBER))
 (59 11 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (56 4 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (42 42 (:REWRITE DEFAULT-CAR))
 (37 37 (:REWRITE DEFAULT-CDR))
 (34 20 (:REWRITE DEFAULT-+-2))
 (30 30 (:REWRITE SUBSETP-MEMBER . 2))
 (30 30 (:REWRITE SUBSETP-MEMBER . 1))
 (28 24 (:REWRITE DEFAULT-<-2))
 (26 24 (:REWRITE DEFAULT-<-1))
 (20 20 (:REWRITE DEFAULT-+-1))
 (7 7 (:REWRITE DEFAULT-COERCE-2))
 (7 7 (:REWRITE DEFAULT-COERCE-1))
 (6 6 (:REWRITE SUBSETP-MEMBER . 4))
 (6 6 (:REWRITE SUBSETP-MEMBER . 3))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER-OF-TAKE))
 (1 1 (:REWRITE ZP-OPEN))
 )
(POSITION-OF-TAKE
 (423 39 (:REWRITE SUBSETP-MEMBER . 1))
 (354 12 (:DEFINITION SUBSETP-EQUAL))
 (330 14 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (94 42 (:REWRITE CONSP-OF-TAKE))
 (91 49 (:REWRITE DEFAULT-CDR))
 (85 43 (:REWRITE DEFAULT-CAR))
 (60 60 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (39 39 (:REWRITE SUBSETP-MEMBER . 2))
 (29 29 (:REWRITE ZP-OPEN))
 (24 24 (:REWRITE SUBSETP-TRANS2))
 (24 24 (:REWRITE SUBSETP-TRANS))
 (19 13 (:REWRITE DEFAULT-+-2))
 (13 13 (:REWRITE DEFAULT-+-1))
 (12 12 (:TYPE-PRESCRIPTION ZP))
 (12 10 (:REWRITE DEFAULT-<-1))
 (10 10 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE SUBSETP-MEMBER . 4))
 (9 9 (:REWRITE SUBSETP-MEMBER . 3))
 (4 4 (:REWRITE DEFAULT-COERCE-2))
 (4 4 (:REWRITE DEFAULT-COERCE-1))
 (1 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 )
(POSITION-WHEN-MEMBER-OF-TAKE
 (172 14 (:LINEAR POSITION-WHEN-MEMBER))
 (110 55 (:TYPE-PRESCRIPTION POSITION-WHEN-MEMBER))
 (87 48 (:REWRITE DEFAULT-CDR))
 (83 38 (:REWRITE DEFAULT-CAR))
 (41 41 (:REWRITE SUBSETP-MEMBER . 2))
 (39 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (37 22 (:REWRITE DEFAULT-+-2))
 (30 30 (:REWRITE ZP-OPEN))
 (26 26 (:REWRITE SUBSETP-TRANS2))
 (26 26 (:REWRITE SUBSETP-TRANS))
 (22 22 (:REWRITE DEFAULT-+-1))
 (17 14 (:REWRITE DEFAULT-<-1))
 (15 15 (:TYPE-PRESCRIPTION ZP))
 (11 11 (:REWRITE SUBSETP-MEMBER . 4))
 (11 11 (:REWRITE SUBSETP-MEMBER . 3))
 (2 2 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE DEFAULT-COERCE-1))
 (1 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 )
(SUBSETP-OF-NTHCDR
 (1523 51 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (1298 130 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1101 162 (:REWRITE SUBSETP-TRANS))
 (1098 66 (:DEFINITION TRUE-LISTP))
 (930 150 (:DEFINITION STRING-LISTP))
 (740 427 (:REWRITE DEFAULT-CAR))
 (694 126 (:DEFINITION LEN))
 (682 682 (:TYPE-PRESCRIPTION STRING-LISTP))
 (528 25 (:REWRITE CONSP-OF-NTHCDR))
 (506 162 (:REWRITE SUBSETP-TRANS2))
 (466 74 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (398 265 (:REWRITE DEFAULT-+-2))
 (391 62 (:LINEAR POSITION-WHEN-MEMBER))
 (347 224 (:REWRITE SUBSETP-MEMBER . 1))
 (330 39 (:DEFINITION POSITION-EQUAL-AC))
 (265 265 (:REWRITE DEFAULT-+-1))
 (230 195 (:REWRITE DEFAULT-<-2))
 (197 62 (:TYPE-PRESCRIPTION POSITION-EQUAL-AC-WHEN-MEMBER))
 (195 195 (:REWRITE DEFAULT-<-1))
 (147 9 (:DEFINITION POSITION-EQUAL))
 (139 104 (:REWRITE SUBSETP-MEMBER . 4))
 (127 3 (:REWRITE CAR-OF-NTHCDR))
 (104 104 (:REWRITE SUBSETP-MEMBER . 3))
 (102 6 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (88 88 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (88 88 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (88 88 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (88 88 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (79 3 (:DEFINITION NTH))
 (41 3 (:REWRITE MEMBER-EQUAL-NTH))
 (21 21 (:DEFINITION FIX))
 (17 17 (:TYPE-PRESCRIPTION NATP-POSITION-AC))
 (12 4 (:TYPE-PRESCRIPTION POSITION-WHEN-MEMBER))
 (9 9 (:REWRITE DEFAULT-COERCE-2))
 (9 9 (:REWRITE DEFAULT-COERCE-1))
 (7 7 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER-OF-TAKE))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(NO-DUPLICATESP-EQUAL-OF-NTHCDR
 (390 15 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (381 158 (:REWRITE DEFAULT-CDR))
 (275 31 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (219 17 (:DEFINITION TRUE-LISTP))
 (187 33 (:DEFINITION STRING-LISTP))
 (181 67 (:REWRITE DEFAULT-CAR))
 (147 147 (:TYPE-PRESCRIPTION STRING-LISTP))
 (127 3 (:REWRITE CAR-OF-NTHCDR))
 (102 6 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (95 58 (:REWRITE DEFAULT-+-2))
 (89 74 (:REWRITE DEFAULT-<-2))
 (79 3 (:DEFINITION NTH))
 (74 74 (:REWRITE DEFAULT-<-1))
 (65 32 (:REWRITE SUBSETP-MEMBER . 3))
 (58 58 (:REWRITE DEFAULT-+-1))
 (34 34 (:REWRITE SUBSETP-MEMBER . 2))
 (34 34 (:REWRITE SUBSETP-MEMBER . 1))
 (32 32 (:REWRITE SUBSETP-MEMBER . 4))
 (25 2 (:DEFINITION SUBSETP-EQUAL))
 (24 12 (:REWRITE ZP-OPEN))
 (22 22 (:LINEAR POSITION-WHEN-MEMBER))
 (22 22 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (10 4 (:REWRITE FOLD-CONSTS-IN-+))
 (6 6 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )
(REMOVE-ASSOC-OF-APPEND
 (490 375 (:REWRITE DEFAULT-CAR))
 (309 21 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (252 158 (:REWRITE DEFAULT-CDR))
 (208 20 (:DEFINITION MEMBER-EQUAL))
 (201 9 (:REWRITE ASSOC-OF-APPEND-1))
 (126 126 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (100 100 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (40 40 (:REWRITE SUBSETP-MEMBER . 2))
 (40 40 (:REWRITE SUBSETP-MEMBER . 1))
 (24 24 (:REWRITE CONSP-OF-APPEND))
 (23 5 (:REWRITE CONSP-OF-REMOVE-ASSOC-1))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(NAT-LISTP-OF-TAKE
 (193 21 (:REWRITE TAKE-OF-LEN-FREE))
 (73 56 (:REWRITE DEFAULT-<-1))
 (64 38 (:REWRITE DEFAULT-+-2))
 (57 37 (:REWRITE DEFAULT-CDR))
 (56 56 (:REWRITE DEFAULT-<-2))
 (51 30 (:REWRITE DEFAULT-CAR))
 (38 38 (:REWRITE DEFAULT-+-1))
 (29 18 (:REWRITE CONSP-OF-TAKE))
 (21 21 (:LINEAR POSITION-WHEN-MEMBER))
 (21 21 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (21 12 (:REWRITE ZP-OPEN))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(ASSOC-WHEN-ZP-LEN
 (9 9 (:REWRITE DEFAULT-CAR))
 (6 6 (:REWRITE DEFAULT-CDR))
 (6 3 (:REWRITE DEFAULT-+-2))
 (4 4 (:LINEAR POSITION-WHEN-MEMBER))
 (4 4 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(MEMBER-OF-TAKE
 (6328 386 (:REWRITE SUBSETP-MEMBER . 1))
 (4871 177 (:REWRITE TAKE-OF-LEN-FREE))
 (2154 1514 (:REWRITE DEFAULT-CDR))
 (1777 999 (:REWRITE DEFAULT-+-2))
 (1241 811 (:REWRITE DEFAULT-CAR))
 (1082 999 (:REWRITE DEFAULT-+-1))
 (949 405 (:REWRITE CONSP-OF-TAKE))
 (912 17 (:REWRITE CAR-OF-NTHCDR))
 (846 26 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (813 50 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (768 68 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (600 94 (:DEFINITION STRING-LISTP))
 (546 33 (:DEFINITION NTH))
 (462 28 (:REWRITE CONSP-OF-NTHCDR))
 (458 402 (:REWRITE DEFAULT-<-2))
 (386 386 (:REWRITE SUBSETP-MEMBER . 2))
 (370 370 (:TYPE-PRESCRIPTION STRING-LISTP))
 (299 299 (:REWRITE SUBSETP-TRANS2))
 (299 299 (:REWRITE SUBSETP-TRANS))
 (84 1 (:REWRITE POSITION-EQUAL-AC-OF-NTHCDR))
 (77 77 (:REWRITE SUBSETP-MEMBER . 4))
 (31 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(POSITION-OF-CDR
 (1351 30 (:DEFINITION SUBSETP-EQUAL))
 (1012 81 (:REWRITE SUBSETP-MEMBER . 1))
 (739 119 (:DEFINITION LEN))
 (648 31 (:REWRITE TAKE-OF-LEN-FREE))
 (501 26 (:REWRITE SUBSETP-MEMBER . 3))
 (474 374 (:REWRITE DEFAULT-CDR))
 (395 14 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (355 176 (:REWRITE DEFAULT-+-2))
 (267 5 (:REWRITE CAR-OF-NTHCDR))
 (248 23 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (240 14 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (207 168 (:REWRITE DEFAULT-CAR))
 (197 176 (:REWRITE DEFAULT-+-1))
 (193 30 (:DEFINITION STRING-LISTP))
 (150 9 (:DEFINITION NTH))
 (142 8 (:REWRITE CONSP-OF-NTHCDR))
 (129 129 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (119 119 (:TYPE-PRESCRIPTION STRING-LISTP))
 (103 103 (:TYPE-PRESCRIPTION TAKE))
 (102 1 (:REWRITE POSITION-EQUAL-AC-OF-NTHCDR))
 (81 81 (:REWRITE SUBSETP-MEMBER . 2))
 (62 32 (:REWRITE DEFAULT-<-2))
 (59 59 (:REWRITE SUBSETP-TRANS2))
 (59 59 (:REWRITE SUBSETP-TRANS))
 (39 39 (:REWRITE CONSP-OF-TAKE))
 (32 32 (:REWRITE DEFAULT-<-1))
 (26 26 (:REWRITE SUBSETP-MEMBER . 4))
 (11 11 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER-OF-TAKE))
 (11 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(MEMBER-EQUAL-NTH-TAKE-WHEN-NO-DUPLICATESP
 (446 36 (:REWRITE TAKE-OF-LEN-FREE))
 (407 24 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (234 175 (:REWRITE DEFAULT-CDR))
 (211 136 (:REWRITE DEFAULT-+-2))
 (176 58 (:REWRITE CONSP-OF-TAKE))
 (164 105 (:REWRITE DEFAULT-CAR))
 (149 119 (:REWRITE DEFAULT-<-2))
 (136 136 (:REWRITE DEFAULT-+-1))
 (119 119 (:REWRITE DEFAULT-<-1))
 (77 77 (:REWRITE SUBSETP-MEMBER . 2))
 (77 77 (:REWRITE SUBSETP-MEMBER . 1))
 (66 66 (:LINEAR POSITION-WHEN-MEMBER))
 (66 66 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (51 51 (:REWRITE SUBSETP-MEMBER . 4))
 (35 35 (:REWRITE SUBSETP-TRANS2))
 (35 35 (:REWRITE SUBSETP-TRANS))
 (13 1 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(CONSP-OF-SET-DIFFERENCE$
 (331 79 (:REWRITE SUBSETP-TRANS2))
 (288 91 (:REWRITE SUBSETP-MEMBER . 1))
 (213 93 (:REWRITE SUBSETP-MEMBER . 2))
 (202 46 (:REWRITE SUBSETP-MEMBER . 3))
 (131 79 (:REWRITE SUBSETP-TRANS))
 (97 97 (:REWRITE DEFAULT-CAR))
 (81 81 (:REWRITE DEFAULT-CDR))
 (46 46 (:REWRITE SUBSETP-MEMBER . 4))
 (23 23 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (23 23 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (23 23 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (23 23 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 )
(MEMBER-OF-SET-DIFFERENCE-EQUAL
 (5773 227 (:DEFINITION SUBSETP-EQUAL))
 (3793 235 (:REWRITE SUBSETP-MEMBER . 3))
 (3355 628 (:REWRITE SUBSETP-MEMBER . 1))
 (1043 1043 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (767 743 (:REWRITE DEFAULT-CDR))
 (741 711 (:REWRITE DEFAULT-CAR))
 (628 628 (:REWRITE SUBSETP-MEMBER . 2))
 (449 449 (:REWRITE SUBSETP-TRANS2))
 (449 449 (:REWRITE SUBSETP-TRANS))
 (235 235 (:REWRITE SUBSETP-MEMBER . 4))
 )
(NO-DUPLICATESP-OF-SET-DIFFERENCE$
 (311 40 (:REWRITE SUBSETP-MEMBER . 3))
 (306 20 (:DEFINITION SUBSETP-EQUAL))
 (174 67 (:REWRITE SUBSETP-MEMBER . 1))
 (100 100 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (74 73 (:REWRITE DEFAULT-CAR))
 (73 71 (:REWRITE DEFAULT-CDR))
 (67 67 (:REWRITE SUBSETP-MEMBER . 2))
 (40 40 (:REWRITE SUBSETP-TRANS2))
 (40 40 (:REWRITE SUBSETP-TRANS))
 (40 40 (:REWRITE SUBSETP-MEMBER . 4))
 )
(LEMMA-1
 (166 6 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (118 13 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (95 7 (:DEFINITION TRUE-LISTP))
 (81 14 (:DEFINITION STRING-LISTP))
 (63 63 (:TYPE-PRESCRIPTION STRING-LISTP))
 (28 28 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (25 25 (:REWRITE DEFAULT-CDR))
 (23 23 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE SUBSETP-MEMBER . 4))
 (3 3 (:REWRITE SUBSETP-MEMBER . 3))
 (3 3 (:REWRITE SUBSETP-MEMBER . 2))
 (3 3 (:REWRITE SUBSETP-MEMBER . 1))
 )
(LEMMA-2
 (1323 12 (:REWRITE MEMBER-OF-SET-DIFFERENCE-EQUAL))
 (965 62 (:DEFINITION SUBSETP-EQUAL))
 (897 228 (:REWRITE SUBSETP-MEMBER . 1))
 (614 125 (:REWRITE SUBSETP-MEMBER . 3))
 (307 307 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (233 230 (:REWRITE DEFAULT-CAR))
 (228 228 (:REWRITE SUBSETP-MEMBER . 2))
 (212 209 (:REWRITE DEFAULT-CDR))
 (125 125 (:REWRITE SUBSETP-MEMBER . 4))
 (124 124 (:REWRITE SUBSETP-TRANS2))
 (124 124 (:REWRITE SUBSETP-TRANS))
 )
(SET-DIFFERENCE$-REDEFINITION)
(LEN-OF-REMOVE-WHEN-MEMBER-1
 (504 87 (:REWRITE SUBSETP-MEMBER . 1))
 (427 24 (:DEFINITION SUBSETP-EQUAL))
 (182 7 (:REWRITE LEN-OF-REMOVE-WHEN-NO-DUPLICATESP))
 (161 7 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (134 133 (:REWRITE DEFAULT-CDR))
 (128 128 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (116 48 (:REWRITE SUBSETP-MEMBER . 3))
 (107 107 (:REWRITE DEFAULT-CAR))
 (87 87 (:REWRITE SUBSETP-MEMBER . 2))
 (79 8 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (66 4 (:DEFINITION TRUE-LISTP))
 (56 9 (:DEFINITION STRING-LISTP))
 (56 1 (:REWRITE POSITION-OF-CDR))
 (52 31 (:REWRITE DEFAULT-+-2))
 (52 2 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (48 48 (:REWRITE SUBSETP-MEMBER . 4))
 (47 47 (:REWRITE SUBSETP-TRANS2))
 (47 47 (:REWRITE SUBSETP-TRANS))
 (42 42 (:TYPE-PRESCRIPTION STRING-LISTP))
 (35 35 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (31 31 (:REWRITE DEFAULT-+-1))
 (29 1 (:DEFINITION TRUE-LIST-FIX))
 (24 5 (:DEFINITION POSITION-EQUAL-AC))
 (18 9 (:REWRITE DEFAULT-<-1))
 (17 17 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 9 (:REWRITE DEFAULT-<-2))
 (3 3 (:DEFINITION FIX))
 (1 1 (:REWRITE DEFAULT-COERCE-2))
 (1 1 (:REWRITE DEFAULT-COERCE-1))
 (1 1 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER-OF-TAKE))
 )
(LEN-OF-SET-DIFFERENCE$-WHEN-SUBSETP
 (1562 21 (:REWRITE REMOVE-WHEN-ABSENT))
 (892 190 (:REWRITE SUBSETP-MEMBER . 1))
 (799 7 (:DEFINITION REMOVE-EQUAL))
 (638 81 (:REWRITE SUBSETP-MEMBER . 3))
 (260 10 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (245 193 (:REWRITE SUBSETP-MEMBER . 2))
 (228 228 (:REWRITE DEFAULT-CDR))
 (208 208 (:REWRITE DEFAULT-CAR))
 (205 136 (:REWRITE SUBSETP-TRANS2))
 (202 136 (:REWRITE SUBSETP-TRANS))
 (180 20 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (145 5 (:DEFINITION TRUE-LIST-FIX))
 (140 10 (:DEFINITION TRUE-LISTP))
 (120 20 (:DEFINITION STRING-LISTP))
 (112 2 (:REWRITE LEN-OF-REMOVE-WHEN-NO-DUPLICATESP))
 (100 100 (:TYPE-PRESCRIPTION STRING-LISTP))
 (81 81 (:REWRITE SUBSETP-MEMBER . 4))
 (52 2 (:REWRITE NO-DUPLICATESP-OF-SET-DIFFERENCE$))
 (50 50 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (50 50 (:TYPE-PRESCRIPTION SET-DIFFERENCE-EQUAL))
 (47 23 (:REWRITE DEFAULT-+-2))
 (28 23 (:REWRITE DEFAULT-+-1))
 (14 5 (:REWRITE DEFAULT-<-2))
 (12 12 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (10 5 (:REWRITE DEFAULT-<-1))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (6 2 (:DEFINITION POSITION-EQUAL-AC))
 (4 4 (:TYPE-PRESCRIPTION REMOVE-EQUAL))
 (4 4 (:DEFINITION ATOM))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE DEFAULT-COERCE-2))
 (1 1 (:REWRITE DEFAULT-COERCE-1))
 )
(MEMBER-OF-REMOVE-DUPLICATES
 (2473 500 (:REWRITE SUBSETP-MEMBER . 1))
 (603 575 (:REWRITE DEFAULT-CAR))
 (589 573 (:REWRITE DEFAULT-CDR))
 (500 500 (:REWRITE SUBSETP-MEMBER . 2))
 (299 299 (:REWRITE SUBSETP-TRANS2))
 (299 299 (:REWRITE SUBSETP-TRANS))
 (221 221 (:REWRITE SUBSETP-MEMBER . 4))
 )
(NO-DUPLICATESP-OF-REMOVE-DUPLICATES
 (90 24 (:REWRITE SUBSETP-MEMBER . 3))
 (75 6 (:DEFINITION SUBSETP-EQUAL))
 (61 30 (:REWRITE SUBSETP-MEMBER . 1))
 (42 40 (:REWRITE DEFAULT-CDR))
 (37 36 (:REWRITE DEFAULT-CAR))
 (30 30 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (30 30 (:REWRITE SUBSETP-MEMBER . 2))
 (24 24 (:REWRITE SUBSETP-MEMBER . 4))
 (12 12 (:REWRITE SUBSETP-TRANS2))
 (12 12 (:REWRITE SUBSETP-TRANS))
 )
(LEN-OF-STRIP-CARS
 (14 14 (:LINEAR POSITION-WHEN-MEMBER))
 (14 14 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (14 7 (:REWRITE DEFAULT-+-2))
 (9 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE DEFAULT-CAR))
 )
(CONSP-OF-LAST)
(MEMBER-OF-CAR-OF-LAST
 (34 12 (:REWRITE SUBSETP-MEMBER . 1))
 (27 3 (:LINEAR NON-NEGATIVITY-OF-CAR-OF-LAST-WHEN-NAT-LISTP))
 (20 1 (:DEFINITION SUBSETP-EQUAL))
 (19 3 (:DEFINITION NAT-LISTP))
 (12 12 (:REWRITE SUBSETP-MEMBER . 2))
 (10 10 (:REWRITE SUBSETP-MEMBER . 4))
 (10 10 (:REWRITE SUBSETP-MEMBER . 3))
 (6 2 (:DEFINITION NATP))
 (5 5 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 )
(APPEND-OF-TAKE-AND-LAST
 (317 23 (:REWRITE TAKE-OF-LEN-FREE))
 (126 71 (:REWRITE DEFAULT-+-2))
 (124 21 (:REWRITE CONSP-OF-TAKE))
 (98 45 (:REWRITE DEFAULT-CAR))
 (71 71 (:REWRITE DEFAULT-+-1))
 (47 26 (:REWRITE DEFAULT-<-2))
 (32 32 (:LINEAR POSITION-WHEN-MEMBER))
 (32 32 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (26 26 (:REWRITE DEFAULT-<-1))
 )
(ATOM-OF-CDR-OF-LAST
 (21 13 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE CONSP-OF-LAST))
 )
(LAST-WHEN-EQUAL-LEN-1
 (81 72 (:REWRITE DEFAULT-CDR))
 (48 24 (:REWRITE DEFAULT-+-2))
 (24 24 (:REWRITE DEFAULT-+-1))
 (24 18 (:REWRITE DEFAULT-CAR))
 (20 20 (:LINEAR POSITION-WHEN-MEMBER))
 (20 20 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(LEN-OF-RESIZE-LIST
 (29 25 (:REWRITE DEFAULT-+-2))
 (25 25 (:REWRITE DEFAULT-+-1))
 (18 17 (:REWRITE DEFAULT-<-1))
 (17 17 (:REWRITE DEFAULT-<-2))
 (14 12 (:REWRITE DEFAULT-CDR))
 (13 13 (:LINEAR POSITION-WHEN-MEMBER))
 (13 13 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 6 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(RESIZE-LIST-OF-LEN-FREE
 (1158 43 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (809 89 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (637 45 (:DEFINITION TRUE-LISTP))
 (545 91 (:DEFINITION STRING-LISTP))
 (445 445 (:TYPE-PRESCRIPTION STRING-LISTP))
 (215 215 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (200 198 (:REWRITE DEFAULT-CDR))
 (127 125 (:REWRITE DEFAULT-CAR))
 (66 41 (:REWRITE DEFAULT-+-2))
 (41 41 (:REWRITE DEFAULT-+-1))
 (28 23 (:REWRITE DEFAULT-<-2))
 (26 23 (:REWRITE DEFAULT-<-1))
 (15 15 (:LINEAR POSITION-WHEN-MEMBER))
 (15 15 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (3 3 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(TRUE-LISTP-OF-PUT-ASSOC
 (513 171 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (313 27 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (237 31 (:DEFINITION STRING-LISTP))
 (147 14 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (139 139 (:TYPE-PRESCRIPTION STRING-LISTP))
 (124 118 (:REWRITE DEFAULT-CAR))
 (86 74 (:REWRITE DEFAULT-CDR))
 )
(ASSOC-AFTER-REMOVE1-ASSOC-WHEN-NO-DUPLICATESP
 (933 44 (:REWRITE REMOVE-WHEN-ABSENT))
 (757 64 (:DEFINITION MEMBER-EQUAL))
 (708 236 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (279 279 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (279 268 (:REWRITE DEFAULT-CAR))
 (188 8 (:REWRITE NO-DUPLICATESP-OF-REMOVE))
 (186 174 (:REWRITE DEFAULT-CDR))
 (128 128 (:REWRITE SUBSETP-MEMBER . 2))
 (128 128 (:REWRITE SUBSETP-MEMBER . 1))
 (122 122 (:REWRITE SUBSETP-MEMBER . 4))
 (122 122 (:REWRITE SUBSETP-MEMBER . 3))
 (75 5 (:REWRITE ASSOC-OF-REMOVE1-ASSOC))
 (41 5 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (7 7 (:REWRITE ASSOC-AFTER-REMOVE1-ASSOC))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(LAST-ALT
 (390 13 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (276 32 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (223 17 (:DEFINITION TRUE-LISTP))
 (191 34 (:DEFINITION STRING-LISTP))
 (142 142 (:TYPE-PRESCRIPTION STRING-LISTP))
 (82 7 (:REWRITE LAST-WHEN-EQUAL-LEN-1))
 (47 30 (:REWRITE DEFAULT-+-2))
 (44 2 (:REWRITE CONSP-OF-NTHCDR))
 (34 34 (:REWRITE DEFAULT-CAR))
 (30 30 (:REWRITE DEFAULT-+-1))
 (16 10 (:REWRITE DEFAULT-<-2))
 (14 10 (:REWRITE DEFAULT-<-1))
 (11 11 (:LINEAR POSITION-WHEN-MEMBER))
 (11 11 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (11 2 (:DEFINITION NFIX))
 )
(NAT-LISTP-WHEN-SUBSETP
 (166 6 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (118 13 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (95 7 (:DEFINITION TRUE-LISTP))
 (81 14 (:DEFINITION STRING-LISTP))
 (63 63 (:TYPE-PRESCRIPTION STRING-LISTP))
 (38 37 (:REWRITE DEFAULT-CDR))
 (34 33 (:REWRITE DEFAULT-CAR))
 (28 28 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (28 4 (:DEFINITION MEMBER-EQUAL))
 (8 8 (:REWRITE SUBSETP-MEMBER . 4))
 (8 8 (:REWRITE SUBSETP-MEMBER . 3))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (8 8 (:REWRITE DEFAULT-<-2))
 (8 8 (:REWRITE DEFAULT-<-1))
 (7 7 (:REWRITE SUBSETP-TRANS2))
 (7 7 (:REWRITE SUBSETP-TRANS))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 )
(REMOVE-OF-SET-DIFFERENCE-EQUAL
 (1467 13 (:REWRITE MEMBER-OF-SET-DIFFERENCE-EQUAL))
 (1070 69 (:DEFINITION SUBSETP-EQUAL))
 (949 311 (:REWRITE SUBSETP-MEMBER . 1))
 (857 198 (:REWRITE SUBSETP-MEMBER . 3))
 (341 341 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (317 309 (:REWRITE DEFAULT-CAR))
 (311 311 (:REWRITE SUBSETP-MEMBER . 2))
 (296 291 (:REWRITE DEFAULT-CDR))
 (198 198 (:REWRITE SUBSETP-MEMBER . 4))
 (137 137 (:REWRITE SUBSETP-TRANS2))
 (137 137 (:REWRITE SUBSETP-TRANS))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(SET-DIFFERENCE$-OF-REMOVE-WHEN-MEMBER-1
 (1087 182 (:REWRITE SUBSETP-MEMBER . 1))
 (831 53 (:DEFINITION SUBSETP-EQUAL))
 (261 261 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (201 198 (:REWRITE DEFAULT-CAR))
 (187 185 (:REWRITE DEFAULT-CDR))
 (182 182 (:REWRITE SUBSETP-MEMBER . 2))
 (173 107 (:REWRITE SUBSETP-MEMBER . 3))
 (107 107 (:REWRITE SUBSETP-MEMBER . 4))
 (105 105 (:REWRITE SUBSETP-TRANS2))
 (105 105 (:REWRITE SUBSETP-TRANS))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(SET-DIFFERENCE$-OF-INTERSECTION$-1
 (932 146 (:REWRITE SUBSETP-MEMBER . 1))
 (883 49 (:DEFINITION SUBSETP-EQUAL))
 (315 73 (:REWRITE SUBSETP-MEMBER . 3))
 (263 263 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (183 176 (:REWRITE DEFAULT-CAR))
 (157 153 (:REWRITE DEFAULT-CDR))
 (146 146 (:REWRITE SUBSETP-MEMBER . 2))
 (103 103 (:REWRITE SUBSETP-TRANS2))
 (103 103 (:REWRITE SUBSETP-TRANS))
 (73 73 (:REWRITE SUBSETP-MEMBER . 4))
 (4 2 (:TYPE-PRESCRIPTION MEMBER-OF-INTERSECTION$ . 2))
 (4 2 (:TYPE-PRESCRIPTION MEMBER-OF-INTERSECTION$ . 1))
 )
(LEN-OF-PUT-ASSOC-EQUAL-2
 (306 102 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (99 7 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (53 53 (:REWRITE DEFAULT-CAR))
 (29 25 (:REWRITE DEFAULT-CDR))
 (22 11 (:REWRITE DEFAULT-+-2))
 (17 17 (:LINEAR POSITION-WHEN-MEMBER))
 (17 17 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (11 11 (:REWRITE DEFAULT-+-1))
 (9 3 (:REWRITE LEN-OF-PUT-ASSOC-EQUAL))
 (3 3 (:TYPE-PRESCRIPTION NULL))
 (3 3 (:DEFINITION NULL))
 )
(INTERSECTION$-OF-REMOVE-1
 (2542 148 (:DEFINITION SUBSETP-EQUAL))
 (2165 436 (:REWRITE SUBSETP-MEMBER . 1))
 (1513 214 (:REWRITE SUBSETP-MEMBER . 3))
 (744 744 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (627 11 (:REWRITE MEMBER-OF-INTERSECTION$))
 (472 464 (:REWRITE DEFAULT-CAR))
 (436 436 (:REWRITE SUBSETP-MEMBER . 2))
 (432 426 (:REWRITE DEFAULT-CDR))
 (299 299 (:REWRITE SUBSETP-TRANS2))
 (299 299 (:REWRITE SUBSETP-TRANS))
 (214 214 (:REWRITE SUBSETP-MEMBER . 4))
 (36 4 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (29 1 (:DEFINITION TRUE-LIST-FIX))
 (28 2 (:DEFINITION TRUE-LISTP))
 (24 4 (:DEFINITION STRING-LISTP))
 (20 20 (:TYPE-PRESCRIPTION STRING-LISTP))
 (10 10 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (2 2 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 )
(SET-DIFFERENCE$-WHEN-NOT-INTERSECTP
 (166 6 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (118 13 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (95 7 (:DEFINITION TRUE-LISTP))
 (81 14 (:DEFINITION STRING-LISTP))
 (63 63 (:TYPE-PRESCRIPTION STRING-LISTP))
 (47 14 (:REWRITE SUBSETP-MEMBER . 3))
 (45 3 (:DEFINITION SUBSETP-EQUAL))
 (40 40 (:REWRITE DEFAULT-CDR))
 (39 39 (:REWRITE DEFAULT-CAR))
 (31 7 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (28 28 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (18 18 (:REWRITE SUBSETP-MEMBER . 2))
 (18 18 (:REWRITE SUBSETP-MEMBER . 1))
 (15 15 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (14 14 (:REWRITE SUBSETP-MEMBER . 4))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (6 6 (:REWRITE SUBSETP-TRANS2))
 (6 6 (:REWRITE SUBSETP-TRANS))
 )
(SET-DIFFERENCE$-OF-APPEND-2
 (1704 14 (:REWRITE INTERSECTP-OF-APPEND-1))
 (1588 27 (:REWRITE INTERSECTP-IS-COMMUTATIVE))
 (811 45 (:DEFINITION SUBSETP-EQUAL))
 (498 24 (:REWRITE MEMBER-OF-BINARY-APPEND))
 (489 291 (:REWRITE SUBSETP-MEMBER . 1))
 (483 212 (:REWRITE SUBSETP-MEMBER . 3))
 (471 402 (:REWRITE DEFAULT-CAR))
 (471 135 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (358 307 (:REWRITE DEFAULT-CDR))
 (303 135 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (291 291 (:REWRITE SUBSETP-MEMBER . 2))
 (240 120 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (225 225 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (212 212 (:REWRITE SUBSETP-MEMBER . 4))
 (135 135 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (135 135 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (135 135 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (135 135 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (135 135 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (135 135 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (135 135 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (135 135 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (135 135 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (135 135 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (122 122 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (120 120 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (90 90 (:REWRITE SUBSETP-TRANS2))
 (90 90 (:REWRITE SUBSETP-TRANS))
 (12 2 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (6 2 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (2 2 (:TYPE-PRESCRIPTION STRING-LISTP))
 (2 2 (:DEFINITION TRUE-LISTP))
 (2 2 (:DEFINITION STRING-LISTP))
 )
(SET-DIFFERENCE$-OF-SELF-LEMMA-1
 (260 10 (:REWRITE APPEND-TO-NIL))
 (183 21 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (145 5 (:DEFINITION BINARY-APPEND))
 (141 11 (:DEFINITION TRUE-LISTP))
 (125 125 (:REWRITE DEFAULT-CAR))
 (121 21 (:DEFINITION STRING-LISTP))
 (118 118 (:REWRITE DEFAULT-CDR))
 (101 101 (:TYPE-PRESCRIPTION STRING-LISTP))
 (93 77 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (88 88 (:REWRITE SUBSETP-MEMBER . 2))
 (87 79 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (75 75 (:REWRITE SUBSETP-MEMBER . 4))
 (73 73 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (73 73 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (73 73 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (73 73 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (73 73 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (73 73 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (73 73 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (73 73 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (73 73 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (73 73 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (51 51 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (49 45 (:REWRITE SUBSETP-TRANS2))
 (44 44 (:REWRITE SUBSETP-TRANS))
 (39 1 (:REWRITE SUBSETP-APPEND1))
 (7 2 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 )
(SET-DIFFERENCE$-OF-SELF)
(SET-DIFFERENCE$-OF-APPEND-1
 (3588 53 (:REWRITE INTERSECTP-IS-COMMUTATIVE))
 (1474 8 (:REWRITE INTERSECTP-OF-APPEND-1))
 (696 40 (:DEFINITION SUBSETP-EQUAL))
 (473 185 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (359 178 (:REWRITE SUBSETP-MEMBER . 3))
 (355 258 (:REWRITE DEFAULT-CDR))
 (337 279 (:REWRITE DEFAULT-CAR))
 (337 244 (:REWRITE SUBSETP-MEMBER . 1))
 (329 185 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (281 185 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (244 244 (:REWRITE SUBSETP-MEMBER . 2))
 (233 185 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (200 200 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (185 185 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (185 185 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (185 185 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (185 185 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (185 185 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (185 185 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (185 185 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (185 185 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (178 178 (:REWRITE SUBSETP-MEMBER . 4))
 (146 2 (:REWRITE MEMBER-OF-BINARY-APPEND))
 (118 118 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (80 80 (:REWRITE SUBSETP-TRANS2))
 (80 80 (:REWRITE SUBSETP-TRANS))
 (24 24 (:REWRITE CONSP-OF-APPEND))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(REMOVE-DUPLICATES-WHEN-NO-DUPLICATESP
 (166 6 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (118 13 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (95 7 (:DEFINITION TRUE-LISTP))
 (81 14 (:DEFINITION STRING-LISTP))
 (63 63 (:TYPE-PRESCRIPTION STRING-LISTP))
 (47 14 (:REWRITE SUBSETP-MEMBER . 3))
 (45 45 (:REWRITE DEFAULT-CDR))
 (37 37 (:REWRITE DEFAULT-CAR))
 (28 28 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (25 2 (:DEFINITION SUBSETP-EQUAL))
 (16 16 (:REWRITE SUBSETP-MEMBER . 2))
 (16 16 (:REWRITE SUBSETP-MEMBER . 1))
 (14 14 (:REWRITE SUBSETP-MEMBER . 4))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )
(NOT-INTERSECTP-OF-SET-DIFFERENCE$-WHEN-SUBSETP-1
 (3179 24 (:REWRITE SET-DIFFERENCE$-WHEN-NOT-INTERSECTP))
 (2530 8 (:DEFINITION SET-DIFFERENCE-EQUAL))
 (1520 472 (:REWRITE SUBSETP-MEMBER . 1))
 (1382 187 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (766 101 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (744 186 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (727 11 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (515 187 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (493 241 (:REWRITE SUBSETP-TRANS2))
 (474 186 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (451 451 (:REWRITE DEFAULT-CAR))
 (431 189 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (422 101 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (416 416 (:REWRITE DEFAULT-CDR))
 (382 241 (:REWRITE SUBSETP-TRANS))
 (320 188 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (316 101 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (256 11 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (242 141 (:REWRITE SUBSETP-MEMBER . 3))
 (201 101 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (201 101 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (189 101 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (141 141 (:REWRITE SUBSETP-MEMBER . 4))
 (63 63 (:TYPE-PRESCRIPTION SET-DIFFERENCE-EQUAL))
 (11 11 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (11 11 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 )
(SUBSETP-OF-SET-DIFFERENCE$
 (3591 61 (:REWRITE INTERSECTP-IS-COMMUTATIVE))
 (1340 628 (:REWRITE SUBSETP-MEMBER . 1))
 (1169 243 (:REWRITE SUBSETP-TRANS))
 (987 243 (:REWRITE SUBSETP-TRANS2))
 (936 21 (:REWRITE MEMBER-OF-SET-DIFFERENCE-EQUAL))
 (661 231 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (634 633 (:REWRITE DEFAULT-CAR))
 (563 562 (:REWRITE DEFAULT-CDR))
 (483 412 (:REWRITE SUBSETP-MEMBER . 3))
 (412 412 (:REWRITE SUBSETP-MEMBER . 4))
 (249 231 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (231 231 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (231 231 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (231 231 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (231 231 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (223 223 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (223 223 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (223 223 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (223 223 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (223 223 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (223 223 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (173 15 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (139 23 (:DEFINITION STRING-LISTP))
 (79 79 (:TYPE-PRESCRIPTION STRING-LISTP))
 (71 71 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (71 71 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (71 71 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (71 71 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 )
(ALISTP-OF-APPEND
 (430 15 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (305 33 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (245 17 (:DEFINITION TRUE-LISTP))
 (209 35 (:DEFINITION STRING-LISTP))
 (165 165 (:TYPE-PRESCRIPTION STRING-LISTP))
 (160 80 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (155 155 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (149 92 (:REWRITE DEFAULT-CDR))
 (136 79 (:REWRITE DEFAULT-CAR))
 (80 80 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (21 21 (:REWRITE CONSP-OF-APPEND))
 )
(TAKE-AS-APPEND-AND-NTH
 (669 53 (:REWRITE TAKE-OF-LEN-FREE))
 (355 67 (:DEFINITION LEN))
 (249 177 (:REWRITE DEFAULT-+-2))
 (177 177 (:REWRITE DEFAULT-+-1))
 (112 90 (:REWRITE DEFAULT-<-2))
 (90 90 (:REWRITE DEFAULT-<-1))
 (89 89 (:LINEAR POSITION-WHEN-MEMBER))
 (89 89 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (80 24 (:REWRITE CONSP-OF-TAKE))
 )
(CONSP-OF-ASSOC-OF-NTH-OF-STRIP-CARS
 (32 8 (:DEFINITION STRIP-CARS))
 (27 1 (:DEFINITION NTH))
 (19 19 (:REWRITE DEFAULT-CDR))
 (19 10 (:REWRITE DEFAULT-+-2))
 (18 18 (:REWRITE DEFAULT-CAR))
 (17 12 (:REWRITE DEFAULT-<-2))
 (12 12 (:REWRITE DEFAULT-<-1))
 (10 10 (:REWRITE DEFAULT-+-1))
 (9 1 (:DEFINITION MEMBER-EQUAL))
 (4 4 (:TYPE-PRESCRIPTION STRIP-CARS))
 (4 4 (:LINEAR POSITION-WHEN-MEMBER))
 (4 4 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (2 2 (:REWRITE SUBSETP-MEMBER . 4))
 (2 2 (:REWRITE SUBSETP-MEMBER . 3))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (1 1 (:REWRITE ZP-OPEN))
 )
(PAINFUL-DEBUGGING-LEMMA-21
 (7 7 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 3 (:REWRITE DEFAULT-+-1))
 (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(FIX-WHEN-ACL2-NUMBERP
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(LENGTH-OF-STRING-APPEND
 (20 4 (:DEFINITION LEN))
 (12 6 (:REWRITE DEFAULT-+-2))
 (8 6 (:REWRITE DEFAULT-+-1))
 (7 5 (:REWRITE DEFAULT-COERCE-1))
 (6 6 (:REWRITE DEFAULT-COERCE-2))
 (6 1 (:REWRITE DEFAULT-COERCE-3))
 (5 5 (:REWRITE DEFAULT-CDR))
 (3 1 (:DEFINITION BINARY-APPEND))
 (1 1 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE CONSP-OF-APPEND))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER))
 (1 1 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(NFIX-OF-POSITION-AC-LINEAR
 (663 340 (:TYPE-PRESCRIPTION NATP-POSITION-EQUAL-AC))
 (323 323 (:TYPE-PRESCRIPTION NATP))
 (258 16 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (186 22 (:DEFINITION MEMBER-EQUAL))
 (77 41 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (77 24 (:REWRITE DEFAULT-<-1))
 (67 24 (:REWRITE DEFAULT-<-2))
 (62 31 (:REWRITE DEFAULT-+-2))
 (47 47 (:REWRITE DEFAULT-CAR))
 (42 42 (:REWRITE SUBSETP-MEMBER . 2))
 (42 42 (:REWRITE SUBSETP-MEMBER . 1))
 (36 36 (:REWRITE DEFAULT-CDR))
 (8 8 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER-OF-TAKE))
 (7 7 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(LENGTH-WHEN-STRINGP
 (10 2 (:DEFINITION LEN))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE DEFAULT-COERCE-1))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER))
 (2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(STRING-APPEND-OF-EMPTY-STRING-1
 (5 5 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE DEFAULT-COERCE-3))
 )
(STRING-APPEND-OF-EMPTY-STRING-2
 (5 5 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE DEFAULT-COERCE-3))
 )
(NFIX-WHEN-NATP
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(NFIX-WHEN-ZP
 (5 1 (:REWRITE NFIX-WHEN-NATP))
 (3 1 (:DEFINITION NATP))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE ZP-OPEN))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(TAKE-OF-APPEND
 (976 49 (:REWRITE TAKE-OF-LEN-FREE))
 (304 183 (:REWRITE DEFAULT-+-2))
 (214 9 (:REWRITE APPEND-TO-NIL))
 (207 11 (:REWRITE LEN-OF-APPEND))
 (201 183 (:REWRITE DEFAULT-+-1))
 (147 17 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (123 71 (:REWRITE DEFAULT-CAR))
 (113 9 (:DEFINITION TRUE-LISTP))
 (97 17 (:DEFINITION STRING-LISTP))
 (93 93 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (90 24 (:REWRITE ZP-OPEN))
 (81 81 (:TYPE-PRESCRIPTION STRING-LISTP))
 (77 77 (:LINEAR POSITION-WHEN-MEMBER))
 (77 77 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (53 24 (:REWRITE FOLD-CONSTS-IN-+))
 (43 33 (:REWRITE DEFAULT-<-2))
 (37 33 (:REWRITE DEFAULT-<-1))
 (9 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 8 (:REWRITE CONSP-OF-APPEND))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 1 (:DEFINITION NATP))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(LEMMA-1
 (6 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-COERCE-2))
 (3 3 (:REWRITE DEFAULT-COERCE-1))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-+-1))
 )
(LEMMA-2)
(SUBSEQ-OF-STRING-APPEND
 (45864 25342 (:REWRITE DEFAULT-+-2))
 (34206 22115 (:REWRITE DEFAULT-CDR))
 (18786 18786 (:REWRITE DEFAULT-COERCE-2))
 (17216 2152 (:DEFINITION CHARACTER-LISTP))
 (11296 7813 (:REWRITE DEFAULT-CAR))
 (11118 11118 (:LINEAR POSITION-WHEN-MEMBER))
 (11118 11118 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (10223 6671 (:REWRITE DEFAULT-UNARY-MINUS))
 (9669 165 (:REWRITE CAR-OF-NTHCDR))
 (8393 330 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (6779 888 (:REWRITE CONSP-OF-APPEND))
 (6055 401 (:REWRITE CONSP-OF-NTHCDR))
 (5355 165 (:DEFINITION NTH))
 (3614 3614 (:REWRITE FOLD-CONSTS-IN-+))
 (2881 142 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (1072 1072 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (118 118 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(THEN-SUBSEQ-EMPTY-1
 (281 2 (:DEFINITION TAKE))
 (237 4 (:REWRITE TAKE-OF-LEN-FREE))
 (156 18 (:DEFINITION LEN))
 (114 2 (:REWRITE CAR-OF-NTHCDR))
 (108 2 (:REWRITE LEN-OF-NTHCDR))
 (102 28 (:REWRITE DEFAULT-CDR))
 (100 18 (:REWRITE NFIX-WHEN-ZP))
 (100 4 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (100 4 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (66 48 (:REWRITE DEFAULT-<-2))
 (66 2 (:DEFINITION NTHCDR))
 (62 2 (:DEFINITION NTH))
 (54 48 (:REWRITE DEFAULT-<-1))
 (54 18 (:REWRITE NFIX-WHEN-NATP))
 (54 4 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (51 31 (:REWRITE DEFAULT-+-2))
 (50 14 (:DEFINITION NFIX))
 (36 2 (:REWRITE CONSP-OF-NTHCDR))
 (34 31 (:REWRITE DEFAULT-+-1))
 (24 8 (:DEFINITION NATP))
 (21 21 (:TYPE-PRESCRIPTION TRUE-LISTP-SUBSEQ-TYPE-PRESCRIPTION))
 (18 18 (:TYPE-PRESCRIPTION ZP))
 (18 18 (:TYPE-PRESCRIPTION NFIX))
 (16 16 (:LINEAR POSITION-WHEN-MEMBER))
 (16 16 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (10 10 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (8 8 (:TYPE-PRESCRIPTION NATP))
 (7 7 (:REWRITE DEFAULT-COERCE-2))
 (6 6 (:REWRITE DEFAULT-COERCE-1))
 (6 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(THEN-SUBSEQ-SAME-1
 (19 19 (:TYPE-PRESCRIPTION TRUE-LISTP-SUBSEQ-TYPE-PRESCRIPTION))
 (18 1 (:REWRITE THEN-SUBSEQ-EMPTY-1))
 (16 1 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (15 3 (:DEFINITION LEN))
 (9 5 (:REWRITE DEFAULT-+-2))
 (6 5 (:REWRITE DEFAULT-+-1))
 (5 5 (:REWRITE DEFAULT-COERCE-2))
 (4 4 (:REWRITE DEFAULT-COERCE-1))
 (4 2 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER))
 (2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1 1 (:TYPE-PRESCRIPTION NFIX))
 (1 1 (:TYPE-PRESCRIPTION LENGTH))
 (1 1 (:REWRITE DEFAULT-COERCE-3))
 )
(SUBSEQ-OF-LENGTH-1
 (1204 8 (:DEFINITION TAKE))
 (1036 16 (:REWRITE TAKE-OF-LEN-FREE))
 (572 56 (:DEFINITION LEN))
 (480 8 (:REWRITE CAR-OF-NTHCDR))
 (468 8 (:REWRITE LEN-OF-NTHCDR))
 (456 120 (:REWRITE DEFAULT-CDR))
 (424 16 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (420 16 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (372 64 (:REWRITE NFIX-WHEN-ZP))
 (312 72 (:REWRITE ZP-OPEN))
 (268 8 (:DEFINITION NTHCDR))
 (256 64 (:REWRITE NFIX-WHEN-NATP))
 (248 8 (:DEFINITION NTH))
 (240 184 (:REWRITE DEFAULT-<-2))
 (232 16 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (200 184 (:REWRITE DEFAULT-<-1))
 (188 52 (:DEFINITION NFIX))
 (174 110 (:REWRITE DEFAULT-+-2))
 (152 8 (:REWRITE CONSP-OF-NTHCDR))
 (144 32 (:DEFINITION NATP))
 (144 16 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (124 110 (:REWRITE DEFAULT-+-1))
 (112 8 (:DEFINITION TRUE-LISTP))
 (96 16 (:DEFINITION STRING-LISTP))
 (80 80 (:TYPE-PRESCRIPTION STRING-LISTP))
 (74 74 (:LINEAR POSITION-WHEN-MEMBER))
 (74 74 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (68 68 (:TYPE-PRESCRIPTION ZP))
 (64 64 (:TYPE-PRESCRIPTION NFIX))
 (60 60 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (60 40 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (52 4 (:REWRITE DEFAULT-COERCE-3))
 (40 4 (:REWRITE CONSP-OF-TAKE))
 (32 32 (:TYPE-PRESCRIPTION NATP))
 (24 24 (:REWRITE DEFAULT-CAR))
 (24 16 (:REWRITE DEFAULT-UNARY-MINUS))
 (16 16 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 (12 12 (:REWRITE DEFAULT-COERCE-2))
 (8 8 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (8 8 (:REWRITE FOLD-CONSTS-IN-+))
 (8 8 (:REWRITE DEFAULT-COERCE-1))
 (1 1 (:REWRITE THEN-SUBSEQ-EMPTY-1))
 )
(SUBSEQ-OF-EMPTY-LIST
 (47 5 (:DEFINITION TAKE))
 (38 11 (:REWRITE ZP-OPEN))
 (37 5 (:REWRITE DEFAULT-COERCE-3))
 (24 4 (:REWRITE CONSP-OF-TAKE))
 (19 10 (:REWRITE TAKE-OF-LEN-FREE))
 (13 13 (:REWRITE DEFAULT-<-2))
 (13 13 (:REWRITE DEFAULT-<-1))
 (13 13 (:DEFINITION NOT))
 (11 11 (:TYPE-PRESCRIPTION TRUE-LISTP-SUBSEQ-TYPE-PRESCRIPTION))
 (10 2 (:REWRITE NFIX-WHEN-NATP))
 (9 9 (:REWRITE DEFAULT-+-2))
 (9 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 2 (:REWRITE NFIX-WHEN-ZP))
 (6 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 2 (:DEFINITION NATP))
 (5 5 (:REWRITE DEFAULT-COERCE-2))
 (4 4 (:TYPE-PRESCRIPTION ZP))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 1 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (1 1 (:TYPE-PRESCRIPTION LENGTH))
 )
(THEN-SUBSEQ-SAME-2
 (10 2 (:DEFINITION LEN))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE DEFAULT-COERCE-1))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-+-1))
 )
(WHEN-APPEND-SAME
 (199 130 (:REWRITE DEFAULT-CDR))
 (92 46 (:REWRITE DEFAULT-+-2))
 (59 59 (:LINEAR POSITION-WHEN-MEMBER))
 (59 59 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (49 46 (:REWRITE DEFAULT-+-1))
 (45 3 (:REWRITE LEN-OF-APPEND))
 (28 25 (:REWRITE DEFAULT-CAR))
 (10 2 (:REWRITE CONSP-OF-LAST))
 )
(SET-DIFFERENCE$-BECOMES-INTERSECTION$
 (1790 92 (:DEFINITION SUBSETP-EQUAL))
 (1192 138 (:REWRITE SUBSETP-MEMBER . 3))
 (891 306 (:REWRITE SUBSETP-MEMBER . 1))
 (526 20 (:REWRITE NOT-INTERSECTP-OF-SET-DIFFERENCE$-WHEN-SUBSETP-1 . 1))
 (457 457 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (349 330 (:REWRITE DEFAULT-CAR))
 (306 306 (:REWRITE SUBSETP-MEMBER . 2))
 (256 247 (:REWRITE DEFAULT-CDR))
 (187 187 (:REWRITE SUBSETP-TRANS2))
 (187 187 (:REWRITE SUBSETP-TRANS))
 (138 138 (:REWRITE SUBSETP-MEMBER . 4))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (61 61 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(SUBSETP-OF-SET-DIFFERENCE$-2
 (1148 18 (:REWRITE SET-DIFFERENCE$-WHEN-NOT-INTERSECTP))
 (882 6 (:DEFINITION SET-DIFFERENCE-EQUAL))
 (452 154 (:REWRITE SUBSETP-MEMBER . 1))
 (420 128 (:REWRITE SUBSETP-TRANS2))
 (339 128 (:REWRITE SUBSETP-TRANS))
 (330 41 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (211 41 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (194 154 (:REWRITE SUBSETP-MEMBER . 2))
 (157 157 (:REWRITE DEFAULT-CAR))
 (151 151 (:REWRITE DEFAULT-CDR))
 (105 85 (:REWRITE SUBSETP-MEMBER . 3))
 (87 15 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (85 85 (:REWRITE SUBSETP-MEMBER . 4))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (15 15 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (15 15 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (15 15 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (12 2 (:REWRITE NOT-INTERSECTP-OF-SET-DIFFERENCE$-WHEN-SUBSETP-1 . 1))
 (9 9 (:TYPE-PRESCRIPTION SET-DIFFERENCE-EQUAL))
 )
(INTERSECTP-WHEN-SUBSETP
 (98 2 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (52 7 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (45 7 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (21 1 (:DEFINITION SUBSETP-EQUAL))
 (16 1 (:REWRITE INTERSECTP-IS-COMMUTATIVE))
 (15 15 (:REWRITE DEFAULT-CAR))
 (10 10 (:REWRITE SUBSETP-MEMBER . 1))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 4))
 (4 4 (:REWRITE SUBSETP-MEMBER . 3))
 (3 3 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 (2 2 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (2 2 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (2 2 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (2 2 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (2 2 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (2 2 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (2 2 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (2 2 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (2 2 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 )
(NTH-UNDER-IFF-1
 (62 14 (:REWRITE NFIX-WHEN-ZP))
 (52 38 (:REWRITE DEFAULT-<-2))
 (44 24 (:REWRITE DEFAULT-+-2))
 (43 21 (:REWRITE SUBSETP-MEMBER . 1))
 (41 38 (:REWRITE DEFAULT-<-1))
 (31 16 (:REWRITE ZP-OPEN))
 (26 26 (:REWRITE DEFAULT-CDR))
 (24 24 (:REWRITE DEFAULT-+-1))
 (21 21 (:TYPE-PRESCRIPTION ZP))
 (21 21 (:REWRITE SUBSETP-MEMBER . 2))
 (20 20 (:LINEAR POSITION-WHEN-MEMBER))
 (20 20 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (20 1 (:DEFINITION SUBSETP-EQUAL))
 (19 19 (:REWRITE SUBSETP-MEMBER . 4))
 (19 19 (:REWRITE SUBSETP-MEMBER . 3))
 (9 3 (:DEFINITION NATP))
 (5 5 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 )
(CONSP-WHEN-MEMBER
 (1 1 (:REWRITE SUBSETP-MEMBER . 4))
 (1 1 (:REWRITE SUBSETP-MEMBER . 3))
 (1 1 (:REWRITE SUBSETP-MEMBER . 2))
 (1 1 (:REWRITE SUBSETP-MEMBER . 1))
 )
(PAINFUL-DEBUGGING-LEMMA-11
 (17 17 (:TYPE-PRESCRIPTION MIN))
 (8 8 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (8 4 (:REWRITE DEFAULT-<-2))
 (8 4 (:REWRITE DEFAULT-<-1))
 )
(PAINFUL-DEBUGGING-LEMMA-22
 (9 9 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (7 7 (:TYPE-PRESCRIPTION MIN))
 (7 4 (:REWRITE DEFAULT-<-2))
 (7 4 (:REWRITE DEFAULT-<-1))
 (4 2 (:REWRITE DEFAULT-+-2))
 (3 2 (:REWRITE DEFAULT-+-1))
 )
(PAINFUL-DEBUGGING-LEMMA-17
 (9 9 (:TYPE-PRESCRIPTION MIN))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 2 (:REWRITE DEFAULT-<-2))
 (3 2 (:REWRITE DEFAULT-<-1))
 (2 1 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(PAINFUL-DEBUGGING-LEMMA-8
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE ZP-OPEN))
 (1 1 (:REWRITE DEFAULT-NUMERATOR))
 (1 1 (:REWRITE DEFAULT-DENOMINATOR))
 )
(PAINFUL-DEBUGGING-LEMMA-9)
(PAINFUL-DEBUGGING-LEMMA-10
 (3 3 (:TYPE-PRESCRIPTION ZP))
 )
(MEMBER-OF-NTH-WHEN-NOT-INTERSECTP
 (176 10 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (156 82 (:REWRITE SUBSETP-MEMBER . 1))
 (102 36 (:REWRITE SUBSETP-MEMBER . 3))
 (84 84 (:REWRITE DEFAULT-CAR))
 (82 82 (:REWRITE SUBSETP-MEMBER . 2))
 (81 81 (:REWRITE DEFAULT-CDR))
 (53 53 (:REWRITE SUBSETP-TRANS2))
 (53 53 (:REWRITE SUBSETP-TRANS))
 (43 32 (:REWRITE DEFAULT-<-2))
 (43 10 (:REWRITE NFIX-WHEN-ZP))
 (40 22 (:REWRITE DEFAULT-+-2))
 (36 36 (:REWRITE SUBSETP-MEMBER . 4))
 (36 12 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (33 32 (:REWRITE DEFAULT-<-1))
 (28 13 (:REWRITE ZP-OPEN))
 (22 22 (:REWRITE DEFAULT-+-1))
 (19 19 (:LINEAR POSITION-WHEN-MEMBER))
 (19 19 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (12 12 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (12 12 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (12 12 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (12 12 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (12 12 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (12 12 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (12 12 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (12 12 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (12 12 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (12 12 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (12 12 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (12 8 (:REWRITE NFIX-WHEN-NATP))
 (3 1 (:DEFINITION NATP))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(TRUE-LIST-LISTP-OF-REMOVE
 (198 22 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (132 22 (:DEFINITION STRING-LISTP))
 (121 11 (:DEFINITION TRUE-LISTP))
 (110 110 (:TYPE-PRESCRIPTION STRING-LISTP))
 (69 68 (:REWRITE DEFAULT-CDR))
 (67 66 (:REWRITE DEFAULT-CAR))
 (32 32 (:REWRITE SUBSETP-MEMBER . 4))
 (32 32 (:REWRITE SUBSETP-MEMBER . 3))
 (32 32 (:REWRITE SUBSETP-MEMBER . 2))
 (32 32 (:REWRITE SUBSETP-MEMBER . 1))
 )
(SUBSETP-OF-SET-DIFFERENCE$-WHEN-SUBSETP
 (9628 317 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (8625 337 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (6115 1941 (:REWRITE SUBSETP-MEMBER . 1))
 (5668 1917 (:REWRITE SUBSETP-TRANS))
 (2053 1987 (:REWRITE DEFAULT-CDR))
 (2007 1939 (:REWRITE DEFAULT-CAR))
 (1171 309 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (631 242 (:REWRITE SUBSETP-MEMBER . 3))
 (353 337 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (351 319 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (337 337 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (337 337 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (337 337 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (319 319 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (319 319 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (319 319 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (242 242 (:REWRITE SUBSETP-MEMBER . 4))
 (138 10 (:REWRITE NOT-INTERSECTP-OF-SET-DIFFERENCE$-WHEN-SUBSETP-1 . 2))
 (127 2 (:REWRITE MEMBER-OF-SET-DIFFERENCE-EQUAL))
 (16 16 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (16 16 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (16 16 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (16 16 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (6 1 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (3 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1 1 (:DEFINITION TRUE-LISTP))
 (1 1 (:DEFINITION STRING-LISTP))
 )
(TRUE-LIST-LISTP-OF-SET-DIFFERENCE
 (628 9 (:DEFINITION INTERSECTP-EQUAL))
 (490 5 (:REWRITE INTERSECTP-IS-COMMUTATIVE))
 (198 22 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (156 88 (:REWRITE SUBSETP-MEMBER . 1))
 (132 22 (:DEFINITION STRING-LISTP))
 (130 129 (:REWRITE DEFAULT-CAR))
 (126 125 (:REWRITE DEFAULT-CDR))
 (121 11 (:DEFINITION TRUE-LISTP))
 (110 110 (:TYPE-PRESCRIPTION STRING-LISTP))
 (100 34 (:REWRITE SUBSETP-MEMBER . 3))
 (88 88 (:REWRITE SUBSETP-MEMBER . 2))
 (63 63 (:REWRITE SUBSETP-TRANS2))
 (63 63 (:REWRITE SUBSETP-TRANS))
 (34 34 (:REWRITE SUBSETP-MEMBER . 4))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (22 22 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 )
(LAST-OF-APPEND
 (688 344 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (344 344 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (244 14 (:REWRITE LEN-OF-APPEND))
 (204 105 (:REWRITE DEFAULT-+-2))
 (128 128 (:LINEAR POSITION-WHEN-MEMBER))
 (128 128 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (123 105 (:REWRITE DEFAULT-+-1))
 (69 11 (:REWRITE COMMUTATIVITY-OF-+))
 (62 36 (:REWRITE DEFAULT-CAR))
 (21 7 (:REWRITE UNICITY-OF-0))
 (14 7 (:REWRITE FIX-WHEN-ACL2-NUMBERP))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(NATP-OF-NTH-WHEN-NAT-LISTP
 (39 7 (:DEFINITION LEN))
 (33 27 (:REWRITE DEFAULT-<-2))
 (31 27 (:REWRITE DEFAULT-<-1))
 (30 7 (:REWRITE NFIX-WHEN-ZP))
 (20 10 (:REWRITE ZP-OPEN))
 (18 10 (:REWRITE DEFAULT-+-2))
 (18 6 (:REWRITE NFIX-WHEN-NATP))
 (12 12 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-+-1))
 (9 9 (:REWRITE DEFAULT-CAR))
 (6 6 (:LINEAR POSITION-WHEN-MEMBER))
 (6 6 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 )
(ACL2-NUMBER-LISTP-WHEN-RATIONAL-LISTP)
(RATIONAL-LISTP-WHEN-INTEGER-LISTP)
(INTEGER-LISTP-WHEN-NAT-LISTP)
(CONSP-OF-STRIP-CARS
 (6 6 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE DEFAULT-CDR))
 )