(STR::RPADCHARS (36 4 (:DEFINITION LEN))
                (24 2 (:DEFINITION CHARACTER-LISTP))
                (19 19 (:REWRITE CONSP-BY-LEN))
                (19 8 (:REWRITE LEN-WHEN-ATOM))
                (14 7 (:REWRITE DEFAULT-+-2))
                (14 2 (:DEFINITION BINARY-APPEND))
                (10 5 (:REWRITE DEFAULT-<-1))
                (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
                (8 8 (:REWRITE DEFAULT-CDR))
                (8 2
                   (:REWRITE CHARACTERP-OF-CAR-WHEN-CHARACTER-LISTP))
                (8 2
                   (:REWRITE CHARACTER-LISTP-OF-CDR-WHEN-CHARACTER-LISTP))
                (7 7 (:REWRITE DEFAULT-+-1))
                (6 6 (:REWRITE CONSP-OF-CDR-BY-LEN))
                (6 3 (:REWRITE DEFAULT-UNARY-MINUS))
                (5 5 (:REWRITE DEFAULT-<-2))
                (4 4 (:REWRITE DEFAULT-CAR))
                (2 2 (:REWRITE NATP-RW)))
(STR::CHARACTER-LISTP-OF-RPADCHARS
     (58 1 (:REWRITE REPEAT-WHEN-ZP))
     (46 1 (:REWRITE ZP-OPEN))
     (36 4 (:REWRITE NEGATIVE-WHEN-NATP))
     (24 2 (:REWRITE NATP-RW))
     (23 1 (:DEFINITION NOT))
     (21 1 (:DEFINITION BINARY-APPEND))
     (18 6 (:REWRITE DEFAULT-<-2))
     (14 1
         (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
     (12 12 (:REWRITE CONSP-BY-LEN))
     (12 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
     (11 1 (:DEFINITION CHARACTER-LISTP))
     (9 1 (:DEFINITION LEN))
     (7 3 (:REWRITE DEFAULT-CDR))
     (6 6 (:TYPE-PRESCRIPTION NATP))
     (6 6 (:REWRITE DEFAULT-<-1))
     (6 4
        (:REWRITE STR::CONSP-OF-MAKE-CHARACTER-LIST))
     (6 2 (:REWRITE DEFAULT-CAR))
     (5 3 (:REWRITE DEFAULT-+-2))
     (5 2 (:REWRITE LEN-WHEN-ATOM))
     (4 3 (:REWRITE DEFAULT-+-1))
     (2 2 (:REWRITE CONSP-OF-CDR-BY-LEN))
     (2 1
        (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
     (2 1 (:REWRITE DEFAULT-UNARY-MINUS))
     (2 1
        (:REWRITE CHARACTERP-OF-CAR-WHEN-CHARACTER-LISTP))
     (2 1
        (:REWRITE CHARACTER-LISTP-OF-CDR-WHEN-CHARACTER-LISTP))
     (1 1 (:TYPE-PRESCRIPTION ZP)))
(STR::LEN-OF-RPADCHARS (204 3 (:REWRITE CONSP-OF-REPEAT))
                       (144 2
                            (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
                       (122 14 (:DEFINITION LEN))
                       (118 4 (:REWRITE ZP-OPEN))
                       (79 1 (:DEFINITION BINARY-APPEND))
                       (71 25 (:REWRITE DEFAULT-<-2))
                       (58 1 (:REWRITE REPEAT-WHEN-ZP))
                       (44 25 (:REWRITE DEFAULT-+-2))
                       (40 40 (:REWRITE CONSP-BY-LEN))
                       (37 25 (:REWRITE DEFAULT-<-1))
                       (30 25 (:REWRITE DEFAULT-+-1))
                       (15 15 (:REWRITE DEFAULT-CDR))
                       (15 15 (:REWRITE CONSP-OF-CDR-BY-LEN))
                       (6 6 (:TYPE-PRESCRIPTION REPEAT))
                       (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
                       (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
                       (2 2
                          (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
                       (1 1 (:TYPE-PRESCRIPTION ZP))
                       (1 1 (:REWRITE EQUAL-CONSTANT-+))
                       (1 1 (:REWRITE DEFAULT-CAR)))
(STR::CHARLISTEQV-IMPLIES-EQUAL-RPADCHARS-1
     (116 2 (:REWRITE REPEAT-WHEN-ZP))
     (92 2 (:REWRITE ZP-OPEN))
     (72 8 (:REWRITE NEGATIVE-WHEN-NATP))
     (48 4 (:REWRITE NATP-RW))
     (42 2 (:DEFINITION BINARY-APPEND))
     (36 12 (:REWRITE DEFAULT-<-2))
     (36 4 (:DEFINITION LEN))
     (33 1
         (:REWRITE STR::CHARLISTEQV-WHEN-NOT-SAME-LENS))
     (32 32 (:REWRITE CONSP-BY-LEN))
     (28 2
         (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
     (24 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
     (22 2 (:DEFINITION CHARACTER-LISTP))
     (20 20
         (:TYPE-PRESCRIPTION MAKE-CHARACTER-LIST))
     (20 8 (:REWRITE LEN-WHEN-ATOM))
     (16 8 (:REWRITE DEFAULT-CDR))
     (14 14 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
     (14 8 (:REWRITE DEFAULT-+-2))
     (12 12 (:TYPE-PRESCRIPTION NATP))
     (12 12 (:REWRITE DEFAULT-<-1))
     (12 8
         (:REWRITE STR::CONSP-OF-MAKE-CHARACTER-LIST))
     (12 4 (:REWRITE DEFAULT-CAR))
     (10 8 (:REWRITE DEFAULT-+-1))
     (6 6 (:REWRITE CONSP-OF-CDR-BY-LEN))
     (4 2
        (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
     (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
     (4 2
        (:REWRITE CHARACTERP-OF-CAR-WHEN-CHARACTER-LISTP))
     (4 2
        (:REWRITE CHARACTER-LISTP-OF-CDR-WHEN-CHARACTER-LISTP))
     (2 2 (:TYPE-PRESCRIPTION ZP))
     (2 1
        (:REWRITE STR::CHARLISTEQV-WHEN-NOT-CONSP-RIGHT))
     (2 1
        (:REWRITE STR::CHARLISTEQV-WHEN-NOT-CONSP-LEFT)))
(STR::ICHARLISTEQV-IMPLIES-ICHARLISTEQV-RPADCHARS-1
     (408 6 (:REWRITE CONSP-OF-REPEAT))
     (288 4
          (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
     (236 8 (:REWRITE ZP-OPEN))
     (158 2 (:DEFINITION BINARY-APPEND))
     (144 2 (:REWRITE CONSP-OF-APPEND))
     (116 2 (:REWRITE REPEAT-WHEN-ZP))
     (108 24 (:REWRITE DEFAULT-<-2))
     (81 2
         (:REWRITE STR::ICHARLISTEQV-WHEN-NOT-CONSP-RIGHT))
     (81 2
         (:REWRITE STR::ICHARLISTEQV-WHEN-NOT-CONSP-LEFT))
     (72 8 (:REWRITE NEGATIVE-WHEN-NATP))
     (48 4 (:REWRITE NATP-RW))
     (36 4 (:DEFINITION LEN))
     (34 2
         (:REWRITE STR::ICHARLISTEQV-WHEN-NOT-SAME-LENS))
     (28 28 (:REWRITE CONSP-BY-LEN))
     (24 24 (:REWRITE DEFAULT-<-1))
     (20 8 (:REWRITE LEN-WHEN-ATOM))
     (14 14 (:TYPE-PRESCRIPTION REPEAT))
     (14 8 (:REWRITE DEFAULT-+-2))
     (12 12 (:TYPE-PRESCRIPTION NATP))
     (10 8 (:REWRITE DEFAULT-+-1))
     (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
     (8 4
        (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
     (6 6 (:REWRITE DEFAULT-CDR))
     (6 6 (:REWRITE CONSP-OF-CDR-BY-LEN))
     (4 4 (:TYPE-PRESCRIPTION BINARY-APPEND))
     (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
     (2 2 (:TYPE-PRESCRIPTION ZP))
     (2 2 (:REWRITE DEFAULT-CAR)))
(STR::RPADSTR (177 5 (:DEFINITION BINARY-APPEND))
              (152 4
                   (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
              (139 3 (:REWRITE CONSP-OF-REPEAT))
              (131 24 (:REWRITE LEN-WHEN-ATOM))
              (85 17 (:REWRITE DEFAULT-CDR))
              (80 80 (:REWRITE CONSP-BY-LEN))
              (66 5 (:REWRITE REPEAT-WHEN-ZP))
              (52 17 (:REWRITE DEFAULT-<-2))
              (40 22 (:REWRITE DEFAULT-+-2))
              (25 5 (:REWRITE NATP-RW))
              (25 5 (:REWRITE DEFAULT-CAR))
              (24 17 (:REWRITE DEFAULT-<-1))
              (22 22 (:REWRITE DEFAULT-+-1))
              (18 18
                  (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
              (17 17 (:REWRITE CONSP-OF-CDR-BY-LEN))
              (8 4 (:REWRITE DEFAULT-UNARY-MINUS))
              (6 6
                 (:REWRITE LEN-OF-NONEMPTY-STRING-IS-POSITIVE))
              (1 1 (:TYPE-PRESCRIPTION ZP)))
(STR::STRINGP-OF-RPADSTR)
(STR::LEN-OF-EXPLODE-OF-RPADSTR
     (298 16 (:DEFINITION LEN))
     (230 33 (:REWRITE LEN-WHEN-ATOM))
     (204 3 (:REWRITE CONSP-OF-REPEAT))
     (144 2
          (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
     (118 4 (:REWRITE ZP-OPEN))
     (93 1 (:DEFINITION BINARY-APPEND))
     (85 17 (:REWRITE DEFAULT-CDR))
     (71 25 (:REWRITE DEFAULT-<-2))
     (70 70 (:REWRITE CONSP-BY-LEN))
     (58 1 (:REWRITE REPEAT-WHEN-ZP))
     (48 27 (:REWRITE DEFAULT-+-2))
     (37 25 (:REWRITE DEFAULT-<-1))
     (32 27 (:REWRITE DEFAULT-+-1))
     (17 17
         (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
     (17 17 (:REWRITE CONSP-OF-CDR-BY-LEN))
     (14 2
         (:REWRITE STR::EQUAL-OF-IMPLODE-WITH-EMPTY-STRING))
     (12 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
     (10 10
         (:TYPE-PRESCRIPTION STRINGP-OF-IMPLODE))
     (10 2 (:DEFINITION ATOM))
     (8 8 (:TYPE-PRESCRIPTION STR::RPADCHARS))
     (5 1 (:REWRITE DEFAULT-CAR))
     (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
     (2 2
        (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
     (1 1 (:TYPE-PRESCRIPTION ZP))
     (1 1 (:REWRITE EQUAL-CONSTANT-+)))
(STR::STREQV-IMPLIES-EQUAL-RPADSTR-1)
(STR::ISTREQV-IMPLIES-ISTREQV-RPADSTR-1
     (601 12 (:REWRITE CONSP-OF-REPEAT))
     (500 6
          (:REWRITE STR::ICHARLISTEQV-WHEN-NOT-SAME-LENS))
     (376 8
          (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
     (332 15 (:REWRITE ZP-OPEN))
     (292 2 (:REWRITE LEN-OF-APPEND))
     (286 4 (:DEFINITION BINARY-APPEND))
     (247 13 (:DEFINITION LEN))
     (219 28 (:REWRITE LEN-WHEN-ATOM))
     (214 4 (:REWRITE CONSP-OF-APPEND))
     (164 2 (:REWRITE LEN-OF-REPEAT))
     (149 6
          (:REWRITE STR::ICHARLISTEQV-WHEN-NOT-CONSP-RIGHT))
     (141 4 (:REWRITE REPEAT-WHEN-ZP))
     (140 45 (:REWRITE DEFAULT-<-2))
     (134 8 (:REWRITE NATP-RW))
     (99 99 (:REWRITE CONSP-BY-LEN))
     (85 17 (:REWRITE DEFAULT-CDR))
     (79 45 (:REWRITE DEFAULT-<-1))
     (43 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
     (42 23 (:REWRITE DEFAULT-+-2))
     (29 23 (:REWRITE DEFAULT-+-1))
     (26 13
         (:TYPE-PRESCRIPTION |x < y  =>  0 < y-x|))
     (24 6 (:REWRITE <-0-+-NEGATIVE-2))
     (22 22 (:TYPE-PRESCRIPTION NATP))
     (20 4 (:REWRITE DEFAULT-CAR))
     (17 17 (:REWRITE CONSP-OF-CDR-BY-LEN))
     (14 2 (:REWRITE |(equal 0 (len x))|))
     (10 10
         (:LINEAR LEN-OF-NONEMPTY-STRING-IS-POSITIVE))
     (8 4 (:REWRITE DEFAULT-UNARY-MINUS))
     (3 3 (:TYPE-PRESCRIPTION ZP))
     (2 2 (:TYPE-PRESCRIPTION NFIX))
     (2 2
        (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
     (2 2
        (:REWRITE LENGTH-ZERO-WHEN-STRINGP-ALT)))
(STR::LPADCHARS (66 2 (:DEFINITION BINARY-APPEND))
                (59 6 (:REWRITE CONSP-OF-REPEAT))
                (59 1 (:REWRITE EQUAL-OF-APPEND-REPEAT))
                (57 5 (:DEFINITION LEN))
                (42 10 (:REWRITE LEN-WHEN-ATOM))
                (24 24 (:REWRITE CONSP-BY-LEN))
                (24 2 (:DEFINITION CHARACTER-LISTP))
                (21 9 (:REWRITE DEFAULT-CDR))
                (20 10 (:REWRITE DEFAULT-<-1))
                (16 8 (:REWRITE DEFAULT-+-2))
                (12 10 (:REWRITE DEFAULT-<-2))
                (8 8 (:REWRITE DEFAULT-+-1))
                (8 2
                   (:REWRITE CHARACTERP-OF-CAR-WHEN-CHARACTER-LISTP))
                (8 2
                   (:REWRITE CHARACTER-LISTP-OF-CDR-WHEN-CHARACTER-LISTP))
                (7 7 (:REWRITE CONSP-OF-CDR-BY-LEN))
                (6 3 (:REWRITE DEFAULT-UNARY-MINUS))
                (6 2 (:REWRITE CAR-OF-REPEAT))
                (2 2 (:REWRITE NATP-RW))
                (2 2 (:REWRITE DEFAULT-CAR)))
(STR::CHARACTER-LISTP-OF-LPADCHARS
     (122 3 (:REWRITE CONSP-OF-REPEAT))
     (106 5 (:DEFINITION NOT))
     (94 3 (:REWRITE ZP-OPEN))
     (78 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
     (78 1 (:DEFINITION BINARY-APPEND))
     (58 1 (:REWRITE REPEAT-WHEN-ZP))
     (42 10 (:REWRITE DEFAULT-<-2))
     (36 4 (:REWRITE NEGATIVE-WHEN-NATP))
     (24 2 (:REWRITE NATP-RW))
     (14 1
         (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
     (11 1 (:DEFINITION CHARACTER-LISTP))
     (10 10 (:REWRITE DEFAULT-<-1))
     (9 9 (:REWRITE CONSP-BY-LEN))
     (9 1 (:DEFINITION LEN))
     (7 3 (:REWRITE DEFAULT-CDR))
     (6 6 (:TYPE-PRESCRIPTION NATP))
     (5 3 (:REWRITE DEFAULT-+-2))
     (5 2 (:REWRITE LEN-WHEN-ATOM))
     (4 3 (:REWRITE DEFAULT-+-1))
     (2 2 (:REWRITE CONSP-OF-CDR-BY-LEN))
     (2 1
        (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
     (2 1 (:REWRITE DEFAULT-UNARY-MINUS))
     (2 1
        (:REWRITE CHARACTERP-OF-CAR-WHEN-CHARACTER-LISTP))
     (2 1
        (:REWRITE CHARACTER-LISTP-OF-CDR-WHEN-CHARACTER-LISTP))
     (1 1 (:TYPE-PRESCRIPTION ZP))
     (1 1 (:REWRITE DEFAULT-CAR))
     (1 1 (:REWRITE CAR-OF-REPEAT)))
(STR::LEN-OF-LPADCHARS (190 4 (:REWRITE CONSP-OF-REPEAT))
                       (122 14 (:DEFINITION LEN))
                       (118 4 (:REWRITE ZP-OPEN))
                       (80 1 (:DEFINITION BINARY-APPEND))
                       (78 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
                       (71 25 (:REWRITE DEFAULT-<-2))
                       (58 1 (:REWRITE REPEAT-WHEN-ZP))
                       (46 26 (:REWRITE DEFAULT-+-2))
                       (41 41 (:REWRITE CONSP-BY-LEN))
                       (37 25 (:REWRITE DEFAULT-<-1))
                       (32 26 (:REWRITE DEFAULT-+-1))
                       (19 15 (:REWRITE DEFAULT-CDR))
                       (15 15 (:REWRITE CONSP-OF-CDR-BY-LEN))
                       (10 10 (:TYPE-PRESCRIPTION REPEAT))
                       (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
                       (4 2
                          (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
                       (2 2
                          (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
                       (1 1 (:TYPE-PRESCRIPTION ZP))
                       (1 1 (:REWRITE EQUAL-CONSTANT-+))
                       (1 1 (:REWRITE CAR-OF-REPEAT)))
(STR::CHARLISTEQV-IMPLIES-EQUAL-LPADCHARS-1
     (244 6 (:REWRITE CONSP-OF-REPEAT))
     (188 6 (:REWRITE ZP-OPEN))
     (156 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
     (156 2 (:DEFINITION BINARY-APPEND))
     (116 2 (:REWRITE REPEAT-WHEN-ZP))
     (84 20 (:REWRITE DEFAULT-<-2))
     (72 8 (:REWRITE NEGATIVE-WHEN-NATP))
     (48 4 (:REWRITE NATP-RW))
     (36 4 (:DEFINITION LEN))
     (33 1
         (:REWRITE STR::CHARLISTEQV-WHEN-NOT-SAME-LENS))
     (28 2
         (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
     (26 26 (:REWRITE CONSP-BY-LEN))
     (22 2 (:DEFINITION CHARACTER-LISTP))
     (20 20 (:REWRITE DEFAULT-<-1))
     (20 8 (:REWRITE LEN-WHEN-ATOM))
     (16 16 (:TYPE-PRESCRIPTION REPEAT))
     (16 8 (:REWRITE DEFAULT-CDR))
     (14 14 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
     (14 8 (:REWRITE DEFAULT-+-2))
     (12 12 (:TYPE-PRESCRIPTION NATP))
     (10 8 (:REWRITE DEFAULT-+-1))
     (6 6 (:REWRITE CONSP-OF-CDR-BY-LEN))
     (4 2
        (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
     (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
     (4 2
        (:REWRITE CHARACTERP-OF-CAR-WHEN-CHARACTER-LISTP))
     (4 2
        (:REWRITE CHARACTER-LISTP-OF-CDR-WHEN-CHARACTER-LISTP))
     (2 2 (:TYPE-PRESCRIPTION ZP))
     (2 2 (:REWRITE DEFAULT-CAR))
     (2 2 (:REWRITE CAR-OF-REPEAT))
     (2 1
        (:REWRITE STR::CHARLISTEQV-WHEN-NOT-CONSP-RIGHT))
     (2 1
        (:REWRITE STR::CHARLISTEQV-WHEN-NOT-CONSP-LEFT)))
(STR::ICHARLISTEQV-IMPLIES-ICHARLISTEQV-LPADCHARS-1
     (380 8 (:REWRITE CONSP-OF-REPEAT))
     (236 8 (:REWRITE ZP-OPEN))
     (164 2 (:REWRITE CONSP-OF-APPEND))
     (160 2 (:DEFINITION BINARY-APPEND))
     (156 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
     (116 2 (:REWRITE REPEAT-WHEN-ZP))
     (108 24 (:REWRITE DEFAULT-<-2))
     (93 2
         (:REWRITE STR::ICHARLISTEQV-WHEN-NOT-CONSP-RIGHT))
     (93 2
         (:REWRITE STR::ICHARLISTEQV-WHEN-NOT-CONSP-LEFT))
     (72 8 (:REWRITE NEGATIVE-WHEN-NATP))
     (48 4 (:REWRITE NATP-RW))
     (36 4 (:DEFINITION LEN))
     (34 2
         (:REWRITE STR::ICHARLISTEQV-WHEN-NOT-SAME-LENS))
     (30 30 (:REWRITE CONSP-BY-LEN))
     (24 24 (:REWRITE DEFAULT-<-1))
     (22 22 (:TYPE-PRESCRIPTION REPEAT))
     (20 8 (:REWRITE LEN-WHEN-ATOM))
     (14 8 (:REWRITE DEFAULT-+-2))
     (14 6 (:REWRITE DEFAULT-CDR))
     (12 12 (:TYPE-PRESCRIPTION NATP))
     (12 4
         (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
     (10 8 (:REWRITE DEFAULT-+-1))
     (8 4
        (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
     (6 6 (:REWRITE CONSP-OF-CDR-BY-LEN))
     (4 4 (:TYPE-PRESCRIPTION TRUE-LISTP))
     (4 4 (:TYPE-PRESCRIPTION BINARY-APPEND))
     (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
     (2 2 (:TYPE-PRESCRIPTION ZP))
     (2 2 (:REWRITE CAR-OF-REPEAT)))
(STR::LPADSTR (152 8 (:DEFINITION LEN))
              (140 9 (:REWRITE CONSP-OF-REPEAT))
              (129 3 (:DEFINITION BINARY-APPEND))
              (94 3 (:REWRITE ZP-OPEN))
              (91 16 (:REWRITE LEN-WHEN-ATOM))
              (64 3 (:REWRITE REPEAT-WHEN-ZP))
              (59 11 (:REWRITE DEFAULT-CDR))
              (50 16 (:REWRITE DEFAULT-<-2))
              (46 46 (:REWRITE CONSP-BY-LEN))
              (44 26 (:REWRITE STR::CONSP-OF-EXPLODE))
              (24 4 (:REWRITE NATP-RW))
              (22 16 (:REWRITE DEFAULT-<-1))
              (22 11 (:REWRITE DEFAULT-+-2))
              (19 4
                  (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
              (12 12
                  (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
              (11 11 (:REWRITE DEFAULT-+-1))
              (11 11 (:REWRITE CONSP-OF-CDR-BY-LEN))
              (8 4 (:REWRITE DEFAULT-UNARY-MINUS))
              (7 3 (:REWRITE CAR-OF-REPEAT))
              (5 5
                 (:LINEAR LEN-OF-NONEMPTY-STRING-IS-POSITIVE))
              (1 1 (:TYPE-PRESCRIPTION ZP)))
(STR::STRINGP-OF-LPADSTR)
(STR::LEN-OF-EXPLODE-OF-LPADSTR
     (298 16 (:DEFINITION LEN))
     (230 33 (:REWRITE LEN-WHEN-ATOM))
     (190 4 (:REWRITE CONSP-OF-REPEAT))
     (118 4 (:REWRITE ZP-OPEN))
     (85 17 (:REWRITE DEFAULT-CDR))
     (84 1 (:DEFINITION BINARY-APPEND))
     (78 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
     (71 25 (:REWRITE DEFAULT-<-2))
     (69 69 (:REWRITE CONSP-BY-LEN))
     (58 1 (:REWRITE REPEAT-WHEN-ZP))
     (50 28 (:REWRITE DEFAULT-+-2))
     (37 25 (:REWRITE DEFAULT-<-1))
     (34 28 (:REWRITE DEFAULT-+-1))
     (17 17
         (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
     (17 17 (:REWRITE CONSP-OF-CDR-BY-LEN))
     (14 2
         (:REWRITE STR::EQUAL-OF-IMPLODE-WITH-EMPTY-STRING))
     (12 2
         (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
     (10 10
         (:TYPE-PRESCRIPTION STRINGP-OF-IMPLODE))
     (10 2 (:DEFINITION ATOM))
     (8 8 (:TYPE-PRESCRIPTION STR::LPADCHARS))
     (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
     (2 2
        (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
     (1 1 (:TYPE-PRESCRIPTION ZP))
     (1 1 (:REWRITE EQUAL-CONSTANT-+))
     (1 1 (:REWRITE CAR-OF-REPEAT)))
(STR::STREQV-IMPLIES-EQUAL-LPADSTR-1)
(STR::ISTREQV-IMPLIES-ISTREQV-LPADSTR-1
     (745 12
          (:REWRITE STR::ICHARLISTEQV-WHEN-NOT-SAME-LENS))
     (573 16 (:REWRITE CONSP-OF-REPEAT))
     (414 22 (:DEFINITION LEN))
     (332 15 (:REWRITE ZP-OPEN))
     (323 46 (:REWRITE LEN-WHEN-ATOM))
     (302 2 (:REWRITE LEN-OF-APPEND))
     (268 4 (:DEFINITION BINARY-APPEND))
     (240 4 (:REWRITE CONSP-OF-APPEND))
     (196 12
          (:REWRITE STR::ICHARLISTEQV-WHEN-NOT-CONSP-RIGHT))
     (164 2 (:REWRITE LEN-OF-REPEAT))
     (145 49 (:REWRITE DEFAULT-<-2))
     (143 143 (:REWRITE CONSP-BY-LEN))
     (141 4 (:REWRITE REPEAT-WHEN-ZP))
     (140 10 (:REWRITE NATP-RW))
     (134 26 (:REWRITE DEFAULT-CDR))
     (84 49 (:REWRITE DEFAULT-<-1))
     (68 16
         (:LINEAR LEN-OF-NONEMPTY-STRING-IS-POSITIVE))
     (64 34 (:REWRITE DEFAULT-+-2))
     (43 8
         (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
     (42 34 (:REWRITE DEFAULT-+-1))
     (34 17
         (:TYPE-PRESCRIPTION |x < y  =>  0 < y-x|))
     (27 27 (:TYPE-PRESCRIPTION NATP))
     (26 26 (:REWRITE CONSP-OF-CDR-BY-LEN))
     (24 6 (:REWRITE <-0-+-NEGATIVE-2))
     (14 2 (:REWRITE |(equal 0 (len x))|))
     (8 4 (:REWRITE DEFAULT-UNARY-MINUS))
     (8 4 (:REWRITE CAR-OF-REPEAT))
     (4 4 (:TYPE-PRESCRIPTION NFIX))
     (3 3 (:TYPE-PRESCRIPTION ZP))
     (3 3
        (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
     (2 2
        (:REWRITE LENGTH-ZERO-WHEN-STRINGP-ALT)))
(STR::TRIM-AUX)
(STR::CHARACTER-LISTP-OF-TRIM-AUX (25 25 (:REWRITE DEFAULT-CAR))
                                  (17 17 (:REWRITE CONSP-BY-LEN))
                                  (14 14 (:REWRITE DEFAULT-CDR)))
(STR::TRUE-LISTP-WHEN-CHARACTER-LISTP)
(STR::TRIM-BAG (46 2 (:DEFINITION STR::TRIM-AUX))
               (15 7 (:REWRITE DEFAULT-CDR))
               (15 7 (:REWRITE DEFAULT-CAR))
               (14 14 (:REWRITE CONSP-BY-LEN))
               (12 2 (:DEFINITION MEMBER-EQUAL))
               (10 2 (:REWRITE REV-WHEN-NOT-CONSP))
               (7 7 (:TYPE-PRESCRIPTION REV))
               (5 3 (:REWRITE CONSP-OF-REV))
               (4 3 (:REWRITE STR::CONSP-OF-EXPLODE))
               (2 2 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
               (1 1
                  (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP)))
(STR::STRINGP-OF-TRIM-BAG)
(STR::TRIM)
(STR::STRINGP-OF-TRIM)
