(STRING-INDEX-MEASURE)
(STRING-INDEX-END)
(NOT-STRING-INDEX-END-CHARACTERP
 (6 1 (:DEFINITION NTH))
 (5 1 (:DEFINITION LEN))
 (3 2 (:REWRITE DEFAULT-<-2))
 (3 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 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE ZP-OPEN))
 (1 1 (:REWRITE DEFAULT-CAR))
 )
(STRING-INDEX-PAST-END)
(LENGTH-EQUIV)
(LENGTH-EQUIV-IS-AN-EQUIVALENCE)
(LENGTH-EQUIV-LINEAR)
(LENGTH-EQUIV-IMPLIES)
(IMPLIES-LENGTH-EQUIV)
(INDEXP)
(INDEXP-CHARACTERP
 (30 6 (:DEFINITION LEN))
 (12 6 (:REWRITE DEFAULT-+-2))
 (7 5 (:REWRITE DEFAULT-<-1))
 (6 6 (:REWRITE DEFAULT-COERCE-2))
 (6 6 (:REWRITE DEFAULT-COERCE-1))
 (6 6 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE DEFAULT-+-1))
 (6 5 (:REWRITE DEFAULT-<-2))
 (2 2 (:LINEAR LENGTH-EQUIV-LINEAR))
 )
(LENGTH-EQUIV-IMPLIES-EQUAL-INDEXP-2
 (29 3 (:REWRITE LENGTH-EQUIV-IMPLIES))
 (15 1 (:REWRITE IMPLIES-LENGTH-EQUIV))
 (12 1 (:DEFINITION =))
 (6 4 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:LINEAR LENGTH-EQUIV-LINEAR))
 )
(BACKREFP)
(BACKREF-INTS)
(LENGTH-EQUIV-IMPLIES-EQUAL-BACKREFP-2
 (29 3 (:REWRITE LENGTH-EQUIV-IMPLIES))
 (15 1 (:REWRITE IMPLIES-LENGTH-EQUIV))
 (14 10 (:REWRITE DEFAULT-<-1))
 (12 1 (:DEFINITION =))
 (10 10 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE BACKREF-INTS))
 (4 4 (:LINEAR LENGTH-EQUIV-LINEAR))
 )
(PSEUDO-BACKREFP)
(BACKREFP-PSEUDO
 (20 4 (:DEFINITION LEN))
 (14 14 (:REWRITE DEFAULT-CDR))
 (12 8 (:REWRITE DEFAULT-<-1))
 (8 8 (:REWRITE DEFAULT-<-2))
 (8 4 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE BACKREF-INTS))
 (2 2 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE DEFAULT-COERCE-1))
 (2 2 (:LINEAR LENGTH-EQUIV-LINEAR))
 )
(GET-BACKREF-STRING
 (5 5 (:TYPE-PRESCRIPTION TRUE-LISTP-SUBSEQ-TYPE-PRESCRIPTION))
 (5 5 (:TYPE-PRESCRIPTION STRINGP-SUBSEQ-TYPE-PRESCRIPTION))
 )
(BACKREFP-STRINGP
 (53 1 (:DEFINITION TAKE))
 (38 6 (:DEFINITION LEN))
 (38 2 (:REWRITE TAKE-OF-TOO-MANY))
 (28 2 (:REWRITE TAKE-OF-LEN-FREE))
 (20 20 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (17 11 (:REWRITE DEFAULT-+-2))
 (16 13 (:REWRITE DEFAULT-CDR))
 (15 13 (:REWRITE DEFAULT-<-2))
 (15 13 (:REWRITE DEFAULT-<-1))
 (12 3 (:REWRITE ZP-OPEN))
 (11 11 (:REWRITE DEFAULT-+-1))
 (11 1 (:REWRITE DEFAULT-COERCE-3))
 (11 1 (:DEFINITION NTHCDR))
 (9 6 (:REWRITE DEFAULT-CAR))
 (8 2 (:REWRITE TAKE-WHEN-ATOM))
 (8 1 (:REWRITE CONSP-OF-TAKE))
 (6 2 (:DEFINITION NFIX))
 (4 4 (:REWRITE DEFAULT-COERCE-2))
 (3 3 (:REWRITE DEFAULT-COERCE-1))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:REWRITE BACKREF-INTS))
 (2 2 (:LINEAR LENGTH-EQUIV-LINEAR))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(BACKREF-LISTP)
(BACKREF-LISTP-NTH
 (200 40 (:DEFINITION LEN))
 (92 52 (:REWRITE DEFAULT-+-2))
 (91 91 (:REWRITE DEFAULT-CDR))
 (90 50 (:REWRITE DEFAULT-<-1))
 (68 68 (:REWRITE DEFAULT-CAR))
 (52 52 (:REWRITE DEFAULT-+-1))
 (50 50 (:REWRITE DEFAULT-<-2))
 (26 26 (:REWRITE BACKREF-INTS))
 (20 20 (:REWRITE DEFAULT-COERCE-2))
 (20 20 (:REWRITE DEFAULT-COERCE-1))
 (14 14 (:REWRITE ZP-OPEN))
 )
