(IN-CHARSET-ELT
 (14 14 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-CHAR-CODE))
 )
(IN-CHARSET
 (15 15 (:REWRITE DEFAULT-CDR))
 (11 11 (:REWRITE DEFAULT-CAR))
 )
(STORE-BACKREFS)
(STORE-BACKREFS-INPUT-LIST
 (2888 1444 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (1385 4 (:DEFINITION BACKREF-LISTP))
 (1308 72 (:DEFINITION MEMBER-EQUAL))
 (1142 34 (:REWRITE MEMBER-MIN-IDX))
 (831 115 (:REWRITE DEFAULT-<-2))
 (826 81 (:REWRITE INTEGERP-NUMBERP))
 (545 115 (:REWRITE DEFAULT-<-1))
 (475 43 (:REWRITE MIN-IDX-IL-TYPE))
 (370 304 (:REWRITE DEFAULT-CAR))
 (272 245 (:REWRITE DEFAULT-CDR))
 (252 36 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (229 55 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (206 158 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (183 15 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (180 180 (:REWRITE SUBSETP-TRANS2))
 (180 180 (:REWRITE SUBSETP-TRANS))
 (178 3 (:REWRITE INPUT-LIST-ELTP-OF-CAR-WHEN-INPUT-LISTP))
 (161 23 (:DEFINITION UPDATE-NTH))
 (158 158 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (144 144 (:REWRITE SUBSETP-MEMBER . 2))
 (144 144 (:REWRITE SUBSETP-MEMBER . 1))
 (118 5 (:REWRITE SUBSETP-OF-CONS))
 (110 110 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (106 2 (:REWRITE INPUT-LISTP-OF-UPDATE-NTH))
 (98 98 (:REWRITE INPUT-LISTP-PSEUDO))
 (86 38 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (67 67 (:REWRITE BACKREF-INTS))
 (55 55 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (38 2 (:REWRITE INPUT-LISTP-OF-CDR-WHEN-INPUT-LISTP))
 (26 26 (:LINEAR LENGTH-EQUIV-LINEAR))
 (23 23 (:REWRITE ZP-OPEN))
 (23 23 (:REWRITE DEFAULT-+-2))
 (23 23 (:REWRITE DEFAULT-+-1))
 (14 14 (:LINEAR MEMBER-MIN-IDX))
 (14 14 (:LINEAR LONGEST-IL-MIN-LEN))
 (13 13 (:LINEAR LONGEST-IL-MAX-LEN))
 (13 13 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(STORE-BACKREFS-PSEUDO-IL
 (173 5 (:DEFINITION PSEUDO-BACKREF-LISTP))
 (102 81 (:REWRITE DEFAULT-CAR))
 (99 78 (:REWRITE DEFAULT-CDR))
 (91 13 (:DEFINITION UPDATE-NTH))
 (56 4 (:DEFINITION MEMBER-EQUAL))
 (47 2 (:REWRITE SUBSETP-OF-CONS))
 (46 38 (:REWRITE DEFAULT-<-1))
 (38 38 (:REWRITE DEFAULT-<-2))
 (38 2 (:REWRITE PSEUDO-INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-PSEUDO-INPUT-LISTP))
 (25 25 (:REWRITE INPUT-LISTP-PSEUDO))
 (24 24 (:REWRITE SUBSETP-TRANS2))
 (24 24 (:REWRITE SUBSETP-TRANS))
 (22 22 (:REWRITE INPUT-LIST-ELTP-THM))
 (21 21 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (20 20 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (20 20 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (17 17 (:REWRITE BACKREF-INTS))
 (15 15 (:REWRITE BACKREF-LISTP-PSEUDO))
 (13 13 (:REWRITE ZP-OPEN))
 (13 13 (:REWRITE DEFAULT-+-2))
 (13 13 (:REWRITE DEFAULT-+-1))
 (9 9 (:REWRITE BACKREFP-PSEUDO))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (6 2 (:REWRITE INTEGERP-NUMBERP))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1 1 (:REWRITE INPUT-LIST-ELTP-PSEUDO))
 )
(STORE-BACKREFS
 (3108 279 (:REWRITE DEFAULT-<-2))
 (2653 259 (:REWRITE INTEGERP-NUMBERP))
 (2374 700 (:REWRITE DEFAULT-CAR))
 (2056 1028 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (1788 200 (:REWRITE LONGEST-IL-TYPE-WEAK))
 (1479 47 (:REWRITE MEMBER-MIN-IDX))
 (1014 270 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (999 279 (:REWRITE DEFAULT-<-1))
 (919 58 (:DEFINITION MEMBER-EQUAL))
 (910 100 (:REWRITE SUBSETP-CAR-MEMBER))
 (714 77 (:REWRITE MIN-IDX-IL-TYPE))
 (547 547 (:REWRITE INPUT-LISTP-PSEUDO))
 (540 540 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (400 103 (:REWRITE INPUT-LIST-ELTP-THM))
 (376 376 (:REWRITE DEFAULT-CDR))
 (291 291 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (270 270 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (210 30 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (182 20 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (150 102 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (136 136 (:REWRITE SUBSETP-TRANS2))
 (136 136 (:REWRITE SUBSETP-TRANS))
 (133 133 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (133 133 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (116 116 (:REWRITE SUBSETP-MEMBER . 2))
 (116 116 (:REWRITE SUBSETP-MEMBER . 1))
 (91 91 (:REWRITE BACKREF-INTS))
 (36 6 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (36 3 (:REWRITE INPUT-LIST-ELTP-OF-CAR-WHEN-INPUT-LISTP))
 (32 32 (:LINEAR LENGTH-EQUIV-LINEAR))
 (27 3 (:DEFINITION TRUE-LISTP))
 (20 20 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (17 1 (:REWRITE SUBSETP-OF-CONS))
 (16 16 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (14 14 (:LINEAR MEMBER-MIN-IDX))
 (12 12 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (12 12 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (12 6 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (6 6 (:TYPE-PRESCRIPTION SET::EMPTYP-TYPE))
 (6 6 (:REWRITE SET::IN-SET))
 )
(STORE-BACKREFS-MIN-IDX
 (598 299 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (348 8 (:REWRITE DEFAULT-<-2))
 (260 16 (:REWRITE INTEGERP-NUMBERP))
 (216 8 (:REWRITE MEMBER-MIN-IDX))
 (180 8 (:REWRITE MIN-IDX-IL-TYPE))
 (124 10 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (120 8 (:DEFINITION MEMBER-EQUAL))
 (112 16 (:REWRITE SUBSETP-CAR-MEMBER))
 (64 16 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (47 44 (:REWRITE DEFAULT-CAR))
 (44 44 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (42 4 (:REWRITE STORE-BACKREFS-PSEUDO-IL))
 (40 40 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (40 8 (:REWRITE DEFAULT-<-1))
 (35 5 (:DEFINITION UPDATE-NTH))
 (34 34 (:REWRITE DEFAULT-CDR))
 (32 32 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (22 22 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (22 22 (:REWRITE INPUT-LISTP-PSEUDO))
 (16 16 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (16 16 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (16 16 (:REWRITE SUBSETP-TRANS2))
 (16 16 (:REWRITE SUBSETP-TRANS))
 (16 16 (:REWRITE SUBSETP-MEMBER . 2))
 (16 16 (:REWRITE SUBSETP-MEMBER . 1))
 (8 8 (:REWRITE INPUT-LIST-ELTP-THM))
 (8 8 (:REWRITE BACKREF-INTS))
 (5 5 (:REWRITE ZP-OPEN))
 (5 5 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR MEMBER-MIN-IDX))
 (2 2 (:LINEAR LONGEST-IL-MIN-LEN))
 (2 1 (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH))
 (1 1 (:TYPE-PRESCRIPTION UPDATE-NTH))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 )
(CHECK-BACKREF
 (42 25 (:REWRITE DEFAULT-<-1))
 (25 25 (:REWRITE DEFAULT-<-2))
 (25 6 (:REWRITE INPUT-LIST-ELTP-THM))
 (20 20 (:TYPE-PRESCRIPTION TRUE-LISTP-SUBSEQ-TYPE-PRESCRIPTION))
 (20 20 (:TYPE-PRESCRIPTION STRINGP-SUBSEQ-TYPE-PRESCRIPTION))
 (14 14 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-CAR))
 (10 1 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (8 1 (:DEFINITION INPUT-LIST-ELTP))
 (3 3 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (2 2 (:REWRITE BACKREF-INTS))
 (2 2 (:LINEAR LENGTH-EQUIV-LINEAR))
 (2 2 (:DEFINITION BACKREF-LISTP))
 (1 1 (:TYPE-PRESCRIPTION BACKREF-LISTP))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE DEFAULT-UNARY-MINUS))
 (1 1 (:LINEAR LONGEST-IL-MAX-LEN))
 (1 1 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(CHECK-BACKREF-INDEXP
 (320 16 (:REWRITE TAKE-OF-TOO-MANY))
 (256 32 (:DEFINITION LEN))
 (240 160 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (240 16 (:REWRITE TAKE-OF-LEN-FREE))
 (208 208 (:TYPE-PRESCRIPTION LEN))
 (121 89 (:REWRITE DEFAULT-+-2))
 (96 60 (:REWRITE DEFAULT-CDR))
 (89 89 (:REWRITE DEFAULT-+-1))
 (88 16 (:REWRITE TAKE-WHEN-ATOM))
 (82 66 (:REWRITE DEFAULT-<-2))
 (80 80 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (76 8 (:DEFINITION NTHCDR))
 (74 66 (:REWRITE DEFAULT-<-1))
 (56 20 (:REWRITE DEFAULT-CAR))
 (48 16 (:DEFINITION NFIX))
 (44 4 (:REWRITE DEFAULT-COERCE-3))
 (32 4 (:REWRITE CONSP-OF-TAKE))
 (24 5 (:REWRITE INPUT-LIST-ELTP-THM))
 (23 23 (:REWRITE FOLD-CONSTS-IN-+))
 (16 16 (:TYPE-PRESCRIPTION NFIX))
 (11 11 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 1 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (8 8 (:REWRITE DEFAULT-COERCE-2))
 (8 1 (:DEFINITION INPUT-LIST-ELTP))
 (4 4 (:REWRITE DEFAULT-COERCE-1))
 (3 3 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (2 2 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (2 2 (:REWRITE BACKREF-INTS))
 (2 2 (:LINEAR LENGTH-EQUIV-LINEAR))
 (2 2 (:DEFINITION BACKREF-LISTP))
 (1 1 (:TYPE-PRESCRIPTION BACKREF-LISTP))
 (1 1 (:LINEAR LONGEST-IL-MAX-LEN))
 (1 1 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(CHECK-BACKREF-GREATER
 (320 16 (:REWRITE TAKE-OF-TOO-MANY))
 (256 32 (:DEFINITION LEN))
 (240 160 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (240 16 (:REWRITE TAKE-OF-LEN-FREE))
 (208 208 (:TYPE-PRESCRIPTION LEN))
 (121 89 (:REWRITE DEFAULT-+-2))
 (96 60 (:REWRITE DEFAULT-CDR))
 (89 89 (:REWRITE DEFAULT-+-1))
 (88 16 (:REWRITE TAKE-WHEN-ATOM))
 (80 80 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (80 64 (:REWRITE DEFAULT-<-2))
 (76 8 (:DEFINITION NTHCDR))
 (70 64 (:REWRITE DEFAULT-<-1))
 (56 20 (:REWRITE DEFAULT-CAR))
 (48 16 (:DEFINITION NFIX))
 (44 4 (:REWRITE DEFAULT-COERCE-3))
 (32 4 (:REWRITE CONSP-OF-TAKE))
 (24 5 (:REWRITE INPUT-LIST-ELTP-THM))
 (23 23 (:REWRITE FOLD-CONSTS-IN-+))
 (16 16 (:TYPE-PRESCRIPTION NFIX))
 (11 11 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 1 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (8 8 (:REWRITE DEFAULT-COERCE-2))
 (8 1 (:DEFINITION INPUT-LIST-ELTP))
 (4 4 (:REWRITE DEFAULT-COERCE-1))
 (3 3 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (2 2 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (2 2 (:REWRITE BACKREF-INTS))
 (2 2 (:LINEAR LENGTH-EQUIV-LINEAR))
 (2 2 (:DEFINITION BACKREF-LISTP))
 (1 1 (:TYPE-PRESCRIPTION BACKREF-LISTP))
 (1 1 (:LINEAR LONGEST-IL-MAX-LEN))
 (1 1 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(RUN-REGEX-MEASURE)
(RUN-REGEX-LIST-MEASURE
 (6 3 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (3 3 (:TYPE-PRESCRIPTION PSEUDO-INPUT-LISTP))
 )
(RUN-REPEAT-MEASURE)
(RUN-REPEAT-LIST-MEASURE
 (6 3 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (3 3 (:TYPE-PRESCRIPTION PSEUDO-INPUT-LISTP))
 )
(REG-STR-BR-GUARD)
(REG-ILIST-GUARD)
(REPEAT-GUARD)
(INTEGERP-+)
(INTEGERP--)
(O-P-RUN-REGEX-MEASURE
 (31 1 (:DEFINITION REGEX-MEASURE))
 (27 13 (:REWRITE DEFAULT-+-2))
 (25 18 (:REWRITE DEFAULT-CAR))
 (16 13 (:REWRITE DEFAULT-+-1))
 (10 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 6 (:REWRITE DEFAULT-CDR))
 (4 2 (:REWRITE INTEGERP-+))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:REWRITE INTEGERP-NUMBERP))
 (2 2 (:REWRITE INTEGERP--))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (1 1 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (1 1 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (1 1 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (1 1 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (1 1 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 )
(O-P-RUN-REGEX-LIST-MEASURE
 (312 4 (:DEFINITION MIN-IDX-IL))
 (296 4 (:DEFINITION MIN))
 (226 113 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (152 12 (:REWRITE INTEGERP-NUMBERP))
 (142 6 (:REWRITE DEFAULT-<-2))
 (137 137 (:TYPE-PRESCRIPTION PSEUDO-INPUT-LISTP))
 (112 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (108 4 (:REWRITE MEMBER-MIN-IDX))
 (86 10 (:REWRITE MIN-IDX-IL-TYPE))
 (60 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (60 4 (:DEFINITION MEMBER-EQUAL))
 (56 30 (:REWRITE DEFAULT-CAR))
 (56 8 (:REWRITE SUBSETP-CAR-MEMBER))
 (40 15 (:REWRITE DEFAULT-+-2))
 (32 2 (:REWRITE INTEGERP-+))
 (31 1 (:DEFINITION REGEX-MEASURE))
 (28 4 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (25 17 (:REWRITE DEFAULT-CDR))
 (24 24 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (22 6 (:REWRITE DEFAULT-<-1))
 (21 15 (:REWRITE DEFAULT-+-1))
 (20 20 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (16 16 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (16 2 (:REWRITE INTEGERP--))
 (15 3 (:DEFINITION LEN))
 (12 12 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (12 12 (:REWRITE INPUT-LISTP-PSEUDO))
 (8 8 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (8 8 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (8 8 (:REWRITE SUBSETP-TRANS2))
 (8 8 (:REWRITE SUBSETP-TRANS))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (4 4 (:REWRITE INPUT-LIST-ELTP-THM))
 (4 4 (:REWRITE BACKREF-INTS))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (1 1 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (1 1 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (1 1 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (1 1 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (1 1 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 )
(O-P-RUN-REPEAT-MEASURE
 (35 28 (:REWRITE DEFAULT-CAR))
 (31 1 (:DEFINITION REGEX-MEASURE))
 (30 16 (:REWRITE DEFAULT-+-2))
 (19 16 (:REWRITE DEFAULT-+-1))
 (11 9 (:REWRITE DEFAULT-CDR))
 (10 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (5 5 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-<-1))
 (4 2 (:REWRITE INTEGERP-+))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:REWRITE INTEGERP-NUMBERP))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE INTEGERP--))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (1 1 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (1 1 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (1 1 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (1 1 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (1 1 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 )
(O-P-RUN-REPEAT-LIST-MEASURE
 (312 4 (:DEFINITION MIN-IDX-IL))
 (296 4 (:DEFINITION MIN))
 (226 113 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (152 12 (:REWRITE INTEGERP-NUMBERP))
 (145 9 (:REWRITE DEFAULT-<-2))
 (137 137 (:TYPE-PRESCRIPTION PSEUDO-INPUT-LISTP))
 (112 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (108 4 (:REWRITE MEMBER-MIN-IDX))
 (86 10 (:REWRITE MIN-IDX-IL-TYPE))
 (72 40 (:REWRITE DEFAULT-CAR))
 (60 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (60 4 (:DEFINITION MEMBER-EQUAL))
 (56 8 (:REWRITE SUBSETP-CAR-MEMBER))
 (45 19 (:REWRITE DEFAULT-+-2))
 (32 2 (:REWRITE INTEGERP-+))
 (31 21 (:REWRITE DEFAULT-CDR))
 (31 1 (:DEFINITION REGEX-MEASURE))
 (28 4 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (25 19 (:REWRITE DEFAULT-+-1))
 (25 9 (:REWRITE DEFAULT-<-1))
 (24 24 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (20 20 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (20 4 (:DEFINITION LEN))
 (16 16 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (16 2 (:REWRITE INTEGERP--))
 (12 12 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (12 12 (:REWRITE INPUT-LISTP-PSEUDO))
 (8 8 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (8 8 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (8 8 (:REWRITE SUBSETP-TRANS2))
 (8 8 (:REWRITE SUBSETP-TRANS))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (4 4 (:REWRITE INPUT-LIST-ELTP-THM))
 (4 4 (:REWRITE BACKREF-INTS))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (1 1 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (1 1 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (1 1 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (1 1 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (1 1 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 )
(RUN-REGEX
 (11847 958 (:REWRITE DEFAULT-<-2))
 (11248 1126 (:REWRITE INTEGERP-NUMBERP))
 (9943 305 (:REWRITE MEMBER-MIN-IDX))
 (6020 620 (:REWRITE SUBSETP-CAR-MEMBER))
 (5646 326 (:DEFINITION MEMBER-EQUAL))
 (5254 2657 (:REWRITE DEFAULT-CAR))
 (4010 1890 (:REWRITE DEFAULT-+-2))
 (3082 398 (:REWRITE DEFAULT-UNARY-MINUS))
 (2884 958 (:REWRITE DEFAULT-<-1))
 (2619 249 (:REWRITE LONGEST-IL-TYPE-WEAK))
 (2482 1890 (:REWRITE DEFAULT-+-1))
 (2226 1113 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (2120 1879 (:REWRITE DEFAULT-CDR))
 (1854 1854 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (1807 667 (:REWRITE INPUT-LIST-ELTP-THM))
 (1680 240 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1633 1633 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1603 743 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1536 72 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-IL))
 (927 927 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (874 874 (:REWRITE SUBSETP-TRANS2))
 (874 874 (:REWRITE SUBSETP-TRANS))
 (865 865 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (865 865 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (652 652 (:REWRITE SUBSETP-MEMBER . 2))
 (652 652 (:REWRITE SUBSETP-MEMBER . 1))
 (594 594 (:REWRITE BACKREF-INTS))
 (576 72 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-FN))
 (468 36 (:REWRITE COMMUTATIVITY-OF-APPEND-UNDER-SET-EQUIV))
 (444 72 (:DEFINITION BINARY-APPEND))
 (412 126 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (256 40 (:REWRITE REMOVE-ALL-LONGER-EQUAL-IL-PSEUDO))
 (253 253 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 (252 144 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (202 202 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (168 168 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (168 168 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (168 96 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (163 163 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (163 163 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (150 20 (:REWRITE INPUT-LIST-ELTP-OF-CAR-WHEN-INPUT-LISTP))
 (135 45 (:REWRITE R-REPEAT-NOT-REGEX))
 (135 45 (:REWRITE R-GROUP-NOT-REGEX))
 (135 45 (:REWRITE R-EXACT-NOT-REGEX))
 (135 45 (:REWRITE R-DISJUNCT-NOT-REGEX))
 (135 45 (:REWRITE R-CONCAT-NOT-REGEX))
 (135 45 (:REWRITE R-CHARSET-NOT-REGEX))
 (135 45 (:REWRITE R-BACKREF-NOT-REGEX))
 (86 86 (:REWRITE DEFAULT-*-2))
 (86 86 (:REWRITE DEFAULT-*-1))
 (80 80 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (78 78 (:LINEAR LENGTH-EQUIV-LINEAR))
 (74 74 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (69 21 (:LINEAR LONGEST-IL-GREATER-COMPARE-TO-MIN))
 (66 66 (:LINEAR MEMBER-MIN-IDX))
 (51 3 (:REWRITE SUBSETP-OF-CONS))
 (39 39 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (24 4 (:REWRITE REMOVE-ALL-LONGER-EQUAL-IL-IL))
 (9 9 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (9 3 (:REWRITE REGEX-R-REPEAT-ACCESSOR-TYPES))
 (7 7 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MIN))
 )
(RUN-REGEX-FLAG
 (12973 1023 (:REWRITE DEFAULT-<-2))
 (12273 1231 (:REWRITE INTEGERP-NUMBERP))
 (10780 336 (:REWRITE MEMBER-MIN-IDX))
 (6454 682 (:REWRITE SUBSETP-CAR-MEMBER))
 (6111 357 (:DEFINITION MEMBER-EQUAL))
 (5863 3096 (:REWRITE DEFAULT-CAR))
 (4518 2124 (:REWRITE DEFAULT-+-2))
 (3640 438 (:REWRITE DEFAULT-UNARY-MINUS))
 (3098 1023 (:REWRITE DEFAULT-<-1))
 (2782 2124 (:REWRITE DEFAULT-+-1))
 (2619 249 (:REWRITE LONGEST-IL-TYPE-WEAK))
 (2397 2096 (:REWRITE DEFAULT-CDR))
 (2226 1113 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (2014 2014 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (2002 848 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1937 711 (:REWRITE INPUT-LIST-ELTP-THM))
 (1788 1788 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1680 240 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1536 72 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-IL))
 (1007 1007 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (936 936 (:REWRITE SUBSETP-TRANS2))
 (936 936 (:REWRITE SUBSETP-TRANS))
 (927 927 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (927 927 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (714 714 (:REWRITE SUBSETP-MEMBER . 2))
 (714 714 (:REWRITE SUBSETP-MEMBER . 1))
 (633 633 (:REWRITE BACKREF-INTS))
 (576 72 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-FN))
 (468 36 (:REWRITE COMMUTATIVITY-OF-APPEND-UNDER-SET-EQUIV))
 (444 72 (:DEFINITION BINARY-APPEND))
 (424 138 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (275 275 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 (256 40 (:REWRITE REMOVE-ALL-LONGER-EQUAL-IL-PSEUDO))
 (252 144 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (224 224 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (204 2 (:TYPE-PRESCRIPTION RETURN-LAST))
 (190 190 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (190 190 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (185 185 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (185 185 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (168 96 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (162 22 (:REWRITE INPUT-LIST-ELTP-OF-CAR-WHEN-INPUT-LISTP))
 (141 47 (:REWRITE R-REPEAT-NOT-REGEX))
 (141 47 (:REWRITE R-GROUP-NOT-REGEX))
 (141 47 (:REWRITE R-EXACT-NOT-REGEX))
 (141 47 (:REWRITE R-DISJUNCT-NOT-REGEX))
 (141 47 (:REWRITE R-CONCAT-NOT-REGEX))
 (141 47 (:REWRITE R-CHARSET-NOT-REGEX))
 (141 47 (:REWRITE R-BACKREF-NOT-REGEX))
 (100 100 (:REWRITE DEFAULT-*-2))
 (100 100 (:REWRITE DEFAULT-*-1))
 (98 98 (:LINEAR LENGTH-EQUIV-LINEAR))
 (88 88 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (77 77 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (75 75 (:LINEAR MEMBER-MIN-IDX))
 (69 21 (:LINEAR LONGEST-IL-GREATER-COMPARE-TO-MIN))
 (51 3 (:REWRITE SUBSETP-OF-CONS))
 (49 49 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (24 4 (:REWRITE REMOVE-ALL-LONGER-EQUAL-IL-IL))
 (9 3 (:REWRITE REGEX-R-REPEAT-ACCESSOR-TYPES))
 (7 7 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MIN))
 (6 6 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (4 1 (:DEFINITION POSP))
 (2 2 (:TYPE-PRESCRIPTION THROW-NONEXEC-ERROR))
 )
(FLAG::FLAG-EQUIV-LEMMA)
(RUN-REGEX-FLAG-EQUIVALENCES)
(FLAG-LEMMA-FOR-RUN-REGEX-SUFFIXES1
 (22804 1737 (:REWRITE MEMBER-MIN-IDX))
 (14119 1609 (:REWRITE SUBSETP-CAR-MEMBER))
 (5104 102 (:DEFINITION TAKE))
 (4040 216 (:REWRITE TAKE-OF-TOO-MANY))
 (4034 4034 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (3478 3478 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (3362 216 (:REWRITE TAKE-OF-LEN-FREE))
 (3030 3030 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (2856 408 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (2522 2522 (:TYPE-PRESCRIPTION LEN))
 (2376 432 (:DEFINITION LEN))
 (2323 883 (:REWRITE R-BACKREF-NOT-REGEX))
 (2292 873 (:REWRITE R-CHARSET-NOT-REGEX))
 (2112 2018 (:REWRITE DEFAULT-+-1))
 (2017 2017 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2017 2017 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2017 2017 (:REWRITE SUBSETP-TRANS2))
 (2017 2017 (:REWRITE SUBSETP-TRANS))
 (1995 873 (:REWRITE R-EXACT-NOT-REGEX))
 (1739 1739 (:REWRITE SUBSETP-MEMBER . 2))
 (1739 1739 (:REWRITE SUBSETP-MEMBER . 1))
 (1134 1050 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (944 944 (:REWRITE BACKREF-INTS))
 (744 744 (:LINEAR LENGTH-EQUIV-LINEAR))
 (702 216 (:REWRITE TAKE-WHEN-ATOM))
 (475 171 (:DEFINITION BINARY-APPEND))
 (468 342 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (467 467 (:LINEAR MEMBER-MIN-IDX))
 (446 446 (:REWRITE NOT-R-BACKREF-P-R-BACKREF-INDEX))
 (336 24 (:DEFINITION PSEUDO-BACKREF-LISTP))
 (298 38 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-IL))
 (256 256 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (256 128 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (256 128 (:REWRITE CONSP-OF-APPEND))
 (247 247 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MIN))
 (238 106 (:REWRITE REGEX-R-CONCAT-ACCESSOR-TYPES))
 (231 231 (:TYPE-PRESCRIPTION CHARSETP))
 (231 33 (:DEFINITION CHARSETP))
 (219 73 (:REWRITE REGEX-R-BACKREF-ACCESSOR-TYPES))
 (213 213 (:REWRITE DEFAULT-COERCE-2))
 (204 204 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (194 86 (:REWRITE REGEX-R-DISJUNCT-ACCESSOR-TYPES))
 (180 180 (:REWRITE FOLD-CONSTS-IN-+))
 (162 162 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MAX))
 (152 128 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (128 128 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (128 128 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (128 128 (:REWRITE CAR-OF-APPEND))
 (127 127 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 (120 120 (:REWRITE DEFAULT-COERCE-1))
 (120 24 (:DEFINITION PSEUDO-BACKREFP))
 (99 33 (:REWRITE REGEX-R-EXACT-ACCESSOR-TYPES))
 (99 33 (:REWRITE REGEX-R-CHARSET-ACCESSOR-TYPES))
 (98 62 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (84 84 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (66 66 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (62 62 (:REWRITE NOT-R-EXACT-P-R-EXACT-VAL))
 (62 62 (:REWRITE NOT-R-CHARSET-P-R-CHARSET-SET))
 (60 60 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (57 57 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (56 38 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-FN))
 (54 54 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (54 54 (:REWRITE BACKREF-LISTP-NTH))
 (33 33 (:DEFINITION CHARSET-MEMBERP))
 (32 24 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (30 30 (:LINEAR LONGEST-IL-GREATER-COMPARE-TO-MIN))
 (24 24 (:TYPE-PRESCRIPTION REMOVE-ALL-LONGER-EQUAL-IL))
 (24 24 (:REWRITE BACKREFP-PSEUDO))
 (22 22 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (18 3 (:DEFINITION STORE-BACKREFS))
 (16 16 (:REWRITE NOT-R-GROUP-P-R-GROUP-INDEX))
 (15 3 (:DEFINITION UPDATE-NTH))
 )
(RUN-REGEX-SUFFIXES1)
(RUN-REPEAT-SUFFIXES1)
(RUN-REGEX-LIST-SUFFIXES1)
(RUN-REPEAT-LIST-SUFFIXES1)
(FLAG-LEMMA-FOR-TRUE-LISTP-RUN-REGEX
 (3046 168 (:REWRITE TAKE-OF-LEN-FREE))
 (2780 168 (:REWRITE TAKE-OF-TOO-MANY))
 (2352 336 (:DEFINITION LEN))
 (2038 154 (:REWRITE DEFAULT-UNARY-MINUS))
 (2016 256 (:REWRITE INTEGERP-NUMBERP))
 (1984 1984 (:TYPE-PRESCRIPTION LEN))
 (1812 302 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (1772 276 (:REWRITE PSEUDO-BACKREF-LISTP-NTH))
 (1764 1176 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (1232 88 (:DEFINITION PSEUDO-BACKREF-LISTP))
 (924 168 (:REWRITE TAKE-WHEN-ATOM))
 (812 210 (:REWRITE INTEGERP-+))
 (764 84 (:DEFINITION NTHCDR))
 (616 616 (:TYPE-PRESCRIPTION PSEUDO-BACKREF-LISTP))
 (604 604 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (604 302 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (586 42 (:REWRITE DEFAULT-COERCE-3))
 (542 110 (:REWRITE INTEGERP--))
 (532 532 (:REWRITE BACKREF-INTS))
 (460 42 (:REWRITE CONSP-OF-TAKE))
 (444 444 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (440 88 (:DEFINITION PSEUDO-BACKREFP))
 (302 302 (:TYPE-PRESCRIPTION SET::EMPTYP-TYPE))
 (302 302 (:REWRITE SET::IN-SET))
 (302 302 (:REWRITE BACKREF-LISTP-TRUE-LISTP))
 (284 6 (:LINEAR LONGEST-IL-MIN-LEN))
 (276 276 (:REWRITE BACKREF-LISTP-NTH))
 (264 264 (:REWRITE BACKREF-LISTP-PSEUDO))
 (256 256 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (239 239 (:REWRITE NOT-R-BACKREF-P-R-BACKREF-INDEX))
 (226 226 (:LINEAR LENGTH-EQUIV-LINEAR))
 (224 16 (:DEFINITION MIN-IDX-IL))
 (208 16 (:DEFINITION MIN))
 (192 16 (:REWRITE MEMBER-MIN-IDX))
 (178 178 (:REWRITE FOLD-CONSTS-IN-+))
 (113 113 (:LINEAR LONGEST-IL-MAX-LEN))
 (112 16 (:REWRITE SUBSETP-CAR-MEMBER))
 (88 88 (:REWRITE BACKREFP-PSEUDO))
 (87 29 (:REWRITE R-REPEAT-NOT-REGEX))
 (87 29 (:REWRITE R-GROUP-NOT-REGEX))
 (87 29 (:REWRITE R-EXACT-NOT-REGEX))
 (87 29 (:REWRITE R-DISJUNCT-NOT-REGEX))
 (87 29 (:REWRITE R-CONCAT-NOT-REGEX))
 (87 29 (:REWRITE R-CHARSET-NOT-REGEX))
 (87 29 (:REWRITE R-BACKREF-NOT-REGEX))
 (84 84 (:REWRITE DEFAULT-COERCE-2))
 (66 6 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-IL))
 (42 42 (:REWRITE DEFAULT-COERCE-1))
 (40 40 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MIN))
 (40 22 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (34 11 (:DEFINITION BINARY-APPEND))
 (32 32 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (32 32 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (30 10 (:REWRITE REGEX-R-REPEAT-ACCESSOR-TYPES))
 (27 6 (:DEFINITION UPDATE-NTH))
 (20 20 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (20 20 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MAX))
 (16 16 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (16 16 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (16 16 (:REWRITE SUBSETP-TRANS2))
 (16 16 (:REWRITE SUBSETP-TRANS))
 (16 16 (:REWRITE SUBSETP-MEMBER . 2))
 (16 16 (:REWRITE SUBSETP-MEMBER . 1))
 (12 6 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-FN))
 (11 11 (:REWRITE NOT-R-EXACT-P-R-EXACT-VAL))
 (11 11 (:REWRITE NOT-R-CHARSET-P-R-CHARSET-SET))
 (9 9 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (6 6 (:TYPE-PRESCRIPTION INPUT-LISTP))
 (6 6 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 (6 6 (:LINEAR MEMBER-MIN-IDX))
 (5 5 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (5 5 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (3 3 (:REWRITE NOT-R-GROUP-P-R-GROUP-INDEX))
 (2 2 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 )
(TRUE-LISTP-RUN-REGEX)
(TRUE-LISTP-RUN-REPEAT)
(TRUE-LISTP-RUN-REGEX-LIST)
(TRUE-LISTP-RUN-REPEAT-LIST)
(RUN-REGEX-SUFFIXES
 (5082 18 (:DEFINITION MIN-IDX-IL))
 (5002 18 (:DEFINITION MIN))
 (4466 379 (:REWRITE DEFAULT-<-2))
 (4198 57 (:REWRITE INTEGERP-NUMBERP))
 (4078 3 (:DEFINITION RUN-REGEX))
 (3888 18 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (3816 3 (:DEFINITION CHECK-BACKREF))
 (3681 6 (:DEFINITION SUBSEQ))
 (2772 9 (:DEFINITION SUBSEQ-LIST))
 (2093 110 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (1695 18 (:REWRITE TAKE-OF-LEN-FREE))
 (1464 3 (:DEFINITION RUN-REPEAT))
 (1380 9 (:DEFINITION TAKE))
 (1353 156 (:DEFINITION NTH))
 (960 195 (:REWRITE ZP-OPEN))
 (876 9 (:REWRITE DEFAULT-COERCE-3))
 (849 9 (:REWRITE CONSP-OF-TAKE))
 (807 162 (:REWRITE INPUT-LIST-ELTP-THM))
 (756 504 (:REWRITE DEFAULT-CAR))
 (735 456 (:REWRITE DEFAULT-CDR))
 (720 240 (:REWRITE PSEUDO-BACKREF-LISTP-NTH))
 (534 18 (:REWRITE TAKE-OF-TOO-MANY))
 (510 379 (:REWRITE DEFAULT-<-1))
 (490 18 (:REWRITE MEMBER-MIN-IDX))
 (336 69 (:REWRITE INTEGERP-+))
 (321 273 (:REWRITE DEFAULT-+-2))
 (288 273 (:REWRITE DEFAULT-+-1))
 (285 30 (:DEFINITION NFIX))
 (274 18 (:DEFINITION MEMBER-EQUAL))
 (266 8 (:LINEAR LONGEST-IL-MIN-LEN))
 (252 36 (:REWRITE SUBSETP-CAR-MEMBER))
 (252 36 (:DEFINITION LEN))
 (240 240 (:TYPE-PRESCRIPTION PSEUDO-BACKREF-LISTP))
 (240 240 (:REWRITE BACKREF-LISTP-PSEUDO))
 (240 45 (:DEFINITION INPUT-LIST-ELTP))
 (216 216 (:TYPE-PRESCRIPTION LEN))
 (195 45 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (180 180 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (180 36 (:REWRITE INTEGERP--))
 (144 9 (:DEFINITION NTHCDR))
 (133 3 (:DEFINITION RUN-REPEAT-LIST))
 (130 3 (:DEFINITION RUN-REGEX-LIST))
 (122 21 (:DEFINITION BINARY-APPEND))
 (120 120 (:TYPE-PRESCRIPTION INDEXP))
 (91 31 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (90 90 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (90 90 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (90 18 (:REWRITE COMMUTATIVITY-OF-+))
 (90 15 (:REWRITE INPUT-LIST-ELTP-OF-CAR-WHEN-INPUT-LISTP))
 (72 18 (:REWRITE TAKE-WHEN-ATOM))
 (60 60 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (60 24 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (56 56 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (54 42 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (52 4 (:REWRITE COMMUTATIVITY-OF-APPEND-UNDER-SET-EQUIV))
 (51 51 (:REWRITE BACKREF-INTS))
 (48 3 (:DEFINITION STORE-BACKREFS))
 (48 3 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-IL))
 (46 46 (:REWRITE SUBSETP-TRANS2))
 (46 46 (:REWRITE SUBSETP-TRANS))
 (45 45 (:TYPE-PRESCRIPTION TAKE))
 (44 38 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (39 13 (:REWRITE R-REPEAT-NOT-REGEX))
 (39 13 (:REWRITE R-GROUP-NOT-REGEX))
 (39 13 (:REWRITE R-EXACT-NOT-REGEX))
 (39 13 (:REWRITE R-DISJUNCT-NOT-REGEX))
 (39 13 (:REWRITE R-CONCAT-NOT-REGEX))
 (39 13 (:REWRITE R-CHARSET-NOT-REGEX))
 (39 13 (:REWRITE R-BACKREF-NOT-REGEX))
 (38 38 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (36 36 (:REWRITE SUBSETP-MEMBER . 2))
 (36 36 (:REWRITE SUBSETP-MEMBER . 1))
 (30 3 (:DEFINITION UPDATE-NTH))
 (28 28 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (27 12 (:REWRITE DEFAULT-UNARY-MINUS))
 (25 19 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (24 3 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-FN))
 (21 21 (:REWRITE FOLD-CONSTS-IN-+))
 (21 3 (:REWRITE COMMUTATIVITY-2-OF-+))
 (18 18 (:TYPE-PRESCRIPTION NFIX))
 (18 18 (:REWRITE DEFAULT-COERCE-2))
 (9 9 (:REWRITE DEFAULT-COERCE-1))
 (8 8 (:LINEAR MEMBER-MIN-IDX))
 (6 6 (:REWRITE REGEX-R-REPEAT-ACCESSOR-TYPES))
 (4 4 (:LINEAR LENGTH-EQUIV-LINEAR))
 (3 3 (:TYPE-PRESCRIPTION IN-CHARSET))
 (3 3 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (3 3 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MIN))
 (3 3 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MAX))
 (3 3 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (3 3 (:REWRITE NOT-R-GROUP-P-R-GROUP-INDEX))
 (3 3 (:REWRITE NOT-R-EXACT-P-R-EXACT-VAL))
 (3 3 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (3 3 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (3 3 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (3 3 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 (3 3 (:REWRITE NOT-R-CHARSET-P-R-CHARSET-SET))
 (3 3 (:REWRITE NOT-R-BACKREF-P-R-BACKREF-INDEX))
 (2 2 (:LINEAR LONGEST-IL-MAX-LEN))
 )
(RUN-REGEX-INPUT-LISTP
 (1881 627 (:REWRITE R-REPEAT-NOT-REGEX))
 (1881 627 (:REWRITE R-GROUP-NOT-REGEX))
 (1881 627 (:REWRITE R-EXACT-NOT-REGEX))
 (1881 627 (:REWRITE R-DISJUNCT-NOT-REGEX))
 (1881 627 (:REWRITE R-CONCAT-NOT-REGEX))
 (1881 627 (:REWRITE R-CHARSET-NOT-REGEX))
 (1881 627 (:REWRITE R-BACKREF-NOT-REGEX))
 (1624 907 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (875 311 (:LINEAR LONGEST-IL-MIN-LEN))
 (480 480 (:TYPE-PRESCRIPTION RUN-REGEX-LIST))
 (321 321 (:TYPE-PRESCRIPTION RUN-REPEAT-LIST))
 (311 311 (:LINEAR MEMBER-MIN-IDX))
 (292 292 (:LINEAR LENGTH-EQUIV-LINEAR))
 (272 272 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (188 146 (:LINEAR LONGEST-IL-MAX-LEN))
 (146 146 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (136 136 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 )
(RUN-REGEX-PSUEDO-INPUT-LISTP)
(RUN-REGEX
 (24858 18 (:DEFINITION RUN-REGEX))
 (23266 18 (:DEFINITION CHECK-BACKREF))
 (22456 36 (:DEFINITION SUBSEQ))
 (20225 1826 (:REWRITE DEFAULT-<-2))
 (19980 13 (:DEFINITION MIN-IDX-IL))
 (19928 13 (:DEFINITION MIN))
 (19544 140 (:REWRITE INTEGERP-NUMBERP))
 (19291 13 (:REWRITE MIN-IDX-IL-TYPE))
 (19213 13 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (17002 54 (:DEFINITION SUBSEQ-LIST))
 (10558 108 (:REWRITE TAKE-OF-LEN-FREE))
 (8415 969 (:DEFINITION NTH))
 (8262 54 (:DEFINITION TAKE))
 (5256 54 (:REWRITE DEFAULT-COERCE-3))
 (5094 54 (:REWRITE CONSP-OF-TAKE))
 (3920 2186 (:REWRITE DEFAULT-CDR))
 (3662 2105 (:REWRITE DEFAULT-CAR))
 (3186 108 (:REWRITE TAKE-OF-TOO-MANY))
 (2107 1826 (:REWRITE DEFAULT-<-1))
 (1998 414 (:REWRITE INTEGERP-+))
 (1892 1604 (:REWRITE DEFAULT-+-2))
 (1694 1604 (:REWRITE DEFAULT-+-1))
 (1512 216 (:DEFINITION LEN))
 (1296 1296 (:TYPE-PRESCRIPTION LEN))
 (1080 1080 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (1080 216 (:REWRITE INTEGERP--))
 (914 823 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (864 54 (:DEFINITION NTHCDR))
 (580 133 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (540 108 (:REWRITE COMMUTATIVITY-OF-+))
 (432 108 (:REWRITE TAKE-WHEN-ATOM))
 (351 13 (:REWRITE MEMBER-MIN-IDX))
 (288 18 (:DEFINITION STORE-BACKREFS))
 (270 270 (:TYPE-PRESCRIPTION TAKE))
 (264 44 (:REWRITE INPUT-LIST-ELTP-OF-CAR-WHEN-INPUT-LISTP))
 (195 13 (:DEFINITION MEMBER-EQUAL))
 (190 43 (:REWRITE R-DISJUNCT-NOT-REGEX))
 (190 43 (:REWRITE R-CONCAT-NOT-REGEX))
 (180 18 (:DEFINITION UPDATE-NTH))
 (171 43 (:REWRITE R-REPEAT-NOT-REGEX))
 (167 43 (:REWRITE R-GROUP-NOT-REGEX))
 (162 72 (:REWRITE DEFAULT-UNARY-MINUS))
 (131 43 (:REWRITE R-CHARSET-NOT-REGEX))
 (126 126 (:REWRITE FOLD-CONSTS-IN-+))
 (126 18 (:REWRITE COMMUTATIVITY-2-OF-+))
 (113 43 (:REWRITE R-BACKREF-NOT-REGEX))
 (108 108 (:REWRITE DEFAULT-COERCE-2))
 (107 107 (:REWRITE BACKREF-INTS))
 (105 43 (:REWRITE R-EXACT-NOT-REGEX))
 (90 19 (:DEFINITION BINARY-APPEND))
 (54 54 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (54 54 (:REWRITE DEFAULT-COERCE-1))
 (38 38 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (28 28 (:REWRITE SUBSETP-TRANS2))
 (28 28 (:REWRITE SUBSETP-TRANS))
 (28 28 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (26 26 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (26 26 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (26 26 (:REWRITE SUBSETP-MEMBER . 2))
 (26 26 (:REWRITE SUBSETP-MEMBER . 1))
 (26 26 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (22 22 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (21 21 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (21 21 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MIN))
 (21 21 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (21 21 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 (20 20 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MAX))
 (20 20 (:REWRITE NOT-R-GROUP-P-R-GROUP-INDEX))
 (20 20 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (20 20 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (20 20 (:REWRITE NOT-R-CHARSET-P-R-CHARSET-SET))
 (20 20 (:REWRITE NOT-R-BACKREF-P-R-BACKREF-INDEX))
 (20 1 (:DEFINITION CHARSETP))
 (18 18 (:REWRITE NOT-R-EXACT-P-R-EXACT-VAL))
 (16 16 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (16 16 (:LINEAR LENGTH-EQUIV-LINEAR))
 (16 1 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-IL))
 (13 13 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (13 13 (:REWRITE INPUT-LISTP-PSEUDO))
 (10 1 (:DEFINITION CHARSET-MEMBERP))
 (8 8 (:LINEAR LONGEST-IL-MAX-LEN))
 (8 1 (:DEFINITION REMOVE-ALL-LONGER-EQUAL-FN))
 (6 1 (:REWRITE INPUT-LIST-ELTP-OF-NTH-WHEN-INPUT-LISTP))
 (5 1 (:REWRITE INDEXP-CHARACTERP))
 (3 1 (:REWRITE REGEX-R-BACKREF-ACCESSOR-TYPES))
 )
(RESOLVE-BACKREFS
 (266 38 (:REWRITE INPUT-LIST-ELTP-THM))
 (105 11 (:DEFINITION INPUT-LIST-ELTP))
 (62 62 (:REWRITE DEFAULT-CAR))
 (52 11 (:REWRITE INPUT-LIST-ELTP-SUFFIC))
 (51 51 (:TYPE-PRESCRIPTION INDEXP))
 (48 8 (:REWRITE INPUT-LIST-ELTP-OF-CAR-WHEN-INPUT-LISTP))
 (43 30 (:REWRITE DEFAULT-<-1))
 (30 30 (:REWRITE DEFAULT-<-2))
 (24 24 (:REWRITE DEFAULT-CDR))
 (22 22 (:REWRITE INPUT-LIST-ELTP-WHEN-MEMBER-EQUAL-OF-INPUT-LISTP))
 (21 21 (:TYPE-PRESCRIPTION INPUT-LIST-ELTP))
 (16 16 (:TYPE-PRESCRIPTION INPUT-LISTP))
 (16 16 (:REWRITE INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (15 15 (:REWRITE BACKREF-INTS))
 (8 8 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 )
(STRING-UNTRANS-GUARD)
(MATCH-REGEX-AT-CHAR
 (810 11 (:DEFINITION RUN-REGEX))
 (748 95 (:REWRITE DEFAULT-<-2))
 (738 9 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (705 5 (:DEFINITION MIN-IDX-IL))
 (702 30 (:REWRITE INTEGERP-NUMBERP))
 (685 5 (:DEFINITION MIN))
 (448 6 (:REWRITE MIN-IDX-IL-TYPE))
 (418 2 (:DEFINITION LONGEST-IL))
 (332 1 (:DEFINITION RESOLVE-BACKREFS))
 (324 1 (:DEFINITION GET-BACKREF-STRING))
 (321 1 (:DEFINITION SUBSEQ))
 (293 93 (:REWRITE DEFAULT-CAR))
 (283 2 (:DEFINITION SUBSEQ-LIST))
 (176 11 (:DEFINITION STORE-BACKREFS))
 (167 95 (:REWRITE DEFAULT-<-1))
 (162 97 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (138 28 (:REWRITE ZP-OPEN))
 (135 5 (:REWRITE MEMBER-MIN-IDX))
 (133 2 (:DEFINITION TAKE))
 (110 11 (:DEFINITION UPDATE-NTH))
 (103 85 (:REWRITE DEFAULT-CDR))
 (102 51 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (98 4 (:REWRITE TAKE-OF-TOO-MANY))
 (89 15 (:DEFINITION NFIX))
 (75 5 (:DEFINITION MEMBER-EQUAL))
 (73 4 (:REWRITE TAKE-OF-LEN-FREE))
 (71 61 (:REWRITE DEFAULT-+-2))
 (70 10 (:REWRITE SUBSETP-CAR-MEMBER))
 (65 61 (:REWRITE DEFAULT-+-1))
 (56 8 (:DEFINITION LEN))
 (53 11 (:DEFINITION BINARY-APPEND))
 (52 52 (:TYPE-PRESCRIPTION LEN))
 (40 40 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (38 4 (:REWRITE IMPLIES-LENGTH-EQUIV))
 (32 2 (:DEFINITION =))
 (31 2 (:REWRITE DEFAULT-COERCE-3))
 (27 6 (:REWRITE INTEGERP-+))
 (26 2 (:DEFINITION NTHCDR))
 (25 25 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (25 2 (:REWRITE CONSP-OF-TAKE))
 (22 22 (:REWRITE REGEX-R-REPEAT-ACCESSOR-TYPES))
 (22 22 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (20 20 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (18 18 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (18 18 (:REWRITE BACKREF-INTS))
 (18 18 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (18 6 (:REWRITE INTEGERP--))
 (17 17 (:REWRITE INPUT-LIST-ELTP-THM))
 (16 4 (:REWRITE TAKE-WHEN-ATOM))
 (12 2 (:REWRITE LENGTH-EQUIV-IMPLIES))
 (11 11 (:TYPE-PRESCRIPTION IN-CHARSET))
 (11 11 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (11 11 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (11 11 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MIN))
 (11 11 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MAX))
 (11 11 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (11 11 (:REWRITE NOT-R-GROUP-P-R-GROUP-INDEX))
 (11 11 (:REWRITE NOT-R-EXACT-P-R-EXACT-VAL))
 (11 11 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (11 11 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (11 11 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (11 11 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 (11 11 (:REWRITE NOT-R-CHARSET-P-R-CHARSET-SET))
 (11 11 (:REWRITE NOT-R-BACKREF-P-R-BACKREF-INDEX))
 (11 11 (:DEFINITION NTH))
 (11 3 (:REWRITE COMMUTATIVITY-OF-+))
 (10 10 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (10 10 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (10 10 (:REWRITE SUBSETP-TRANS2))
 (10 10 (:REWRITE SUBSETP-TRANS))
 (10 10 (:REWRITE SUBSETP-MEMBER . 2))
 (10 10 (:REWRITE SUBSETP-MEMBER . 1))
 (10 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (9 9 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (9 9 (:REWRITE INPUT-LISTP-PSEUDO))
 (9 3 (:REWRITE R-REPEAT-NOT-REGEX))
 (9 3 (:REWRITE R-GROUP-NOT-REGEX))
 (9 3 (:REWRITE R-EXACT-NOT-REGEX))
 (9 3 (:REWRITE R-DISJUNCT-NOT-REGEX))
 (9 3 (:REWRITE R-CONCAT-NOT-REGEX))
 (9 3 (:REWRITE R-CHARSET-NOT-REGEX))
 (9 3 (:REWRITE R-BACKREF-NOT-REGEX))
 (6 6 (:TYPE-PRESCRIPTION TRUE-LISTP-SUBSEQ-TYPE-PRESCRIPTION))
 (6 6 (:TYPE-PRESCRIPTION STRINGP-SUBSEQ-TYPE-PRESCRIPTION))
 (5 5 (:LINEAR LONGEST-IL-MAX-LEN))
 (5 5 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (4 4 (:TYPE-PRESCRIPTION TAKE))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE DEFAULT-COERCE-1))
 (1 1 (:LINEAR MEMBER-MIN-IDX))
 )
(MATCH-REGEX-FUN
 (5658 24 (:REWRITE TAKE-OF-LEN-FREE))
 (3951 20 (:LINEAR LONGEST-IL-MIN-LEN))
 (3846 48 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (3716 12 (:DEFINITION TAKE))
 (3596 50 (:DEFINITION RUN-REGEX))
 (3434 17 (:DEFINITION LONGEST-IL))
 (3323 447 (:REWRITE DEFAULT-<-2))
 (3111 66 (:REWRITE LONGEST-IL-TYPE-WEAK))
 (3050 130 (:REWRITE INTEGERP-NUMBERP))
 (2075 415 (:REWRITE DEFAULT-CAR))
 (2073 15 (:DEFINITION MIN-IDX-IL))
 (2013 15 (:DEFINITION MIN))
 (1464 23 (:LINEAR LONGEST-IL-MAX-LEN))
 (1278 15 (:REWRITE MIN-IDX-IL-TYPE))
 (1257 8 (:REWRITE DEFAULT-COERCE-3))
 (1233 8 (:REWRITE CONSP-OF-TAKE))
 (987 2 (:DEFINITION RESOLVE-BACKREFS))
 (971 2 (:DEFINITION GET-BACKREF-STRING))
 (835 160 (:DEFINITION REG-STR-BR-GUARD))
 (819 24 (:REWRITE TAKE-OF-TOO-MANY))
 (791 50 (:DEFINITION STORE-BACKREFS))
 (723 447 (:REWRITE DEFAULT-<-1))
 (715 5 (:LINEAR MIN-IDX-IL-MAX))
 (636 132 (:REWRITE ZP-OPEN))
 (566 283 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (542 542 (:TYPE-PRESCRIPTION PSEUDO-INPUT-LISTP))
 (491 50 (:DEFINITION UPDATE-NTH))
 (469 361 (:REWRITE DEFAULT-+-2))
 (465 75 (:REWRITE RUN-REGEX-PSUEDO-INPUT-LISTP))
 (464 361 (:REWRITE DEFAULT-+-1))
 (461 394 (:REWRITE DEFAULT-CDR))
 (426 30 (:REWRITE RUN-REGEX-SUFFIXES1))
 (420 55 (:REWRITE RUN-REGEX-INPUT-LISTP))
 (405 15 (:REWRITE MEMBER-MIN-IDX))
 (392 15 (:LINEAR LONGEST-IL-GREATER-COMPARE-TO-MIN))
 (368 48 (:DEFINITION LEN))
 (320 240 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (310 310 (:TYPE-PRESCRIPTION LEN))
 (260 130 (:TYPE-PRESCRIPTION MIN-IDX-IL-TYPE))
 (248 50 (:DEFINITION BINARY-APPEND))
 (225 15 (:DEFINITION MEMBER-EQUAL))
 (210 30 (:REWRITE SUBSETP-CAR-MEMBER))
 (164 26 (:REWRITE INTEGERP-+))
 (160 160 (:TYPE-PRESCRIPTION REG-STR-BR-GUARD))
 (160 160 (:DEFINITION BACKREF-LISTP))
 (126 12 (:DEFINITION NTHCDR))
 (120 24 (:REWRITE TAKE-WHEN-ATOM))
 (115 115 (:TYPE-PRESCRIPTION INPUT-LISTP))
 (106 106 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (102 98 (:REWRITE REGEX-R-REPEAT-ACCESSOR-TYPES))
 (100 100 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (96 96 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (90 90 (:REWRITE INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (80 80 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (75 75 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (71 71 (:REWRITE BACKREF-INTS))
 (68 68 (:REWRITE INPUT-LIST-ELTP-THM))
 (63 49 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (60 60 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (53 53 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (53 53 (:REWRITE INPUT-LISTP-PSEUDO))
 (51 27 (:REWRITE DEFAULT-UNARY-MINUS))
 (50 50 (:TYPE-PRESCRIPTION IN-CHARSET))
 (50 50 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (50 50 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MIN))
 (50 50 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MAX))
 (50 50 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (50 50 (:REWRITE NOT-R-GROUP-P-R-GROUP-INDEX))
 (50 50 (:REWRITE NOT-R-EXACT-P-R-EXACT-VAL))
 (50 50 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (50 50 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (50 50 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (50 50 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 (50 50 (:REWRITE NOT-R-CHARSET-P-R-CHARSET-SET))
 (50 50 (:REWRITE NOT-R-BACKREF-P-R-BACKREF-INDEX))
 (50 50 (:DEFINITION NTH))
 (48 16 (:REWRITE INTEGERP--))
 (45 45 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (30 30 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (30 30 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (30 30 (:REWRITE SUBSETP-TRANS2))
 (30 30 (:REWRITE SUBSETP-TRANS))
 (30 30 (:REWRITE SUBSETP-MEMBER . 2))
 (30 30 (:REWRITE SUBSETP-MEMBER . 1))
 (24 24 (:TYPE-PRESCRIPTION NFIX))
 (16 16 (:TYPE-PRESCRIPTION TAKE))
 (16 16 (:REWRITE DEFAULT-COERCE-2))
 (8 8 (:REWRITE DEFAULT-COERCE-1))
 (8 8 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (6 2 (:REWRITE R-REPEAT-NOT-REGEX))
 (6 2 (:REWRITE R-GROUP-NOT-REGEX))
 (6 2 (:REWRITE R-EXACT-NOT-REGEX))
 (6 2 (:REWRITE R-DISJUNCT-NOT-REGEX))
 (6 2 (:REWRITE R-CONCAT-NOT-REGEX))
 (6 2 (:REWRITE R-CHARSET-NOT-REGEX))
 (6 2 (:REWRITE R-BACKREF-NOT-REGEX))
 (6 1 (:REWRITE LENGTH-EQUIV-IMPLIES))
 (5 5 (:LINEAR MEMBER-MIN-IDX))
 )
(MATCH-REGEX
 (31 2 (:REWRITE IMPLIES-LENGTH-EQUIV))
 (28 1 (:DEFINITION =))
 (6 6 (:LINEAR LENGTH-EQUIV-LINEAR))
 (6 1 (:REWRITE LENGTH-EQUIV-IMPLIES))
 (3 3 (:LINEAR LONGEST-IL-MAX-LEN))
 (3 3 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (3 1 (:REWRITE R-REPEAT-NOT-REGEX))
 (3 1 (:REWRITE R-GROUP-NOT-REGEX))
 (3 1 (:REWRITE R-EXACT-NOT-REGEX))
 (3 1 (:REWRITE R-DISJUNCT-NOT-REGEX))
 (3 1 (:REWRITE R-CONCAT-NOT-REGEX))
 (3 1 (:REWRITE R-CHARSET-NOT-REGEX))
 (3 1 (:REWRITE R-BACKREF-NOT-REGEX))
 (2 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE DEFAULT-<-2))
 )
(MATCH-REGEX-AT-CHAR-STRING
 (992 3 (:DEFINITION RESOLVE-BACKREFS))
 (972 3 (:DEFINITION GET-BACKREF-STRING))
 (751 10 (:DEFINITION TAKE))
 (605 67 (:REWRITE DEFAULT-CAR))
 (531 14 (:REWRITE LONGEST-IL-TYPE-WEAK))
 (531 3 (:DEFINITION LONGEST-IL))
 (510 6 (:DEFINITION RUN-REGEX))
 (506 20 (:REWRITE TAKE-OF-TOO-MANY))
 (505 20 (:REWRITE TAKE-OF-LEN-FREE))
 (363 3 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (295 295 (:TYPE-PRESCRIPTION LENGTH))
 (280 40 (:DEFINITION LEN))
 (258 42 (:REWRITE ZP-OPEN))
 (252 126 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (250 250 (:TYPE-PRESCRIPTION LEN))
 (226 119 (:REWRITE DEFAULT-<-2))
 (207 111 (:REWRITE DEFAULT-+-2))
 (200 200 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (196 7 (:REWRITE RUN-REGEX-PSUEDO-INPUT-LISTP))
 (193 111 (:REWRITE DEFAULT-+-1))
 (182 7 (:DEFINITION REG-STR-BR-GUARD))
 (179 119 (:REWRITE DEFAULT-<-1))
 (158 62 (:REWRITE INTEGERP-NUMBERP))
 (157 108 (:REWRITE DEFAULT-CDR))
 (146 146 (:TYPE-PRESCRIPTION PSEUDO-INPUT-LISTP))
 (145 10 (:REWRITE DEFAULT-COERCE-3))
 (141 26 (:DEFINITION NFIX))
 (119 7 (:DEFINITION INDEXP))
 (115 10 (:REWRITE CONSP-OF-TAKE))
 (110 10 (:DEFINITION NTHCDR))
 (105 30 (:REWRITE INTEGERP-+))
 (96 6 (:DEFINITION STORE-BACKREFS))
 (88 62 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (80 20 (:REWRITE TAKE-WHEN-ATOM))
 (71 21 (:LINEAR LONGEST-IL-MAX-LEN))
 (66 30 (:REWRITE INTEGERP--))
 (60 60 (:TYPE-PRESCRIPTION INPUT-LISTP))
 (60 60 (:REWRITE INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (60 10 (:LINEAR LONGEST-IL-MIN-LEN))
 (60 10 (:LINEAR LONGEST-IL-GREATER-COMPARE-TO-MIN))
 (60 6 (:DEFINITION UPDATE-NTH))
 (42 10 (:REWRITE DEFAULT-UNARY-MINUS))
 (41 41 (:REWRITE BACKREF-INTS))
 (38 38 (:REWRITE INPUT-LIST-ELTP-THM))
 (30 30 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (27 6 (:DEFINITION BINARY-APPEND))
 (22 22 (:LINEAR LENGTH-EQUIV-LINEAR))
 (21 7 (:DEFINITION NATP))
 (20 20 (:TYPE-PRESCRIPTION NFIX))
 (20 20 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (20 20 (:REWRITE DEFAULT-COERCE-2))
 (19 19 (:TYPE-PRESCRIPTION REGEX-P))
 (18 6 (:REWRITE REGEX-R-REPEAT-ACCESSOR-TYPES))
 (12 12 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (11 11 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (10 10 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (10 10 (:REWRITE INPUT-LISTP-PSEUDO))
 (10 10 (:REWRITE FOLD-CONSTS-IN-+))
 (10 10 (:REWRITE DEFAULT-COERCE-1))
 (7 7 (:TYPE-PRESCRIPTION REG-STR-BR-GUARD))
 (7 7 (:DEFINITION BACKREF-LISTP))
 (6 6 (:TYPE-PRESCRIPTION IN-CHARSET))
 (6 6 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (6 6 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MIN))
 (6 6 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MAX))
 (6 6 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (6 6 (:REWRITE NOT-R-GROUP-P-R-GROUP-INDEX))
 (6 6 (:REWRITE NOT-R-EXACT-P-R-EXACT-VAL))
 (6 6 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (6 6 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (6 6 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (6 6 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 (6 6 (:REWRITE NOT-R-CHARSET-P-R-CHARSET-SET))
 (6 6 (:REWRITE NOT-R-BACKREF-P-R-BACKREF-INDEX))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (6 6 (:DEFINITION NTH))
 )
(STRING-OR-NULL-LISTP)
(RESOLVE-BACKREFS-STRLIST
 (363 6 (:DEFINITION TAKE))
 (276 12 (:REWRITE TAKE-OF-TOO-MANY))
 (183 12 (:REWRITE TAKE-OF-LEN-FREE))
 (168 24 (:DEFINITION LEN))
 (156 156 (:TYPE-PRESCRIPTION LEN))
 (150 18 (:REWRITE ZP-OPEN))
 (120 120 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (93 6 (:REWRITE DEFAULT-COERCE-3))
 (81 51 (:REWRITE DEFAULT-+-2))
 (81 18 (:REWRITE INTEGERP-+))
 (78 6 (:DEFINITION NTHCDR))
 (75 6 (:REWRITE CONSP-OF-TAKE))
 (72 72 (:TYPE-PRESCRIPTION LENGTH))
 (71 51 (:REWRITE DEFAULT-CDR))
 (69 12 (:DEFINITION NFIX))
 (63 51 (:REWRITE DEFAULT-+-1))
 (54 42 (:REWRITE DEFAULT-<-2))
 (54 18 (:REWRITE INTEGERP--))
 (50 29 (:REWRITE DEFAULT-CAR))
 (48 12 (:REWRITE TAKE-WHEN-ATOM))
 (45 42 (:REWRITE DEFAULT-<-1))
 (33 33 (:REWRITE BACKREF-INTS))
 (30 30 (:REWRITE INPUT-LIST-ELTP-THM))
 (30 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (27 12 (:REWRITE INTEGERP-NUMBERP))
 (12 12 (:TYPE-PRESCRIPTION NFIX))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (12 12 (:REWRITE DEFAULT-COERCE-2))
 (6 6 (:REWRITE FOLD-CONSTS-IN-+))
 (6 6 (:REWRITE DEFAULT-COERCE-1))
 )
(STRING-OR-NULL-LISTP-CDR
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(MATCH-REGEX-AT-CHAR-STRLIST
 (2384 28 (:DEFINITION RUN-REGEX))
 (2312 7 (:DEFINITION RESOLVE-BACKREFS))
 (2268 7 (:DEFINITION GET-BACKREF-STRING))
 (2124 12 (:DEFINITION LONGEST-IL))
 (2061 251 (:REWRITE DEFAULT-CAR))
 (2051 18 (:DEFINITION TAKE))
 (1971 39 (:REWRITE LONGEST-IL-TYPE-WEAK))
 (1715 36 (:REWRITE TAKE-OF-LEN-FREE))
 (1452 12 (:REWRITE PSEUDO-INPUT-LISTP-OF-CDR-WHEN-PSEUDO-INPUT-LISTP))
 (1404 54 (:DEFINITION REG-STR-BR-GUARD))
 (1381 1381 (:TYPE-PRESCRIPTION LENGTH))
 (1156 36 (:REWRITE TAKE-OF-TOO-MANY))
 (918 54 (:DEFINITION INDEXP))
 (840 30 (:REWRITE RUN-REGEX-INPUT-LISTP))
 (824 428 (:REWRITE DEFAULT-<-2))
 (818 409 (:TYPE-PRESCRIPTION LONGEST-IL-TYPE-WEAK))
 (725 428 (:REWRITE DEFAULT-<-1))
 (672 24 (:REWRITE RUN-REGEX-PSUEDO-INPUT-LISTP))
 (634 110 (:REWRITE ZP-OPEN))
 (603 304 (:REWRITE DEFAULT-CDR))
 (538 265 (:REWRITE DEFAULT-+-2))
 (504 72 (:DEFINITION LEN))
 (500 68 (:LINEAR LONGEST-IL-MAX-LEN))
 (481 481 (:TYPE-PRESCRIPTION PSEUDO-INPUT-LISTP))
 (470 470 (:TYPE-PRESCRIPTION LEN))
 (452 10 (:LINEAR LONGEST-IL-MIN-LEN))
 (452 10 (:LINEAR LONGEST-IL-GREATER-COMPARE-TO-MIN))
 (448 28 (:DEFINITION STORE-BACKREFS))
 (440 227 (:REWRITE INTEGERP-NUMBERP))
 (365 64 (:DEFINITION NFIX))
 (360 360 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (345 265 (:REWRITE DEFAULT-+-1))
 (305 227 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (280 28 (:DEFINITION UPDATE-NTH))
 (269 18 (:REWRITE DEFAULT-COERCE-3))
 (215 18 (:REWRITE CONSP-OF-TAKE))
 (214 18 (:DEFINITION NTHCDR))
 (213 54 (:REWRITE INTEGERP-+))
 (186 30 (:REWRITE RUN-REGEX-SUFFIXES1))
 (162 54 (:DEFINITION NATP))
 (144 36 (:REWRITE TAKE-WHEN-ATOM))
 (138 54 (:REWRITE INTEGERP--))
 (128 28 (:DEFINITION BINARY-APPEND))
 (120 120 (:TYPE-PRESCRIPTION INPUT-LISTP))
 (120 120 (:REWRITE INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (116 116 (:LINEAR LENGTH-EQUIV-LINEAR))
 (110 110 (:TYPE-PRESCRIPTION REGEX-P))
 (103 103 (:REWRITE BACKREF-INTS))
 (96 96 (:REWRITE INPUT-LIST-ELTP-THM))
 (84 28 (:REWRITE REGEX-R-REPEAT-ACCESSOR-TYPES))
 (82 18 (:REWRITE DEFAULT-UNARY-MINUS))
 (72 72 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-SUBSETP-EQUAL))
 (60 60 (:REWRITE INPUT-LISTP-WHEN-NOT-CONSP))
 (58 58 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 (56 56 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (54 54 (:DEFINITION BACKREF-LISTP))
 (39 3 (:DEFINITION STRING-OR-NULL-LISTP))
 (36 36 (:TYPE-PRESCRIPTION TAKE))
 (36 36 (:TYPE-PRESCRIPTION NFIX))
 (36 36 (:REWRITE PSEUDO-INPUT-LISTP-WHEN-NOT-CONSP))
 (36 36 (:REWRITE INPUT-LISTP-PSEUDO))
 (36 36 (:REWRITE DEFAULT-COERCE-2))
 (32 32 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (28 28 (:TYPE-PRESCRIPTION IN-CHARSET))
 (28 28 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-REGEX))
 (28 28 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MIN))
 (28 28 (:REWRITE NOT-R-REPEAT-P-R-REPEAT-MAX))
 (28 28 (:REWRITE NOT-R-GROUP-P-R-GROUP-REGEX))
 (28 28 (:REWRITE NOT-R-GROUP-P-R-GROUP-INDEX))
 (28 28 (:REWRITE NOT-R-EXACT-P-R-EXACT-VAL))
 (28 28 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-RIGHT))
 (28 28 (:REWRITE NOT-R-DISJUNCT-P-R-DISJUNCT-LEFT))
 (28 28 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-RIGHT))
 (28 28 (:REWRITE NOT-R-CONCAT-P-R-CONCAT-LEFT))
 (28 28 (:REWRITE NOT-R-CHARSET-P-R-CHARSET-SET))
 (28 28 (:REWRITE NOT-R-BACKREF-P-R-BACKREF-INDEX))
 (28 28 (:DEFINITION NTH))
 (18 18 (:REWRITE FOLD-CONSTS-IN-+))
 (18 18 (:REWRITE DEFAULT-COERCE-1))
 )
(MATCH-REGEX-STRING
 (43 26 (:REWRITE DEFAULT-<-1))
 (28 26 (:REWRITE DEFAULT-<-2))
 (8 8 (:LINEAR LENGTH-EQUIV-LINEAR))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 4 (:LINEAR LONGEST-IL-MAX-LEN))
 (4 4 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )
(MATCH-REGEX-STRLIST
 (38 23 (:REWRITE DEFAULT-<-1))
 (25 23 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE DEFAULT-CAR))
 (10 10 (:LINEAR LENGTH-EQUIV-LINEAR))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-+-1))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (5 5 (:LINEAR LONGEST-IL-MAX-LEN))
 (5 5 (:LINEAR BACKREF-LISTP-NTH-LINEAR))
 )