(TRUNCATE-LIST-EXTRA-HYPOTHESIS
 (152492 38 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-2))
 (149235 23 (:DEFINITION LOFAT-PLACE-FILE))
 (39130 14 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (26377 1479 (:DEFINITION FIND-D-E))
 (26292 138 (:REWRITE LEN-OF-NATS=>CHARS))
 (26154 138 (:REWRITE LEN-OF-INSERT-D-E))
 (19413 92 (:REWRITE LOFAT-REMOVE-FILE-CORRECTNESS-LEMMA-13))
 (19399 253 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-8))
 (17712 138 (:REWRITE LEN-OF-PLACE-D-E))
 (15552 1092 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (14006 4550 (:REWRITE DEFAULT-CDR))
 (13478 184 (:REWRITE UPDATE-FATI-OF-UPDATE-FATI-COINCIDENT))
 (11776 184 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (11766 498 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (11569 782 (:REWRITE D-E-CC-UNDER-IFF . 2))
 (11440 88 (:DEFINITION LOFAT-FIND-FILE))
 (11372 92 (:DEFINITION INTEGER-LISTP))
 (10196 14 (:REWRITE TAKE-OF-LEN-FREE))
 (9969 1092 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (9545 9545 (:TYPE-PRESCRIPTION COUNT-FREE-CLUSTERS))
 (9545 138 (:REWRITE LAST-WHEN-EQUAL-LEN-1))
 (9430 184 (:REWRITE UPDATE-FATI-OF-FATI-WHEN-FAT32$C-P))
 (9164 138 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (8956 8956 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (8195 1617 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (8142 476 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (7991 4395 (:REWRITE DEFAULT-<-2))
 (7991 138 (:REWRITE INTEGERP-OF-CAR-OF-LAST-WHEN-INTEGER-LISTP))
 (7761 27 (:LINEAR GETOPT::DEFOPTIONS-LEMMA-8))
 (7707 27 (:DEFINITION STR::STRPREFIXP$INLINE))
 (7379 1451 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (7334 578 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (7155 590 (:REWRITE STR::CONSP-OF-EXPLODE))
 (6923 6923 (:TYPE-PRESCRIPTION D-E-FILE-SIZE))
 (6910 138 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (6716 414 (:REWRITE CONSP-OF-LAST))
 (6436 302 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (6382 2899 (:REWRITE DEFAULT-CAR))
 (6095 69 (:DEFINITION LAST))
 (5796 69 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-29))
 (5770 2557 (:REWRITE DEFAULT-+-2))
 (5697 4395 (:REWRITE DEFAULT-<-1))
 (5541 1755 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (5390 869 (:REWRITE NFIX-WHEN-ZP))
 (5350 5350 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (5129 920 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-COINCIDENT-LEMMA-8))
 (4725 23 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (4678 88 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (4669 1311 (:REWRITE LOFAT-FILE-P-WHEN-LOFAT-DIRECTORY-FILE-P-OR-LOFAT-REGULAR-FILE-P))
 (4536 119 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (4476 4476 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (4440 138 (:DEFINITION PLACE-D-E))
 (4428 184 (:REWRITE PLACE-CONTENTS-EXPANSION-1))
 (4335 54 (:LINEAR LOFAT-PLACE-FILE-HELPER-GUARD-LEMMA-1))
 (4081 237 (:DEFINITION MEMBER-EQUAL))
 (3850 777 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (3818 782 (:LINEAR D-E-FILE-SIZE-CORRECTNESS-1))
 (3818 184 (:REWRITE D-E-CC-UNDER-IFF . 3))
 (3751 243 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-2))
 (3726 3726 (:TYPE-PRESCRIPTION FIND-N-FREE-CLUSTERS))
 (3680 3680 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (3588 184 (:REWRITE LOFAT-FILE->CONTENTS-OF-LOFAT-FILE))
 (3588 23 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-33))
 (3581 119 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (3473 2116 (:TYPE-PRESCRIPTION LAST))
 (3465 281 (:REWRITE SUBSETP-CAR-MEMBER))
 (3450 3450 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-D-E-CC))
 (3427 3427 (:TYPE-PRESCRIPTION INTEGERP-OF-D-E-CC-CONTENTS))
 (3404 184 (:REWRITE LOFAT-FILE-CONTENTS-FIX-WHEN-LOFAT-FILE-CONTENTS-P))
 (3240 27 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (3174 3174 (:TYPE-PRESCRIPTION LOFAT-FILE))
 (2947 27 (:REWRITE PREFIXP-OF-CONS-LEFT))
 (2833 27 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (2759 2557 (:REWRITE DEFAULT-+-1))
 (2668 184 (:REWRITE LOFAT-FILE-CONTENTS-P-WHEN-STRINGP))
 (2579 8 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
 (2311 4 (:REWRITE CHARACTER-LISTP-OF-TAKE))
 (2242 2242 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (2231 92 (:DEFINITION NTH))
 (2231 46 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (2208 207 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (2168 154 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (2144 2144 (:TYPE-PRESCRIPTION NATP-OF-PLACE-CONTENTS))
 (1920 640 (:REWRITE PLACE-CONTENTS-EXPANSION-2))
 (1910 541 (:REWRITE DEFAULT-*-2))
 (1890 27 (:DEFINITION CEILING))
 (1863 207 (:DEFINITION NFIX))
 (1794 138 (:REWRITE DISTRIBUTIVITY))
 (1656 552 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-5))
 (1656 138 (:REWRITE CONSP-OF-FIND-N-FREE-CLUSTERS))
 (1632 1632 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (1610 92 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1575 525 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (1551 1551 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (1519 1519 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (1510 132 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (1491 1491 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (1424 320 (:REWRITE NATP-OF-PLACE-CONTENTS))
 (1384 550 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1384 550 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1312 270 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (1311 1311 (:REWRITE LOFAT-FILE-P-OF-LOFAT-FILE))
 (1311 138 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (1288 115 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (1284 428 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (1284 428 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (1253 1253 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (1248 416 (:REWRITE LOFAT-OPENDIR-CORRECTNESS-LEMMA-1))
 (1199 29 (:REWRITE STRING-LISTP-WHEN-FAT32-FILENAME-LIST-P))
 (1158 1158 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1150 230 (:DEFINITION BINARY-APPEND))
 (1147 1147 (:TYPE-PRESCRIPTION GOOD-ROOT-D-E-P))
 (1147 76 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1108 115 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-8))
 (1058 207 (:LINEAR PSEUDO-ROOT-D-E-CORRECTNESS-1))
 (1039 7 (:DEFINITION TAKE))
 (1010 10 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-145))
 (999 111 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (978 138 (:REWRITE D-E-LIST-FIX-WHEN-D-E-LIST-P))
 (966 483 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-1))
 (966 138 (:REWRITE LEN-OF-FIND-N-FREE-CLUSTERS))
 (920 92 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-1-LEMMA-25))
 (856 856 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (856 856 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (856 856 (:LINEAR LEN-WHEN-PREFIXP))
 (856 856 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (845 845 (:TYPE-PRESCRIPTION ZP))
 (828 138 (:DEFINITION MIN))
 (826 70 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (810 27 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
 (794 17 (:LINEAR M1-REGULAR-FILE-P-CORRECTNESS-2))
 (766 33 (:REWRITE GOOD-ROOT-D-E-P-OF-PSEUDO-ROOT-D-E))
 (720 11 (:REWRITE PREFIXP-OF-CONS-RIGHT))
 (713 23 (:REWRITE INTERSECTP-IS-COMMUTATIVE))
 (621 621 (:TYPE-PRESCRIPTION FAT-ENTRY-COUNT))
 (578 578 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (558 186 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (550 550 (:REWRITE SUBSETP-TRANS2))
 (550 550 (:REWRITE SUBSETP-TRANS))
 (541 541 (:REWRITE DEFAULT-*-1))
 (529 23 (:REWRITE FATI-OF-CLEAR-CC . 3))
 (528 176 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (513 27 (:REWRITE DEFAULT-UNARY-/))
 (471 54 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (451 451 (:REWRITE SUBSETP-MEMBER . 2))
 (451 451 (:REWRITE SUBSETP-MEMBER . 1))
 (438 70 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (428 428 (:LINEAR POSITION-WHEN-MEMBER))
 (428 428 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (414 138 (:REWRITE USEFUL-D-E-LIST-P-OF-CDR))
 (414 138 (:REWRITE NATS=>STRING-OF-STRING=>NATS))
 (390 297 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (368 184 (:REWRITE LOFAT-FILE-CONTENTS-P-WHEN-D-E-LISTP))
 (368 92 (:REWRITE D-E-CC-CORRECTNESS-1))
 (345 92 (:DEFINITION STOBJ-FIND-N-FREE-CLUSTERS-CORRECTNESS-1))
 (331 16 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (302 302 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (302 302 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (298 23 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (276 276 (:TYPE-PRESCRIPTION ATOM-OF-CDR-OF-LAST))
 (276 276 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-13))
 (276 276 (:REWRITE D-E-FILENAME-OF-D-E-SET-FIRST-CLUSTER-FILE-SIZE))
 (276 276 (:LINEAR D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-DISJOINT-LEMMA-12))
 (276 138 (:REWRITE STR-FIX-WHEN-STRINGP))
 (276 92 (:TYPE-PRESCRIPTION MAKE-CLUSTERS-OF-NIL))
 (264 264 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (264 88 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (262 132 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-4 . 1))
 (254 254 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (253 253 (:TYPE-PRESCRIPTION NATS=>STRING))
 (253 253 (:REWRITE PSEUDO-ROOT-D-E-CORRECTNESS-1))
 (230 115 (:REWRITE FAT-LENGTH-OF-CLEAR-CC))
 (230 23 (:REWRITE D-E-FIRST-CLUSTER-OF-D-E-INSTALL-DIRECTORY-BIT))
 (207 207 (:TYPE-PRESCRIPTION STOBJ-FIND-N-FREE-CLUSTERS))
 (207 207 (:TYPE-PRESCRIPTION FAT-LENGTH))
 (207 23 (:REWRITE D-E-FIRST-CLUSTER-OF-MAKE-D-E-WITH-FILENAME))
 (190 38 (:REWRITE LIST-EQUIV-OF-NIL-RIGHT))
 (184 184 (:TYPE-PRESCRIPTION LOFAT-PLACE-FILE-HELPER))
 (184 184 (:TYPE-PRESCRIPTION LOFAT-FILE-CONTENTS-P))
 (184 92 (:REWRITE LOFAT-REGULAR-FILE-P-CORRECTNESS-1))
 (184 23 (:REWRITE D-E-CC-CONTENTS-OF-CLEAR-CC))
 (161 161 (:REWRITE LOFAT-FS-P-OF-CLEAR-CC))
 (153 27 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-2))
 (151 130 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (146 146 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (144 4 (:DEFINITION CHARACTER-LISTP))
 (138 138 (:TYPE-PRESCRIPTION STRINGP-OF-D-E-CC-CONTENTS))
 (138 138 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (138 138 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (138 138 (:REWRITE EXPLODE-OF-NATS=>STRING))
 (138 138 (:REWRITE D-E-P-OF-SET-FIRST-CLUSTER-FILE-SIZE))
 (135 135 (:TYPE-PRESCRIPTION NONNEGATIVE-INTEGER-QUOTIENT))
 (135 54 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (135 54 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (130 26 (:REWRITE LOFAT-TO-HIFAT-CORRECTNESS-2))
 (128 14 (:REWRITE TAKE-WHEN-ATOM))
 (120 16 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LISTP))
 (119 119 (:TYPE-PRESCRIPTION PREFIXP))
 (119 119 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (119 119 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (119 119 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (119 119 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (115 115 (:TYPE-PRESCRIPTION NATP-OF-LOFAT-PLACE-FILE))
 (115 115 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (115 115 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (115 23 (:REWRITE FAT32-MASKED-ENTRY-P-OF-D-E-FIRST-CLUSTER))
 (112 112 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (108 27 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (96 16 (:REWRITE STR::CHARACTER-LISTP-WHEN-DEC-DIGIT-CHAR-LISTP))
 (92 92 (:TYPE-PRESCRIPTION NATP-OF-UPDATE-DIR-CONTENTS))
 (92 92 (:TYPE-PRESCRIPTION MAKE-CLUSTERS))
 (92 92 (:REWRITE NTH-WHEN-PREFIXP))
 (92 92 (:REWRITE INTEGER-LISTP-OF-D-E-CC))
 (80 10 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-40))
 (73 73 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (69 69 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (69 69 (:REWRITE FIND-N-FREE-CLUSTERS-WHEN-ZP))
 (69 69 (:REWRITE D-E-DIRECTORY-P-OF-PSEUDO-ROOT-D-E))
 (69 23 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-5))
 (69 23 (:REWRITE EFFECTIVE-FAT-OF-CLEAR-CC . 2))
 (64 8 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
 (60 16 (:LINEAR HIFAT-ENTRY-COUNT-WHEN-HIFAT-SUBSETP))
 (56 28 (:REWRITE DEFAULT-UNARY-MINUS))
 (54 27 (:REWRITE DEFAULT-NUMERATOR))
 (54 27 (:REWRITE DEFAULT-DENOMINATOR))
 (54 27 (:DEFINITION IFIX))
 (48 23 (:REWRITE LOFAT-PLACE-FILE-HELPER-CORRECTNESS-1))
 (48 12 (:REWRITE REPEAT-WHEN-ZP))
 (46 46 (:TYPE-PRESCRIPTION INTERSECTP-EQUAL))
 (46 46 (:TYPE-PRESCRIPTION FAT32-MASKED-ENTRY-P))
 (46 46 (:REWRITE SUBSETP-NIL))
 (46 46 (:REWRITE SET-EQUIV-OF-NIL))
 (46 46 (:REWRITE INTERSECTP-MEMBER . 1))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (46 46 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (46 46 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (46 23 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-7))
 (46 23 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (42 42 (:TYPE-PRESCRIPTION LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1 . 1))
 (40 16 (:REWRITE CONSP-OF-REPEAT))
 (38 38 (:TYPE-PRESCRIPTION STR::STRPREFIXP$INLINE))
 (38 38 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (38 38 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-4))
 (35 15 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (35 15 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (27 27 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (25 6 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (24 24 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-SUBSETP-EQUAL))
 (24 12 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-NOT-CONSP))
 (24 12 (:REWRITE STR::DEC-DIGIT-CHAR-LISTP-WHEN-NOT-CONSP))
 (24 6 (:LINEAR LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1))
 (23 23 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-6 . 2))
 (23 23 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-6 . 1))
 (23 23 (:REWRITE FATI-OF-CLEAR-CC . 2))
 (23 23 (:REWRITE EFFECTIVE-FAT-OF-CLEAR-CC . 3))
 (23 23 (:REWRITE COUNT-OF-CLUSTERS-OF-CLEAR-CC))
 (22 22 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (22 11 (:REWRITE GETOPT::DEFOPTIONS-LEMMA-8))
 (20 4 (:REWRITE CONSP-OF-TAKE))
 (18 18 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-17))
 (18 3 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (17 17 (:REWRITE M1-FILE-CONTENTS-P-OF-M1-FILE->CONTENTS))
 (16 16 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (16 16 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (16 6 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-4 . 2))
 (12 12 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-58))
 (12 4 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-OF-REPEAT))
 (12 4 (:REWRITE STR::DEC-DIGIT-CHAR-LISTP-OF-REPEAT))
 (11 11 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (8 4 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-OF-TAKE))
 (8 4 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-OF-CDR-WHEN-HEX-DIGIT-CHAR-LISTP))
 (8 4 (:REWRITE STR::DEC-DIGIT-CHAR-LISTP-OF-TAKE))
 (8 4 (:REWRITE STR::DEC-DIGIT-CHAR-LISTP-OF-CDR-WHEN-DEC-DIGIT-CHAR-LISTP))
 (8 1 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-43))
 (6 6 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (4 4 (:REWRITE CHARACTER-LISTP-OF-EXPLODE))
 (3 1 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-14))
 )
(TRUNCATE-LIST-CORRECTNESS-1-LEMMA-1
 (1563 20 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (1304 19 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (995 38 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (789 24 (:REWRITE SUBSETP-CAR-MEMBER))
 (645 12 (:DEFINITION MEMBER-EQUAL))
 (630 123 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (387 27 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (252 19 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (239 19 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (144 19 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (138 117 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (138 117 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (117 117 (:REWRITE SUBSETP-TRANS2))
 (117 117 (:REWRITE SUBSETP-TRANS))
 (63 35 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (60 60 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (51 5 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (48 48 (:TYPE-PRESCRIPTION NONEMPTY-STRING-LISTP))
 (48 48 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (48 48 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (38 38 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (38 38 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (38 38 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (32 32 (:REWRITE DEFAULT-CAR))
 (30 5 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (28 28 (:REWRITE DEFAULT-CDR))
 (24 24 (:REWRITE SUBSETP-MEMBER . 2))
 (24 24 (:REWRITE SUBSETP-MEMBER . 1))
 (24 24 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 )
(TRUNCATE-LIST-CORRECTNESS-1-LEMMA-2
 (4647 41 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-2))
 (2698 19 (:DEFINITION LOFAT-FIND-FILE))
 (2499 90 (:DEFINITION LEN))
 (1821 126 (:REWRITE STR::CONSP-OF-EXPLODE))
 (1713 6 (:LINEAR GETOPT::DEFOPTIONS-LEMMA-8))
 (1701 6 (:DEFINITION STR::STRPREFIXP$INLINE))
 (1639 19 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (1551 229 (:REWRITE DEFAULT-CDR))
 (1545 120 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (1292 76 (:DEFINITION FIND-D-E))
 (1170 9 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (975 75 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (942 12 (:LINEAR LOFAT-PLACE-FILE-HELPER-GUARD-LEMMA-1))
 (935 24 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (893 38 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (849 42 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (800 6 (:REWRITE PREFIXP-OF-CONS-LEFT))
 (684 76 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (684 9 (:DEFINITION CEILING))
 (600 600 (:TYPE-PRESCRIPTION ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (542 24 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (532 57 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (515 6 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (456 57 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (390 78 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (380 76 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (373 373 (:TYPE-PRESCRIPTION LEN))
 (340 5 (:LINEAR M1-REGULAR-FILE-P-CORRECTNESS-2))
 (324 36 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (309 173 (:REWRITE DEFAULT-+-2))
 (300 300 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (285 285 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (270 9 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
 (266 266 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (243 101 (:REWRITE DEFAULT-CAR))
 (228 76 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (225 75 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (225 75 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (225 9 (:REWRITE DEFAULT-UNARY-/))
 (212 63 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (211 51 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (210 173 (:REWRITE DEFAULT-+-1))
 (209 19 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (206 117 (:REWRITE DEFAULT-<-2))
 (190 38 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (189 63 (:REWRITE LOFAT-OPENDIR-CORRECTNESS-LEMMA-1))
 (156 117 (:REWRITE DEFAULT-<-1))
 (152 152 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (152 152 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (152 152 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (148 37 (:REWRITE COMMUTATIVITY-OF-+))
 (133 133 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (118 118 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (118 118 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (114 114 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (114 19 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (97 1 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-145))
 (83 12 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (81 27 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (81 27 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (81 18 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (81 18 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (76 76 (:TYPE-PRESCRIPTION D-E-P))
 (76 76 (:TYPE-PRESCRIPTION D-E-LIST-P))
 (75 75 (:TYPE-PRESCRIPTION M1-FILE-P))
 (75 75 (:TYPE-PRESCRIPTION HIFAT-SUBSETP))
 (75 75 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (75 75 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (75 75 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (75 75 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (71 7 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-2))
 (59 6 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (57 57 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (57 57 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (57 57 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (57 19 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (54 54 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (54 54 (:LINEAR LOWER-BOUND-OF-LEN-WHEN-SUBLISTP))
 (54 54 (:LINEAR LISTPOS-UPPER-BOUND-STRONG-2))
 (54 54 (:LINEAR LEN-WHEN-PREFIXP))
 (54 54 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (54 9 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (45 45 (:TYPE-PRESCRIPTION NONNEGATIVE-INTEGER-QUOTIENT))
 (42 21 (:REWRITE DEFAULT-*-2))
 (38 38 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (38 38 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (38 8 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (30 6 (:REWRITE LIST-EQUIV-OF-NIL-RIGHT))
 (29 29 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-FIX))
 (27 27 (:LINEAR POSITION-WHEN-MEMBER))
 (27 27 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (27 9 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (24 24 (:TYPE-PRESCRIPTION PREFIXP))
 (24 24 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (24 24 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (24 24 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (24 24 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (24 24 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (21 21 (:TYPE-PRESCRIPTION LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1 . 1))
 (21 21 (:REWRITE DEFAULT-*-1))
 (20 2 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-40))
 (19 19 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (19 19 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (18 9 (:REWRITE NFIX-WHEN-ZP))
 (18 9 (:REWRITE NFIX-WHEN-NATP))
 (18 9 (:REWRITE DEFAULT-UNARY-MINUS))
 (18 9 (:REWRITE DEFAULT-NUMERATOR))
 (18 9 (:REWRITE DEFAULT-DENOMINATOR))
 (18 9 (:DEFINITION IFIX))
 (18 6 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (18 4 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (15 3 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (15 3 (:REWRITE LOFAT-TO-HIFAT-CORRECTNESS-2))
 (12 4 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-5))
 (12 3 (:LINEAR LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (10 1 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-43))
 (9 9 (:TYPE-PRESCRIPTION FAT32$C-P))
 (9 9 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-17))
 (6 6 (:TYPE-PRESCRIPTION STR::STRPREFIXP$INLINE))
 (6 6 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (6 6 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (6 6 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (6 6 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (6 6 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-58))
 (6 6 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (5 5 (:REWRITE M1-FILE-CONTENTS-P-OF-M1-FILE->CONTENTS))
 (4 4 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (4 4 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 (4 4 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 )