(BACKREF-LISTP-NTH-LINEAR
 (250 50 (:DEFINITION LEN))
 (159 91 (:REWRITE DEFAULT-<-1))
 (138 126 (:REWRITE DEFAULT-CDR))
 (116 66 (:REWRITE DEFAULT-+-2))
 (105 91 (:REWRITE DEFAULT-<-2))
 (100 91 (:REWRITE DEFAULT-CAR))
 (66 66 (:REWRITE DEFAULT-+-1))
 (32 32 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (25 25 (:REWRITE DEFAULT-COERCE-2))
 (25 25 (:REWRITE DEFAULT-COERCE-1))
 (22 22 (:REWRITE BACKREF-INTS))
 (21 21 (:REWRITE BACKREF-LISTP-NTH))
 (18 18 (:REWRITE ZP-OPEN))
 )
(LENGTH-EQUIV-IMPLIES-EQUAL-BACKREF-LISTP-2
 (364 26 (:REWRITE IMPLIES-LENGTH-EQUIV))
 (325 13 (:DEFINITION =))
 (96 66 (:REWRITE DEFAULT-<-1))
 (84 84 (:REWRITE DEFAULT-CAR))
 (78 78 (:LINEAR LENGTH-EQUIV-LINEAR))
 (78 13 (:REWRITE LENGTH-EQUIV-IMPLIES))
 (66 66 (:REWRITE DEFAULT-<-2))
 (39 39 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (34 34 (:REWRITE DEFAULT-CDR))
 (30 30 (:REWRITE BACKREF-INTS))
 )
(PSEUDO-BACKREF-LISTP)
(PSEUDO-BACKREF-LISTP-NTH
 (52 52 (:REWRITE DEFAULT-CAR))
 (41 39 (:REWRITE DEFAULT-CDR))
 (26 26 (:REWRITE BACKREF-INTS))
 (20 20 (:REWRITE DEFAULT-<-2))
 (20 20 (:REWRITE DEFAULT-<-1))
 (14 14 (:REWRITE ZP-OPEN))
 (12 12 (:REWRITE DEFAULT-+-2))
 (12 12 (:REWRITE DEFAULT-+-1))
 (12 12 (:REWRITE BACKREF-LISTP-NTH))
 (10 10 (:REWRITE BACKREFP-PSEUDO))
 )
(BACKREF-LISTP-PSEUDO
 (100 20 (:DEFINITION LEN))
 (57 57 (:REWRITE DEFAULT-CAR))
 (50 30 (:REWRITE DEFAULT-<-1))
 (45 45 (:REWRITE DEFAULT-CDR))
 (40 20 (:REWRITE DEFAULT-+-2))
 (30 30 (:REWRITE DEFAULT-<-2))
 (20 20 (:REWRITE DEFAULT-+-1))
 (16 16 (:REWRITE BACKREF-INTS))
 (10 10 (:REWRITE DEFAULT-COERCE-2))
 (10 10 (:REWRITE DEFAULT-COERCE-1))
 (7 7 (:REWRITE BACKREFP-PSEUDO))
 )
(BACKREF-LISTP-TRUE-LISTP
 (60 12 (:DEFINITION LEN))
 (27 15 (:REWRITE DEFAULT-<-1))
 (24 24 (:REWRITE DEFAULT-CDR))
 (24 12 (:REWRITE DEFAULT-+-2))
 (24 4 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (16 2 (:DEFINITION TRUE-LISTP))
 (15 15 (:REWRITE DEFAULT-<-2))
 (12 12 (:REWRITE DEFAULT-CAR))
 (12 12 (:REWRITE DEFAULT-+-1))
 (8 8 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (8 4 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (6 6 (:REWRITE DEFAULT-COERCE-2))
 (6 6 (:REWRITE DEFAULT-COERCE-1))
 (6 6 (:REWRITE BACKREF-INTS))
 (4 4 (:TYPE-PRESCRIPTION SET::EMPTYP-TYPE))
 (4 4 (:REWRITE SET::IN-SET))
 )
(INPUT-LIST-ELTP)
(INPUT-LIST-ELTP-THM)
(INPUT-LIST-ELTP-SUFFIC
 (60 12 (:DEFINITION LEN))
 (56 22 (:REWRITE INPUT-LIST-ELTP-THM))
 (36 24 (:REWRITE DEFAULT-<-1))
 (32 32 (:REWRITE DEFAULT-CDR))
 (25 25 (:REWRITE DEFAULT-CAR))
 (24 24 (:REWRITE DEFAULT-<-2))
 (24 12 (:REWRITE DEFAULT-+-2))
 (12 12 (:REWRITE DEFAULT-+-1))
 (9 9 (:REWRITE BACKREF-INTS))
 (6 6 (:REWRITE DEFAULT-COERCE-2))
 (6 6 (:REWRITE DEFAULT-COERCE-1))
 (2 2 (:LINEAR LENGTH-EQUIV-LINEAR))
 (1 1 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(LENGTH-EQUIV-IMPLIES-EQUAL-INPUT-LIST-ELTP-2
 (274 32 (:REWRITE INPUT-LIST-ELTP-THM))
 (272 4 (:DEFINITION BACKREF-LISTP))
 (228 12 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (178 4 (:DEFINITION BACKREFP))
 (38 26 (:REWRITE DEFAULT-<-1))
 (32 14 (:LINEAR LENGTH-EQUIV-LINEAR))
 (28 28 (:REWRITE DEFAULT-CAR))
 (28 2 (:REWRITE IMPLIES-LENGTH-EQUIV))
 (26 26 (:REWRITE DEFAULT-<-2))
 (25 1 (:DEFINITION =))
 (20 20 (:REWRITE DEFAULT-CDR))
 (18 18 (:TYPE-PRESCRIPTION INDEXP))
 (14 14 (:TYPE-PRESCRIPTION BACKREF-LISTP))
 (10 10 (:REWRITE BACKREF-INTS))
 (7 7 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (6 1 (:REWRITE LENGTH-EQUIV-IMPLIES))
 )
(PSEUDO-INPUT-LIST-ELTP)
(INPUT-LIST-ELTP-PSEUDO
 (460 6 (:DEFINITION BACKREF-LISTP))
 (430 32 (:REWRITE INPUT-LIST-ELTP-THM))
 (322 6 (:DEFINITION BACKREFP))
 (210 6 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (90 18 (:DEFINITION LEN))
 (54 36 (:REWRITE DEFAULT-<-1))
 (50 50 (:REWRITE DEFAULT-CDR))
 (41 41 (:REWRITE DEFAULT-CAR))
 (36 36 (:REWRITE DEFAULT-<-2))
 (36 18 (:REWRITE DEFAULT-+-2))
 (18 18 (:REWRITE DEFAULT-+-1))
 (13 13 (:REWRITE BACKREF-INTS))
 (9 9 (:REWRITE DEFAULT-COERCE-2))
 (9 9 (:REWRITE DEFAULT-COERCE-1))
 (6 6 (:TYPE-PRESCRIPTION INDEXP))
 (2 2 (:LINEAR LENGTH-EQUIV-LINEAR))
 (1 1 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(STD::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM)
(INPUT-LISTP)
(INPUT-LISTP-OF-CONS)
(INPUT-LISTP-OF-CDR-WHEN-INPUT-LISTP)
(INPUT-LISTP-WHEN-NOT-CONSP)
(INPUT-LIST-ELTP-OF-CAR-WHEN-INPUT-LISTP)
(INPUT-LISTP-OF-APPEND)
(INPUT-LISTP-OF-LIST-FIX)
(INPUT-LISTP-OF-SFIX)
(INPUT-LISTP-OF-INSERT)
(INPUT-LISTP-OF-DELETE)
(INPUT-LISTP-OF-MERGESORT)
(INPUT-LISTP-OF-UNION)
(INPUT-LISTP-OF-INTERSECT-1)
(INPUT-LISTP-OF-INTERSECT-2)
(INPUT-LISTP-OF-DIFFERENCE)
(INPUT-LISTP-OF-DUPLICATED-MEMBERS)
(INPUT-LISTP-OF-REV)
(INPUT-LISTP-OF-RCONS)
(INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP)
(INPUT-LISTP-WHEN-SUBSETP-EQUAL)
(INPUT-LISTP-SET-EQUIV-CONGRUENCE)
(INPUT-LISTP-OF-SET-DIFFERENCE-EQUAL)
(INPUT-LISTP-OF-INTERSECTION-EQUAL-1)
(INPUT-LISTP-OF-INTERSECTION-EQUAL-2)
(INPUT-LISTP-OF-UNION-EQUAL)
(INPUT-LISTP-OF-TAKE)
(INPUT-LISTP-OF-REPEAT)
(INPUT-LIST-ELTP-OF-NTH-WHEN-INPUT-LISTP)
(INPUT-LISTP-OF-UPDATE-NTH)
(INPUT-LISTP-OF-BUTLAST)
(INPUT-LISTP-OF-NTHCDR)
(INPUT-LISTP-OF-LAST)
(INPUT-LISTP-OF-REMOVE)
(INPUT-LISTP-OF-REVAPPEND)
(LENGTH-EQUIV-IMPLIES-EQUAL-INPUT-LISTP-2
 (2292 253 (:REWRITE INPUT-LIST-ELTP-THM))
 (1357 44 (:REWRITE INPUT-LIST-ELTP-OF-CAR-WHEN-INPUT-LISTP))
 (299 200 (:REWRITE DEFAULT-<-1))
 (274 274 (:REWRITE DEFAULT-CAR))
 (243 18 (:REWRITE IMPLIES-LENGTH-EQUIV))
 (216 9 (:DEFINITION =))
 (200 200 (:REWRITE DEFAULT-<-2))
 (198 198 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (154 154 (:REWRITE DEFAULT-CDR))
 (114 114 (:REWRITE INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (78 78 (:REWRITE BACKREF-INTS))
 (65 8 (:REWRITE INPUT-LISTP-OF-CDR-WHEN-INPUT-LISTP))
 (54 9 (:REWRITE LENGTH-EQUIV-IMPLIES))
 (26 26 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(STD::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM)
(PSEUDO-INPUT-LISTP)
(PSEUDO-INPUT-LISTP-OF-CONS)
(PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP)
(PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP)
(PSEUDO-INPUT-LIST-ELTP-OF-CAR-WHEN-PSEUDO-INPUT-LISTP)
(PSEUDO-INPUT-LISTP-OF-APPEND)
(PSEUDO-INPUT-LISTP-OF-LIST-FIX)
(PSEUDO-INPUT-LISTP-OF-SFIX)
(PSEUDO-INPUT-LISTP-OF-INSERT)
(PSEUDO-INPUT-LISTP-OF-DELETE)
(PSEUDO-INPUT-LISTP-OF-MERGESORT)
(PSEUDO-INPUT-LISTP-OF-UNION)
(PSEUDO-INPUT-LISTP-OF-INTERSECT-1)
(PSEUDO-INPUT-LISTP-OF-INTERSECT-2)
(PSEUDO-INPUT-LISTP-OF-DIFFERENCE)
(PSEUDO-INPUT-LISTP-OF-DUPLICATED-MEMBERS)
(PSEUDO-INPUT-LISTP-OF-REV)
(PSEUDO-INPUT-LISTP-OF-RCONS)
(PSEUDO-INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-PSEUDO-INPUT-LISTP)
(PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL)
(PSEUDO-INPUT-LISTP-SET-EQUIV-CONGRUENCE)
(PSEUDO-INPUT-LISTP-OF-SET-DIFFERENCE-EQUAL)
(PSEUDO-INPUT-LISTP-OF-INTERSECTION-EQUAL-1)
(PSEUDO-INPUT-LISTP-OF-INTERSECTION-EQUAL-2)
(PSEUDO-INPUT-LISTP-OF-UNION-EQUAL)
(PSEUDO-INPUT-LISTP-OF-TAKE)
(PSEUDO-INPUT-LISTP-OF-REPEAT)
(PSEUDO-INPUT-LIST-ELTP-OF-NTH-WHEN-PSEUDO-INPUT-LISTP)
(PSEUDO-INPUT-LISTP-OF-UPDATE-NTH)
(PSEUDO-INPUT-LISTP-OF-BUTLAST)
(PSEUDO-INPUT-LISTP-OF-NTHCDR)
(PSEUDO-INPUT-LISTP-OF-LAST)
(PSEUDO-INPUT-LISTP-OF-REMOVE)
(PSEUDO-INPUT-LISTP-OF-REVAPPEND)
(INPUT-LISTP-PSEUDO
 (2475 21 (:DEFINITION BACKREF-LISTP))
 (1934 137 (:REWRITE INPUT-LIST-ELTP-THM))
 (1797 21 (:DEFINITION BACKREFP))
 (1630 46 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (1524 17 (:REWRITE INPUT-LIST-ELTP-OF-CAR-WHEN-INPUT-LISTP))
 (650 130 (:DEFINITION LEN))
 (279 149 (:REWRITE DEFAULT-<-1))
 (273 273 (:REWRITE DEFAULT-CDR))
 (260 130 (:REWRITE DEFAULT-+-2))
 (208 208 (:REWRITE DEFAULT-CAR))
 (149 149 (:REWRITE DEFAULT-<-2))
 (130 130 (:REWRITE DEFAULT-+-1))
 (117 117 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (105 5 (:DEFINITION PSEUDO-BACKREF-LISTP))
 (92 92 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (82 30 (:REWRITE PSEUDO-INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-PSEUDO-INPUT-LISTP))
 (65 65 (:REWRITE DEFAULT-COERCE-2))
 (65 65 (:REWRITE DEFAULT-COERCE-1))
 (65 5 (:DEFINITION PSEUDO-BACKREFP))
 (63 63 (:REWRITE BACKREF-INTS))
 (48 36 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (44 44 (:REWRITE INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (32 32 (:TYPE-PRESCRIPTION INDEXP))
 (30 2 (:DEFINITION MEMBER-EQUAL))
 (28 4 (:REWRITE SUBSETP-CAR-MEMBER))
 (22 22 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (18 18 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (14 2 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (14 2 (:REWRITE INPUT-LISTP-OF-CDR-WHEN-INPUT-LISTP))
 (13 13 (:REWRITE INPUT-LIST-ELTP-PSEUDO))
 (12 12 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (6 6 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (6 6 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (6 6 (:REWRITE SUBSETP-TRANS2))
 (6 6 (:REWRITE SUBSETP-TRANS))
 (5 5 (:REWRITE BACKREFP-PSEUDO))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 )
(BACKREF-LISTP-UPDATE-NTH
 (640 100 (:REWRITE INPUT-LIST-ELTP-THM))
 (490 98 (:DEFINITION LEN))
 (426 250 (:REWRITE DEFAULT-CAR))
 (338 268 (:REWRITE DEFAULT-CDR))
 (310 212 (:REWRITE DEFAULT-<-1))
 (236 34 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (224 126 (:REWRITE DEFAULT-+-2))
 (212 212 (:REWRITE DEFAULT-<-2))
 (202 34 (:DEFINITION INPUT-LIST-ELTP))
 (126 126 (:REWRITE DEFAULT-+-1))
 (68 68 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (68 68 (:REWRITE BACKREF-INTS))
 (61 61 (:REWRITE DEFAULT-COERCE-2))
 (61 61 (:REWRITE DEFAULT-COERCE-1))
 (34 34 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (34 34 (:TYPE-PRESCRIPTION INDEXP))
 (34 16 (:REWRITE ZP-OPEN))
 (18 6 (:REWRITE FOLD-CONSTS-IN-+))
 (6 6 (:LINEAR LENGTH-EQUIV-LINEAR))
 (3 3 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(PSEUDO-BACKREF-LISTP-UPDATE-NTH
 (111 70 (:REWRITE DEFAULT-CAR))
 (100 62 (:REWRITE DEFAULT-CDR))
 (41 41 (:REWRITE DEFAULT-<-2))
 (41 41 (:REWRITE DEFAULT-<-1))
 (41 41 (:REWRITE BACKREF-LISTP-PSEUDO))
 (36 36 (:REWRITE INPUT-LIST-ELTP-THM))
 (36 36 (:REWRITE BACKREF-INTS))
 (18 18 (:REWRITE BACKREFP-PSEUDO))
 (10 7 (:REWRITE ZP-OPEN))
 (8 8 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-+-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(MIN-IDX-IL
 (1646 18 (:DEFINITION BACKREF-LISTP))
 (1621 102 (:REWRITE INPUT-LIST-ELTP-THM))
 (1002 18 (:DEFINITION BACKREFP))
 (623 18 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (339 36 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (315 63 (:DEFINITION LEN))
 (243 27 (:DEFINITION MEMBER-EQUAL))
 (214 214 (:REWRITE DEFAULT-CDR))
 (195 195 (:REWRITE DEFAULT-CAR))
 (170 115 (:REWRITE DEFAULT-<-1))
 (126 63 (:REWRITE DEFAULT-+-2))
 (123 115 (:REWRITE DEFAULT-<-2))
 (96 96 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (63 63 (:REWRITE DEFAULT-COERCE-2))
 (63 63 (:REWRITE DEFAULT-COERCE-1))
 (63 63 (:REWRITE DEFAULT-+-1))
 (54 54 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (51 51 (:REWRITE SUBSETP-MEMBER . 2))
 (51 51 (:REWRITE SUBSETP-MEMBER . 1))
 (42 42 (:REWRITE BACKREF-INTS))
 (19 19 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (18 18 (:TYPE-PRESCRIPTION INDEXP))
 (5 5 (:TYPE-PRESCRIPTION MIN))
 (2 2 (:LINEAR LENGTH-EQUIV-LINEAR))
 (1 1 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(MIN-IDX-IL-TYPE
 (200 40 (:DEFINITION LEN))
 (80 40 (:REWRITE DEFAULT-+-2))
 (71 71 (:REWRITE DEFAULT-CDR))
 (64 36 (:REWRITE DEFAULT-<-1))
 (56 56 (:REWRITE DEFAULT-CAR))
 (54 36 (:REWRITE DEFAULT-<-2))
 (44 44 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (40 40 (:REWRITE DEFAULT-+-1))
 (20 20 (:REWRITE DEFAULT-COERCE-2))
 (20 20 (:REWRITE DEFAULT-COERCE-1))
 (12 12 (:REWRITE INPUT-LISTP-PSEUDO))
 (4 4 (:REWRITE INPUT-LIST-ELTP-THM))
 (2 2 (:REWRITE BACKREF-INTS))
 )
(MIN-IDX-IL-LTE-CAR
 (72 12 (:REWRITE DEFAULT-<-2))
 (34 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (21 1 (:DEFINITION PSEUDO-BACKREF-LISTP))
 (18 12 (:REWRITE DEFAULT-<-1))
 (17 17 (:REWRITE DEFAULT-CAR))
 (16 2 (:DEFINITION LENGTH))
 (13 1 (:DEFINITION PSEUDO-BACKREFP))
 (10 10 (:REWRITE DEFAULT-CDR))
 (10 2 (:DEFINITION LEN))
 (6 6 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (4 2 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (3 3 (:REWRITE INPUT-LISTP-PSEUDO))
 (3 3 (:REWRITE BACKREF-LISTP-PSEUDO))
 (2 2 (:TYPE-PRESCRIPTION LEN))
 (2 2 (:REWRITE INPUT-LIST-ELTP-THM))
 (2 2 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE DEFAULT-COERCE-1))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE BACKREF-INTS))
 (1 1 (:REWRITE BACKREFP-PSEUDO))
 )
(MIN-IDX-IL-MAX
 (730 365 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (285 16 (:REWRITE DEFAULT-<-2))
 (148 22 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (100 20 (:DEFINITION LEN))
 (40 20 (:REWRITE DEFAULT-+-2))
 (35 16 (:REWRITE DEFAULT-<-1))
 (25 25 (:REWRITE DEFAULT-CDR))
 (20 20 (:REWRITE DEFAULT-+-1))
 (14 14 (:REWRITE DEFAULT-CAR))
 (10 10 (:REWRITE DEFAULT-COERCE-2))
 (10 10 (:REWRITE DEFAULT-COERCE-1))
 )
(MEMBER-MIN-IDX
 (868 434 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (353 21 (:REWRITE DEFAULT-<-2))
 (194 38 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (150 30 (:DEFINITION LEN))
 (60 30 (:REWRITE DEFAULT-+-2))
 (42 42 (:REWRITE DEFAULT-CDR))
 (30 30 (:REWRITE DEFAULT-+-1))
 (17 11 (:REWRITE SUBSETP-MEMBER . 3))
 (15 15 (:REWRITE DEFAULT-COERCE-2))
 (15 15 (:REWRITE DEFAULT-COERCE-1))
 (11 11 (:REWRITE SUBSETP-MEMBER . 4))
 (11 11 (:REWRITE SUBSETP-MEMBER . 2))
 (11 11 (:REWRITE SUBSETP-MEMBER . 1))
 (11 11 (:REWRITE INTERSECTP-MEMBER . 3))
 (11 11 (:REWRITE INTERSECTP-MEMBER . 2))
 (2 2 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (2 2 (:LINEAR LENGTH-EQUIV-LINEAR))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 (1 1 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(INTEGERP-NUMBERP)
(MIN-IDX-APPEND
 (5975 130 (:REWRITE DEFAULT-<-2))
 (5819 230 (:REWRITE INTEGERP-NUMBERP))
 (4701 114 (:REWRITE MIN-IDX-IL-TYPE))
 (3329 114 (:REWRITE MEMBER-MIN-IDX))
 (1987 114 (:DEFINITION MEMBER-EQUAL))
 (1868 934 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (1784 224 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1554 101 (:REWRITE SUBSETP-APPEND1))
 (1535 178 (:REWRITE SUBSETP-CAR-MEMBER))
 (1532 25 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (958 130 (:REWRITE DEFAULT-<-1))
 (954 754 (:REWRITE SUBSETP-TRANS2))
 (934 934 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (934 934 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (754 754 (:REWRITE SUBSETP-TRANS))
 (660 132 (:DEFINITION LEN))
 (644 635 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (595 411 (:REWRITE DEFAULT-CDR))
 (570 570 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (464 25 (:REWRITE PSEUDO-INPUT-LISTP-OF-APPEND))
 (415 409 (:REWRITE DEFAULT-CAR))
 (275 50 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (264 132 (:REWRITE DEFAULT-+-2))
 (228 228 (:REWRITE SUBSETP-MEMBER . 2))
 (228 228 (:REWRITE SUBSETP-MEMBER . 1))
 (217 217 (:REWRITE INPUT-LISTP-PSEUDO))
 (164 116 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (132 132 (:REWRITE DEFAULT-COERCE-2))
 (132 132 (:REWRITE DEFAULT-COERCE-1))
 (132 132 (:REWRITE DEFAULT-+-1))
 (114 114 (:REWRITE INPUT-LIST-ELTP-THM))
 (114 114 (:REWRITE BACKREF-INTS))
 (80 10 (:REWRITE COMMUTATIVITY-OF-APPEND-UNDER-SET-EQUIV))
 (48 48 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (33 33 (:LINEAR MEMBER-MIN-IDX))
 (26 26 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (4 4 (:LINEAR LENGTH-EQUIV-LINEAR))
 (2 2 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(LONGEST-IL
 (546 26 (:DEFINITION PSEUDO-BACKREF-LISTP))
 (338 26 (:DEFINITION PSEUDO-BACKREFP))
 (271 93 (:REWRITE INTEGERP-NUMBERP))
 (266 266 (:REWRITE DEFAULT-CDR))
 (194 194 (:REWRITE INPUT-LIST-ELTP-THM))
 (165 165 (:REWRITE BACKREF-INTS))
 (99 46 (:REWRITE DEFAULT-+-2))
 (93 93 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (78 78 (:REWRITE BACKREF-LISTP-PSEUDO))
 (65 46 (:REWRITE DEFAULT-+-1))
 (41 41 (:REWRITE INPUT-LISTP-PSEUDO))
 (36 36 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (32 8 (:REWRITE COMMUTATIVITY-OF-+))
 (32 8 (:DEFINITION INTEGER-ABS))
 (32 4 (:DEFINITION LENGTH))
 (30 3 (:REWRITE ACL2-COUNT-WHEN-MEMBER))
 (26 26 (:REWRITE BACKREFP-PSEUDO))
 (20 4 (:DEFINITION LEN))
 (18 3 (:DEFINITION MEMBER-EQUAL))
 (15 15 (:REWRITE FOLD-CONSTS-IN-+))
 (8 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 8 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 (4 4 (:TYPE-PRESCRIPTION LEN))
 (4 4 (:REWRITE DEFAULT-REALPART))
 (4 4 (:REWRITE DEFAULT-NUMERATOR))
 (4 4 (:REWRITE DEFAULT-IMAGPART))
 (4 4 (:REWRITE DEFAULT-DENOMINATOR))
 (4 4 (:REWRITE DEFAULT-COERCE-2))
 (4 4 (:REWRITE DEFAULT-COERCE-1))
 (3 3 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (3 3 (:REWRITE MEMBER-SELF))
 (2 2 (:LINEAR ACL2-COUNT-CAR-CDR-LINEAR))
 )
(LONGEST-IL-TYPE-WEAK
 (284 96 (:REWRITE INTEGERP-NUMBERP))
 (268 104 (:REWRITE DEFAULT-<-2))
 (211 211 (:REWRITE DEFAULT-CDR))
 (157 157 (:REWRITE INPUT-LIST-ELTP-THM))
 (142 142 (:REWRITE BACKREF-INTS))
 (96 96 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (51 51 (:REWRITE BACKREF-LISTP-PSEUDO))
 (25 25 (:REWRITE INPUT-LISTP-PSEUDO))
 (23 23 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (17 17 (:REWRITE BACKREFP-PSEUDO))
 )
(LONGEST-IL-TYPE-STRONG
 (2920 1460 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (2862 22 (:DEFINITION BACKREF-LISTP))
 (1390 22 (:DEFINITION BACKREFP))
 (1276 38 (:DEFINITION MEMBER-EQUAL))
 (1136 176 (:REWRITE DEFAULT-<-2))
 (1086 371 (:REWRITE DEFAULT-CAR))
 (861 87 (:REWRITE INTEGERP-NUMBERP))
 (476 383 (:REWRITE DEFAULT-CDR))
 (390 78 (:DEFINITION LEN))
 (380 176 (:REWRITE DEFAULT-<-1))
 (296 296 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (156 78 (:REWRITE DEFAULT-+-2))
 (148 148 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (83 83 (:REWRITE BACKREF-INTS))
 (78 78 (:REWRITE DEFAULT-COERCE-2))
 (78 78 (:REWRITE DEFAULT-COERCE-1))
 (78 78 (:REWRITE DEFAULT-+-1))
 (76 76 (:REWRITE SUBSETP-MEMBER . 2))
 (76 76 (:REWRITE SUBSETP-MEMBER . 1))
 (39 39 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (12 12 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (4 4 (:LINEAR LENGTH-EQUIV-LINEAR))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 (2 2 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(LONGEST-IL-MAX-LEN
 (2470 1235 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (545 37 (:REWRITE DEFAULT-<-2))
 (482 54 (:REWRITE LONGEST-IL-TYPE-WEAK))
 (440 91 (:REWRITE DEFAULT-CAR))
 (439 48 (:REWRITE INTEGERP-NUMBERP))
 (188 52 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (114 37 (:REWRITE DEFAULT-<-1))
 (106 106 (:REWRITE INPUT-LISTP-PSEUDO))
 (104 104 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (85 17 (:DEFINITION LEN))
 (61 61 (:REWRITE DEFAULT-CDR))
 (52 52 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (34 17 (:REWRITE DEFAULT-+-2))
 (21 21 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (21 21 (:REWRITE INPUT-LIST-ELTP-THM))
 (21 21 (:REWRITE BACKREF-INTS))
 (17 17 (:REWRITE DEFAULT-COERCE-2))
 (17 17 (:REWRITE DEFAULT-COERCE-1))
 (17 17 (:REWRITE DEFAULT-+-1))
 (10 10 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (4 4 (:LINEAR LENGTH-EQUIV-LINEAR))
 (2 2 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(LONGEST-IL-MIN-LEN
 (888 444 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (744 372 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (436 18 (:REWRITE DEFAULT-<-2))
 (351 36 (:REWRITE INTEGERP-NUMBERP))
 (260 12 (:REWRITE MEMBER-MIN-IDX))
 (197 18 (:REWRITE DEFAULT-<-1))
 (167 55 (:REWRITE DEFAULT-CAR))
 (143 12 (:DEFINITION MEMBER-EQUAL))
 (108 16 (:REWRITE SUBSETP-CAR-MEMBER))
 (97 15 (:REWRITE LONGEST-IL-TYPE-WEAK))
 (96 18 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (90 12 (:REWRITE MIN-IDX-IL-TYPE))
 (52 52 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (51 17 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (43 43 (:REWRITE INPUT-LISTP-PSEUDO))
 (38 38 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (35 7 (:DEFINITION LEN))
 (31 31 (:REWRITE DEFAULT-CDR))
 (22 22 (:REWRITE SUBSETP-MEMBER . 2))
 (22 22 (:REWRITE SUBSETP-MEMBER . 1))
 (19 19 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (16 16 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (16 16 (:REWRITE SUBSETP-TRANS2))
 (16 16 (:REWRITE SUBSETP-TRANS))
 (16 16 (:REWRITE INPUT-LIST-ELTP-THM))
 (16 16 (:REWRITE BACKREF-INTS))
 (14 14 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (14 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-COERCE-2))
 (7 7 (:REWRITE DEFAULT-COERCE-1))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:LINEAR MEMBER-MIN-IDX))
 (4 4 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 )
(LONGEST-IL-GREATER-COMPARE-TO-MIN
 (88 88 (:TYPE-PRESCRIPTION PSEUDO-INPUT-LISTP))
 (88 44 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (74 37 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (62 1 (:DEFINITION MIN-IDX-IL))
 (58 1 (:DEFINITION MIN))
 (51 1 (:DEFINITION LONGEST-IL))
 (38 2 (:REWRITE DEFAULT-<-2))
 (34 4 (:REWRITE INTEGERP-NUMBERP))
 (29 9 (:REWRITE DEFAULT-CAR))
 (27 1 (:REWRITE MEMBER-MIN-IDX))
 (21 3 (:REWRITE LONGEST-IL-TYPE-WEAK))
 (15 1 (:DEFINITION MEMBER-EQUAL))
 (14 2 (:REWRITE SUBSETP-CAR-MEMBER))
 (10 2 (:REWRITE DEFAULT-<-1))
 (9 3 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (9 1 (:REWRITE MIN-IDX-IL-TYPE))
 (7 7 (:REWRITE INPUT-LISTP-PSEUDO))
 (6 6 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (5 5 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (4 4 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (4 4 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (2 2 (:REWRITE INPUT-LIST-ELTP-THM))
 (2 2 (:REWRITE BACKREF-INTS))
 )
(REMOVE-ALL-LONGER-EQUAL-FN)
(REMOVE-ALL-LONGER-EQUAL-IL
 (3 3 (:REWRITE INPUT-LISTP-PSEUDO))
 (2 2 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-CAR))
 )
(REMOVE-ALL-LONGER-EQUAL-SHORTER
 (2012 87 (:REWRITE DEFAULT-<-2))
 (1380 91 (:REWRITE INTEGERP-NUMBERP))
 (931 33 (:REWRITE MIN-IDX-IL-TYPE))
 (774 25 (:REWRITE MEMBER-MIN-IDX))
 (627 21 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (426 26 (:DEFINITION MEMBER-EQUAL))
 (386 50 (:REWRITE SUBSETP-CAR-MEMBER))
 (384 90 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (352 10 (:LINEAR LONGEST-IL-MIN-LEN))
 (257 1 (:REWRITE INPUT-LISTP-OF-CONS))
 (234 18 (:REWRITE COMMUTATIVITY-OF-APPEND-UNDER-SET-EQUIV))
 (230 1 (:DEFINITION INPUT-LIST-ELTP))
 (225 45 (:DEFINITION LEN))
 (202 87 (:REWRITE DEFAULT-<-1))
 (198 188 (:REWRITE DEFAULT-CAR))
 (193 178 (:REWRITE DEFAULT-CDR))
 (187 69 (:REWRITE INPUT-LIST-ELTP-THM))
 (174 30 (:DEFINITION BINARY-APPEND))
 (170 2 (:DEFINITION BACKREF-LISTP))
 (151 124 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (129 8 (:DEFINITION INDEXP))
 (125 125 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (118 58 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (114 2 (:DEFINITION BACKREFP))
 (109 4 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (108 108 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (90 45 (:REWRITE DEFAULT-+-2))
 (88 55 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (81 4 (:REWRITE PSEUDO-INPUT-LISTP-OF-APPEND))
 (62 62 (:REWRITE INPUT-LISTP-PSEUDO))
 (62 62 (:REWRITE BACKREF-INTS))
 (56 53 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (55 55 (:REWRITE SUBSETP-TRANS2))
 (55 55 (:REWRITE SUBSETP-TRANS))
 (52 52 (:REWRITE SUBSETP-MEMBER . 2))
 (52 52 (:REWRITE SUBSETP-MEMBER . 1))
 (47 14 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (45 45 (:REWRITE DEFAULT-COERCE-2))
 (45 45 (:REWRITE DEFAULT-COERCE-1))
 (45 45 (:REWRITE DEFAULT-+-1))
 (38 1 (:REWRITE MEMBER-OF-APPEND))
 (36 36 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (32 32 (:REWRITE INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (26 5 (:DEFINITION NATP))
 (22 22 (:TYPE-PRESCRIPTION INPUT-LISTP))
 (22 2 (:REWRITE INPUT-LISTP-OF-APPEND))
 (18 2 (:REWRITE MIN-IDX-APPEND))
 (14 14 (:TYPE-PRESCRIPTION BACKREF-LISTP))
 (14 1 (:REWRITE SUBSETP-OF-APPEND-WHEN-SUBSET-OF-EITHER))
 (12 12 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (10 10 (:LINEAR MEMBER-MIN-IDX))
 (10 4 (:REWRITE CONSP-OF-APPEND))
 (8 8 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (8 2 (:REWRITE CAR-OF-APPEND))
 (6 1 (:REWRITE INPUT-LIST-ELTP-OF-CAR-WHEN-INPUT-LISTP))
 (3 3 (:TYPE-PRESCRIPTION INDEXP))
 (2 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (2 2 (:LINEAR LENGTH-EQUIV-LINEAR))
 (1 1 (:LINEAR LONGEST-IL-MAX-LEN))
 (1 1 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(REMOVE-ALL-LONGER-EQUAL-IL-IL
 (70 70 (:TYPE-PRESCRIPTION REMOVE-ALL-LONGER-EQUAL-IL))
 (35 7 (:REWRITE DEFAULT-<-2))
 (35 5 (:DEFINITION BINARY-APPEND))
 (33 15 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (33 2 (:REWRITE SUBSETP-APPEND1))
 (29 21 (:REWRITE SUBSETP-TRANS2))
 (28 14 (:REWRITE INTEGERP-NUMBERP))
 (27 15 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (25 10 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (21 21 (:REWRITE SUBSETP-TRANS))
 (21 7 (:REWRITE DEFAULT-<-1))
 (20 20 (:REWRITE DEFAULT-CAR))
 (14 14 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (12 12 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (7 7 (:REWRITE INPUT-LIST-ELTP-THM))
 (7 7 (:REWRITE BACKREF-INTS))
 )
(REMOVE-ALL-LONGER-EQUAL-IL-PSEUDO
 (56 56 (:TYPE-PRESCRIPTION REMOVE-ALL-LONGER-EQUAL-IL))
 (33 2 (:REWRITE SUBSETP-APPEND1))
 (28 13 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (28 4 (:DEFINITION BINARY-APPEND))
 (26 18 (:REWRITE SUBSETP-TRANS2))
 (25 5 (:REWRITE DEFAULT-<-2))
 (22 13 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (20 10 (:REWRITE INTEGERP-NUMBERP))
 (20 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (18 18 (:REWRITE SUBSETP-TRANS))
 (15 15 (:REWRITE DEFAULT-CAR))
 (15 5 (:REWRITE DEFAULT-<-1))
 (14 14 (:REWRITE INPUT-LISTP-PSEUDO))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (9 9 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (5 5 (:REWRITE INPUT-LIST-ELTP-THM))
 (5 5 (:REWRITE BACKREF-INTS))
 )