(TRUNCATE-LIST-EXTRA-HYPOTHESIS
 (190118 38 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-2))
 (186861 23 (:DEFINITION LOFAT-PLACE-FILE))
 (48946 14 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (38209 1479 (:DEFINITION FIND-D-E))
 (34020 138 (:REWRITE LEN-OF-NATS=>CHARS))
 (33882 138 (:REWRITE LEN-OF-INSERT-D-E))
 (27679 253 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-8))
 (24336 138 (:REWRITE LEN-OF-PLACE-D-E))
 (23829 92 (:REWRITE LOFAT-REMOVE-FILE-CORRECTNESS-LEMMA-13))
 (20672 1092 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (19790 4550 (:REWRITE DEFAULT-CDR))
 (17664 184 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (16544 88 (:DEFINITION LOFAT-FIND-FILE))
 (15750 498 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (15420 92 (:DEFINITION INTEGER-LISTP))
 (14064 14 (:REWRITE TAKE-OF-LEN-FREE))
 (13478 184 (:REWRITE UPDATE-FATI-OF-UPDATE-FATI-COINCIDENT))
 (12844 138 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (12697 1092 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (11569 782 (:REWRITE D-E-CC-UNDER-IFF . 2))
 (11495 27 (:LINEAR GETOPT::DEFOPTIONS-LEMMA-8))
 (11441 27 (:DEFINITION STR::STRPREFIXP$INLINE))
 (11236 476 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (10751 138 (:REWRITE INTEGERP-OF-CAR-OF-LAST-WHEN-INTEGER-LISTP))
 (10465 138 (:REWRITE LAST-WHEN-EQUAL-LEN-1))
 (10428 578 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (10028 414 (:REWRITE CONSP-OF-LAST))
 (9545 9545 (:TYPE-PRESCRIPTION COUNT-FREE-CLUSTERS))
 (9430 184 (:REWRITE UPDATE-FATI-OF-FATI-WHEN-FAT32$C-P))
 (9302 138 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (8956 8956 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (8828 2899 (:REWRITE DEFAULT-CAR))
 (8195 1617 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (7991 4395 (:REWRITE DEFAULT-<-2))
 (7612 302 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (7567 69 (:DEFINITION LAST))
 (7379 1451 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (7185 590 (:REWRITE STR::CONSP-OF-EXPLODE))
 (6926 119 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (6923 6923 (:TYPE-PRESCRIPTION D-E-FILE-SIZE))
 (6759 6759 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (6759 6759 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (6759 6759 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (6759 6759 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (6759 6759 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (6759 6759 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (6759 6759 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (6759 6759 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (6615 237 (:DEFINITION MEMBER-EQUAL))
 (6171 54 (:LINEAR LOFAT-PLACE-FILE-HELPER-GUARD-LEMMA-1))
 (5796 69 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-29))
 (5770 2557 (:REWRITE DEFAULT-+-2))
 (5697 4395 (:REWRITE DEFAULT-<-1))
 (5645 23 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (5587 119 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (5544 138 (:DEFINITION PLACE-D-E))
 (5542 88 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (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))
 (5188 777 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (5129 920 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-COINCIDENT-LEMMA-8))
 (4830 230 (:DEFINITION BINARY-APPEND))
 (4675 27 (:REWRITE PREFIXP-OF-CONS-LEFT))
 (4669 1311 (:REWRITE LOFAT-FILE-P-WHEN-LOFAT-DIRECTORY-FILE-P-OR-LOFAT-REGULAR-FILE-P))
 (4649 281 (:REWRITE SUBSETP-CAR-MEMBER))
 (4476 4476 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (4465 243 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-2))
 (4428 184 (:REWRITE PLACE-CONTENTS-EXPANSION-1))
 (4324 23 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-33))
 (3835 8 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
 (3818 782 (:LINEAR D-E-FILE-SIZE-CORRECTNESS-1))
 (3818 184 (:REWRITE D-E-CC-UNDER-IFF . 3))
 (3726 3726 (:TYPE-PRESCRIPTION FIND-N-FREE-CLUSTERS))
 (3695 27 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (3680 3680 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (3680 207 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (3672 27 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (3588 184 (:REWRITE LOFAT-FILE->CONTENTS-OF-LOFAT-FILE))
 (3519 92 (:DEFINITION NTH))
 (3473 2116 (:TYPE-PRESCRIPTION LAST))
 (3471 4 (:REWRITE CHARACTER-LISTP-OF-TAKE))
 (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))
 (3174 3174 (:TYPE-PRESCRIPTION LOFAT-FILE))
 (2967 46 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (2783 138 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (2759 2557 (:REWRITE DEFAULT-+-1))
 (2722 550 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2722 550 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2668 184 (:REWRITE LOFAT-FILE-CONTENTS-P-WHEN-STRINGP))
 (2576 115 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (2242 2242 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (2168 154 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (2144 2144 (:TYPE-PRESCRIPTION NATP-OF-PLACE-CONTENTS))
 (2091 29 (:REWRITE STRING-LISTP-WHEN-FAT32-FILENAME-LIST-P))
 (1920 640 (:REWRITE PLACE-CONTENTS-EXPANSION-2))
 (1910 541 (:REWRITE DEFAULT-*-2))
 (1890 27 (:DEFINITION CEILING))
 (1863 207 (:DEFINITION NFIX))
 (1794 138 (:REWRITE DISTRIBUTIVITY))
 (1794 92 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1700 132 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (1660 115 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-8))
 (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))
 (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))
 (1491 1491 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (1424 320 (:REWRITE NATP-OF-PLACE-CONTENTS))
 (1356 76 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1349 7 (:DEFINITION TAKE))
 (1312 270 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (1311 1311 (:REWRITE LOFAT-FILE-P-OF-LOFAT-FILE))
 (1284 428 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (1284 428 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (1270 10 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-145))
 (1253 1253 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (1248 416 (:REWRITE LOFAT-OPENDIR-CORRECTNESS-LEMMA-1))
 (1248 11 (:REWRITE PREFIXP-OF-CONS-RIGHT))
 (1158 1158 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1147 1147 (:TYPE-PRESCRIPTION GOOD-ROOT-D-E-P))
 (1108 17 (:LINEAR M1-REGULAR-FILE-P-CORRECTNESS-2))
 (1058 207 (:LINEAR PSEUDO-ROOT-D-E-CORRECTNESS-1))
 (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))
 (903 54 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (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))
 (798 38 (:REWRITE LIST-EQUIV-OF-NIL-RIGHT))
 (766 33 (:REWRITE GOOD-ROOT-D-E-P-OF-PSEUDO-ROOT-D-E))
 (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-/))
 (459 16 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (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))
 (398 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))
 (343 130 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (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))
 (276 23 (:REWRITE LOFAT-PLACE-FILE-HELPER-CORRECTNESS-1))
 (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))
 (249 27 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-2))
 (240 14 (:REWRITE TAKE-WHEN-ATOM))
 (240 4 (:DEFINITION CHARACTER-LISTP))
 (230 115 (:REWRITE FAT-LENGTH-OF-CLEAR-CC))
 (230 23 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-7))
 (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))
 (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))
 (162 18 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-17))
 (161 161 (:REWRITE LOFAT-FS-P-OF-CLEAR-CC))
 (146 146 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (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 8 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
 (125 15 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (120 16 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LIST*P))
 (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))
 (99 11 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (96 16 (:REWRITE STR::CHARACTER-LISTP-WHEN-DEC-DIGIT-CHAR-LIST*P))
 (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))
 (72 6 (:LINEAR LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1))
 (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))
 (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 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 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-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-LIST*P-WHEN-SUBSETP-EQUAL))
 (24 12 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-NOT-CONSP))
 (24 12 (:REWRITE STR::DEC-DIGIT-CHAR-LIST*P-WHEN-NOT-CONSP))
 (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 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-LIST*P-OF-REPEAT))
 (12 4 (:REWRITE STR::DEC-DIGIT-CHAR-LIST*P-OF-REPEAT))
 (8 4 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-OF-TAKE))
 (8 4 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-OF-CDR-WHEN-HEX-DIGIT-CHAR-LIST*P))
 (8 4 (:REWRITE STR::DEC-DIGIT-CHAR-LIST*P-OF-TAKE))
 (8 4 (:REWRITE STR::DEC-DIGIT-CHAR-LIST*P-OF-CDR-WHEN-DEC-DIGIT-CHAR-LIST*P))
 (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
 (2115 20 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (1856 19 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (1547 38 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (1221 24 (:REWRITE SUBSETP-CAR-MEMBER))
 (957 12 (:DEFINITION MEMBER-EQUAL))
 (870 123 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (441 27 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (378 117 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (378 117 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (252 19 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (239 19 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (145 35 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (144 19 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (117 117 (:REWRITE SUBSETP-TRANS2))
 (117 117 (:REWRITE SUBSETP-TRANS))
 (86 86 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (86 86 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (86 86 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (86 86 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (86 86 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (86 86 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (86 86 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (86 86 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (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
 (6559 41 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-2))
 (4027 90 (:DEFINITION LEN))
 (3762 19 (:DEFINITION LOFAT-FIND-FILE))
 (2585 6 (:LINEAR GETOPT::DEFOPTIONS-LEMMA-8))
 (2573 6 (:DEFINITION STR::STRPREFIXP$INLINE))
 (2447 229 (:REWRITE DEFAULT-CDR))
 (2181 126 (:REWRITE STR::CONSP-OF-EXPLODE))
 (2145 120 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (1927 19 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (1900 76 (:DEFINITION FIND-D-E))
 (1575 75 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (1447 24 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (1390 12 (:LINEAR LOFAT-PLACE-FILE-HELPER-GUARD-LEMMA-1))
 (1314 9 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (1264 6 (:REWRITE PREFIXP-OF-CONS-LEFT))
 (1197 38 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (1089 42 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (870 24 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (707 6 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (684 76 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (684 57 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (684 9 (:DEFINITION CEILING))
 (675 75 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (608 57 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (600 600 (:TYPE-PRESCRIPTION ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (500 5 (:LINEAR M1-REGULAR-FILE-P-CORRECTNESS-2))
 (433 433 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 2))
 (433 433 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-TRUELIST-ALISTP . 1))
 (433 433 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 2))
 (433 433 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-SYMBOL-SYMBOL-ALISTP . 1))
 (433 433 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 2))
 (433 433 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-TRUELIST-ALISTP . 1))
 (433 433 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 2))
 (433 433 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-KEYWORD-SYMBOL-ALISTP . 1))
 (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))
 (331 101 (:REWRITE DEFAULT-CAR))
 (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))
 (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))
 (179 12 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (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))
 (126 6 (:REWRITE LIST-EQUIV-OF-NIL-RIGHT))
 (119 7 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-2))
 (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))
 (113 1 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-145))
 (107 6 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (102 8 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (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))
 (81 9 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-17))
 (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))
 (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))
 (50 4 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (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))
 (36 4 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (36 4 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (36 4 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (36 3 (:LINEAR LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1))
 (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))
 (15 3 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (15 3 (:REWRITE LOFAT-TO-HIFAT-CORRECTNESS-2))
 (12 4 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-5))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (10 1 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-43))
 (9 9 (:TYPE-PRESCRIPTION FAT32$C-P))
 (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-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )