(RM-LIST-EXTRA-HYPOTHESIS
 (394 7 (:REWRITE STRING-LISTP-WHEN-FAT32-FILENAME-LIST-P))
 (342 38 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (318 4 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (282 41 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (261 8 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (213 12 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (205 4 (:REWRITE SUBSETP-CAR-MEMBER))
 (183 2 (:DEFINITION MEMBER-EQUAL))
 (136 41 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (136 41 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (98 98 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (73 6 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (62 19 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (50 4 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (45 4 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (41 41 (:REWRITE SUBSETP-TRANS2))
 (41 41 (:REWRITE SUBSETP-TRANS))
 (30 4 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (29 29 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (29 29 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (29 29 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (29 29 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (29 29 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (29 29 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (29 29 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (29 29 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (23 1 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (10 10 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (8 8 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (8 8 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (8 8 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (7 7 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (6 1 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (5 5 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 )
(RM-LIST-CORRECTNESS-1-LEMMA-1
 (886 13 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (706 13 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (529 26 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (407 8 (:REWRITE SUBSETP-CAR-MEMBER))
 (319 4 (:DEFINITION MEMBER-EQUAL))
 (290 41 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (173 8 (:REWRITE RM-2-GUARD-LEMMA-1))
 (167 13 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (147 9 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (138 13 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (137 27 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (126 39 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (126 39 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (102 13 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (42 42 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (42 42 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (42 42 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (42 42 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (42 42 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (42 42 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (42 42 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (42 42 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (39 39 (:REWRITE SUBSETP-TRANS2))
 (39 39 (:REWRITE SUBSETP-TRANS))
 (34 34 (:TYPE-PRESCRIPTION NONEMPTY-STRING-LISTP))
 (34 34 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (34 34 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (31 4 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (26 26 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (26 26 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (26 26 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (24 4 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (20 20 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (17 17 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (17 17 (:REWRITE DEFAULT-CDR))
 (17 17 (:REWRITE DEFAULT-CAR))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (6 2 (:REWRITE LOFAT-UNLINK-REFINEMENT))
 (4 4 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 )
(RM-LIST-CORRECTNESS-1-LEMMA-2
 (60234 257 (:DEFINITION LOFAT-FIND-FILE))
 (24564 1028 (:DEFINITION FIND-D-E))
 (23487 257 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (21446 586 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (16444 484 (:REWRITE SUBSETP-CAR-MEMBER))
 (15640 115 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (15623 514 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (13541 257 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (12566 179 (:DEFINITION MEMBER-EQUAL))
 (12018 148 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (11718 264 (:DEFINITION LEN))
 (11603 123 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (11017 1588 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (9252 1028 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (8968 771 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (8050 115 (:DEFINITION CEILING))
 (7940 771 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (5504 2302 (:REWRITE DEFAULT-CDR))
 (5140 1028 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (4966 1434 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (4950 1434 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4337 274 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (4140 460 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (3855 3855 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (3505 3505 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (3505 3505 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (3505 3505 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (3505 3505 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (3505 3505 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (3505 3505 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (3505 3505 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (3505 3505 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (3450 115 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
 (3105 345 (:REWRITE ZP-OPEN))
 (3084 1028 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (2911 14 (:REWRITE ABS-PLACE-FILE-HELPER-OF-CTX-APP-LEMMA-1))
 (2732 214 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (2558 4 (:REWRITE LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (2511 2 (:REWRITE SUBLISTP-WHEN-PREFIXP))
 (2297 8 (:REWRITE COLLAPSE-HIFAT-PLACE-FILE-LEMMA-113))
 (2274 1323 (:REWRITE DEFAULT-<-2))
 (2219 1353 (:REWRITE DEFAULT-+-2))
 (2185 115 (:REWRITE DEFAULT-UNARY-/))
 (2183 2183 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (2064 2064 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (2056 2056 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (1948 487 (:REWRITE COMMUTATIVITY-OF-+))
 (1840 1353 (:REWRITE DEFAULT-+-1))
 (1814 1323 (:REWRITE DEFAULT-<-1))
 (1670 4 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (1658 5 (:DEFINITION FAT32-FILENAME-LIST-PREFIXP))
 (1602 1602 (:REWRITE DEFAULT-CAR))
 (1572 4 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1542 1542 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (1542 514 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (1434 1434 (:REWRITE SUBSETP-TRANS2))
 (1434 1434 (:REWRITE SUBSETP-TRANS))
 (1346 4 (:DEFINITION STRING-LISTP))
 (1204 99 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (1196 100 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-2))
 (1056 2 (:DEFINITION TRUE-LISTP))
 (1037 1037 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1036 1036 (:TYPE-PRESCRIPTION D-E-P))
 (920 920 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (901 213 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (888 48 (:REWRITE STR::CONSP-OF-EXPLODE))
 (864 96 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-17))
 (785 298 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (771 771 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (771 771 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (771 771 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (771 257 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (750 250 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (709 99 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (690 690 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (679 8 (:REWRITE STRING-LISTP-WHEN-FAT32-FILENAME-LIST-P))
 (639 213 (:REWRITE LOFAT-OPENDIR-CORRECTNESS-LEMMA-1))
 (586 586 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (575 575 (:TYPE-PRESCRIPTION NONNEGATIVE-INTEGER-QUOTIENT))
 (575 230 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (575 230 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (500 500 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (460 115 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (404 33 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (384 32 (:LINEAR LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1))
 (369 123 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (369 123 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (358 358 (:REWRITE SUBSETP-MEMBER . 2))
 (358 358 (:REWRITE SUBSETP-MEMBER . 1))
 (324 36 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (288 36 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-40))
 (280 56 (:REWRITE LOFAT-TO-HIFAT-CORRECTNESS-2))
 (257 257 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (246 246 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (246 246 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (246 246 (:LINEAR LEN-WHEN-PREFIXP))
 (246 246 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (236 236 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (234 78 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-5))
 (232 8 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (230 115 (:REWRITE NFIX-WHEN-ZP))
 (230 115 (:REWRITE NFIX-WHEN-NATP))
 (230 115 (:REWRITE DEFAULT-UNARY-MINUS))
 (230 115 (:REWRITE DEFAULT-NUMERATOR))
 (230 115 (:REWRITE DEFAULT-DENOMINATOR))
 (230 115 (:REWRITE DEFAULT-*-2))
 (230 115 (:DEFINITION IFIX))
 (224 224 (:TYPE-PRESCRIPTION LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1 . 1))
 (210 8 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (198 198 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (198 198 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (191 39 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (187 39 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (172 4 (:REWRITE LEN-WHEN-PREFIXP))
 (138 4 (:REWRITE LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (123 123 (:LINEAR POSITION-WHEN-MEMBER))
 (123 123 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (118 118 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (115 115 (:TYPE-PRESCRIPTION ZP))
 (115 115 (:TYPE-PRESCRIPTION FAT32$C-P))
 (115 115 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (115 115 (:REWRITE DEFAULT-*-1))
 (115 19 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (100 14 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (77 4 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (72 72 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (72 72 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (64 64 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-58))
 (54 6 (:REWRITE CONSP-OF-LIST-FIX))
 (43 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (43 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (41 15 (:REWRITE LOFAT-FS-P-OF-RM-LIST))
 (24 24 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 (24 4 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (21 2 (:REWRITE SUBLISTP-WHEN-ATOM-RIGHT))
 (20 20 (:TYPE-PRESCRIPTION STRING-LISTP))
 (20 4 (:REWRITE TRUE-LISTP-WHEN-D-E-P))
 (20 4 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (18 2 (:REWRITE SUBLISTP-WHEN-ATOM-LEFT))
 (16 16 (:TYPE-PRESCRIPTION PREFIXP))
 (15 4 (:REWRITE FAT32-FILENAME-LIST-P-OF-LIST-FIX))
 (14 14 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 2))
 (14 14 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (12 12 (:REWRITE LOFAT-FS-P-OF-LOFAT-UNLINK))
 (12 4 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (10 10 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (8 8 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (8 8 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (8 8 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (8 8 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (8 4 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (6 6 (:TYPE-PRESCRIPTION SUBLISTP))
 (6 6 (:REWRITE TRUE-LISTP-OF-CDR-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP))
 (6 6 (:REWRITE TRUE-LISTP-OF-CDR-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP))
 (4 4 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 (4 4 (:TYPE-PRESCRIPTION SET::EMPTYP-TYPE))
 (4 4 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (4 4 (:REWRITE TRUE-LISTP-WHEN-FUNCTION-SYMBOL-LISTP))
 (4 4 (:REWRITE SET::IN-SET))
 (2 2 (:REWRITE SUBSETP-OF-CDR))
 (2 2 (:REWRITE SUBLISTP-COMPLETE))
 (1 1 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 )
(RM-LIST-CORRECTNESS-1
 (72966 563 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (63892 491 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (57945 1288 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (51434 270 (:DEFINITION LOFAT-FIND-FILE))
 (49812 270 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (40999 890 (:REWRITE SUBSETP-CAR-MEMBER))
 (33536 248 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (33342 5135 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (26340 520 (:DEFINITION LEN))
 (25160 1080 (:DEFINITION FIND-D-E))
 (22621 1381 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (17462 248 (:DEFINITION CEILING))
 (16090 540 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (12876 4553 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (12876 4553 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (12010 3536 (:REWRITE DEFAULT-CDR))
 (10874 6 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-2))
 (9720 1080 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (9260 810 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (8638 958 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (8180 810 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (7440 248 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
 (6636 728 (:REWRITE ZP-OPEN))
 (6604 315 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (6089 21 (:REWRITE STR::CONSP-OF-EXPLODE))
 (6070 6070 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (6070 6070 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (6070 6070 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6070 6070 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6070 6070 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (6070 6070 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (6070 6070 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (6070 6070 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (5400 1080 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (5065 40 (:REWRITE RM-2-GUARD-LEMMA-1))
 (5000 483 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (4814 248 (:REWRITE DEFAULT-UNARY-/))
 (4553 4553 (:REWRITE SUBSETP-TRANS2))
 (4553 4553 (:REWRITE SUBSETP-TRANS))
 (4425 729 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (4050 4050 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (3974 2246 (:REWRITE DEFAULT-<-2))
 (3834 2300 (:REWRITE DEFAULT-+-2))
 (3581 1 (:LINEAR GETOPT::DEFOPTIONS-LEMMA-8))
 (3579 1 (:DEFINITION STR::STRPREFIXP$INLINE))
 (3240 1080 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (3192 693 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (3066 2300 (:REWRITE DEFAULT-+-1))
 (3064 766 (:REWRITE COMMUTATIVITY-OF-+))
 (3012 2246 (:REWRITE DEFAULT-<-1))
 (3006 2566 (:REWRITE DEFAULT-CAR))
 (2706 270 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (2701 729 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (2598 2598 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (2571 2 (:LINEAR LOFAT-PLACE-FILE-HELPER-GUARD-LEMMA-1))
 (2508 275 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (2328 2328 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (2325 146 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (2237 26 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (2160 2160 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (2160 2160 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (1874 1373 (:REWRITE SUBSETP-MEMBER . 1))
 (1776 540 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (1713 1 (:LINEAR M1-REGULAR-FILE-P-CORRECTNESS-2))
 (1668 240 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (1620 1620 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (1599 27 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (1530 4 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (1518 27 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (1482 468 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (1480 344 (:REWRITE LOFAT-TO-HIFAT-CORRECTNESS-2))
 (1438 1438 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (1373 1373 (:REWRITE SUBSETP-MEMBER . 2))
 (1308 496 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (1308 496 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (1288 1288 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (1268 1 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (1240 1240 (:TYPE-PRESCRIPTION NONNEGATIVE-INTEGER-QUOTIENT))
 (1221 1 (:REWRITE PREFIXP-OF-CONS-LEFT))
 (1080 1080 (:TYPE-PRESCRIPTION D-E-P))
 (1043 966 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (1026 248 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (1006 1006 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (966 966 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (898 4 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (876 146 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (856 856 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (810 810 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (810 810 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (810 810 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (810 270 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (753 251 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (753 251 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (720 240 (:REWRITE LOFAT-OPENDIR-CORRECTNESS-LEMMA-1))
 (502 502 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (502 502 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (502 502 (:LINEAR LEN-WHEN-PREFIXP))
 (502 502 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (500 250 (:REWRITE DEFAULT-*-2))
 (496 248 (:REWRITE NFIX-WHEN-ZP))
 (496 248 (:REWRITE NFIX-WHEN-NATP))
 (496 248 (:REWRITE DEFAULT-UNARY-MINUS))
 (496 248 (:REWRITE DEFAULT-NUMERATOR))
 (496 248 (:REWRITE DEFAULT-DENOMINATOR))
 (496 248 (:DEFINITION IFIX))
 (452 428 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (320 320 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (282 248 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (270 270 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (251 251 (:LINEAR POSITION-WHEN-MEMBER))
 (251 251 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (250 250 (:REWRITE DEFAULT-*-1))
 (248 248 (:TYPE-PRESCRIPTION ZP))
 (248 248 (:TYPE-PRESCRIPTION FAT32$C-P))
 (247 2 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (243 27 (:REWRITE MEMBER-WHEN-ATOM))
 (235 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (168 14 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 (135 135 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (110 55 (:REWRITE SET-EQUIV-ASYM))
 (55 55 (:TYPE-PRESCRIPTION SET-EQUIV))
 (55 55 (:REWRITE SUBSETP-OF-CDR))
 (50 50 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (35 27 (:REWRITE SUBSETP-MEMBER . 3))
 (27 27 (:REWRITE SUBSETP-MEMBER . 4))
 (27 27 (:REWRITE NON-FREE-INDEX-LISTP-CORRECTNESS-2 . 1))
 (27 27 (:REWRITE INTERSECTP-MEMBER . 3))
 (27 27 (:REWRITE INTERSECTP-MEMBER . 2))
 (27 27 (:REWRITE FREE-INDEX-LISTP-CORRECTNESS-1))
 (21 1 (:REWRITE LIST-EQUIV-OF-NIL-RIGHT))
 (14 14 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (7 7 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (6 6 (:TYPE-PRESCRIPTION M1-DIRECTORY-FILE-P))
 (6 6 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (4 4 (:TYPE-PRESCRIPTION PREFIXP))
 (4 4 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (4 4 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (4 4 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (4 4 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (4 4 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (3 1 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (1 1 (:TYPE-PRESCRIPTION STR::STRPREFIXP$INLINE))
 (1 1 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (1 1 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (1 1 (:REWRITE M1-FILE-CONTENTS-P-OF-M1-FILE->CONTENTS))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 )
(LS-LIST-CORRECTNESS-1-LEMMA-1
 (1350 18 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (1134 18 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (916 36 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (688 16 (:REWRITE SUBSETP-CAR-MEMBER))
 (544 8 (:DEFINITION MEMBER-EQUAL))
 (442 61 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (208 56 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (208 56 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (198 18 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (164 18 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (138 28 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (128 8 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (108 18 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (59 59 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (59 59 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (59 59 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (59 59 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (59 59 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (59 59 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (59 59 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (59 59 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (56 56 (:REWRITE SUBSETP-TRANS2))
 (56 56 (:REWRITE SUBSETP-TRANS))
 (40 40 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (36 36 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (36 36 (:TYPE-PRESCRIPTION NONEMPTY-STRING-LISTP))
 (36 36 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (36 36 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (36 36 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (36 12 (:REWRITE LOFAT-LSTAT-REFINEMENT))
 (33 33 (:REWRITE DEFAULT-CAR))
 (24 24 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 (20 20 (:REWRITE DEFAULT-CDR))
 (18 18 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (16 16 (:REWRITE SUBSETP-MEMBER . 2))
 (16 16 (:REWRITE SUBSETP-MEMBER . 1))
 )
(LS-LIST-CORRECTNESS-1-LEMMA-2
 (392 2 (:DEFINITION LOFAT-FIND-FILE))
 (200 8 (:DEFINITION FIND-D-E))
 (194 2 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (147 3 (:DEFINITION LEN))
 (126 4 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (72 8 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (72 6 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (68 4 (:REWRITE ZP-OPEN))
 (67 17 (:REWRITE DEFAULT-CDR))
 (64 6 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (60 2 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (42 42 (:TYPE-PRESCRIPTION CLUSTER-SIZE))
 (40 8 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (36 4 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (35 2 (:REWRITE STR::CONSP-OF-EXPLODE))
 (30 30 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 (30 30 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (25 7 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (24 8 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (22 12 (:REWRITE DEFAULT-<-2))
 (22 2 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (21 7 (:REWRITE LOFAT-OPENDIR-CORRECTNESS-LEMMA-1))
 (20 20 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (20 20 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (20 20 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (20 20 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (20 20 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (20 20 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (20 20 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (20 20 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (19 19 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (19 19 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (16 16 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (16 16 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (16 16 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (16 1 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (15 15 (:TYPE-PRESCRIPTION LEN))
 (14 14 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (14 12 (:REWRITE DEFAULT-<-1))
 (12 12 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (12 7 (:REWRITE DEFAULT-+-2))
 (12 6 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (12 4 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (12 2 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (12 2 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (10 10 (:REWRITE DEFAULT-CAR))
 (9 7 (:REWRITE DEFAULT-+-1))
 (8 8 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (8 8 (:TYPE-PRESCRIPTION D-E-P))
 (8 8 (:TYPE-PRESCRIPTION D-E-LIST-P))
 (8 2 (:REWRITE COMMUTATIVITY-OF-+))
 (6 6 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (6 6 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (6 6 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (6 6 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (6 6 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (6 6 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (6 2 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (6 2 (:REWRITE LOFAT-LSTAT-REFINEMENT))
 (6 2 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (6 2 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-5))
 (6 2 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (6 2 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (6 2 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (6 2 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (5 1 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (4 4 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (4 4 (:TYPE-PRESCRIPTION FAT32$C-P))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (4 4 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (4 4 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 4 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (3 3 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 (2 2 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER))
 (2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(LS-LIST-CORRECTNESS-1
 (3967 65 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (3271 65 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (2744 130 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (1805 260 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (1350 47 (:REWRITE SUBSETP-CAR-MEMBER))
 (897 16 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (849 16 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (789 183 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (789 183 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (785 113 (:REWRITE SUBSETP-MEMBER . 1))
 (631 65 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (617 100 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (586 39 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (332 35 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (262 262 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (262 262 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (262 262 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (262 262 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (262 262 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (262 262 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (262 262 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (262 262 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (246 35 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (190 130 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (183 183 (:REWRITE SUBSETP-TRANS2))
 (183 183 (:REWRITE SUBSETP-TRANS))
 (146 146 (:REWRITE DEFAULT-CDR))
 (144 144 (:REWRITE DEFAULT-CAR))
 (144 16 (:REWRITE MEMBER-WHEN-ATOM))
 (135 45 (:REWRITE LOFAT-LSTAT-REFINEMENT))
 (130 130 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (130 130 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (113 113 (:REWRITE SUBSETP-MEMBER . 2))
 (106 106 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (90 90 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 (80 80 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (60 30 (:REWRITE SET-EQUIV-ASYM))
 (53 53 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (50 6 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (40 16 (:REWRITE SUBSETP-MEMBER . 3))
 (36 6 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (30 30 (:TYPE-PRESCRIPTION SET-EQUIV))
 (30 30 (:REWRITE SUBSETP-OF-CDR))
 (16 16 (:REWRITE SUBSETP-MEMBER . 4))
 (16 16 (:REWRITE NON-FREE-INDEX-LISTP-CORRECTNESS-2 . 1))
 (16 16 (:REWRITE INTERSECTP-MEMBER . 3))
 (16 16 (:REWRITE INTERSECTP-MEMBER . 2))
 (16 16 (:REWRITE FREE-INDEX-LISTP-CORRECTNESS-1))
 )
(LSTAT-AFTER-UNLINK-1
 (7812 42 (:DEFINITION LOFAT-FIND-FILE))
 (3864 168 (:DEFINITION FIND-D-E))
 (2668 42 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (2478 84 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (1768 13 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (1719 37 (:DEFINITION LEN))
 (1512 168 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (1428 126 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (1260 126 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (910 13 (:DEFINITION CEILING))
 (872 334 (:REWRITE DEFAULT-CDR))
 (840 168 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (630 630 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (504 168 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (468 52 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (403 403 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (390 13 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
 (387 387 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (387 387 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (387 387 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (387 387 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (387 387 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (387 387 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (387 387 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (387 387 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (378 42 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (360 48 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (351 39 (:REWRITE ZP-OPEN))
 (336 336 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (336 336 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (333 18 (:REWRITE STR::CONSP-OF-EXPLODE))
 (304 186 (:REWRITE DEFAULT-+-2))
 (295 175 (:REWRITE DEFAULT-<-2))
 (272 68 (:REWRITE COMMUTATIVITY-OF-+))
 (254 186 (:REWRITE DEFAULT-+-1))
 (252 252 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (252 84 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (247 13 (:REWRITE DEFAULT-UNARY-/))
 (243 175 (:REWRITE DEFAULT-<-1))
 (213 213 (:REWRITE DEFAULT-CAR))
 (210 42 (:REWRITE SUBSETP-CAR-MEMBER))
 (204 68 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (174 57 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (171 57 (:REWRITE LOFAT-OPENDIR-CORRECTNESS-LEMMA-1))
 (168 168 (:TYPE-PRESCRIPTION D-E-P))
 (168 168 (:TYPE-PRESCRIPTION D-E-LIST-P))
 (127 15 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-2))
 (126 126 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (126 126 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (126 126 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (126 42 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (84 84 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (84 42 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (82 10 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-17))
 (81 9 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (78 78 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (65 65 (:TYPE-PRESCRIPTION NONNEGATIVE-INTEGER-QUOTIENT))
 (65 26 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (65 26 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (60 9 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (57 57 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (52 52 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (52 13 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (48 48 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (48 3 (:DEFINITION MEMBER-EQUAL))
 (42 42 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (42 42 (:REWRITE SUBSETP-REFL))
 (39 13 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (39 13 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (36 12 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-5))
 (36 4 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (36 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (36 3 (:LINEAR LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1))
 (32 4 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-40))
 (28 8 (:REWRITE LOFAT-TO-HIFAT-CORRECTNESS-2))
 (27 27 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (26 26 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (26 26 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (26 26 (:LINEAR LEN-WHEN-PREFIXP))
 (26 26 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (26 13 (:REWRITE NFIX-WHEN-ZP))
 (26 13 (:REWRITE NFIX-WHEN-NATP))
 (26 13 (:REWRITE DEFAULT-UNARY-MINUS))
 (26 13 (:REWRITE DEFAULT-NUMERATOR))
 (26 13 (:REWRITE DEFAULT-DENOMINATOR))
 (26 13 (:REWRITE DEFAULT-*-2))
 (26 13 (:DEFINITION IFIX))
 (21 21 (:TYPE-PRESCRIPTION LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1 . 1))
 (20 20 (:TYPE-PRESCRIPTION STRINGP-OF-GET-CC-CONTENTS))
 (13 13 (:TYPE-PRESCRIPTION ZP))
 (13 13 (:TYPE-PRESCRIPTION FAT32$C-P))
 (13 13 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (13 13 (:REWRITE DEFAULT-*-1))
 (13 13 (:LINEAR POSITION-WHEN-MEMBER))
 (13 13 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (13 3 (:REWRITE HIFAT-REMOVE-FILE-CORRECTNESS-4))
 (9 1 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 (8 8 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (8 8 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 (6 6 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-58))
 (1 1 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 )
(LS-1-AFTER-RM-1
 (10990 30 (:DEFINITION INTERSECTION-EQUAL))
 (8248 22 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (7257 942 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (6248 8 (:REWRITE STRINGP-OF-NTH))
 (6136 8 (:DEFINITION STRING-LISTP))
 (5467 84 (:DEFINITION MEMBER-EQUAL))
 (4784 90 (:REWRITE INTERSECTION$-WHEN-SUBSETP . 1))
 (4782 168 (:REWRITE SUBSETP-CAR-MEMBER))
 (4325 16 (:REWRITE STRING-LISTP-WHEN-FAT32-FILENAME-LIST-P))
 (3577 8 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (3454 64 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (3304 63 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (3262 64 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (3091 676 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (3014 676 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2918 135 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (2045 2045 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (1732 126 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (1693 20 (:REWRITE SUBSETP-INTERSECTION-EQUAL))
 (1592 238 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (1063 63 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (1036 676 (:REWRITE SUBSETP-TRANS))
 (991 991 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (991 991 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (991 991 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (991 991 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (991 991 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (991 991 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (991 991 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (991 991 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (900 8 (:REWRITE FAT32-FILENAME-P-OF-NTH-WHEN-FAT32-FILENAME-LIST-P))
 (842 119 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (688 676 (:REWRITE SUBSETP-TRANS2))
 (667 40 (:REWRITE STRING-TO-LOFAT-IGNORE))
 (576 64 (:REWRITE MEMBER-WHEN-ATOM))
 (539 32 (:REWRITE FAT32-FILENAME-LIST-P-OF-INTERSECTION-EQUAL-2))
 (520 7 (:DEFINITION LS-LIST))
 (483 22 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (473 32 (:REWRITE FAT32-FILENAME-LIST-P-OF-INTERSECTION-EQUAL-1))
 (406 62 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (384 8 (:REWRITE NONEMPTY-STRINGP-OF-NTH-WHEN-NONEMPTY-STRING-LISTP))
 (383 4 (:REWRITE MEMBER-OF-NTH-WHEN-NOT-INTERSECTP))
 (364 22 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (327 327 (:REWRITE DEFAULT-CDR))
 (320 320 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (255 8 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (241 241 (:REWRITE DEFAULT-CAR))
 (239 239 (:TYPE-PRESCRIPTION INTERSECTION-EQUAL))
 (225 15 (:DEFINITION LEN))
 (224 16 (:REWRITE NONEMPTY-STRING-LISTP-OF-INTERSECTION-EQUAL-2))
 (224 16 (:REWRITE NONEMPTY-STRING-LISTP-OF-INTERSECTION-EQUAL-1))
 (216 4 (:REWRITE CONSP-OF-NTH-WHEN-ALISTP))
 (198 198 (:REWRITE SUBSETP-MEMBER . 2))
 (198 198 (:REWRITE SUBSETP-MEMBER . 1))
 (196 98 (:REWRITE SET-EQUIV-ASYM))
 (164 4 (:REWRITE INTERSECTP-IS-COMMUTATIVE))
 (144 4 (:DEFINITION ALISTP))
 (126 126 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (126 126 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (126 126 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (124 124 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (108 8 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (107 12 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (106 106 (:TYPE-PRESCRIPTION SET-EQUIV))
 (98 98 (:REWRITE SUBSETP-OF-CDR))
 (84 8 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (64 64 (:REWRITE NON-FREE-INDEX-LISTP-CORRECTNESS-2 . 1))
 (64 64 (:REWRITE INTERSECTP-MEMBER . 3))
 (64 64 (:REWRITE INTERSECTP-MEMBER . 2))
 (64 64 (:REWRITE FREE-INDEX-LISTP-CORRECTNESS-1))
 (60 60 (:REWRITE SUBSETP-MEMBER . 4))
 (60 60 (:REWRITE SUBSETP-MEMBER . 3))
 (40 40 (:TYPE-PRESCRIPTION STRING-LISTP))
 (30 15 (:REWRITE DEFAULT-+-2))
 (20 20 (:TYPE-PRESCRIPTION ALISTP))
 (20 4 (:REWRITE LOFAT-TO-HIFAT-CORRECTNESS-2))
 (17 11 (:REWRITE DEFAULT-<-2))
 (16 16 (:TYPE-PRESCRIPTION STRINGP-OF-GET-CC-CONTENTS))
 (16 16 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (16 16 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (15 15 (:REWRITE DEFAULT-+-1))
 (12 12 (:REWRITE NTH-WHEN-PREFIXP))
 (12 4 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (12 4 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (11 11 (:REWRITE DEFAULT-<-1))
 (10 10 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (8 8 (:TYPE-PRESCRIPTION INTERSECTP-EQUAL))
 (8 8 (:REWRITE SUBSETP-REFL))
 (8 8 (:REWRITE INTERSECTP-MEMBER . 1))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (8 8 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (8 8 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (8 8 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (8 8 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (4 4 (:LINEAR POSITION-WHEN-MEMBER))
 (4 4 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1 1 (:TYPE-PRESCRIPTION LOFAT-TO-STRING))
 )