(HIFAT-ENTRY-COUNT
 (3010 13 (:DEFINITION ACL2-COUNT))
 (1704 10 (:REWRITE RATIONALP-OF-CAR-WHEN-RATIONAL-LISTP))
 (1623 10 (:REWRITE RATIONAL-LISTP-WHEN-INTEGER-LISTP))
 (1526 26 (:DEFINITION INTEGER-LISTP))
 (1482 63 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (1375 5 (:DEFINITION RATIONAL-LISTP))
 (804 103 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (755 40 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (624 52 (:REWRITE NAT-LISTP-OF-CDR-WHEN-NAT-LISTP))
 (411 35 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (317 65 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (263 89 (:REWRITE DEFAULT-+-2))
 (220 10 (:REWRITE LENGTH-WHEN-STRINGP))
 (182 182 (:REWRITE DEFAULT-CAR))
 (161 89 (:REWRITE DEFAULT-+-1))
 (160 20 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (147 147 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (147 147 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (144 114 (:REWRITE DEFAULT-CDR))
 (126 3 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (110 10 (:DEFINITION LEN))
 (103 103 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (103 103 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (103 103 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (100 20 (:REWRITE COMMUTATIVITY-OF-+))
 (92 4 (:DEFINITION MEMBER-EQUAL))
 (87 6 (:REWRITE SUBSETP-CAR-MEMBER))
 (85 23 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (80 20 (:DEFINITION INTEGER-ABS))
 (74 10 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (63 63 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (51 6 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (48 8 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (45 6 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (40 40 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (36 3 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (30 30 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (30 20 (:REWRITE STR::CONSP-OF-EXPLODE))
 (24 4 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (23 23 (:REWRITE FOLD-CONSTS-IN-+))
 (23 21 (:REWRITE DEFAULT-<-2))
 (23 21 (:REWRITE DEFAULT-<-1))
 (20 20 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (20 20 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (20 20 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (20 20 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (20 20 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (20 20 (:REWRITE DEFAULT-UNARY-MINUS))
 (20 10 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (18 3 (:DEFINITION ASSOC-EQUAL))
 (17 1 (:LINEAR ACL2-COUNT-OF-M1-FILE->CONTENTS . 1))
 (16 16 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (13 1 (:REWRITE ACL2-COUNT-WHEN-MEMBER))
 (12 6 (:REWRITE SET-EQUIV-ASYM))
 (12 6 (:REWRITE RATIONAL-LISTP-OF-CDR-WHEN-RATIONAL-LISTP))
 (12 4 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (12 4 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (10 10 (:REWRITE RATIONAL-LISTP-WHEN-NOT-CONSP))
 (10 10 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (10 10 (:REWRITE DEFAULT-REALPART))
 (10 10 (:REWRITE DEFAULT-NUMERATOR))
 (10 10 (:REWRITE DEFAULT-IMAGPART))
 (10 10 (:REWRITE DEFAULT-DENOMINATOR))
 (8 8 (:REWRITE SUBSETP-TRANS2))
 (8 8 (:REWRITE SUBSETP-TRANS))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (8 8 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (8 8 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (6 6 (:TYPE-PRESCRIPTION SET-EQUIV))
 (6 6 (:REWRITE SUBSETP-OF-CDR))
 (6 6 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (6 3 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (4 4 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (3 3 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (3 3 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (3 3 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (3 3 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (3 3 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (3 3 (:LINEAR ACL2-COUNT-OF-CONSP-POSITIVE))
 (1 1 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (1 1 (:LINEAR ACL2-COUNT-CAR-CDR-LINEAR))
 )
(HIFAT-ENTRY-COUNT-OF-HIFAT-FILE-ALIST-FIX
 (1186 22 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (1126 287 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (982 152 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (966 85 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (694 82 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (554 14 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (481 69 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (433 392 (:REWRITE DEFAULT-CAR))
 (392 338 (:REWRITE DEFAULT-CDR))
 (378 378 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (368 14 (:DEFINITION MEMBER-EQUAL))
 (341 180 (:REWRITE DEFAULT-+-2))
 (340 20 (:REWRITE SUBSETP-CAR-MEMBER))
 (269 180 (:REWRITE DEFAULT-+-1))
 (265 265 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (247 247 (:REWRITE SUBSETP-TRANS2))
 (247 247 (:REWRITE SUBSETP-TRANS))
 (244 238 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (244 238 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (238 80 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (198 33 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (186 186 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (130 44 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (120 22 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (78 26 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (70 70 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (70 70 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (66 66 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (56 8 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (50 50 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (46 46 (:REWRITE FOLD-CONSTS-IN-+))
 (41 41 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (41 41 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (33 33 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (32 16 (:REWRITE SET-EQUIV-ASYM))
 (28 28 (:REWRITE SUBSETP-MEMBER . 2))
 (28 28 (:REWRITE SUBSETP-MEMBER . 1))
 (16 16 (:TYPE-PRESCRIPTION SET-EQUIV))
 (16 16 (:REWRITE SUBSETP-OF-CDR))
 (4 4 (:REWRITE CONS-CAR-CDR))
 )
(M1-FILE-ALIST-P-OF-REMOVE1-ASSOC-EQUAL
 (129 13 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (105 25 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (54 18 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (49 49 (:REWRITE DEFAULT-CAR))
 (36 6 (:DEFINITION ASSOC-EQUAL))
 (25 25 (:REWRITE SUBSETP-TRANS2))
 (25 25 (:REWRITE SUBSETP-TRANS))
 (22 22 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (22 22 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (22 22 (:REWRITE DEFAULT-CDR))
 (18 18 (:TYPE-PRESCRIPTION ZP))
 (18 18 (:TYPE-PRESCRIPTION LEN))
 (7 7 (:TYPE-PRESCRIPTION NULL))
 (7 7 (:DEFINITION NULL))
 (6 6 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (6 6 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (6 6 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 )
(HIFAT-ENTRY-COUNT-WHEN-HIFAT-NO-DUPS-P
 (25513 6315 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (21560 1138 (:REWRITE SUBSETP-CAR-MEMBER))
 (21392 564 (:DEFINITION MEMBER-EQUAL))
 (19729 410 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (16390 618 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (13225 1241 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (11694 1052 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (7734 281 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (4180 281 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (3755 1991 (:REWRITE DEFAULT-+-2))
 (3738 269 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (3558 3558 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (2905 1991 (:REWRITE DEFAULT-+-1))
 (2904 2904 (:REWRITE SUBSETP-TRANS2))
 (2904 2904 (:REWRITE SUBSETP-TRANS))
 (2646 1323 (:REWRITE SET-EQUIV-ASYM))
 (1997 1955 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1997 1955 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1614 538 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (1375 559 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (1323 1323 (:TYPE-PRESCRIPTION SET-EQUIV))
 (1323 1323 (:REWRITE SUBSETP-OF-CDR))
 (1226 246 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (1128 1128 (:REWRITE SUBSETP-MEMBER . 2))
 (1128 1128 (:REWRITE SUBSETP-MEMBER . 1))
 (1004 64 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (908 344 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (809 211 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-29))
 (756 286 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (611 611 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (600 55 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE->CONTENTS-OF-HIFAT-FIND-FILE-LEMMA-1))
 (597 597 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (510 360 (:REWRITE SUBSETP-MEMBER . 3))
 (490 98 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (484 484 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (360 360 (:REWRITE SUBSETP-MEMBER . 4))
 (360 360 (:REWRITE INTERSECTP-MEMBER . 3))
 (360 360 (:REWRITE INTERSECTP-MEMBER . 2))
 (356 356 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (350 350 (:REWRITE MEMBER-WHEN-ATOM))
 (296 24 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE-FIX))
 (228 228 (:TYPE-PRESCRIPTION HIFAT-FILE-ALIST-FIX))
 (201 201 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (176 16 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (162 54 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (161 161 (:TYPE-PRESCRIPTION NULL))
 (161 161 (:DEFINITION NULL))
 (144 24 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (120 10 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (96 16 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (96 8 (:REWRITE HIFAT-SUBSETP-OF-REMOVE1-ASSOC-1))
 (72 72 (:TYPE-PRESCRIPTION HIFAT-SUBSETP))
 (48 48 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (32 32 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (32 32 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (32 32 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (31 31 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (31 31 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (24 24 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (24 24 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (16 16 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (8 8 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 )
(HIFAT-ENTRY-COUNT-OF-CDR-1
 (8959 2119 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (8504 328 (:REWRITE SUBSETP-CAR-MEMBER))
 (6464 264 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (5804 531 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (5544 77 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (2042 195 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (1004 502 (:REWRITE SET-EQUIV-ASYM))
 (907 66 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (902 496 (:REWRITE DEFAULT-+-2))
 (780 780 (:REWRITE SUBSETP-TRANS2))
 (780 780 (:REWRITE SUBSETP-TRANS))
 (714 714 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (709 496 (:REWRITE DEFAULT-+-1))
 (531 510 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (531 510 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (502 502 (:TYPE-PRESCRIPTION SET-EQUIV))
 (502 502 (:REWRITE SUBSETP-OF-CDR))
 (399 133 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (338 338 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (312 312 (:REWRITE SUBSETP-MEMBER . 2))
 (312 312 (:REWRITE SUBSETP-MEMBER . 1))
 (182 182 (:REWRITE SUBSETP-MEMBER . 4))
 (182 182 (:REWRITE INTERSECTP-MEMBER . 3))
 (182 182 (:REWRITE INTERSECTP-MEMBER . 2))
 (153 153 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (134 134 (:REWRITE FOLD-CONSTS-IN-+))
 (132 51 (:REWRITE DEFAULT-<-2))
 (120 40 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (114 114 (:TYPE-PRESCRIPTION HIFAT-FILE-ALIST-FIX))
 (110 38 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (102 102 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (102 102 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (89 51 (:REWRITE DEFAULT-<-1))
 (22 4 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (12 2 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (8 4 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (5 5 (:REWRITE SUBSETP-NIL))
 (5 5 (:REWRITE SET-EQUIV-OF-NIL))
 (4 4 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-ENTRY-COUNT-OF-CDR-2
 (743 181 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (740 38 (:REWRITE SUBSETP-CAR-MEMBER))
 (730 18 (:DEFINITION MEMBER-EQUAL))
 (624 28 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (436 8 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (434 40 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (140 12 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (100 50 (:REWRITE SET-EQUIV-ASYM))
 (72 12 (:DEFINITION ASSOC-EQUAL))
 (53 53 (:REWRITE SUBSETP-TRANS2))
 (53 53 (:REWRITE SUBSETP-TRANS))
 (52 22 (:REWRITE SUBSETP-MEMBER . 3))
 (50 50 (:TYPE-PRESCRIPTION SET-EQUIV))
 (50 50 (:REWRITE SUBSETP-OF-CDR))
 (49 8 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (46 12 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (36 36 (:REWRITE SUBSETP-MEMBER . 2))
 (36 36 (:REWRITE SUBSETP-MEMBER . 1))
 (34 34 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (34 34 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (24 24 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (24 12 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (24 3 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (22 22 (:REWRITE SUBSETP-MEMBER . 4))
 (22 22 (:REWRITE INTERSECTP-MEMBER . 3))
 (22 22 (:REWRITE INTERSECTP-MEMBER . 2))
 (21 11 (:REWRITE DEFAULT-+-2))
 (20 20 (:REWRITE MEMBER-WHEN-ATOM))
 (18 6 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (17 11 (:REWRITE DEFAULT-+-1))
 (12 12 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (11 11 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (11 11 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (9 2 (:REWRITE DEFAULT-<-2))
 (5 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(INDUCTION-SCHEME
 (11533 27 (:REWRITE RATIONALP-OF-CAR-WHEN-RATIONAL-LISTP))
 (11194 40 (:REWRITE RATIONAL-LISTP-WHEN-INTEGER-LISTP))
 (10620 116 (:DEFINITION INTEGER-LISTP))
 (10557 296 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (9051 19 (:DEFINITION RATIONAL-LISTP))
 (7109 266 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (5924 607 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (5419 420 (:REWRITE NAT-LISTP-OF-CDR-WHEN-NAT-LISTP))
 (4635 34 (:REWRITE RATIONAL-LISTP-OF-CDR-WHEN-RATIONAL-LISTP))
 (3958 1350 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (3468 6 (:DEFINITION INDUCTION-SCHEME))
 (3439 614 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (3049 607 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (2741 199 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (2414 52 (:REWRITE SUBSETP-CAR-MEMBER))
 (2298 150 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (1954 26 (:DEFINITION MEMBER-EQUAL))
 (1603 1603 (:REWRITE DEFAULT-CAR))
 (1456 1423 (:REWRITE DEFAULT-CDR))
 (960 10 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (957 957 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (957 957 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (804 6 (:REWRITE MEMBER-OF-REMOVE1-ASSOC))
 (607 607 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (607 607 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (607 607 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (606 606 (:REWRITE SUBSETP-TRANS2))
 (606 606 (:REWRITE SUBSETP-TRANS))
 (565 565 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (565 565 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (512 50 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (414 8 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (339 27 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (322 108 (:REWRITE DEFAULT-+-2))
 (299 28 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-29))
 (296 296 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (244 54 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (213 27 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (200 108 (:REWRITE DEFAULT-+-1))
 (194 15 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (149 11 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (140 140 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (121 11 (:DEFINITION LEN))
 (115 21 (:DEFINITION ASSOC-EQUAL))
 (112 46 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (105 14 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (104 14 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (94 7 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (80 20 (:DEFINITION INTEGER-ABS))
 (79 79 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (58 58 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (52 52 (:REWRITE SUBSETP-MEMBER . 2))
 (52 52 (:REWRITE SUBSETP-MEMBER . 1))
 (52 7 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (46 46 (:TYPE-PRESCRIPTION NULL))
 (46 46 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (46 46 (:DEFINITION NULL))
 (40 40 (:REWRITE RATIONAL-LISTP-WHEN-NOT-CONSP))
 (37 10 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (34 34 (:REWRITE SUBSETP-MEMBER . 4))
 (34 34 (:REWRITE SUBSETP-MEMBER . 3))
 (34 34 (:REWRITE MEMBER-WHEN-ATOM))
 (34 34 (:REWRITE INTERSECTP-MEMBER . 3))
 (34 34 (:REWRITE INTERSECTP-MEMBER . 2))
 (33 33 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (33 22 (:REWRITE STR::CONSP-OF-EXPLODE))
 (29 29 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (28 28 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (28 28 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (26 21 (:REWRITE DEFAULT-<-2))
 (23 21 (:REWRITE DEFAULT-<-1))
 (22 22 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (22 22 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (20 20 (:REWRITE DEFAULT-UNARY-MINUS))
 (18 18 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (18 6 (:REWRITE ASSOC-OF-REMOVE1-ASSOC))
 (14 14 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (12 12 (:REWRITE ASSOC-AFTER-REMOVE1-ASSOC))
 (12 8 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (11 11 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (10 10 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (10 10 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (10 10 (:REWRITE DEFAULT-REALPART))
 (10 10 (:REWRITE DEFAULT-NUMERATOR))
 (10 10 (:REWRITE DEFAULT-IMAGPART))
 (10 10 (:REWRITE DEFAULT-DENOMINATOR))
 (10 10 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (9 9 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (8 8 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (8 4 (:REWRITE SET-EQUIV-ASYM))
 (4 4 (:TYPE-PRESCRIPTION SET-EQUIV))
 (4 4 (:REWRITE SUBSETP-OF-CDR))
 (4 4 (:LINEAR ACL2-COUNT-OF-CONSP-POSITIVE))
 (3 3 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (3 3 (:LINEAR ACL2-COUNT-CAR-CDR-LINEAR))
 (3 1 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (2 2 (:TYPE-PRESCRIPTION HIFAT-SUBSETP))
 (2 2 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (1 1 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (1 1 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 )
(INDUCTION-SCHEME-CORRECTNESS
 (18767 3850 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (16489 498 (:REWRITE SUBSETP-CAR-MEMBER))
 (14763 237 (:DEFINITION MEMBER-EQUAL))
 (11127 768 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (9492 417 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (8217 110 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (6092 281 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (6088 215 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-29))
 (4198 35 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (3646 138 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (3600 99 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (3228 3228 (:REWRITE SUBSETP-TRANS2))
 (3228 3228 (:REWRITE SUBSETP-TRANS))
 (2844 2844 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2844 2844 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2814 21 (:REWRITE MEMBER-OF-REMOVE1-ASSOC))
 (2058 98 (:REWRITE M1-FILE-ALIST-P-OF-REMOVE1-ASSOC-EQUAL))
 (1845 221 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (1398 1224 (:REWRITE DEFAULT-CDR))
 (1186 1186 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (1029 57 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (843 15 (:REWRITE ASSOC-OF-REMOVE1-ASSOC))
 (675 225 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (651 123 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (490 62 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (488 244 (:REWRITE SET-EQUIV-ASYM))
 (482 482 (:REWRITE SUBSETP-MEMBER . 2))
 (336 112 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (281 281 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (244 244 (:TYPE-PRESCRIPTION SET-EQUIV))
 (244 244 (:REWRITE SUBSETP-OF-CDR))
 (236 236 (:REWRITE SUBSETP-MEMBER . 4))
 (236 236 (:REWRITE INTERSECTP-MEMBER . 3))
 (236 236 (:REWRITE INTERSECTP-MEMBER . 2))
 (236 124 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (220 220 (:REWRITE MEMBER-WHEN-ATOM))
 (170 58 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (153 29 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (132 22 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (132 12 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (126 126 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (72 48 (:REWRITE ASSOC-AFTER-REMOVE1-ASSOC))
 (72 12 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (71 71 (:TYPE-PRESCRIPTION NULL))
 (71 71 (:DEFINITION NULL))
 (44 44 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (44 44 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (24 24 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (24 24 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (24 24 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (22 22 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (12 12 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (6 1 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-3))
 (6 1 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE->CONTENTS-OF-HIFAT-FIND-FILE-LEMMA-1))
 )
(HIFAT-ENTRY-COUNT-WHEN-HIFAT-SUBSETP
 (19516 4416 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (16077 664 (:REWRITE SUBSETP-CAR-MEMBER))
 (14637 312 (:DEFINITION MEMBER-EQUAL))
 (13710 232 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (9639 743 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (6621 408 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (3012 3012 (:REWRITE SUBSETP-TRANS2))
 (3012 3012 (:REWRITE SUBSETP-TRANS))
 (2563 2563 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2563 2563 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1931 49 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (1718 98 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (1488 1488 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (1464 251 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (1133 607 (:REWRITE DEFAULT-+-2))
 (1086 543 (:REWRITE SET-EQUIV-ASYM))
 (1082 90 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (1028 78 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (902 607 (:REWRITE DEFAULT-+-1))
 (810 270 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (632 632 (:REWRITE SUBSETP-MEMBER . 2))
 (564 564 (:REWRITE SUBSETP-OF-CDR))
 (543 543 (:TYPE-PRESCRIPTION SET-EQUIV))
 (525 42 (:DEFINITION ALISTP))
 (412 102 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (402 3 (:REWRITE MEMBER-OF-REMOVE1-ASSOC))
 (336 84 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (322 116 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (267 267 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (209 209 (:REWRITE SUBSETP-MEMBER . 4))
 (209 209 (:REWRITE INTERSECTP-MEMBER . 3))
 (209 209 (:REWRITE INTERSECTP-MEMBER . 2))
 (198 198 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (190 190 (:REWRITE MEMBER-WHEN-ATOM))
 (168 168 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (145 145 (:REWRITE FOLD-CONSTS-IN-+))
 (91 3 (:REWRITE ASSOC-OF-REMOVE1-ASSOC))
 (84 84 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (57 24 (:REWRITE DEFAULT-<-2))
 (46 24 (:REWRITE DEFAULT-<-1))
 (43 43 (:TYPE-PRESCRIPTION NULL))
 (43 43 (:DEFINITION NULL))
 (12 12 (:REWRITE ASSOC-AFTER-REMOVE1-ASSOC))
 )
(HIFAT-ENTRY-COUNT-WHEN-HIFAT-EQUIV
 (24 8 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (16 4 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (4 2 (:REWRITE DEFAULT-<-2))
 (4 2 (:REWRITE DEFAULT-<-1))
 )
(HIFAT-ENTRY-COUNT-OF-REMOVE-ASSOC-EQUAL
 (6534 176 (:DEFINITION MEMBER-EQUAL))
 (6513 353 (:REWRITE SUBSETP-CAR-MEMBER))
 (6251 1550 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (6105 119 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (4228 28 (:LINEAR HIFAT-ENTRY-COUNT-WHEN-HIFAT-SUBSETP))
 (3185 277 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (2048 132 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (1395 174 (:REWRITE M1-FILE-ALIST-P-OF-REMOVE-ASSOC-EQUAL))
 (1144 64 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (795 34 (:REWRITE CONSP-OF-REMOVE-ASSOC-1))
 (744 372 (:REWRITE SET-EQUIV-ASYM))
 (737 401 (:REWRITE DEFAULT-+-2))
 (596 596 (:REWRITE SUBSETP-TRANS2))
 (596 596 (:REWRITE SUBSETP-TRANS))
 (578 401 (:REWRITE DEFAULT-+-1))
 (570 570 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (380 332 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (380 332 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (380 220 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (372 372 (:TYPE-PRESCRIPTION SET-EQUIV))
 (372 372 (:REWRITE SUBSETP-OF-CDR))
 (352 352 (:REWRITE SUBSETP-MEMBER . 2))
 (352 352 (:REWRITE SUBSETP-MEMBER . 1))
 (321 107 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (235 235 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (232 232 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (227 25 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (172 58 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (141 58 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (121 121 (:REWRITE SUBSETP-MEMBER . 4))
 (121 121 (:REWRITE INTERSECTP-MEMBER . 3))
 (121 121 (:REWRITE INTERSECTP-MEMBER . 2))
 (120 120 (:REWRITE MEMBER-WHEN-ATOM))
 (100 100 (:REWRITE FOLD-CONSTS-IN-+))
 (44 20 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (42 42 (:TYPE-PRESCRIPTION HIFAT-SUBSETP))
 (31 11 (:REWRITE DEFAULT-<-1))
 (24 2 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (23 11 (:REWRITE DEFAULT-<-2))
 (20 20 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (5 1 (:LINEAR HIFAT-ENTRY-COUNT-OF-CDR-2))
 (2 2 (:REWRITE M1-FILE-ALIST-P-OF-HIFAT-FILE-ALIST-FIX))
 )
(HIFAT-ENTRY-COUNT-OF-PUT-ASSOC-EQUAL-LEMMA-1
 (505 433 (:REWRITE DEFAULT-CDR))
 (423 417 (:REWRITE DEFAULT-CAR))
 (376 82 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (295 82 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (242 22 (:DEFINITION LEN))
 (232 38 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (190 38 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (174 12 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (142 142 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (134 134 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (112 6 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (92 92 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (89 24 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (80 16 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (72 44 (:REWRITE DEFAULT-<-1))
 (71 71 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (66 66 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (66 44 (:REWRITE STR::CONSP-OF-EXPLODE))
 (62 62 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (44 44 (:REWRITE DEFAULT-<-2))
 (44 22 (:REWRITE DEFAULT-+-2))
 (38 38 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (38 38 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (38 38 (:REWRITE SUBSETP-TRANS2))
 (38 38 (:REWRITE SUBSETP-TRANS))
 (32 32 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (32 32 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (26 26 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (23 11 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (22 22 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (22 22 (:REWRITE DEFAULT-+-1))
 (13 13 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (11 11 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (4 4 (:TYPE-PRESCRIPTION HIFAT-SUBSETP))
 (2 2 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (2 2 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (2 2 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 )
(CONSP-OF-ASSOC-OF-HIFAT-FILE-ALIST-FIX
 (1086 48 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (736 48 (:DEFINITION MEMBER-EQUAL))
 (615 607 (:REWRITE DEFAULT-CAR))
 (577 113 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (395 392 (:REWRITE DEFAULT-CDR))
 (373 68 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (356 356 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (270 10 (:REWRITE SUBSETP-CAR-MEMBER))
 (258 43 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (243 50 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (240 240 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (183 56 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (174 58 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (165 55 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (154 154 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (153 53 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (151 47 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (133 46 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (133 46 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (96 96 (:REWRITE SUBSETP-MEMBER . 2))
 (96 96 (:REWRITE SUBSETP-MEMBER . 1))
 (91 91 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (90 90 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (86 86 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (80 5 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (72 25 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (72 10 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (68 68 (:REWRITE SUBSETP-TRANS2))
 (68 68 (:REWRITE SUBSETP-TRANS))
 (45 45 (:REWRITE CONS-CAR-CDR))
 (43 43 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (25 25 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (6 2 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (6 2 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (1 1 (:REWRITE-QUOTED-CONSTANT M1-FILE-FIX-UNDER-M1-FILE-EQUIV))
 )
(HIFAT-ENTRY-COUNT-OF-PUT-ASSOC-EQUAL
 (77312 234 (:LINEAR HIFAT-ENTRY-COUNT-WHEN-HIFAT-SUBSETP))
 (60561 15783 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (51048 1356 (:DEFINITION MEMBER-EQUAL))
 (49434 2724 (:REWRITE SUBSETP-CAR-MEMBER))
 (45988 908 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (26937 908 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (26418 2342 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (26278 3044 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (20982 102 (:REWRITE HIFAT-NO-DUPS-P-OF-PUT-ASSOC))
 (19622 2037 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (12534 586 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (8500 4425 (:REWRITE DEFAULT-+-2))
 (7870 7870 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (7495 7495 (:REWRITE SUBSETP-TRANS2))
 (7495 7495 (:REWRITE SUBSETP-TRANS))
 (6949 646 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (6660 4425 (:REWRITE DEFAULT-+-1))
 (6444 3222 (:REWRITE SET-EQUIV-ASYM))
 (4198 3908 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (3916 3908 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (3228 1076 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (3222 3222 (:TYPE-PRESCRIPTION SET-EQUIV))
 (3222 3222 (:REWRITE SUBSETP-OF-CDR))
 (2712 2712 (:REWRITE SUBSETP-MEMBER . 2))
 (2712 2712 (:REWRITE SUBSETP-MEMBER . 1))
 (2165 1015 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (1542 1542 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (1526 1526 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (1512 126 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (1377 478 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (1293 1293 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (1226 920 (:REWRITE MEMBER-WHEN-ATOM))
 (1112 932 (:REWRITE SUBSETP-MEMBER . 3))
 (985 437 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (970 970 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (932 932 (:REWRITE SUBSETP-MEMBER . 4))
 (932 932 (:REWRITE INTERSECTP-MEMBER . 3))
 (932 932 (:REWRITE INTERSECTP-MEMBER . 2))
 (584 44 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE->CONTENTS-OF-HIFAT-FIND-FILE-LEMMA-1))
 (504 42 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (120 120 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (120 120 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (112 14 (:LINEAR HIFAT-ENTRY-COUNT-OF-CDR-2))
 (40 40 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-3))
 (40 40 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-1))
 (34 17 (:REWRITE DEFAULT-UNARY-MINUS))
 (12 12 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (12 12 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (2 2 (:REWRITE SUBSETP-NIL))
 (2 2 (:REWRITE SET-EQUIV-OF-NIL))
 )
(HIFAT-ENTRY-COUNT-OF-HIFAT-REMOVE-FILE
 (478 7 (:DEFINITION REMOVE-ASSOC-EQUAL))
 (426 49 (:DEFINITION ASSOC-EQUAL))
 (415 21 (:REWRITE REMOVE-ASSOC-WHEN-ABSENT-1))
 (335 335 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (220 20 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (206 206 (:REWRITE DEFAULT-CAR))
 (192 6 (:DEFINITION PUT-ASSOC-EQUAL))
 (167 23 (:REWRITE HIFAT-ENTRY-COUNT-OF-PUT-ASSOC-EQUAL-LEMMA-1))
 (152 8 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (124 124 (:REWRITE DEFAULT-CDR))
 (120 120 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (120 20 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (116 20 (:LINEAR HIFAT-ENTRY-COUNT-WHEN-HIFAT-SUBSETP))
 (54 9 (:REWRITE CONSP-OF-ASSOC-OF-HIFAT-FILE-ALIST-FIX))
 (40 40 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (40 8 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (40 8 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (36 36 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (36 6 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (29 29 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (26 26 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (25 25 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (24 8 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (23 23 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (20 20 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (13 13 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (11 5 (:REWRITE DEFAULT-<-1))
 (10 5 (:REWRITE DEFAULT-<-2))
 (8 8 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (8 4 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (4 2 (:REWRITE DEFAULT-+-2))
 (3 2 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(HIFAT-ENTRY-COUNT-OF-HIFAT-PLACE-FILE
 (20744 678 (:DEFINITION PUT-ASSOC-EQUAL))
 (16850 1178 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (11314 11314 (:REWRITE DEFAULT-CAR))
 (10752 10752 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (9869 955 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (8885 8885 (:REWRITE DEFAULT-CDR))
 (7928 156 (:REWRITE EQUAL-OF-M1-FILE))
 (7491 247 (:REWRITE HIFAT-ENTRY-COUNT-OF-PUT-ASSOC-EQUAL-LEMMA-1))
 (6852 6852 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (5910 751 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (3011 2966 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (2896 112 (:LINEAR HIFAT-ENTRY-COUNT-WHEN-HIFAT-SUBSETP))
 (2402 32 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (1970 1970 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (1616 16 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (1483 1483 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (1404 234 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (1233 1233 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (1161 591 (:REWRITE DEFAULT-<-2))
 (985 985 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (925 925 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (743 317 (:REWRITE DEFAULT-+-2))
 (726 726 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (726 726 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-4))
 (592 591 (:REWRITE DEFAULT-<-1))
 (554 317 (:REWRITE DEFAULT-+-1))
 (468 156 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (360 180 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (301 301 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (273 273 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (247 247 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (156 156 (:TYPE-PRESCRIPTION D-E-P))
 (156 156 (:REWRITE D-E-P-OF-M1-FILE->D-E))
 (136 68 (:REWRITE DEFAULT-UNARY-MINUS))
 (123 13 (:REWRITE CONSP-OF-ASSOC-OF-HIFAT-FILE-ALIST-FIX))
 (102 6 (:REWRITE ABS-PLACE-FILE-HELPER-OF-CTX-APP-LEMMA-1))
 (94 94 (:REWRITE FOLD-CONSTS-IN-+))
 (80 8 (:REWRITE M1-FILE-ALIST-P-OF-PUT-ASSOC))
 (67 13 (:DEFINITION LEN))
 (60 12 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (60 12 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (56 8 (:REWRITE HIFAT-NO-DUPS-P-OF-PUT-ASSOC))
 (36 36 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (32 32 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (30 30 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (27 9 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (27 9 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (27 6 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (24 24 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (24 24 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (18 18 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (16 16 (:TYPE-PRESCRIPTION PUT-ASSOC-EQUAL))
 (15 15 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-PREFIXP))
 (10 10 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-3 . 1))
 (10 10 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE->CONTENTS-OF-HIFAT-FIND-FILE))
 (9 9 (:LINEAR POSITION-WHEN-MEMBER))
 (9 9 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 6 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-EQUIV$INLINE))
 (6 6 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (6 6 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (6 6 (:REWRITE SUBSETP-TRANS2))
 (6 6 (:REWRITE SUBSETP-TRANS))
 (6 6 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 (2 2 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-3))
 (2 2 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-1))
 )