(LOFAT-PWRITE
 (7299 2457 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (991 7 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (910 7 (:DEFINITION LOFAT-FIND-FILE))
 (734 44 (:DEFINITION LEN))
 (720 6 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (420 28 (:DEFINITION FIND-D-E))
 (420 6 (:DEFINITION CEILING))
 (301 14 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (300 147 (:REWRITE DEFAULT-CDR))
 (252 28 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (217 118 (:REWRITE DEFAULT-+-2))
 (216 24 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (199 118 (:REWRITE DEFAULT-<-1))
 (186 28 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (182 21 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (180 6 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
 (170 118 (:REWRITE DEFAULT-<-2))
 (165 21 (:REWRITE ZP-OPEN))
 (154 21 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (151 29 (:DEFINITION ASSOC-EQUAL))
 (144 60 (:REWRITE STR::CONSP-OF-EXPLODE))
 (140 28 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (137 118 (:REWRITE DEFAULT-+-1))
 (123 123 (:REWRITE DEFAULT-CAR))
 (114 6 (:REWRITE DEFAULT-UNARY-/))
 (106 34 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (105 105 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (84 28 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (76 19 (:REWRITE COMMUTATIVITY-OF-+))
 (67 31 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (56 56 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (56 56 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (50 50 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (49 49 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (49 7 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (45 15 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (43 43 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (42 14 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (36 36 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (30 30 (:TYPE-PRESCRIPTION NONNEGATIVE-INTEGER-QUOTIENT))
 (30 12 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (30 12 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (28 28 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (24 9 (:REWRITE NFIX-WHEN-ZP))
 (24 6 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (21 21 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (21 21 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (21 7 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (21 7 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (21 7 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (21 7 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (20 4 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (16 8 (:REWRITE DEFAULT-*-2))
 (14 14 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (12 12 (:LINEAR D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-DISJOINT-LEMMA-12))
 (12 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (12 6 (:REWRITE DEFAULT-NUMERATOR))
 (12 6 (:REWRITE DEFAULT-DENOMINATOR))
 (12 6 (:DEFINITION IFIX))
 (10 10 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (10 10 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (9 3 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-5))
 (8 8 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (8 8 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (8 8 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (8 8 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (8 8 (:REWRITE DEFAULT-*-1))
 (8 2 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (7 7 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (7 7 (:LINEAR POSITION-WHEN-MEMBER))
 (7 7 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (7 1 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LIST*P))
 (7 1 (:DEFINITION ALISTP))
 (6 6 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (6 3 (:REWRITE LOFAT-FILE-CONTENTS-P-WHEN-D-E-LISTP))
 (6 2 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-2))
 (4 4 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (4 4 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (4 4 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (4 4 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-SUBSETP-EQUAL))
 (2 1 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-NOT-CONSP))
 )
(INTEGERP-OF-LOFAT-PWRITE
 (34706 6 (:DEFINITION LOFAT-PLACE-FILE))
 (7506 126 (:REWRITE LENGTH-WHEN-STRINGP))
 (7082 547 (:DEFINITION LEN))
 (6032 48 (:REWRITE LOFAT-FILE->CONTENTS-OF-LOFAT-FILE))
 (5984 48 (:REWRITE LOFAT-FILE-CONTENTS-FIX-WHEN-LOFAT-FILE-CONTENTS-P))
 (5792 48 (:REWRITE LOFAT-FILE-CONTENTS-P-WHEN-STRINGP))
 (5298 48 (:REWRITE PLACE-CONTENTS-EXPANSION-1))
 (5262 294 (:DEFINITION FIND-D-E))
 (4560 24 (:REWRITE LEN-OF-NATS=>CHARS))
 (4536 24 (:REWRITE LEN-OF-INSERT-D-E))
 (4266 192 (:REWRITE PLACE-CONTENTS-EXPANSION-2))
 (3677 357 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-2))
 (3498 66 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-8))
 (3248 48 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 1))
 (3126 219 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (3072 24 (:REWRITE LEN-OF-PLACE-D-E))
 (2934 342 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (2355 96 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (2010 219 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (1985 949 (:REWRITE DEFAULT-+-2))
 (1953 15 (:DEFINITION LOFAT-FIND-FILE))
 (1837 1360 (:REWRITE DEFAULT-CDR))
 (1827 1827 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (1738 194 (:REWRITE ZP-OPEN))
 (1729 282 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (1590 318 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (1560 60 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (1548 48 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (1392 24 (:DEFINITION INTEGER-LISTP))
 (1285 198 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-2))
 (1218 342 (:REWRITE LOFAT-FILE-P-WHEN-LOFAT-DIRECTORY-FILE-P-OR-LOFAT-REGULAR-FILE-P))
 (1143 680 (:REWRITE DEFAULT-<-2))
 (1122 306 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (1074 342 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (1068 1068 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (1062 36 (:REWRITE INTEGERP-OF-CAR-OF-LAST-WHEN-INTEGER-LISTP))
 (1060 1060 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (1056 528 (:TYPE-PRESCRIPTION LOFAT-FILE-CONTENTS-FIX))
 (1056 96 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (1032 36 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (1023 771 (:REWRITE DEFAULT-CAR))
 (1018 949 (:REWRITE DEFAULT-+-1))
 (977 15 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (972 18 (:REWRITE LAST-WHEN-EQUAL-LEN-1))
 (828 828 (:TYPE-PRESCRIPTION LOFAT-FILE))
 (822 822 (:TYPE-PRESCRIPTION STRINGP-OF-IMPLODE))
 (804 204 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (801 680 (:REWRITE DEFAULT-<-1))
 (795 265 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (795 265 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (792 24 (:REWRITE INTEGERP-OF-NTH-WHEN-INTEGER-LISTP))
 (786 558 (:TYPE-PRESCRIPTION LAST))
 (786 204 (:REWRITE STR::CONSP-OF-EXPLODE))
 (768 192 (:TYPE-PRESCRIPTION MAKE-CLUSTERS-OF-NIL))
 (768 24 (:DEFINITION PLACE-D-E))
 (744 248 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (728 107 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (708 708 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (684 684 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (672 672 (:TYPE-PRESCRIPTION NATP-OF-PLACE-CONTENTS))
 (642 6 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (638 638 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 (600 114 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-COINCIDENT-LEMMA-8))
 (537 537 (:TYPE-PRESCRIPTION LOFAT-DIRECTORY-FILE-P))
 (530 530 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (528 24 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (524 524 (:TYPE-PRESCRIPTION LOFAT-FILE-P))
 (492 96 (:DEFINITION ASSOC-EQUAL))
 (480 480 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-D-E-CC))
 (465 465 (:TYPE-PRESCRIPTION CLUSTER-SIZE))
 (462 462 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (456 78 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (444 444 (:TYPE-PRESCRIPTION INTEGERP-OF-D-E-CC-CONTENTS))
 (435 435 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (426 90 (:REWRITE CONSP-OF-LAST))
 (420 48 (:REWRITE UPDATE-FATI-OF-UPDATE-FATI-COINCIDENT))
 (408 408 (:TYPE-PRESCRIPTION STOBJ-FIND-N-FREE-CLUSTERS))
 (390 390 (:TYPE-PRESCRIPTION D-E-P))
 (390 13 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (388 388 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (386 386 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (342 342 (:REWRITE LOFAT-FILE-P-OF-LOFAT-FILE))
 (336 96 (:REWRITE DEFAULT-*-2))
 (320 240 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (312 24 (:REWRITE DISTRIBUTIVITY))
 (300 300 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (300 300 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (288 96 (:REWRITE NATP-OF-PLACE-CONTENTS))
 (282 282 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (276 72 (:DEFINITION STOBJ-FIND-N-FREE-CLUSTERS-CORRECTNESS-1))
 (267 79 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (265 265 (:LINEAR POSITION-WHEN-MEMBER))
 (265 265 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (264 48 (:REWRITE UPDATE-FATI-OF-FATI-WHEN-FAT32$C-P))
 (261 261 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (252 252 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (252 126 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-1))
 (252 63 (:REWRITE COMMUTATIVITY-OF-+))
 (240 60 (:DEFINITION BINARY-APPEND))
 (240 48 (:REWRITE NFIX-WHEN-NATP))
 (240 48 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 2))
 (240 24 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-1-LEMMA-25))
 (234 78 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-5))
 (234 26 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (192 192 (:TYPE-PRESCRIPTION MAKE-CLUSTERS))
 (192 48 (:REWRITE NFIX-WHEN-ZP))
 (174 114 (:REWRITE D-E-CC-UNDER-IFF . 2))
 (168 168 (:TYPE-PRESCRIPTION GOOD-ROOT-D-E-P))
 (168 24 (:REWRITE D-E-LIST-FIX-WHEN-D-E-LIST-P))
 (162 36 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (162 18 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-29))
 (160 48 (:REWRITE STR::EXPLODE-OF-IMPLODE))
 (158 158 (:TYPE-PRESCRIPTION FAT32$C-P))
 (156 30 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (150 21 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (144 48 (:DEFINITION NFIX))
 (123 123 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (120 120 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (120 96 (:REWRITE CLUSTER-SIZE-OF-UPDATE-FATI))
 (120 24 (:REWRITE NTH-WHEN-D-E-P . 2))
 (117 11 (:REWRITE LOFAT-FILE-FIX-WHEN-LOFAT-FILE-P))
 (108 36 (:REWRITE LOFAT-FS-P-OF-CLEAR-CC))
 (96 96 (:REWRITE DEFAULT-*-1))
 (96 48 (:REWRITE LOFAT-FILE-CONTENTS-P-WHEN-D-E-LISTP))
 (96 24 (:REWRITE D-E-CC-CORRECTNESS-1))
 (90 24 (:REWRITE LOFAT-REMOVE-FILE-CORRECTNESS-LEMMA-13))
 (90 24 (:REWRITE LOFAT-FS-P-OF-UPDATE-FATI))
 (86 30 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (84 27 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (82 82 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (78 13 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (72 72 (:TYPE-PRESCRIPTION ATOM-OF-CDR-OF-LAST))
 (72 24 (:REWRITE USEFUL-D-E-LIST-P-OF-CDR))
 (72 24 (:REWRITE NATS=>STRING-OF-STRING=>NATS))
 (63 63 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT->FID$INLINE))
 (48 48 (:TYPE-PRESCRIPTION NATP-OF-UPDATE-DIR-CONTENTS))
 (48 48 (:TYPE-PRESCRIPTION LOFAT-PLACE-FILE-HELPER))
 (48 48 (:TYPE-PRESCRIPTION LOFAT-FILE-CONTENTS-P))
 (48 48 (:REWRITE STR::MAKE-CHARACTER-LIST-IS-IDENTITY-UNDER-CHARLISTEQV))
 (48 48 (:REWRITE D-E-FILENAME-OF-D-E-SET-FIRST-CLUSTER-FILE-SIZE))
 (48 24 (:REWRITE STR-FIX-WHEN-STRINGP))
 (48 24 (:REWRITE LOFAT-REGULAR-FILE-P-CORRECTNESS-1))
 (48 6 (:REWRITE D-E-FIRST-CLUSTER-OF-D-E-INSTALL-DIRECTORY-BIT))
 (45 45 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (45 15 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (45 5 (:REWRITE LOFAT-FS-P-OF-LOFAT-PLACE-FILE-LEMMA-8))
 (42 6 (:REWRITE D-E-FIRST-CLUSTER-OF-MAKE-D-E-WITH-FILENAME))
 (39 39 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (39 13 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (39 13 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (38 38 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-3))
 (36 36 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (36 36 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (36 12 (:REWRITE D-E-CC-UNDER-IFF . 3))
 (36 6 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-2))
 (35 21 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (33 33 (:REWRITE FAT32-FILENAME-LIST-P-OF-FILE-TABLE-ELEMENT->FID))
 (30 30 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (30 30 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (24 24 (:TYPE-PRESCRIPTION STRINGP-OF-D-E-CC-CONTENTS))
 (24 24 (:TYPE-PRESCRIPTION NFIX))
 (24 24 (:TYPE-PRESCRIPTION NATS=>STRING))
 (24 24 (:REWRITE NAT-LISTP-OF-STOBJ-FIND-N-FREE-CLUSTERS . 1))
 (24 24 (:REWRITE INTEGER-LISTP-OF-D-E-CC))
 (24 24 (:REWRITE EXPLODE-OF-NATS=>STRING))
 (24 24 (:REWRITE D-E-P-OF-SET-FIRST-CLUSTER-FILE-SIZE))
 (24 24 (:REWRITE CLUSTER-SIZE-OF-CLEAR-CC))
 (24 6 (:REWRITE LOFAT-PLACE-FILE-HELPER-CORRECTNESS-1))
 (24 6 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-7))
 (21 7 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-5))
 (18 18 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (18 18 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (18 6 (:REWRITE GOOD-ROOT-D-E-P-OF-PSEUDO-ROOT-D-E))
 (18 6 (:REWRITE FATI-OF-CLEAR-CC . 3))
 (15 5 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-2))
 (12 6 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 6 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (6 6 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-6 . 2))
 (6 6 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-6 . 1))
 (6 6 (:REWRITE FATI-OF-CLEAR-CC . 2))
 )
(LOFAT-FS-P-OF-LOFAT-PWRITE
 (132859 9 (:DEFINITION LOFAT-PLACE-FILE))
 (47691 72 (:REWRITE PLACE-CONTENTS-EXPANSION-1))
 (46143 288 (:REWRITE PLACE-CONTENTS-EXPANSION-2))
 (39852 720 (:LINEAR FIND-N-FREE-CLUSTERS-CORRECTNESS-7))
 (39591 1119 (:REWRITE ZP-OPEN))
 (34065 108 (:DEFINITION STOBJ-FIND-N-FREE-CLUSTERS-CORRECTNESS-1))
 (33710 619 (:REWRITE NFIX-WHEN-ZP))
 (28494 72 (:REWRITE UPDATE-FATI-OF-UPDATE-FATI-COINCIDENT))
 (22914 54 (:REWRITE EFFECTIVE-FAT-OF-UPDATE-FATI))
 (21780 54 (:REWRITE UPDATE-FATI-OF-FATI-WHEN-FAT32$C-P))
 (21056 619 (:REWRITE NFIX-WHEN-NATP))
 (20853 441 (:DEFINITION NATP))
 (20232 360 (:REWRITE LEN-OF-EFFECTIVE-FAT))
 (17361 2106 (:REWRITE LEN-OF-FIND-N-FREE-CLUSTERS))
 (14651 2246 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (13932 990 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (13338 2106 (:DEFINITION MIN))
 (12178 186 (:REWRITE LENGTH-WHEN-STRINGP))
 (12028 695 (:DEFINITION LEN))
 (10002 27 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-29))
 (9972 9972 (:TYPE-PRESCRIPTION COUNT-FREE-CLUSTERS))
 (9832 72 (:REWRITE LOFAT-FILE->CONTENTS-OF-LOFAT-FILE))
 (9760 72 (:REWRITE LOFAT-FILE-CONTENTS-FIX-WHEN-LOFAT-FILE-CONTENTS-P))
 (9472 72 (:REWRITE LOFAT-FILE-CONTENTS-P-WHEN-STRINGP))
 (9189 63 (:REWRITE LOFAT-FS-P-OF-UPDATE-FATI))
 (8877 4695 (:REWRITE DEFAULT-+-2))
 (8449 5902 (:REWRITE DEFAULT-<-1))
 (8283 5902 (:REWRITE DEFAULT-<-2))
 (7917 427 (:DEFINITION FIND-D-E))
 (7377 108 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-8))
 (6984 36 (:REWRITE LEN-OF-NATS=>CHARS))
 (6948 36 (:REWRITE LEN-OF-INSERT-D-E))
 (6156 4695 (:REWRITE DEFAULT-+-1))
 (5996 1984 (:REWRITE DEFAULT-CDR))
 (5880 1464 (:REWRITE COMMUTATIVITY-OF-+))
 (5463 525 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-2))
 (4872 72 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 1))
 (4869 333 (:REWRITE INTEGERP-OF-NTH-WHEN-INTEGER-LISTP))
 (4726 318 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (4704 36 (:REWRITE LEN-OF-PLACE-D-E))
 (4608 72 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (4533 499 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (4446 234 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
 (3969 297 (:REWRITE D-E-CC-UNDER-IFF . 2))
 (3600 720 (:LINEAR NTH-WHEN-D-E-P))
 (3588 36 (:DEFINITION INTEGER-LISTP))
 (3448 137 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (3374 3374 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (3123 36 (:REWRITE LOFAT-REMOVE-FILE-CORRECTNESS-LEMMA-13))
 (2992 192 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (2979 1521 (:REWRITE FIND-N-FREE-CLUSTERS-WHEN-ZP))
 (2978 318 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (2769 63 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (2688 2688 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (2658 448 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (2643 19 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (2628 162 (:REWRITE CONSP-OF-LAST))
 (2619 2619 (:TYPE-PRESCRIPTION D-E-FILE-SIZE))
 (2573 463 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (2483 19 (:DEFINITION LOFAT-FIND-FILE))
 (2396 1172 (:REWRITE DEFAULT-CAR))
 (2304 2304 (:TYPE-PRESCRIPTION FAT-ENTRY-COUNT))
 (2265 54 (:REWRITE INTEGERP-OF-CAR-OF-LAST-WHEN-INTEGER-LISTP))
 (2160 54 (:DEFINITION UPDATE-NTH))
 (2061 27 (:REWRITE LAST-WHEN-EQUAL-LEN-1))
 (1942 322 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-2))
 (1920 16 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (1842 54 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (1827 513 (:REWRITE LOFAT-FILE-P-WHEN-LOFAT-DIRECTORY-FILE-P-OR-LOFAT-REGULAR-FILE-P))
 (1773 1773 (:TYPE-PRESCRIPTION NFIX))
 (1773 297 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-COINCIDENT-LEMMA-8))
 (1584 792 (:TYPE-PRESCRIPTION LOFAT-FILE-CONTENTS-FIX))
 (1584 9 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-33))
 (1574 1574 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (1569 499 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (1521 345 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (1521 306 (:LINEAR D-E-FILE-SIZE-CORRECTNESS-1))
 (1504 1504 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (1399 314 (:REWRITE STR::CONSP-OF-EXPLODE))
 (1398 466 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1359 828 (:TYPE-PRESCRIPTION LAST))
 (1356 1356 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (1341 1341 (:TYPE-PRESCRIPTION INTEGERP-OF-D-E-CC-CONTENTS))
 (1242 1242 (:TYPE-PRESCRIPTION LOFAT-FILE))
 (1233 1233 (:TYPE-PRESCRIPTION STRINGP-OF-IMPLODE))
 (1206 1206 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-D-E-CC))
 (1200 36 (:DEFINITION PLACE-D-E))
 (1152 288 (:TYPE-PRESCRIPTION MAKE-CLUSTERS-OF-NIL))
 (1152 198 (:DEFINITION NFIX))
 (1128 376 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (1128 376 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (1125 333 (:REWRITE NTH-WHEN-D-E-P . 2))
 (1120 16 (:DEFINITION CEILING))
 (1116 1116 (:TYPE-PRESCRIPTION FIND-N-FREE-CLUSTERS))
 (1053 18 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (1044 82 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (1008 1008 (:TYPE-PRESCRIPTION NATP-OF-PLACE-CONTENTS))
 (990 45 (:REWRITE EFFECTIVE-FAT-OF-CLEAR-CC . 2))
 (987 9 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (900 90 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (891 18 (:REWRITE FATI-OF-CLEAR-CC . 3))
 (829 829 (:TYPE-PRESCRIPTION LOFAT-FILE-P))
 (820 820 (:TYPE-PRESCRIPTION LOFAT-DIRECTORY-FILE-P))
 (752 752 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (747 27 (:REWRITE D-E-CC-UNDER-IFF . 3))
 (726 726 (:LINEAR D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-DISJOINT-LEMMA-12))
 (723 723 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (720 225 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-5))
 (709 265 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (703 137 (:DEFINITION ASSOC-EQUAL))
 (662 662 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (657 657 (:TYPE-PRESCRIPTION NATP))
 (630 36 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (625 625 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (624 624 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (594 594 (:LINEAR LOFAT-TO-HIFAT-HELPER-AFTER-DELETE-AND-CLEAR-1-LEMMA-1))
 (594 594 (:LINEAR LOFAT-FIND-FILE-CORRECTNESS-1-LEMMA-8))
 (591 591 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (548 166 (:REWRITE DEFAULT-*-2))
 (544 408 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (513 513 (:REWRITE LOFAT-FILE-P-OF-LOFAT-FILE))
 (513 54 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (513 36 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (504 45 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (486 486 (:TYPE-PRESCRIPTION EFFECTIVE-FAT))
 (480 16 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
 (468 36 (:REWRITE DISTRIBUTIVITY))
 (459 459 (:TYPE-PRESCRIPTION GOOD-ROOT-D-E-P))
 (450 90 (:DEFINITION BINARY-APPEND))
 (442 442 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (432 144 (:REWRITE NATP-OF-PLACE-CONTENTS))
 (432 108 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (417 246 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (378 189 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-1))
 (376 376 (:LINEAR POSITION-WHEN-MEMBER))
 (376 376 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (360 360 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-47))
 (360 360 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-1-LEMMA-44))
 (360 72 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 2))
 (360 36 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-1-LEMMA-25))
 (333 36 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (324 324 (:REWRITE FIND-N-FREE-CLUSTERS-CORRECTNESS-8))
 (324 36 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-13))
 (324 36 (:REWRITE LOFAT-FS-P-OF-LOFAT-PLACE-FILE-LEMMA-8))
 (315 180 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (304 214 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (304 16 (:REWRITE DEFAULT-UNARY-/))
 (288 288 (:TYPE-PRESCRIPTION MAKE-CLUSTERS))
 (279 9 (:REWRITE INTERSECTP-IS-COMMUTATIVE))
 (276 36 (:REWRITE D-E-LIST-FIX-WHEN-D-E-LIST-P))
 (261 45 (:REWRITE LOFAT-FILE-FIX-WHEN-LOFAT-FILE-P))
 (252 252 (:TYPE-PRESCRIPTION LOFAT-TO-HIFAT-CORRECTNESS-1 . 2))
 (240 72 (:REWRITE STR::EXPLODE-OF-IMPLODE))
 (234 234 (:REWRITE FIND-N-FREE-CLUSTERS-CORRECTNESS-2 . 1))
 (216 36 (:REWRITE GOOD-ROOT-D-E-P-OF-PSEUDO-ROOT-D-E))
 (215 28 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (189 9 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-2))
 (180 144 (:REWRITE CLUSTER-SIZE-OF-UPDATE-FATI))
 (171 171 (:REWRITE NTH-WHEN-D-E-P . 3))
 (171 171 (:REWRITE COUNT-OF-CLUSTERS-OF-CLEAR-CC))
 (166 166 (:REWRITE DEFAULT-*-1))
 (162 162 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (162 162 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (153 153 (:TYPE-PRESCRIPTION STOBJ-FIND-N-FREE-CLUSTERS))
 (146 146 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (144 72 (:REWRITE LOFAT-FILE-CONTENTS-P-WHEN-D-E-LISTP))
 (144 36 (:REWRITE D-E-CC-CORRECTNESS-1))
 (136 37 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (132 132 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (117 117 (:TYPE-PRESCRIPTION FAT-LENGTH))
 (115 115 (:TYPE-PRESCRIPTION FAT32$C-P))
 (114 114 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT->FID$INLINE))
 (114 38 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (108 108 (:TYPE-PRESCRIPTION ATOM-OF-CDR-OF-LAST))
 (108 54 (:REWRITE FAT32-UPDATE-LOWER-28-CORRECTNESS-1 . 1))
 (108 36 (:REWRITE USEFUL-D-E-LIST-P-OF-CDR))
 (108 36 (:REWRITE NATS=>STRING-OF-STRING=>NATS))
 (100 100 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-3))
 (96 3 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (90 90 (:TYPE-PRESCRIPTION FAT32-MASKED-ENTRY-P))
 (90 45 (:REWRITE FAT-LENGTH-OF-CLEAR-CC))
 (90 18 (:REWRITE FAT32-MASKED-ENTRY-P-OF-D-E-FIRST-CLUSTER))
 (90 3 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (81 81 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (80 80 (:TYPE-PRESCRIPTION NONNEGATIVE-INTEGER-QUOTIENT))
 (80 32 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (78 78 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (78 9 (:REWRITE D-E-FIRST-CLUSTER-OF-D-E-INSTALL-DIRECTORY-BIT))
 (72 72 (:TYPE-PRESCRIPTION NATP-OF-UPDATE-DIR-CONTENTS))
 (72 72 (:TYPE-PRESCRIPTION LOFAT-PLACE-FILE-HELPER))
 (72 72 (:TYPE-PRESCRIPTION LOFAT-FILE-CONTENTS-P))
 (72 72 (:REWRITE STR::MAKE-CHARACTER-LIST-IS-IDENTITY-UNDER-CHARLISTEQV))
 (72 72 (:REWRITE D-E-FILENAME-OF-D-E-SET-FIRST-CLUSTER-FILE-SIZE))
 (72 36 (:REWRITE STR-FIX-WHEN-STRINGP))
 (72 36 (:REWRITE LOFAT-REGULAR-FILE-P-CORRECTNESS-1))
 (72 36 (:LINEAR LOFAT-TO-HIFAT-CORRECTNESS-1))
 (72 9 (:REWRITE D-E-CC-CONTENTS-OF-CLEAR-CC))
 (69 9 (:REWRITE D-E-FIRST-CLUSTER-OF-MAKE-D-E-WITH-FILENAME))
 (64 16 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (63 63 (:TYPE-PRESCRIPTION NATS=>STRING))
 (63 63 (:REWRITE LOFAT-FS-P-OF-CLEAR-CC))
 (63 21 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (57 57 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (57 19 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (54 54 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (48 48 (:TYPE-PRESCRIPTION FAT32-UPDATE-LOWER-28))
 (48 24 (:REWRITE UNICITY-OF-0))
 (46 46 (:REWRITE FAT32-FILENAME-LIST-P-OF-FILE-TABLE-ELEMENT->FID))
 (45 45 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (45 45 (:REWRITE EFFECTIVE-FAT-OF-CLEAR-CC . 3))
 (45 45 (:REWRITE D-E-DIRECTORY-P-OF-PSEUDO-ROOT-D-E))
 (45 45 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (42 9 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-7))
 (36 36 (:TYPE-PRESCRIPTION STRINGP-OF-D-E-CC-CONTENTS))
 (36 36 (:REWRITE SUBSETP-TRANS2))
 (36 36 (:REWRITE SUBSETP-TRANS))
 (36 36 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-47))
 (36 36 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-1-LEMMA-44))
 (36 36 (:REWRITE INTEGER-LISTP-OF-D-E-CC))
 (36 36 (:REWRITE EXPLODE-OF-NATS=>STRING))
 (36 36 (:REWRITE D-E-P-OF-SET-FIRST-CLUSTER-FILE-SIZE))
 (36 36 (:REWRITE CLUSTER-SIZE-OF-CLEAR-CC))
 (36 9 (:REWRITE LOFAT-PLACE-FILE-HELPER-CORRECTNESS-1))
 (32 16 (:REWRITE DEFAULT-UNARY-MINUS))
 (32 16 (:REWRITE DEFAULT-NUMERATOR))
 (32 16 (:REWRITE DEFAULT-DENOMINATOR))
 (32 16 (:DEFINITION IFIX))
 (24 24 (:REWRITE FIX-WHEN-ACL2-NUMBERP))
 (21 7 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-5))
 (20 20 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (20 20 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (18 18 (:TYPE-PRESCRIPTION INTERSECTP-EQUAL))
 (18 18 (:REWRITE INTERSECTP-MEMBER . 1))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (18 18 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (18 18 (:REWRITE FATI-OF-CLEAR-CC . 2))
 (18 9 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (12 4 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-2))
 (9 9 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (9 9 (:REWRITE NAT-LISTP-OF-STOBJ-FIND-N-FREE-CLUSTERS . 1))
 (3 3 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (3 3 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-6 . 2))
 (3 3 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-6 . 1))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-1
 (46824 2 (:DEFINITION LOFAT-PLACE-FILE))
 (24388 32 (:REWRITE PLACE-CONTENTS-EXPANSION-1))
 (22584 116 (:REWRITE PLACE-CONTENTS-EXPANSION-2))
 (14648 1256 (:REWRITE LEN-OF-FIND-N-FREE-CLUSTERS))
 (13320 122 (:DEFINITION NATP))
 (13210 366 (:REWRITE NFIX-WHEN-NATP))
 (12958 60 (:DEFINITION STOBJ-FIND-N-FREE-CLUSTERS-CORRECTNESS-1))
 (12637 268 (:REWRITE ZP-OPEN))
 (11804 374 (:LINEAR FIND-N-FREE-CLUSTERS-CORRECTNESS-7))
 (9896 36 (:REWRITE EFFECTIVE-FAT-OF-UPDATE-FATI))
 (9545 366 (:REWRITE NFIX-WHEN-ZP))
 (8868 1468 (:DEFINITION MIN))
 (8838 642 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (7416 32 (:REWRITE UPDATE-FATI-OF-UPDATE-FATI-COINCIDENT))
 (7034 7034 (:TYPE-PRESCRIPTION COUNT-FREE-CLUSTERS))
 (5896 8 (:REWRITE COUNT-FREE-CLUSTERS-OF-UPDATE-NTH))
 (5184 24 (:REWRITE UPDATE-FATI-OF-FATI-WHEN-FAT32$C-P))
 (5120 260 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-1-LEMMA-44))
 (4573 2867 (:REWRITE DEFAULT-<-1))
 (4012 60 (:REWRITE LENGTH-WHEN-STRINGP))
 (3738 16 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-10))
 (3590 32 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-188))
 (3465 2867 (:REWRITE DEFAULT-<-2))
 (3312 12 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-29))
 (3257 229 (:DEFINITION LEN))
 (3052 218 (:REWRITE INTEGERP-OF-NTH-WHEN-INTEGER-LISTP))
 (2968 40 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-44))
 (2394 126 (:DEFINITION FIND-D-E))
 (2328 224 (:REWRITE LEN-OF-EFFECTIVE-FAT))
 (2280 12 (:REWRITE LEN-OF-NATS=>CHARS))
 (2272 976 (:REWRITE FIND-N-FREE-CLUSTERS-WHEN-ZP))
 (2268 12 (:REWRITE LEN-OF-INSERT-D-E))
 (2175 1173 (:REWRITE DEFAULT-+-2))
 (2000 400 (:LINEAR NTH-WHEN-D-E-P))
 (1877 53 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-8))
 (1673 554 (:REWRITE DEFAULT-CDR))
 (1561 11 (:REWRITE NTH-OF-EFFECTIVE-FAT))
 (1556 94 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (1536 12 (:REWRITE LEN-OF-PLACE-D-E))
 (1524 40 (:REWRITE LOFAT-FS-P-OF-UPDATE-FATI))
 (1472 200 (:REWRITE LOFAT-FS-P-OF-LOFAT-PLACE-FILE-LEMMA-8))
 (1466 8 (:REWRITE LOFAT-REMOVE-FILE-CORRECTNESS-LEMMA-13))
 (1464 1173 (:REWRITE DEFAULT-+-1))
 (1396 1396 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (1296 36 (:DEFINITION UPDATE-NTH))
 (1280 200 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-47))
 (1278 150 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (1102 58 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
 (1090 1090 (:TYPE-PRESCRIPTION NFIX))
 (1066 22 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (918 34 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (904 94 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (886 70 (:REWRITE D-E-CC-UNDER-IFF . 2))
 (884 104 (:REWRITE STR::CONSP-OF-EXPLODE))
 (874 874 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (781 8 (:DEFINITION INTEGER-LISTP))
 (775 248 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-2))
 (721 721 (:TYPE-PRESCRIPTION D-E-FILE-SIZE))
 (690 138 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (633 24 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (600 10 (:REWRITE FATI-OF-CLEAR-CC . 3))
 (590 241 (:REWRITE DEFAULT-CAR))
 (584 36 (:REWRITE CONSP-OF-LAST))
 (556 556 (:TYPE-PRESCRIPTION FIND-N-FREE-CLUSTERS))
 (554 218 (:REWRITE NTH-WHEN-D-E-P . 2))
 (524 524 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (516 172 (:TYPE-PRESCRIPTION MAKE-CLUSTERS-OF-NIL))
 (487 12 (:REWRITE INTEGERP-OF-CAR-OF-LAST-WHEN-INTEGER-LISTP))
 (486 96 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-COINCIDENT-LEMMA-8))
 (474 150 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (458 6 (:REWRITE LAST-WHEN-EQUAL-LEN-1))
 (441 3 (:DEFINITION FREE-INDEX-LISTP))
 (428 60 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (424 212 (:TYPE-PRESCRIPTION MIN))
 (415 415 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (398 13 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (395 90 (:LINEAR D-E-FILE-SIZE-CORRECTNESS-1))
 (384 12 (:DEFINITION PLACE-D-E))
 (383 253 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (373 373 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-D-E-CC))
 (369 19 (:REWRITE D-E-CC-UNDER-IFF . 3))
 (360 52 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (336 336 (:TYPE-PRESCRIPTION EFFECTIVE-FAT))
 (318 122 (:LINEAR COUNT-FREE-CLUSTERS-CORRECTNESS-1))
 (304 2 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-33))
 (302 184 (:TYPE-PRESCRIPTION LAST))
 (292 292 (:TYPE-PRESCRIPTION NATP-OF-PLACE-CONTENTS))
 (288 32 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-1-LEMMA-44))
 (284 32 (:REWRITE EFFECTIVE-FAT-OF-CLEAR-CC . 2))
 (264 264 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (260 52 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (256 256 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (242 6 (:REWRITE FAT32-MASKED-ENTRY-P-OF-NTH-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (216 30 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (214 214 (:REWRITE FIND-N-FREE-CLUSTERS-CORRECTNESS-8))
 (212 32 (:REWRITE EFFECTIVE-FAT-OF-CLEAR-CC . 3))
 (203 2 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (202 202 (:REWRITE LOFAT-FILE-FIX-WHEN-LOFAT-FILE-P))
 (194 4 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (192 64 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (192 64 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (184 56 (:REWRITE DEFAULT-*-2))
 (184 5 (:REWRITE NOT-INTERSECTP-LIST-OF-LOFAT-TO-HIFAT-HELPER))
 (180 180 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (172 172 (:TYPE-PRESCRIPTION MAKE-CLUSTERS))
 (171 5 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-56))
 (170 6 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-FIND-N-FREE-CLUSTERS . 1))
 (168 168 (:TYPE-PRESCRIPTION ZP))
 (162 162 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (156 156 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (156 12 (:REWRITE DISTRIBUTIVITY))
 (152 104 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (152 82 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (150 150 (:TYPE-PRESCRIPTION D-E-LIST-P))
 (150 150 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (148 148 (:TYPE-PRESCRIPTION ATOM))
 (148 30 (:DEFINITION BINARY-APPEND))
 (128 128 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (128 128 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (128 40 (:REWRITE NATP-OF-PLACE-CONTENTS))
 (127 127 (:LINEAR D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-DISJOINT-LEMMA-12))
 (125 125 (:TYPE-PRESCRIPTION NATP))
 (116 116 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (114 114 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (114 12 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (112 88 (:REWRITE CLUSTER-SIZE-OF-UPDATE-FATI))
 (112 10 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (104 104 (:REWRITE COUNT-OF-CLUSTERS-OF-CLEAR-CC))
 (104 4 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (102 60 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (100 8 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (96 6 (:REWRITE ACL2-NUMBERP-OF-CAR-WHEN-ACL2-NUMBER-LISTP))
 (95 95 (:TYPE-PRESCRIPTION NAT-LISTP))
 (84 40 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (84 12 (:REWRITE D-E-LIST-FIX-WHEN-D-E-LIST-P))
 (80 80 (:TYPE-PRESCRIPTION STOBJ-FIND-N-FREE-CLUSTERS))
 (80 8 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-1-LEMMA-25))
 (74 8 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (74 8 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (72 36 (:REWRITE FAT32-UPDATE-LOWER-28-CORRECTNESS-1 . 1))
 (70 70 (:REWRITE NTH-WHEN-D-E-P . 3))
 (66 66 (:TYPE-PRESCRIPTION FAT32-MASKED-ENTRY-P))
 (64 64 (:TYPE-PRESCRIPTION FAT-LENGTH))
 (64 64 (:LINEAR POSITION-WHEN-MEMBER))
 (64 64 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (62 2 (:REWRITE INTERSECTP-IS-COMMUTATIVE))
 (61 6 (:REWRITE ACL2-NUMBER-LISTP-WHEN-RATIONAL-LISTP))
 (60 56 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-80))
 (58 58 (:REWRITE FIND-N-FREE-CLUSTERS-CORRECTNESS-2 . 1))
 (56 56 (:REWRITE DEFAULT-*-1))
 (52 52 (:TYPE-PRESCRIPTION FAT32$C-P))
 (48 24 (:REWRITE FAT-LENGTH-OF-CLEAR-CC))
 (48 8 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (40 8 (:REWRITE FAT32-MASKED-ENTRY-P-OF-D-E-FIRST-CLUSTER))
 (39 5 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (36 36 (:TYPE-PRESCRIPTION LENGTH))
 (36 36 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (36 12 (:REWRITE USEFUL-D-E-LIST-P-OF-CDR))
 (36 12 (:REWRITE NATS=>STRING-OF-STRING=>NATS))
 (34 34 (:REWRITE LOFAT-FS-P-OF-CLEAR-CC))
 (34 6 (:REWRITE RATIONAL-LISTP-WHEN-INTEGER-LISTP))
 (32 32 (:TYPE-PRESCRIPTION LOFAT-PLACE-FILE-HELPER))
 (31 31 (:TYPE-PRESCRIPTION FAT32-MASKED-ENTRY-LIST-P))
 (31 10 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-17))
 (29 29 (:TYPE-PRESCRIPTION FREE-INDEX-LISTP))
 (28 28 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (26 26 (:REWRITE CLUSTER-SIZE-OF-CLEAR-CC))
 (24 24 (:TYPE-PRESCRIPTION ATOM-OF-CDR-OF-LAST))
 (24 24 (:REWRITE D-E-FILENAME-OF-D-E-SET-FIRST-CLUSTER-FILE-SIZE))
 (24 12 (:REWRITE STR-FIX-WHEN-STRINGP))
 (24 4 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (24 4 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (22 22 (:TYPE-PRESCRIPTION NATS=>STRING))
 (19 3 (:REWRITE NATP-OF-CAR-WHEN-NAT-LISTP))
 (18 18 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (18 18 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (16 16 (:TYPE-PRESCRIPTION MAKE-EMPTY-SUBDIR-CONTENTS))
 (16 16 (:TYPE-PRESCRIPTION FAT32-UPDATE-LOWER-28))
 (16 8 (:REWRITE FAT32-ENTRY-MASK-OF-FAT32-UPDATE-LOWER-28))
 (16 2 (:REWRITE D-E-CC-CONTENTS-OF-CLEAR-CC))
 (14 14 (:REWRITE NAT-LISTP-OF-STOBJ-FIND-N-FREE-CLUSTERS . 1))
 (14 14 (:REWRITE FREE-INDEX-LISTP-OF-FIND-N-FREE-CLUSTERS))
 (14 2 (:REWRITE FOLD-CONSTS-IN-+))
 (14 2 (:LINEAR LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1))
 (14 2 (:DEFINITION NFIX))
 (12 12 (:TYPE-PRESCRIPTION STRINGP-OF-D-E-CC-CONTENTS))
 (12 12 (:REWRITE INTEGER-LISTP-OF-D-E-CC))
 (12 12 (:REWRITE EXPLODE-OF-NATS=>STRING))
 (12 12 (:REWRITE D-E-P-OF-SET-FIRST-CLUSTER-FILE-SIZE))
 (12 2 (:REWRITE D-E-FIRST-CLUSTER-OF-D-E-INSTALL-DIRECTORY-BIT))
 (11 6 (:REWRITE RATIONAL-LISTP-WHEN-NOT-CONSP))
 (11 6 (:REWRITE ACL2-NUMBER-LISTP-WHEN-NOT-CONSP))
 (10 10 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (10 10 (:REWRITE FATI-OF-CLEAR-CC . 2))
 (10 10 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (10 6 (:REWRITE FAT32-ENTRY-LIST-P-OF-EFFECTIVE-FAT))
 (10 2 (:REWRITE D-E-FIRST-CLUSTER-OF-MAKE-D-E-WITH-FILENAME))
 (8 8 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (8 8 (:TYPE-PRESCRIPTION NATP-OF-UPDATE-DIR-CONTENTS))
 (8 8 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (8 8 (:REWRITE SUBSETP-TRANS2))
 (8 8 (:REWRITE SUBSETP-TRANS))
 (8 8 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-58))
 (8 8 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (6 6 (:TYPE-PRESCRIPTION RATIONAL-LISTP))
 (6 6 (:TYPE-PRESCRIPTION FAT32-ENTRY-LIST-P))
 (6 6 (:TYPE-PRESCRIPTION ACL2-NUMBER-LISTP))
 (6 2 (:REWRITE UNICITY-OF-0))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (5 5 (:REWRITE NON-FREE-INDEX-LIST-LISTP-CORRECTNESS-1))
 (5 5 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (5 5 (:LINEAR LOFAT-TO-HIFAT-HELPER-AFTER-DELETE-AND-CLEAR-1-LEMMA-1))
 (5 5 (:LINEAR LOFAT-FIND-FILE-CORRECTNESS-1-LEMMA-8))
 (4 4 (:TYPE-PRESCRIPTION INTERSECTP-EQUAL))
 (4 4 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (4 4 (:REWRITE INTERSECTP-MEMBER . 1))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (4 4 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (4 2 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (4 2 (:REWRITE FIX-WHEN-ACL2-NUMBERP))
 (2 2 (:REWRITE LOFAT-PLACE-FILE-HELPER-CORRECTNESS-1))
 (2 2 (:REWRITE FAT32-FILENAME-P-OF-FAT32-FILENAME-FIX))
 (1 1 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-6 . 2))
 (1 1 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-6 . 1))
 (1 1 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-D-E-CC))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-20
 (93 9 (:DEFINITION LEN))
 (52 20 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (50 1 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (42 14 (:REWRITE STR::CONSP-OF-EXPLODE))
 (38 14 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (38 6 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (35 5 (:REWRITE NFIX-WHEN-ZP))
 (32 1 (:DEFINITION BINARY-APPEND))
 (31 10 (:REWRITE DEFAULT-CDR))
 (31 1 (:DEFINITION M1-FILE-CONTENTS-P))
 (27 14 (:REWRITE DEFAULT-+-2))
 (27 6 (:REWRITE ZP-OPEN))
 (22 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (16 16 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (16 16 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (14 14 (:REWRITE DEFAULT-+-1))
 (12 12 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (12 12 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (10 6 (:REWRITE DEFAULT-<-2))
 (10 4 (:REWRITE CONSP-OF-REPEAT))
 (9 6 (:REWRITE DEFAULT-<-1))
 (8 8 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (6 6 (:TYPE-PRESCRIPTION ZP))
 (6 2 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (6 2 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (6 1 (:REWRITE M1-FILE-CONTENTS-P-CORRECTNESS-1))
 (4 4 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (4 4 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (4 4 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (4 2 (:REWRITE DEFAULT-*-2))
 (4 1 (:REWRITE REPEAT-WHEN-ZP))
 (4 1 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER))
 (2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-2
 (238 22 (:DEFINITION LEN))
 (112 44 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (107 13 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (91 31 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (77 28 (:REWRITE STR::CONSP-OF-EXPLODE))
 (66 6 (:REWRITE NFIX-WHEN-ZP))
 (65 23 (:REWRITE DEFAULT-CDR))
 (60 30 (:REWRITE DEFAULT-+-2))
 (60 3 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (50 8 (:REWRITE ZP-OPEN))
 (34 34 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (34 34 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (33 3 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (32 32 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (32 30 (:REWRITE DEFAULT-+-1))
 (32 1 (:DEFINITION BINARY-APPEND))
 (30 30 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (30 30 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (24 15 (:REWRITE DEFAULT-<-1))
 (24 8 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (24 8 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (23 15 (:REWRITE DEFAULT-<-2))
 (22 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (18 3 (:REWRITE M1-FILE-CONTENTS-P-CORRECTNESS-1))
 (16 16 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (12 12 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (12 6 (:REWRITE DEFAULT-*-2))
 (10 10 (:TYPE-PRESCRIPTION REPEAT))
 (10 4 (:REWRITE CONSP-OF-REPEAT))
 (9 9 (:TYPE-PRESCRIPTION ZP))
 (8 8 (:LINEAR POSITION-WHEN-MEMBER))
 (8 8 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 6 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (6 6 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (6 6 (:REWRITE DEFAULT-*-1))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (4 1 (:REWRITE REPEAT-WHEN-ZP))
 (4 1 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (2 2 (:REWRITE APPEND-NTHCDR-DIRNAME-BASENAME-LEMMA-1 . 3))
 (2 1 (:REWRITE LOFAT-FILE-CONTENTS-P-WHEN-D-E-LISTP))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:DEFINITION NATP))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-22
 (238 22 (:DEFINITION LEN))
 (112 44 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (107 13 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (91 31 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (77 28 (:REWRITE STR::CONSP-OF-EXPLODE))
 (66 6 (:REWRITE NFIX-WHEN-ZP))
 (65 23 (:REWRITE DEFAULT-CDR))
 (60 30 (:REWRITE DEFAULT-+-2))
 (60 3 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (50 8 (:REWRITE ZP-OPEN))
 (45 45 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (36 36 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (34 34 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (34 34 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (33 3 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (32 30 (:REWRITE DEFAULT-+-1))
 (32 1 (:DEFINITION BINARY-APPEND))
 (30 30 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (30 30 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (27 9 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (27 9 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (22 14 (:REWRITE DEFAULT-<-2))
 (22 14 (:REWRITE DEFAULT-<-1))
 (22 2 (:REWRITE LENGTH-WHEN-STRINGP))
 (22 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (18 18 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (18 3 (:REWRITE M1-FILE-CONTENTS-P-CORRECTNESS-1))
 (12 12 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (12 6 (:REWRITE DEFAULT-*-2))
 (12 4 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (10 10 (:TYPE-PRESCRIPTION REPEAT))
 (10 4 (:REWRITE CONSP-OF-REPEAT))
 (9 9 (:TYPE-PRESCRIPTION ZP))
 (9 9 (:LINEAR POSITION-WHEN-MEMBER))
 (9 9 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 6 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (6 6 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (6 6 (:REWRITE DEFAULT-*-1))
 (4 4 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (4 1 (:REWRITE REPEAT-WHEN-ZP))
 (4 1 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (2 2 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (2 2 (:TYPE-PRESCRIPTION TAKE))
 (2 2 (:TYPE-PRESCRIPTION LENGTH))
 (2 2 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (2 2 (:REWRITE APPEND-NTHCDR-DIRNAME-BASENAME-LEMMA-1 . 3))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:DEFINITION NATP))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-6
 (1042 60 (:DEFINITION LEN))
 (918 6 (:REWRITE LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (760 4 (:REWRITE ABS-PLACE-FILE-HELPER-OF-CTX-APP-LEMMA-1))
 (639 71 (:REWRITE LOFAT-FS-P-OF-LOFAT-PLACE-FILE-LEMMA-8))
 (590 94 (:REWRITE STR::CONSP-OF-EXPLODE))
 (560 4 (:DEFINITION LOFAT-FIND-FILE))
 (443 92 (:REWRITE DEFAULT-CDR))
 (300 4 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (272 16 (:DEFINITION FIND-D-E))
 (223 72 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (213 71 (:REWRITE LOFAT-FILE-FIX-WHEN-LOFAT-FILE-P))
 (202 2 (:DEFINITION FAT32-FILENAME-LIST-PREFIXP))
 (189 36 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (188 8 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (165 41 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (146 146 (:TYPE-PRESCRIPTION LOFAT-FILE-P))
 (146 146 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-3))
 (144 16 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (141 73 (:REWRITE DEFAULT-+-2))
 (138 10 (:REWRITE ZP-OPEN))
 (120 4 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (112 12 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (96 12 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (94 40 (:REWRITE DEFAULT-<-1))
 (84 84 (:TYPE-PRESCRIPTION CLUSTER-SIZE))
 (80 16 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (79 72 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-2))
 (78 73 (:REWRITE DEFAULT-+-1))
 (72 8 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (70 70 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (70 70 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (67 40 (:REWRITE DEFAULT-<-2))
 (64 64 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (60 60 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (54 24 (:REWRITE DEFAULT-CAR))
 (48 16 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (45 15 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (45 15 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (44 4 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (42 42 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 (36 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (32 32 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (32 32 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (32 32 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (30 30 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (28 28 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (24 24 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (24 24 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (24 12 (:REWRITE DEFAULT-*-2))
 (24 8 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (24 4 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (24 4 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (23 3 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-2))
 (20 20 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (20 20 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (16 16 (:TYPE-PRESCRIPTION D-E-P))
 (16 16 (:TYPE-PRESCRIPTION D-E-LIST-P))
 (15 15 (:LINEAR POSITION-WHEN-MEMBER))
 (15 15 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (14 14 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-PREFIXP))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (12 12 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (12 12 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (12 12 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (12 12 (:REWRITE DEFAULT-*-1))
 (12 4 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (12 4 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (12 4 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (12 4 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (8 8 (:TYPE-PRESCRIPTION ZP))
 (8 8 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (8 8 (:TYPE-PRESCRIPTION FAT32$C-P))
 (8 8 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (6 2 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (5 3 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (5 1 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 2))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (3 1 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 (2 2 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (2 2 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-1))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-7
 (1042 60 (:DEFINITION LEN))
 (918 6 (:REWRITE LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (760 4 (:REWRITE ABS-PLACE-FILE-HELPER-OF-CTX-APP-LEMMA-1))
 (639 71 (:REWRITE LOFAT-FS-P-OF-LOFAT-PLACE-FILE-LEMMA-8))
 (590 94 (:REWRITE STR::CONSP-OF-EXPLODE))
 (560 4 (:DEFINITION LOFAT-FIND-FILE))
 (443 92 (:REWRITE DEFAULT-CDR))
 (300 4 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (272 16 (:DEFINITION FIND-D-E))
 (223 72 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (213 71 (:REWRITE LOFAT-FILE-FIX-WHEN-LOFAT-FILE-P))
 (202 2 (:DEFINITION FAT32-FILENAME-LIST-PREFIXP))
 (189 36 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (188 8 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (165 41 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (146 146 (:TYPE-PRESCRIPTION LOFAT-FILE-P))
 (146 146 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-3))
 (144 16 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (141 73 (:REWRITE DEFAULT-+-2))
 (138 10 (:REWRITE ZP-OPEN))
 (120 4 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (112 12 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (96 12 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (94 40 (:REWRITE DEFAULT-<-1))
 (84 84 (:TYPE-PRESCRIPTION CLUSTER-SIZE))
 (80 16 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (79 72 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-2))
 (78 73 (:REWRITE DEFAULT-+-1))
 (72 8 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (70 70 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (70 70 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (67 40 (:REWRITE DEFAULT-<-2))
 (64 64 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (60 60 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (54 24 (:REWRITE DEFAULT-CAR))
 (48 16 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (45 15 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (45 15 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (44 4 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (42 42 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 (36 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (32 32 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (32 32 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (32 32 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (30 30 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (28 28 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (24 24 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (24 24 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (24 12 (:REWRITE DEFAULT-*-2))
 (24 8 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (24 4 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (24 4 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (23 3 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-2))
 (20 20 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (20 20 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (16 16 (:TYPE-PRESCRIPTION D-E-P))
 (16 16 (:TYPE-PRESCRIPTION D-E-LIST-P))
 (15 15 (:LINEAR POSITION-WHEN-MEMBER))
 (15 15 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (14 14 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-PREFIXP))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (12 12 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (12 12 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (12 12 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (12 12 (:REWRITE DEFAULT-*-1))
 (12 4 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (12 4 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (12 4 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (12 4 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (8 8 (:TYPE-PRESCRIPTION ZP))
 (8 8 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (8 8 (:TYPE-PRESCRIPTION FAT32$C-P))
 (8 8 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (6 3 (:REWRITE LOFAT-FILE-CONTENTS-P-WHEN-D-E-LISTP))
 (6 2 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (5 3 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (5 1 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 2))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (3 1 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 (2 2 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (2 2 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-1))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-8
 (1093 63 (:DEFINITION LEN))
 (918 6 (:REWRITE LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (760 4 (:REWRITE ABS-PLACE-FILE-HELPER-OF-CTX-APP-LEMMA-1))
 (657 73 (:REWRITE LOFAT-FS-P-OF-LOFAT-PLACE-FILE-LEMMA-8))
 (617 100 (:REWRITE STR::CONSP-OF-EXPLODE))
 (560 4 (:DEFINITION LOFAT-FIND-FILE))
 (464 95 (:REWRITE DEFAULT-CDR))
 (300 4 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (272 16 (:DEFINITION FIND-D-E))
 (229 74 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (219 73 (:REWRITE LOFAT-FILE-FIX-WHEN-LOFAT-FILE-P))
 (202 2 (:DEFINITION FAT32-FILENAME-LIST-PREFIXP))
 (191 38 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (188 8 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (176 44 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (167 167 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (153 80 (:REWRITE DEFAULT-+-2))
 (150 150 (:TYPE-PRESCRIPTION LOFAT-FILE-P))
 (150 150 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-3))
 (144 16 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (139 11 (:REWRITE ZP-OPEN))
 (120 4 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (112 12 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (96 12 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (87 80 (:REWRITE DEFAULT-+-1))
 (84 84 (:TYPE-PRESCRIPTION CLUSTER-SIZE))
 (81 74 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-2))
 (80 16 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (76 42 (:REWRITE DEFAULT-<-1))
 (74 74 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (74 74 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (72 8 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (70 42 (:REWRITE DEFAULT-<-2))
 (68 68 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (60 60 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (54 24 (:REWRITE DEFAULT-CAR))
 (48 16 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (48 16 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (48 16 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (44 4 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (42 42 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 (36 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (32 32 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (32 32 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (32 32 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (32 32 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (28 28 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (24 24 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (24 24 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (24 12 (:REWRITE DEFAULT-*-2))
 (24 8 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (24 4 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (24 4 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (23 3 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-2))
 (20 20 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (20 20 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (16 16 (:TYPE-PRESCRIPTION D-E-P))
 (16 16 (:TYPE-PRESCRIPTION D-E-LIST-P))
 (16 16 (:LINEAR POSITION-WHEN-MEMBER))
 (16 16 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (14 14 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-PREFIXP))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (12 12 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (12 12 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (12 12 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (12 12 (:REWRITE DEFAULT-*-1))
 (12 4 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (12 4 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (12 4 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (12 4 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (10 10 (:TYPE-PRESCRIPTION ZP))
 (9 3 (:DEFINITION NATP))
 (8 8 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (8 8 (:TYPE-PRESCRIPTION FAT32$C-P))
 (8 8 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (6 2 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (5 3 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (5 1 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (5 1 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 2))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 2))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 (2 2 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (2 2 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-1))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-48
 (2950 136 (:DEFINITION LEN))
 (2457 273 (:REWRITE LOFAT-FS-P-OF-LOFAT-PLACE-FILE-LEMMA-8))
 (1915 182 (:REWRITE STR::CONSP-OF-EXPLODE))
 (1400 14 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (1276 184 (:REWRITE DEFAULT-CDR))
 (1214 4 (:REWRITE NTHCDR-WHEN->=-N-LEN-L-UNDER-LIST-EQUIV))
 (883 27 (:REWRITE ZP-OPEN))
 (849 276 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (840 6 (:DEFINITION LOFAT-FIND-FILE))
 (819 273 (:REWRITE LOFAT-FILE-FIX-WHEN-LOFAT-FILE-P))
 (725 4 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (702 19 (:REWRITE NFIX-WHEN-ZP))
 (671 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (657 2 (:REWRITE CONSP-OF-NTHCDR))
 (641 2 (:REWRITE TAKE-OF-LEN-FREE))
 (599 3 (:DEFINITION NATP))
 (558 558 (:TYPE-PRESCRIPTION LOFAT-FILE-P))
 (558 558 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-3))
 (450 6 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (440 4 (:REWRITE LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (408 24 (:DEFINITION FIND-D-E))
 (385 2 (:REWRITE ABS-PLACE-FILE-HELPER-OF-CTX-APP-LEMMA-1))
 (369 1 (:DEFINITION BINARY-APPEND))
 (368 2 (:REWRITE TAKE-OF-TOO-MANY))
 (352 88 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (325 166 (:REWRITE DEFAULT-+-2))
 (297 276 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-2))
 (282 12 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (218 218 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (218 2 (:DEFINITION NTHCDR))
 (216 24 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (180 6 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (179 166 (:REWRITE DEFAULT-+-1))
 (168 18 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (150 50 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (150 50 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (144 144 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (144 144 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (144 18 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (139 81 (:REWRITE DEFAULT-<-2))
 (126 126 (:TYPE-PRESCRIPTION CLUSTER-SIZE))
 (120 24 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (118 81 (:REWRITE DEFAULT-<-1))
 (115 1 (:DEFINITION TAKE))
 (108 12 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (101 1 (:DEFINITION FAT32-FILENAME-LIST-PREFIXP))
 (100 100 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (90 90 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (72 34 (:REWRITE DEFAULT-CAR))
 (72 24 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (69 9 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-2))
 (66 66 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 (66 6 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (60 60 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (60 30 (:REWRITE DEFAULT-*-2))
 (50 50 (:LINEAR POSITION-WHEN-MEMBER))
 (50 50 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (48 48 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (48 48 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (48 48 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (42 42 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (36 36 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (36 12 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (36 6 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (36 6 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (36 4 (:REWRITE APPEND-NTHCDR-DIRNAME-BASENAME-LEMMA-1 . 3))
 (30 30 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (30 30 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (30 30 (:REWRITE DEFAULT-*-1))
 (27 9 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (24 24 (:TYPE-PRESCRIPTION D-E-P))
 (18 18 (:TYPE-PRESCRIPTION ZP))
 (18 18 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (18 18 (:TYPE-PRESCRIPTION D-E-FIRST-CLUSTER))
 (18 18 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (18 18 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (18 6 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (18 6 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (18 6 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (18 6 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (18 2 (:REWRITE TAKE-WHEN-ATOM))
 (18 1 (:REWRITE CAR-OF-TAKE))
 (15 9 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (15 3 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (14 14 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-1))
 (14 1 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
 (12 12 (:TYPE-PRESCRIPTION FAT32$C-P))
 (12 12 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (9 3 (:REWRITE CONSP-OF-TAKE))
 (7 7 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-PREFIXP))
 (7 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (7 1 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LIST*P))
 (6 6 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (6 6 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (6 6 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (4 4 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 2))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (2 1 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-NOT-CONSP))
 (1 1 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-49
 (1793 81 (:DEFINITION LEN))
 (1539 171 (:REWRITE LOFAT-FS-P-OF-LOFAT-PLACE-FILE-LEMMA-8))
 (1200 114 (:REWRITE STR::CONSP-OF-EXPLODE))
 (900 9 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (781 98 (:REWRITE DEFAULT-CDR))
 (671 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (657 2 (:REWRITE CONSP-OF-NTHCDR))
 (641 2 (:REWRITE TAKE-OF-LEN-FREE))
 (594 9 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (523 172 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (513 171 (:REWRITE LOFAT-FILE-FIX-WHEN-LOFAT-FILE-P))
 (413 14 (:REWRITE ZP-OPEN))
 (386 2 (:REWRITE NTHCDR-WHEN->=-N-LEN-L-UNDER-LIST-EQUIV))
 (369 1 (:DEFINITION BINARY-APPEND))
 (365 2 (:REWRITE TAKE-OF-TOO-MANY))
 (362 2 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (359 13 (:REWRITE NFIX-WHEN-ZP))
 (346 346 (:TYPE-PRESCRIPTION LOFAT-FILE-P))
 (346 346 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-3))
 (299 1 (:DEFINITION NATP))
 (280 2 (:DEFINITION LOFAT-FIND-FILE))
 (219 55 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (191 96 (:REWRITE DEFAULT-+-2))
 (179 172 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-2))
 (150 2 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (136 8 (:DEFINITION FIND-D-E))
 (118 118 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (114 1 (:DEFINITION TAKE))
 (106 1 (:DEFINITION NTHCDR))
 (101 96 (:REWRITE DEFAULT-+-1))
 (94 4 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (86 86 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (86 86 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (81 27 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (81 27 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (72 8 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (60 35 (:REWRITE DEFAULT-<-2))
 (60 2 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (56 6 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (54 54 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (54 35 (:REWRITE DEFAULT-<-1))
 (48 6 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (42 42 (:TYPE-PRESCRIPTION CLUSTER-SIZE))
 (40 8 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (38 38 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (38 19 (:REWRITE DEFAULT-*-2))
 (38 12 (:REWRITE DEFAULT-CAR))
 (36 4 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (30 30 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (27 27 (:LINEAR POSITION-WHEN-MEMBER))
 (27 27 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (24 8 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (23 3 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-2))
 (22 22 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 (22 2 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (19 19 (:REWRITE DEFAULT-*-1))
 (18 2 (:REWRITE TAKE-WHEN-ATOM))
 (18 1 (:REWRITE CAR-OF-TAKE))
 (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))
 (15 5 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (14 14 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (14 1 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
 (12 12 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (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 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (10 10 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (9 9 (:TYPE-PRESCRIPTION ZP))
 (9 9 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (9 9 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-1))
 (9 3 (:REWRITE CONSP-OF-TAKE))
 (8 8 (:TYPE-PRESCRIPTION D-E-P))
 (7 1 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LIST*P))
 (6 6 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (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 2 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (6 2 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (6 2 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (6 2 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (5 3 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (5 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (5 1 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (4 4 (:TYPE-PRESCRIPTION FAT32$C-P))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (3 3 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (2 2 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (2 2 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (2 1 (:REWRITE LOFAT-FILE-CONTENTS-P-WHEN-D-E-LISTP))
 (2 1 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-NOT-CONSP))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-50
 (1793 81 (:DEFINITION LEN))
 (1548 172 (:REWRITE LOFAT-FS-P-OF-LOFAT-PLACE-FILE-LEMMA-8))
 (1211 115 (:REWRITE STR::CONSP-OF-EXPLODE))
 (900 9 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (781 98 (:REWRITE DEFAULT-CDR))
 (671 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (657 2 (:REWRITE CONSP-OF-NTHCDR))
 (641 2 (:REWRITE TAKE-OF-LEN-FREE))
 (594 9 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (526 173 (:REWRITE LOFAT-DIRECTORY-FILE-P-WHEN-LOFAT-FILE-P))
 (516 172 (:REWRITE LOFAT-FILE-FIX-WHEN-LOFAT-FILE-P))
 (496 10 (:REWRITE LENGTH-WHEN-STRINGP))
 (413 14 (:REWRITE ZP-OPEN))
 (386 2 (:REWRITE NTHCDR-WHEN->=-N-LEN-L-UNDER-LIST-EQUIV))
 (369 1 (:DEFINITION BINARY-APPEND))
 (365 2 (:REWRITE TAKE-OF-TOO-MANY))
 (362 2 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (359 13 (:REWRITE NFIX-WHEN-ZP))
 (348 348 (:TYPE-PRESCRIPTION LOFAT-FILE-P))
 (348 348 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-3))
 (299 1 (:DEFINITION NATP))
 (280 2 (:DEFINITION LOFAT-FIND-FILE))
 (219 55 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (197 197 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (191 96 (:REWRITE DEFAULT-+-2))
 (180 173 (:REWRITE LOFAT-DIRECTORY-FILE-P-CORRECTNESS-2))
 (150 2 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (136 8 (:DEFINITION FIND-D-E))
 (122 122 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (115 1 (:DEFINITION TAKE))
 (110 1 (:DEFINITION NTHCDR))
 (101 96 (:REWRITE DEFAULT-+-1))
 (94 4 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (86 86 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (86 86 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (84 28 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (84 28 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (72 8 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (60 2 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (59 34 (:REWRITE DEFAULT-<-2))
 (56 56 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (56 6 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (49 34 (:REWRITE DEFAULT-<-1))
 (48 6 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (42 42 (:TYPE-PRESCRIPTION CLUSTER-SIZE))
 (40 8 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (38 38 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (38 19 (:REWRITE DEFAULT-*-2))
 (38 12 (:REWRITE DEFAULT-CAR))
 (36 4 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (30 30 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (28 28 (:LINEAR POSITION-WHEN-MEMBER))
 (28 28 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (24 8 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (23 3 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-2))
 (22 22 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 (22 2 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (19 19 (:REWRITE DEFAULT-*-1))
 (18 2 (:REWRITE TAKE-WHEN-ATOM))
 (18 2 (:REWRITE APPEND-NTHCDR-DIRNAME-BASENAME-LEMMA-1 . 3))
 (18 1 (:REWRITE CAR-OF-TAKE))
 (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))
 (15 5 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (14 14 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (14 1 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
 (12 12 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (12 4 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (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 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (10 10 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (9 9 (:TYPE-PRESCRIPTION ZP))
 (9 9 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (9 9 (:REWRITE LOFAT-PLACE-FILE-GUARD-LEMMA-1))
 (9 3 (:REWRITE CONSP-OF-TAKE))
 (8 8 (:TYPE-PRESCRIPTION TAKE))
 (8 8 (:TYPE-PRESCRIPTION D-E-P))
 (7 1 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LIST*P))
 (6 6 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (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 2 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (6 2 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (6 2 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (6 2 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (5 3 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (5 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (5 1 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (4 4 (:TYPE-PRESCRIPTION FAT32$C-P))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (3 3 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (2 2 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (2 2 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (2 2 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (2 1 (:REWRITE STR::HEX-DIGIT-CHAR-LIST*P-WHEN-NOT-CONSP))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-26
 (289000 136308 (:REWRITE DEFAULT-+-2))
 (260413 12211 (:DEFINITION FIND-D-E))
 (218834 971 (:REWRITE LOFAT-PLACE-FILE-HELPER-CORRECTNESS-1))
 (187729 105231 (:REWRITE DEFAULT-CDR))
 (169878 3388 (:DEFINITION NATP))
 (169194 136308 (:REWRITE DEFAULT-+-1))
 (132664 4916 (:REWRITE PLACE-CONTENTS-EXPANSION-2))
 (104520 8913 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-COINCIDENT-LEMMA-8))
 (85416 51885 (:REWRITE DEFAULT-<-1))
 (84417 51885 (:REWRITE DEFAULT-<-2))
 (75724 75724 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (69177 69177 (:TYPE-PRESCRIPTION LOFAT-FILE-CONTENTS-FIX))
 (63695 63695 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (63075 12380 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (62327 21203 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (58228 58228 (:TYPE-PRESCRIPTION INTEGERP-OF-D-E-CC-CONTENTS))
 (57565 973 (:DEFINITION FAT32-FILENAME-LIST-PREFIXP))
 (55038 26770 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (52010 3944 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-1-LEMMA-25))
 (46731 9965 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-5))
 (43173 9191 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (40256 3944 (:REWRITE D-E-CC-CORRECTNESS-1))
 (38497 38497 (:TYPE-PRESCRIPTION MAKE-CLUSTERS))
 (38446 18983 (:REWRITE DEFAULT-*-2))
 (37862 37862 (:LINEAR POSITION-WHEN-MEMBER))
 (37862 37862 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (37862 37862 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (37862 37862 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (36129 36129 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (31488 31488 (:TYPE-PRESCRIPTION GOOD-ROOT-D-E-P))
 (29253 1005 (:REWRITE INTEGERP-OF-NTH-WHEN-INTEGER-LISTP))
 (27551 24975 (:REWRITE DEFAULT-CAR))
 (27546 27546 (:TYPE-PRESCRIPTION LOFAT-FS-P))
 (26840 26840 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (26100 10655 (:DEFINITION STOBJ-FIND-N-FREE-CLUSTERS-CORRECTNESS-1))
 (24222 10977 (:REWRITE DEFAULT-UNARY-MINUS))
 (23576 7734 (:REWRITE D-E-LIST-P-WHEN-NOT-CONSP))
 (22664 22664 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (21392 938 (:REWRITE SUBSETP-CAR-MEMBER))
 (20454 3373 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (20272 20272 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (18983 18983 (:REWRITE DEFAULT-*-1))
 (18144 578 (:DEFINITION MEMBER-EQUAL))
 (16938 3638 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (16836 5612 (:REWRITE LOFAT-REMOVE-FILE-CORRECTNESS-LEMMA-26))
 (14960 448 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (14762 1269 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (13332 4444 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-DISJOINT-LEMMA-4))
 (12111 8913 (:REWRITE D-E-CC-UNDER-IFF . 2))
 (12002 204 (:REWRITE LAST-WHEN-EQUAL-LEN-1))
 (11720 11720 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (9777 3259 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (9693 224 (:DEFINITION INTEGER-LISTP))
 (8283 2761 (:REWRITE D-E-CC-UNDER-IFF . 3))
 (7708 5770 (:TYPE-PRESCRIPTION LAST))
 (7588 1473 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (6818 6818 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (6784 169 (:DEFINITION PLACE-D-E))
 (6736 421 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (6255 264 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (5836 1005 (:REWRITE NTH-WHEN-D-E-P . 2))
 (5651 408 (:REWRITE INTEGERP-OF-CAR-OF-LAST-WHEN-INTEGER-LISTP))
 (4865 1946 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (4840 4840 (:TYPE-PRESCRIPTION MAKE-EMPTY-SUBDIR-CONTENTS))
 (4776 4776 (:LINEAR D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-DISJOINT-LEMMA-12))
 (4196 3484 (:REWRITE CLUSTER-SIZE-OF-UPDATE-FATI))
 (3838 610 (:REWRITE CONSP-OF-LAST))
 (3656 668 (:REWRITE UPDATE-FATI-OF-FATI-WHEN-FAT32$C-P))
 (3630 2420 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-80))
 (3500 1034 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (3409 3409 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (3388 3388 (:TYPE-PRESCRIPTION NATP))
 (2977 20 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (2970 390 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-29))
 (2943 871 (:REWRITE LOFAT-FS-P-OF-UPDATE-FATI))
 (2734 2526 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2734 2526 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2526 2526 (:REWRITE SUBSETP-TRANS2))
 (2526 2526 (:REWRITE SUBSETP-TRANS))
 (2458 2458 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (2068 2068 (:TYPE-PRESCRIPTION FAT32$C-P))
 (1946 1946 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 2))
 (1946 1946 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (1824 792 (:REWRITE LOFAT-FS-P-OF-CLEAR-CC))
 (1692 1098 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-81))
 (1536 384 (:DEFINITION BINARY-APPEND))
 (1324 264 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (1304 244 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (1251 169 (:REWRITE D-E-LIST-FIX-WHEN-D-E-LIST-P))
 (1048 1048 (:REWRITE SUBSETP-MEMBER . 2))
 (1048 1048 (:REWRITE SUBSETP-MEMBER . 1))
 (1005 1005 (:REWRITE NAT-LISTP-OF-STOBJ-FIND-N-FREE-CLUSTERS . 1))
 (973 973 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 (973 973 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (816 816 (:TYPE-PRESCRIPTION ATOM-OF-CDR-OF-LAST))
 (768 768 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (712 712 (:REWRITE CLUSTER-SIZE-OF-CLEAR-CC))
 (642 214 (:REWRITE FATI-OF-CLEAR-CC . 3))
 (507 169 (:REWRITE USEFUL-D-E-LIST-P-OF-CDR))
 (480 48 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 (438 120 (:REWRITE LOFAT-REMOVE-FILE-CORRECTNESS-LEMMA-13))
 (368 368 (:REWRITE INTEGER-LISTP-OF-D-E-CC))
 (264 264 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (244 244 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (244 244 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (216 36 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (214 214 (:REWRITE FATI-OF-CLEAR-CC . 2))
 (177 177 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (169 169 (:REWRITE D-E-P-OF-SET-FIRST-CLUSTER-FILE-SIZE))
 (96 96 (:REWRITE SUBSETP-NIL))
 (96 96 (:REWRITE SET-EQUIV-OF-NIL))
 (40 20 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (36 12 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (36 12 (:LINEAR LOFAT-FIND-FILE-CORRECTNESS-1-LEMMA-8))
 (28 12 (:LINEAR LOFAT-TO-HIFAT-HELPER-AFTER-DELETE-AND-CLEAR-1-LEMMA-1))
 (6 2 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-78))
 )
(LOFAT-PWRITE-REFINEMENT
 (51934 438 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (50808 412 (:DEFINITION LOFAT-FIND-FILE))
 (45575 2043 (:DEFINITION LEN))
 (37775 624 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-2))
 (37680 314 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (30777 64 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (23904 1700 (:DEFINITION FIND-D-E))
 (21980 314 (:DEFINITION CEILING))
 (20417 7863 (:REWRITE DEFAULT-CDR))
 (19923 6641 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (16944 850 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (14545 2083 (:REWRITE ZP-OPEN))
 (13344 772 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (11304 1256 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (10352 1262 (:REWRITE FIND-D-E-CORRECTNESS-2))
 (9730 5873 (:REWRITE DEFAULT-+-2))
 (9420 314 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
 (9198 1262 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (8695 4924 (:REWRITE DEFAULT-<-2))
 (8500 1700 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (7931 1547 (:DEFINITION ASSOC-EQUAL))
 (6913 5873 (:REWRITE DEFAULT-+-1))
 (6857 6779 (:REWRITE DEFAULT-CAR))
 (6399 4924 (:REWRITE DEFAULT-<-1))
 (6362 6362 (:TYPE-PRESCRIPTION FIND-D-E-CORRECTNESS-1))
 (6207 1495 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (5966 314 (:REWRITE DEFAULT-UNARY-/))
 (5870 104 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 1))
 (5752 104 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 2))
 (5100 1700 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (4670 354 (:REWRITE D-E-CC-UNDER-IFF . 3))
 (4461 1410 (:REWRITE STR::CONSP-OF-EXPLODE))
 (4356 26 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-30))
 (3654 794 (:REWRITE LOFAT-FILE-P-WHEN-LOFAT-DIRECTORY-FILE-P-OR-LOFAT-REGULAR-FILE-P))
 (3400 3400 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (3400 3400 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (3180 3180 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (3016 412 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (2954 2954 (:REWRITE USEFUL-D-E-LIST-P-OF-ROOT-D-E-LIST))
 (2768 2768 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (2496 2496 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (2472 2472 (:TYPE-PRESCRIPTION COUNT-OF-CLUSTERS))
 (2472 824 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-1))
 (2407 8 (:LINEAR LEN-OF-EXPLODE-OF-M1-FILE-CONTENTS-FIX))
 (2158 2158 (:TYPE-PRESCRIPTION D-E-FILE-SIZE))
 (1884 1884 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (1872 624 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (1872 624 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (1570 1570 (:TYPE-PRESCRIPTION NONNEGATIVE-INTEGER-QUOTIENT))
 (1570 628 (:LINEAR LOFAT-FS-P-CORRECTNESS-1))
 (1570 628 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (1494 332 (:LINEAR D-E-FILE-SIZE-CORRECTNESS-1))
 (1422 302 (:REWRITE LOFAT-TO-HIFAT-CORRECTNESS-2))
 (1368 412 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (1293 544 (:REWRITE NFIX-WHEN-ZP))
 (1288 1288 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (1256 314 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (1248 1248 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (1238 326 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (1236 1236 (:REWRITE-QUOTED-CONSTANT LOFAT-FILE-CONTENTS-FIX-UNDER-LOFAT-FILE-CONTENTS-EQUIV))
 (1236 412 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (952 476 (:REWRITE DEFAULT-*-2))
 (728 182 (:LINEAR HIFAT-ENTRY-COUNT-WHEN-HIFAT-SUBSETP))
 (704 88 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-2))
 (696 232 (:REWRITE LOFAT-UNLINK-REFINEMENT-LEMMA-4))
 (694 694 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (656 328 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-FIX))
 (628 314 (:REWRITE DEFAULT-UNARY-MINUS))
 (628 314 (:REWRITE DEFAULT-NUMERATOR))
 (628 314 (:REWRITE DEFAULT-DENOMINATOR))
 (628 314 (:DEFINITION IFIX))
 (624 624 (:LINEAR POSITION-WHEN-MEMBER))
 (624 624 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (476 476 (:REWRITE DEFAULT-*-1))
 (456 456 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (456 456 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (447 77 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-2))
 (412 412 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (363 121 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-5))
 (332 332 (:REWRITE PSEUDO-ROOT-D-E-CORRECTNESS-1))
 (332 332 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-6 . 1))
 (314 314 (:TYPE-PRESCRIPTION FAT32$C-P))
 (314 314 (:REWRITE LOFAT-FS-P-CORRECTNESS-1))
 (276 276 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (247 247 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (247 247 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (224 32 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (196 98 (:REWRITE LOFAT-REGULAR-FILE-P-CORRECTNESS-1))
 (182 182 (:TYPE-PRESCRIPTION LOFAT-TO-HIFAT-CORRECTNESS-1 . 1))
 (141 3 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-145))
 (126 126 (:TYPE-PRESCRIPTION LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1 . 1))
 (123 18 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-40))
 (96 32 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (91 91 (:REWRITE LOFAT-TO-HIFAT-CORRECTNESS-1))
 (91 91 (:REWRITE HIFAT-NO-DUPS-P-OF-LOFAT-TO-HIFAT))
 (84 84 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (84 84 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-4))
 (72 18 (:LINEAR LOFAT-TO-HIFAT-HELPER-CORRECTNESS-1))
 (72 12 (:REWRITE M1-FILE-CONTENTS-P-CORRECTNESS-1))
 (64 32 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE))
 (60 60 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (54 54 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-17))
 (36 36 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-58))
 (34 34 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-3 . 1))
 (32 32 (:TYPE-PRESCRIPTION M1-DIRECTORY-FILE-P))
 (30 30 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (3 3 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-43))
 )
(LOFAT-MKDIR-REFINEMENT-LEMMA-8
 (36 2 (:DEFINITION FIND-D-E))
 (22 1 (:REWRITE HIFAT-ENTRY-COUNT-OF-LOFAT-TO-HIFAT-HELPER-OF-DELETE-D-E-LEMMA-3))
 (20 2 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (12 2 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (6 6 (:TYPE-PRESCRIPTION MAKE-D-E-LIST))
 (6 2 (:REWRITE D-E-LIST-P-WHEN-USEFUL-D-E-LIST-P))
 (4 4 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (3 3 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (3 3 (:REWRITE DEFAULT-CAR))
 (2 2 (:TYPE-PRESCRIPTION USEFUL-D-E-LIST-P))
 (2 2 (:TYPE-PRESCRIPTION D-E-P))
 (2 2 (:REWRITE USEFUL-D-E-LIST-P-OF-MAKE-D-E-LIST))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (2 1 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (2 1 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-PLACE-FILE-COINCIDENT-LEMMA-15))
 (1 1 (:TYPE-PRESCRIPTION D-E-DIRECTORY-P))
 (1 1 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 )
(LOFAT-PWRITE-REFINEMENT-LEMMA-28
 (16142 897 (:DEFINITION FIND-D-E))
 (13033 18 (:REWRITE LOFAT-TO-HIFAT-HELPER-AFTER-DELETE-AND-CLEAR-2-LEMMA-2))
 (11364 311 (:REWRITE NFIX-WHEN-ZP))
 (10563 24 (:DEFINITION MEMBER-INTERSECTP-EQUAL))
 (10486 93 (:REWRITE NOT-INTERSECTP-LIST-OF-LOFAT-TO-HIFAT-HELPER))
 (10221 39 (:DEFINITION FREE-INDEX-LISTP))
 (9413 18 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-DISJOINT-LEMMA-2))
 (9385 949 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (6463 42 (:REWRITE REMOVE-ASSOC-WHEN-ABSENT-1))
 (5751 106 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-LEMMA-1))
 (5596 914 (:REWRITE D-E-P-OF-CAR-WHEN-D-E-LIST-P))
 (5065 16 (:REWRITE LOFAT-TO-HIFAT-HELPER-OF-LOFAT-REMOVE-FILE-DISJOINT-LEMMA-1 . 1))
 (4813 106 (:REWRITE LOFAT-FIND-FILE-CORRECTNESS-LEMMA-2))
 (4767 25 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (4027 2159 (:REWRITE DEFAULT-CDR))
 (3984 24 (:REWRITE LOFAT-PREAD-REFINEMENT-LEMMA-1))
 (3975 287 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (3580 287 (:DEFINITION MEMBER-EQUAL))
 (3523 1934 (:REWRITE DEFAULT-+-2))
 (3234 174 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (3006 523 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (2672 32 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (2368 2131 (:REWRITE DEFAULT-CAR))
 (2327 1224 (:REWRITE DEFAULT-<-2))
 (2303 1934 (:REWRITE DEFAULT-+-1))
 (2160 96 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (2160 48 (:DEFINITION INTEGER-LISTP))
 (2130 2130 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (2096 56 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (2094 74 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-2))
 (1961 117 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (1908 1224 (:REWRITE DEFAULT-<-1))
 (1824 1824 (:TYPE-PRESCRIPTION D-E-FILENAME))
 (1801 31 (:LINEAR LEN-OF-EXPLODE-OF-M1-FILE-CONTENTS-FIX))
 (1763 116 (:REWRITE D-E-CC-UNDER-IFF . 3))
 (1691 101 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (1664 6 (:REWRITE HIFAT-NO-DUPS-P-OF-HIFAT-PLACE-FILE))
 (1624 14 (:DEFINITION DELETE-D-E))
 (1609 20 (:REWRITE EQUAL-OF-M1-FILE))
 (1535 653 (:REWRITE HIFAT-TO-LOFAT-INVERSION-LEMMA-17))
 (1522 148 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1517 1517 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-D-E-CC))
 (1386 42 (:REWRITE DELETE-D-E-CORRECTNESS-1))
 (1329 183 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (1159 163 (:DEFINITION ASSOC-EQUAL))
 (1092 34 (:REWRITE SUBSETP-OF-CONS))
 (1037 405 (:REWRITE D-E-CC-CONTENTS-OF-LOFAT-REMOVE-FILE-COINCIDENT-LEMMA-8))
 (976 4 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-188))
 (912 64 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (828 828 (:TYPE-PRESCRIPTION D-E-FILE-SIZE))
 (792 30 (:REWRITE ACL2-NUMBERP-OF-CAR-WHEN-ACL2-NUMBER-LISTP))
 (753 29 (:DEFINITION PUT-ASSOC-EQUAL))
 (624 48 (:REWRITE NAT-LISTP-OF-CDR-WHEN-NAT-LISTP))
 (616 14 (:DEFINITION REMOVE-ASSOC-EQUAL))
 (576 126 (:LINEAR D-E-FILE-SIZE-CORRECTNESS-1))
 (574 574 (:REWRITE SUBSETP-MEMBER . 2))
 (574 574 (:REWRITE SUBSETP-MEMBER . 1))
 (560 112 (:LINEAR NTH-WHEN-D-E-P))
 (558 99 (:REWRITE M1-FILE-CONTENTS-P-CORRECTNESS-1))
 (547 6 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-44))
 (480 48 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (469 241 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (466 34 (:REWRITE SUBSETP-CONS-2))
 (462 198 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (416 8 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (411 39 (:REWRITE NATP-OF-CAR-WHEN-NAT-LISTP))
 (393 30 (:REWRITE ACL2-NUMBER-LISTP-WHEN-RATIONAL-LISTP))
 (376 376 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (374 102 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-52))
 (366 198 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (330 2 (:REWRITE LOFAT-TO-HIFAT-INVERSION-LEMMA-11))
 (306 8 (:DEFINITION UPDATE-NTH))
 (300 50 (:REWRITE LOFAT-FS-P-OF-LOFAT-PLACE-FILE-LEMMA-1))
 (289 18 (:REWRITE LOFAT-REMOVE-FILE-CORRECTNESS-LEMMA-31))
 (282 94 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (282 94 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (240 2 (:LINEAR LEN-OF-FAT32-BUILD-INDEX-LIST-1 . 1))
 (226 101 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (224 224 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (224 112 (:REWRITE SET-EQUIV-ASYM))
 (199 199 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-64))
 (198 198 (:REWRITE SUBSETP-TRANS2))
 (198 198 (:REWRITE SUBSETP-TRANS))
 (194 194 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (192 192 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (192 64 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (188 188 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (181 101 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (180 2 (:REWRITE D-E-CC-OF-PLACE-CONTENTS-COINCIDENT-1))
 (177 59 (:REWRITE USEFUL-D-E-LIST-P-OF-CDR))
 (173 173 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-FIX))
 (172 86 (:REWRITE DEFAULT-*-2))
 (170 17 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (168 168 (:TYPE-PRESCRIPTION MEMBER-INTERSECTP-EQUAL))
 (168 168 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (168 168 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (168 168 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (160 64 (:REWRITE MEMBER-WHEN-ATOM))
 (154 46 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (150 50 (:REWRITE LOFAT-FS-P-OF-LOFAT-PLACE-FILE-LEMMA-2))
 (150 30 (:REWRITE RATIONAL-LISTP-WHEN-INTEGER-LISTP))
 (144 32 (:LINEAR HIFAT-ENTRY-COUNT-WHEN-HIFAT-SUBSETP))
 (144 24 (:REWRITE NATP-OF-CAAR-WHEN-FILE-TABLE-P))
 (144 24 (:REWRITE NATP-OF-CAAR-WHEN-FD-TABLE-P))
 (144 24 (:REWRITE NATP-OF-CAAR-WHEN-DIR-STREAM-TABLE-P))
 (141 141 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (140 2 (:DEFINITION CEILING))
 (132 3 (:DEFINITION PLACE-D-E))
 (131 47 (:REWRITE NTH-WHEN-D-E-P . 2))
 (123 30 (:REWRITE RATIONAL-LISTP-WHEN-NOT-CONSP))
 (123 30 (:REWRITE ACL2-NUMBER-LISTP-WHEN-NOT-CONSP))
 (117 117 (:REWRITE NON-FREE-INDEX-LIST-LISTP-CORRECTNESS-1))
 (112 112 (:TYPE-PRESCRIPTION SET-EQUIV))
 (112 112 (:REWRITE SUBSETP-OF-CDR))
 (112 112 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (112 16 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (102 34 (:TYPE-PRESCRIPTION MAKE-CLUSTERS-OF-NIL))
 (102 24 (:REWRITE M1-FILE->CONTENTS-OF-M1-FILE))
 (101 101 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (101 101 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (96 96 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (96 48 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (86 86 (:REWRITE DEFAULT-*-1))
 (81 81 (:LINEAR POSITION-WHEN-MEMBER))
 (81 81 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (80 80 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-121 . 2))
 (80 80 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-121 . 1))
 (74 1 (:REWRITE LEN-UPDATE-NTH))
 (73 33 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (72 24 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-61))
 (72 8 (:REWRITE CONSP-OF-FAT32-BUILD-INDEX-LIST))
 (64 64 (:REWRITE SUBSETP-MEMBER . 4))
 (64 64 (:REWRITE SUBSETP-MEMBER . 3))
 (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 (:TYPE-PRESCRIPTION HIFAT-PLACE-FILE-OF-APPEND-LEMMA-1))
 (60 60 (:REWRITE INTEGER-LISTP-OF-D-E-CC))
 (60 2 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
 (57 57 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (56 56 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-D-E-FIX))
 (56 56 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (56 56 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (56 56 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-46))
 (56 56 (:REWRITE FREE-INDEX-LIST-LISTP-CORRECTNESS-1))
 (56 56 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-47))
 (56 56 (:LINEAR LOFAT-PLACE-FILE-CORRECTNESS-1-LEMMA-44))
 (54 54 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (54 54 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (48 48 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (48 48 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (48 48 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (48 24 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-93))
 (48 15 (:REWRITE LOFAT-PLACE-FILE-HELPER-CORRECTNESS-1))
 (45 15 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-D-E-CC))
 (45 9 (:LINEAR LEN-OF-D-E-LIST-FROM-FIRST-CLUSTER-WHEN-SUBDIR-CONTENTS-P . 2))
 (42 42 (:TYPE-PRESCRIPTION DELETE-D-E))
 (42 42 (:REWRITE FIND-D-E-CORRECTNESS-1))
 (40 24 (:REWRITE NTH-WHEN-D-E-P . 3))
 (38 2 (:REWRITE DEFAULT-UNARY-/))
 (34 34 (:TYPE-PRESCRIPTION MAKE-CLUSTERS))
 (32 32 (:TYPE-PRESCRIPTION M1-FILE->D-E$INLINE))
 (32 16 (:REWRITE DEFAULT-UNARY-MINUS))
 (28 28 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (27 9 (:LINEAR LENGTH-OF-D-E-CC-CONTENTS . 1))
 (24 24 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (24 24 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (24 24 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (24 8 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (24 3 (:REWRITE D-E-LIST-FIX-WHEN-D-E-LIST-P))
 (23 23 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (22 22 (:TYPE-PRESCRIPTION ATOM))
 (22 10 (:LINEAR HIFAT-TO-LOFAT-INVERSION-LEMMA-19))
 (20 20 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (18 18 (:TYPE-PRESCRIPTION SUBDIR-CONTENTS-P))
 (18 18 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-6))
 (18 18 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (18 18 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-4))
 (17 17 (:TYPE-PRESCRIPTION M1-DIRECTORY-FILE-P))
 (17 17 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (16 16 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (13 9 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-40))
 (13 4 (:REWRITE NATP-OF-PLACE-CONTENTS))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FAT32-BUILD-INDEX-LIST))
 (12 12 (:REWRITE M1-FILE-P-OF-M1-FILE-HIFAT-FILE-ALIST-FIX))
 (12 12 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-LEMMA-47))
 (12 12 (:REWRITE LOFAT-PLACE-FILE-CORRECTNESS-1-LEMMA-44))
 (10 10 (:TYPE-PRESCRIPTION NONNEGATIVE-INTEGER-QUOTIENT))
 (8 2 (:LINEAR NATP-OF-CLUSTER-SIZE))
 (7 1 (:DEFINITION MAX))
 (6 6 (:TYPE-PRESCRIPTION LENGTH))
 (6 6 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-1))
 (6 5 (:REWRITE LOFAT-MKDIR-REFINEMENT-LEMMA-7))
 (4 4 (:TYPE-PRESCRIPTION LOFAT-TO-HIFAT-CORRECTNESS-1 . 1))
 (4 2 (:REWRITE DEFAULT-NUMERATOR))
 (4 2 (:REWRITE DEFAULT-DENOMINATOR))
 (4 2 (:REWRITE D-E-CC-OF-PLACE-CONTENTS-COINCIDENT-2))
 (4 2 (:DEFINITION IFIX))
 (3 3 (:REWRITE D-E-P-OF-SET-FIRST-CLUSTER-FILE-SIZE))
 (2 2 (:REWRITE LOFAT-TO-HIFAT-CORRECTNESS-1))
 (2 2 (:REWRITE LOFAT-REMOVE-FILE-CORRECTNESS-LEMMA-15))
 (2 2 (:REWRITE HIFAT-NO-DUPS-P-OF-LOFAT-TO-HIFAT))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )