(HIFAT-SUBSETP
 (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))
 (3515 1205 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (3049 607 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (2595 458 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (2298 150 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (2091 158 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (2022 6 (:DEFINITION HIFAT-SUBSETP))
 (1493 1493 (:REWRITE DEFAULT-CAR))
 (1476 30 (:REWRITE SUBSETP-CAR-MEMBER))
 (1388 1355 (:REWRITE DEFAULT-CDR))
 (1178 15 (:DEFINITION MEMBER-EQUAL))
 (957 957 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (957 957 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (867 9 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (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))
 (450 450 (:REWRITE SUBSETP-TRANS2))
 (450 450 (:REWRITE SUBSETP-TRANS))
 (431 431 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (431 431 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (322 108 (:REWRITE DEFAULT-+-2))
 (296 296 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (272 8 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (266 46 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (200 108 (:REWRITE DEFAULT-+-1))
 (188 14 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (149 11 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (132 132 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (121 11 (:DEFINITION LEN))
 (109 20 (:DEFINITION ASSOC-EQUAL))
 (104 42 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (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))
 (56 56 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (53 53 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (52 7 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (44 44 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (40 40 (:REWRITE RATIONAL-LISTP-WHEN-NOT-CONSP))
 (33 33 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (33 22 (:REWRITE STR::CONSP-OF-EXPLODE))
 (30 30 (:REWRITE SUBSETP-MEMBER . 2))
 (30 30 (:REWRITE SUBSETP-MEMBER . 1))
 (28 28 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (28 28 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (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))
 (21 6 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (20 20 (:REWRITE DEFAULT-UNARY-MINUS))
 (14 14 (:REWRITE SUBSETP-MEMBER . 4))
 (14 14 (:REWRITE SUBSETP-MEMBER . 3))
 (14 14 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (14 14 (:REWRITE MEMBER-WHEN-ATOM))
 (14 14 (:REWRITE INTERSECTP-MEMBER . 3))
 (14 14 (:REWRITE INTERSECTP-MEMBER . 2))
 (12 8 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (11 11 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (10 10 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (10 10 (:REWRITE DEFAULT-REALPART))
 (10 10 (:REWRITE DEFAULT-NUMERATOR))
 (10 10 (:REWRITE DEFAULT-IMAGPART))
 (10 10 (:REWRITE DEFAULT-DENOMINATOR))
 (9 9 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (8 8 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (8 4 (:REWRITE SET-EQUIV-ASYM))
 (5 5 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (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))
 )
(HIFAT-SUBSETP-OF-REMOVE1-ASSOC-1
 (12713 303 (:REWRITE SUBSETP-CAR-MEMBER))
 (11274 2031 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (11132 149 (:DEFINITION MEMBER-EQUAL))
 (8313 525 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (6796 67 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (4402 246 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (2138 17 (:REWRITE ASSOC-OF-REMOVE1-ASSOC))
 (2031 2031 (:REWRITE SUBSETP-TRANS2))
 (2031 2031 (:REWRITE SUBSETP-TRANS))
 (1995 95 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (1962 1962 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1962 1962 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (670 95 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (651 651 (:REWRITE DEFAULT-CDR))
 (632 632 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (475 161 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (301 301 (:REWRITE SUBSETP-MEMBER . 2))
 (288 36 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (261 87 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (169 169 (:REWRITE SUBSETP-MEMBER . 4))
 (169 169 (:REWRITE INTERSECTP-MEMBER . 3))
 (169 169 (:REWRITE INTERSECTP-MEMBER . 2))
 (164 164 (:REWRITE MEMBER-WHEN-ATOM))
 (144 72 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (67 67 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (53 53 (:TYPE-PRESCRIPTION NULL))
 (53 53 (:DEFINITION NULL))
 )
(HIFAT-NO-DUPS-P-OF-REMOVE1-ASSOC-EQUAL
 (3461 101 (:DEFINITION MEMBER-EQUAL))
 (3436 205 (:REWRITE SUBSETP-CAR-MEMBER))
 (3053 717 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (1756 38 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1719 152 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1645 61 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (1202 1202 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (798 266 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (793 82 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (710 38 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (464 232 (:REWRITE SET-EQUIV-ASYM))
 (433 433 (:REWRITE DEFAULT-CDR))
 (396 36 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (390 39 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (366 53 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (345 38 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (310 38 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (262 262 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (232 232 (:TYPE-PRESCRIPTION SET-EQUIV))
 (232 232 (:REWRITE SUBSETP-OF-CDR))
 (216 36 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (216 36 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (214 214 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (202 202 (:REWRITE SUBSETP-MEMBER . 2))
 (202 202 (:REWRITE SUBSETP-MEMBER . 1))
 (183 51 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (174 129 (:REWRITE SUBSETP-MEMBER . 3))
 (135 45 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (133 27 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (129 129 (:REWRITE SUBSETP-MEMBER . 4))
 (129 129 (:REWRITE INTERSECTP-MEMBER . 3))
 (129 129 (:REWRITE INTERSECTP-MEMBER . 2))
 (128 128 (:REWRITE SUBSETP-TRANS2))
 (128 128 (:REWRITE SUBSETP-TRANS))
 (126 126 (:REWRITE MEMBER-WHEN-ATOM))
 (125 125 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (125 125 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (123 123 (:TYPE-PRESCRIPTION M1-FILE-P))
 (113 39 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (111 37 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (107 107 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (96 16 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (74 74 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (72 72 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (72 72 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (72 72 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (72 72 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (72 72 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (72 4 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (51 51 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (36 36 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (36 36 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (36 4 (:REWRITE M1-FILE-FIX-WHEN-M1-FILE-P))
 (23 23 (:TYPE-PRESCRIPTION NULL))
 (23 23 (:DEFINITION NULL))
 (3 3 (:REWRITE SUBSETP-REFL))
 )
(HIFAT-SUBSETP-PRESERVES-ASSOC
 (4821 1607 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1152 51 (:REWRITE SUBSETP-CAR-MEMBER))
 (860 21 (:DEFINITION MEMBER-EQUAL))
 (813 153 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (753 64 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (671 11 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (336 21 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (278 22 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (194 22 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (168 168 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (166 42 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (153 153 (:REWRITE SUBSETP-TRANS2))
 (153 153 (:REWRITE SUBSETP-TRANS))
 (144 144 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (144 144 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (132 22 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (126 42 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (122 122 (:REWRITE DEFAULT-CDR))
 (120 20 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (112 112 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (92 92 (:TYPE-PRESCRIPTION M1-FILE-P))
 (84 28 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (84 14 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (84 14 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (84 14 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (56 56 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (48 48 (:REWRITE SUBSETP-MEMBER . 2))
 (44 44 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (44 44 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (44 44 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (44 44 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (31 31 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (29 29 (:REWRITE SUBSETP-MEMBER . 4))
 (29 29 (:REWRITE INTERSECTP-MEMBER . 3))
 (29 29 (:REWRITE INTERSECTP-MEMBER . 2))
 (28 28 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (28 28 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (20 20 (:REWRITE MEMBER-WHEN-ATOM))
 (14 14 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (14 14 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-SUBSETP-TRANSITIVE-LEMMA-1
 (6588 381 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (4316 858 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (3810 188 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (3800 166 (:REWRITE SUBSETP-CAR-MEMBER))
 (3234 81 (:DEFINITION MEMBER-EQUAL))
 (2044 36 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1391 573 (:REWRITE DEFAULT-CDR))
 (1264 81 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1112 1112 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (818 818 (:REWRITE SUBSETP-TRANS2))
 (818 818 (:REWRITE SUBSETP-TRANS))
 (802 802 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (802 802 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (773 265 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (571 170 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (270 90 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (236 48 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (165 165 (:REWRITE SUBSETP-MEMBER . 2))
 (94 94 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (94 94 (:REWRITE SUBSETP-MEMBER . 4))
 (94 94 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (94 94 (:REWRITE INTERSECTP-MEMBER . 3))
 (94 94 (:REWRITE INTERSECTP-MEMBER . 2))
 (94 94 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (90 90 (:REWRITE MEMBER-WHEN-ATOM))
 (79 79 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (32 16 (:REWRITE SET-EQUIV-ASYM))
 (16 16 (:TYPE-PRESCRIPTION SET-EQUIV))
 (16 16 (:REWRITE SUBSETP-OF-CDR))
 )
(HIFAT-SUBSETP-TRANSITIVE-LEMMA-2
 (2935 237 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (2569 516 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (2368 42 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (2214 51 (:DEFINITION MEMBER-EQUAL))
 (2154 521 (:REWRITE DEFAULT-CDR))
 (2116 105 (:REWRITE SUBSETP-CAR-MEMBER))
 (1154 56 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (1120 75 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (644 644 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (484 61 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (429 143 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (416 416 (:REWRITE SUBSETP-TRANS2))
 (416 416 (:REWRITE SUBSETP-TRANS))
 (378 378 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (378 378 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (180 60 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (130 30 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (104 104 (:REWRITE SUBSETP-MEMBER . 2))
 (90 9 (:DEFINITION ALISTP))
 (80 40 (:REWRITE SET-EQUIV-ASYM))
 (73 73 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (72 18 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (50 50 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (50 50 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (50 50 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (41 41 (:REWRITE SUBSETP-MEMBER . 4))
 (41 41 (:REWRITE INTERSECTP-MEMBER . 3))
 (41 41 (:REWRITE INTERSECTP-MEMBER . 2))
 (40 40 (:TYPE-PRESCRIPTION SET-EQUIV))
 (40 40 (:REWRITE SUBSETP-OF-CDR))
 (38 38 (:REWRITE MEMBER-WHEN-ATOM))
 (36 36 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (18 18 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (15 5 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (10 10 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 )
(HIFAT-SUBSETP-TRANSITIVE-LEMMA-3
 (20117 952 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (16371 420 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (15840 310 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (15009 3081 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (9948 160 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (9940 199 (:DEFINITION MEMBER-EQUAL))
 (9390 405 (:REWRITE SUBSETP-CAR-MEMBER))
 (5494 359 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (3377 157 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE-FIX))
 (2811 2811 (:REWRITE SUBSETP-TRANS2))
 (2811 2811 (:REWRITE SUBSETP-TRANS))
 (2544 2544 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2544 2544 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2268 2268 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (1344 448 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (669 223 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (403 403 (:REWRITE SUBSETP-MEMBER . 2))
 (314 314 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (294 44 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (230 230 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (216 108 (:REWRITE SET-EQUIV-ASYM))
 (163 163 (:REWRITE SUBSETP-MEMBER . 4))
 (163 163 (:REWRITE INTERSECTP-MEMBER . 3))
 (163 163 (:REWRITE INTERSECTP-MEMBER . 2))
 (157 157 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (156 156 (:REWRITE MEMBER-WHEN-ATOM))
 (108 108 (:TYPE-PRESCRIPTION SET-EQUIV))
 (108 108 (:REWRITE SUBSETP-OF-CDR))
 (90 15 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (90 15 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (80 80 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (80 80 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (80 80 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (50 5 (:DEFINITION ALISTP))
 (40 10 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (30 30 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (30 30 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (20 20 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (18 6 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (15 15 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (15 15 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (12 12 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (10 10 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-SUBSETP-TRANSITIVE-LEMMA-4
 (12 4 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (4 4 (:TYPE-PRESCRIPTION ZP))
 (4 4 (:TYPE-PRESCRIPTION LEN))
 )
(HIFAT-SUBSETP-TRANSITIVE-LEMMA-5
 (822 274 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (127 7 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (96 4 (:REWRITE SUBSETP-CAR-MEMBER))
 (80 16 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (80 2 (:DEFINITION MEMBER-EQUAL))
 (66 2 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (42 7 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (40 2 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-4))
 (39 7 (:DEFINITION ASSOC-EQUAL))
 (39 2 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (35 35 (:REWRITE DEFAULT-CAR))
 (32 2 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (24 1 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (16 16 (:REWRITE SUBSETP-TRANS2))
 (16 16 (:REWRITE SUBSETP-TRANS))
 (15 15 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (15 15 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (13 1 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (11 1 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (8 8 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (6 2 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (6 1 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (6 1 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (4 4 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 (3 3 (:TYPE-PRESCRIPTION M1-FILE-P))
 (3 3 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (3 1 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (2 2 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (2 2 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (2 2 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (2 2 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (1 1 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (1 1 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-SUBSETP-TRANSITIVE-LEMMA-6
 (9020 377 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (7884 1310 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (6988 488 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (3870 107 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (3145 3145 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (1298 1298 (:REWRITE SUBSETP-TRANS2))
 (1298 1298 (:REWRITE SUBSETP-TRANS))
 (1295 1295 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1295 1295 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (925 23 (:REWRITE SUBSETP-MEMBER . 3))
 (911 767 (:REWRITE DEFAULT-CDR))
 (686 683 (:REWRITE DEFAULT-CAR))
 (624 19 (:REWRITE SUBSETP-CAR-MEMBER))
 (517 47 (:DEFINITION LEN))
 (493 130 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (363 68 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (356 52 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (242 242 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (240 240 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (190 190 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (160 84 (:REWRITE DEFAULT-<-1))
 (141 141 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (141 94 (:REWRITE STR::CONSP-OF-EXPLODE))
 (130 130 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (121 121 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (116 116 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (104 104 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (104 104 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (96 16 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (94 47 (:REWRITE DEFAULT-+-2))
 (84 84 (:REWRITE DEFAULT-<-2))
 (65 65 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (51 3 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (47 47 (:REWRITE DEFAULT-+-1))
 (36 4 (:REWRITE FAT32-FILENAME-LIST-P-CORRECTNESS-1))
 (32 32 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (23 23 (:REWRITE SUBSETP-MEMBER . 4))
 (23 23 (:REWRITE SUBSETP-MEMBER . 2))
 (23 23 (:REWRITE SUBSETP-MEMBER . 1))
 (23 23 (:REWRITE MEMBER-WHEN-ATOM))
 (23 23 (:REWRITE INTERSECTP-MEMBER . 3))
 (23 23 (:REWRITE INTERSECTP-MEMBER . 2))
 (16 16 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (12 12 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (12 6 (:REWRITE SET-EQUIV-ASYM))
 (12 2 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (9 3 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (9 3 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (6 6 (:TYPE-PRESCRIPTION SET-EQUIV))
 (6 6 (:REWRITE SUBSETP-OF-CDR))
 (6 6 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (3 3 (:REWRITE SUBSETP-REFL))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER))
 (2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1 1 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 )
(HIFAT-SUBSETP-TRANSITIVE
 (7709 1558 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (6564 119 (:DEFINITION MEMBER-EQUAL))
 (6398 736 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (6335 241 (:REWRITE SUBSETP-CAR-MEMBER))
 (5242 262 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (5177 78 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (4116 1372 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (3805 3805 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (3591 158 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (3075 234 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1740 1740 (:REWRITE DEFAULT-CAR))
 (1533 1533 (:REWRITE SUBSETP-TRANS2))
 (1533 1533 (:REWRITE SUBSETP-TRANS))
 (1530 1530 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1530 1530 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1407 72 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (1375 52 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (1074 59 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (947 52 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (662 662 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (608 111 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (432 144 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (396 36 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (368 368 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (243 81 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (238 238 (:REWRITE SUBSETP-MEMBER . 2))
 (238 238 (:REWRITE SUBSETP-MEMBER . 1))
 (216 36 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (216 36 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (154 154 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (88 88 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (72 72 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (72 72 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (72 72 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (72 72 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (72 72 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (54 54 (:REWRITE SUBSETP-MEMBER . 4))
 (54 54 (:REWRITE SUBSETP-MEMBER . 3))
 (54 54 (:REWRITE MEMBER-WHEN-ATOM))
 (54 54 (:REWRITE INTERSECTP-MEMBER . 3))
 (54 54 (:REWRITE INTERSECTP-MEMBER . 2))
 (36 36 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (36 36 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (20 10 (:REWRITE SET-EQUIV-ASYM))
 (10 10 (:TYPE-PRESCRIPTION SET-EQUIV))
 (10 10 (:REWRITE SUBSETP-OF-CDR))
 (3 3 (:REWRITE SUBSETP-REFL))
 )
(HIFAT-SUBSETP-WHEN-ATOM
 (20 2 (:REWRITE SUBSETP-CAR-MEMBER))
 (17 1 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (16 4 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (11 1 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (8 8 (:REWRITE DEFAULT-CAR))
 (6 6 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (6 1 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (6 1 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (6 1 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (2 2 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (2 2 (:TYPE-PRESCRIPTION NONEMPTY-STRING-LISTP))
 (2 2 (:TYPE-PRESCRIPTION M1-FILE-ALIST-P))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 (2 2 (:REWRITE SUBSETP-NIL))
 (2 2 (:REWRITE SUBSETP-MEMBER . 4))
 (2 2 (:REWRITE SUBSETP-MEMBER . 3))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:REWRITE SET-EQUIV-OF-NIL))
 (2 2 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (2 2 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 3))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 2))
 (2 2 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (1 1 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (1 1 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (1 1 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (1 1 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (1 1 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(HIFAT-SUBSETP-REFLEXIVE-LEMMA-1
 (5594 181 (:DEFINITION MEMBER-EQUAL))
 (3989 907 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (3826 212 (:REWRITE SUBSETP-CAR-MEMBER))
 (3368 71 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (2770 554 (:TYPE-PRESCRIPTION ASSOC-OF-APPEND-2))
 (2662 63 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (2283 195 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1104 787 (:REWRITE DEFAULT-CDR))
 (1084 122 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (923 35 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (851 232 (:REWRITE SUBSETP-MEMBER . 3))
 (682 232 (:REWRITE MEMBER-WHEN-ATOM))
 (554 554 (:TYPE-PRESCRIPTION ATOM))
 (541 82 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (500 500 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (452 226 (:REWRITE SET-EQUIV-ASYM))
 (385 35 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (362 362 (:REWRITE SUBSETP-MEMBER . 2))
 (362 362 (:REWRITE SUBSETP-MEMBER . 1))
 (327 327 (:REWRITE SUBSETP-TRANS2))
 (327 327 (:REWRITE SUBSETP-TRANS))
 (314 78 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (296 296 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (296 296 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (293 141 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (288 96 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (232 232 (:REWRITE SUBSETP-MEMBER . 4))
 (232 232 (:REWRITE INTERSECTP-MEMBER . 3))
 (232 232 (:REWRITE INTERSECTP-MEMBER . 2))
 (226 226 (:TYPE-PRESCRIPTION SET-EQUIV))
 (226 226 (:REWRITE SUBSETP-OF-CDR))
 (220 20 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (210 35 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (210 35 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (201 67 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (177 177 (:TYPE-PRESCRIPTION M1-FILE-P))
 (175 35 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (105 35 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (77 77 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (75 75 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (70 70 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (70 70 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (70 70 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (70 70 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (70 70 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (65 65 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (60 20 (:REWRITE M1-FILE-FIX-WHEN-M1-FILE-P))
 (35 35 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (35 35 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (12 6 (:REWRITE COMMUTATIVITY-OF-APPEND-UNDER-SET-EQUIV))
 (6 2 (:REWRITE CONSP-OF-ASSOC-EQUAL-OF-APPEND))
 )
(HIFAT-SUBSETP-REFLEXIVE-LEMMA-2
 (596 24 (:DEFINITION MEMBER-EQUAL))
 (435 30 (:REWRITE SUBSETP-CAR-MEMBER))
 (375 90 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (285 8 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (180 15 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (150 150 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (144 144 (:REWRITE DEFAULT-CAR))
 (130 65 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (118 16 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (118 8 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (107 83 (:REWRITE DEFAULT-CDR))
 (88 8 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (86 32 (:REWRITE MEMBER-WHEN-ATOM))
 (66 16 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (66 8 (:DEFINITION ASSOC-EQUAL))
 (65 65 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (65 65 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (63 21 (:REWRITE CAR-OF-APPEND))
 (60 30 (:REWRITE SET-EQUIV-ASYM))
 (48 48 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (48 48 (:REWRITE SUBSETP-MEMBER . 2))
 (48 48 (:REWRITE SUBSETP-MEMBER . 1))
 (48 8 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (48 8 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (40 8 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (32 32 (:REWRITE SUBSETP-MEMBER . 4))
 (32 32 (:REWRITE SUBSETP-MEMBER . 3))
 (32 32 (:REWRITE INTERSECTP-MEMBER . 3))
 (32 32 (:REWRITE INTERSECTP-MEMBER . 2))
 (30 30 (:TYPE-PRESCRIPTION SET-EQUIV))
 (30 30 (:REWRITE SUBSETP-OF-CDR))
 (30 5 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (30 5 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (29 8 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (24 24 (:TYPE-PRESCRIPTION M1-FILE-P))
 (24 8 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (24 8 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (24 8 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (20 20 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (17 5 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (17 5 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (16 16 (:TYPE-PRESCRIPTION ZP))
 (16 16 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (16 16 (:TYPE-PRESCRIPTION LEN))
 (16 16 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (16 16 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (16 16 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (16 16 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (16 16 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (15 15 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (15 15 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (15 15 (:REWRITE SUBSETP-TRANS2))
 (15 15 (:REWRITE SUBSETP-TRANS))
 (12 12 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (10 10 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (8 8 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (8 8 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (8 8 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (8 8 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (6 6 (:REWRITE CONSP-OF-APPEND))
 )
(HIFAT-SUBSETP-REFLEXIVE-LEMMA-3
 (143 1 (:DEFINITION HIFAT-NO-DUPS-P))
 (58 4 (:REWRITE SUBSETP-CAR-MEMBER))
 (58 2 (:DEFINITION MEMBER-EQUAL))
 (50 12 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (42 1 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (24 2 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (20 20 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (15 15 (:REWRITE DEFAULT-CAR))
 (10 10 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (10 10 (:REWRITE DEFAULT-CDR))
 (8 4 (:REWRITE SET-EQUIV-ASYM))
 (8 2 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (6 6 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (6 2 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (6 2 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (6 2 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (6 1 (:DEFINITION ASSOC-EQUAL))
 (4 4 (:TYPE-PRESCRIPTION SET-EQUIV))
 (4 4 (:REWRITE SUBSETP-OF-CDR))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 (4 1 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (4 1 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (3 1 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 (2 2 (:TYPE-PRESCRIPTION M1-FILE-P))
 (2 2 (:TYPE-PRESCRIPTION LEN))
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 (2 2 (:REWRITE SUBSETP-MEMBER . 4))
 (2 2 (:REWRITE SUBSETP-MEMBER . 3))
 (2 2 (:REWRITE MEMBER-WHEN-ATOM))
 (2 2 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (2 2 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 3))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 2))
 (1 1 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (1 1 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (1 1 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (1 1 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (1 1 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 )
(INDUCTION-SCHEME
 (83278 29 (:DEFINITION ACL2-COUNT))
 (74778 86 (:REWRITE RATIONALP-OF-CAR-WHEN-RATIONAL-LISTP))
 (73640 140 (:REWRITE RATIONAL-LISTP-WHEN-INTEGER-LISTP))
 (71948 701 (:DEFINITION INTEGER-LISTP))
 (66273 48 (:DEFINITION RATIONAL-LISTP))
 (64144 1910 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (53808 100 (:REWRITE RATIONAL-LISTP-OF-CDR-WHEN-RATIONAL-LISTP))
 (48660 1513 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (36021 3942 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (31433 2448 (:REWRITE NAT-LISTP-OF-CDR-WHEN-NAT-LISTP))
 (17095 3528 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (12541 1090 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (7514 7514 (:REWRITE DEFAULT-CAR))
 (6124 6124 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (6124 6124 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (5425 5347 (:REWRITE DEFAULT-CDR))
 (3942 3942 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (3942 3942 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (3942 3942 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (1910 1910 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (688 26 (:REWRITE LENGTH-WHEN-STRINGP))
 (653 53 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (629 223 (:REWRITE DEFAULT-+-2))
 (403 223 (:REWRITE DEFAULT-+-1))
 (292 24 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (286 26 (:DEFINITION LEN))
 (281 27 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (260 52 (:REWRITE COMMUTATIVITY-OF-+))
 (208 52 (:DEFINITION INTEGER-ABS))
 (148 20 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (146 12 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (140 140 (:REWRITE RATIONAL-LISTP-WHEN-NOT-CONSP))
 (106 106 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (106 106 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (96 6 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (88 88 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (78 78 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (78 52 (:REWRITE STR::CONSP-OF-EXPLODE))
 (74 10 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (70 9 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (57 53 (:REWRITE DEFAULT-<-1))
 (55 55 (:REWRITE FOLD-CONSTS-IN-+))
 (55 53 (:REWRITE DEFAULT-<-2))
 (54 54 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (54 54 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (52 52 (:REWRITE DEFAULT-UNARY-MINUS))
 (52 26 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (44 44 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (44 44 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (32 32 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (30 1 (:REWRITE M1-FILE-CONTENTS-FIX-WHEN-M1-FILE-CONTENTS-P))
 (26 26 (:TYPE-PRESCRIPTION LEN))
 (26 26 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (26 26 (:REWRITE DEFAULT-REALPART))
 (26 26 (:REWRITE DEFAULT-NUMERATOR))
 (26 26 (:REWRITE DEFAULT-IMAGPART))
 (26 26 (:REWRITE DEFAULT-DENOMINATOR))
 (22 22 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (17 2 (:REWRITE M1-FILE-CONTENTS-P-CORRECTNESS-1))
 (16 16 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (16 16 (:LINEAR ACL2-COUNT-WHEN-MEMBER))
 (15 1 (:REWRITE ACL2-COUNT-WHEN-MEMBER))
 (12 2 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (10 1 (:DEFINITION MEMBER-EQUAL))
 (8 8 (:LINEAR ACL2-COUNT-OF-CONSP-POSITIVE))
 (7 7 (:LINEAR ACL2-COUNT-CAR-CDR-LINEAR))
 (5 5 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 )
(HIFAT-SUBSETP-REFLEXIVE-LEMMA-4
 (6013 1286 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (5535 145 (:DEFINITION MEMBER-EQUAL))
 (4332 69 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (3305 234 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (2500 180 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (2498 52 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (2196 44 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (1674 24 (:REWRITE ASSOC-OF-APPEND-1))
 (1269 1269 (:REWRITE DEFAULT-CAR))
 (895 895 (:REWRITE SUBSETP-TRANS2))
 (895 895 (:REWRITE SUBSETP-TRANS))
 (792 112 (:DEFINITION ASSOC-EQUAL))
 (784 784 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (784 784 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (622 622 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (504 12 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (504 12 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (309 103 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (302 134 (:REWRITE MEMBER-WHEN-ATOM))
 (292 146 (:REWRITE SET-EQUIV-ASYM))
 (290 290 (:REWRITE SUBSETP-MEMBER . 2))
 (290 290 (:REWRITE SUBSETP-MEMBER . 1))
 (273 123 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (216 6 (:REWRITE ALISTP-OF-APPEND))
 (184 64 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (176 16 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (163 163 (:REWRITE SUBSETP-OF-CDR))
 (147 147 (:TYPE-PRESCRIPTION SET-EQUIV))
 (144 36 (:DEFINITION BINARY-APPEND))
 (144 15 (:DEFINITION ALISTP))
 (134 134 (:REWRITE SUBSETP-MEMBER . 4))
 (134 134 (:REWRITE SUBSETP-MEMBER . 3))
 (134 134 (:REWRITE INTERSECTP-MEMBER . 3))
 (134 134 (:REWRITE INTERSECTP-MEMBER . 2))
 (108 27 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (104 29 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (96 16 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (96 16 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (90 30 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (70 70 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (70 70 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (68 68 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (54 54 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (54 54 (:TYPE-PRESCRIPTION ALISTP))
 (34 34 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (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))
 (32 32 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (30 30 (:TYPE-PRESCRIPTION NULL))
 (30 30 (:DEFINITION NULL))
 (27 27 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (22 1 (:REWRITE SUBSETP-OF-CONS))
 (18 6 (:REWRITE CONSP-OF-ASSOC-EQUAL-OF-APPEND))
 (16 16 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (16 16 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (12 12 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (7 1 (:REWRITE SUBSETP-CONS-2))
 (3 3 (:TYPE-PRESCRIPTION INDUCTION-SCHEME))
 (2 1 (:REWRITE SET-EQUIV-OF-NIL))
 (1 1 (:REWRITE SUBSETP-NIL))
 )
(HIFAT-SUBSETP-REFLEXIVE-LEMMA-5
 (31 5 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (24 4 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (14 5 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (11 5 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (10 10 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (8 8 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (4 4 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (3 1 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (1 1 (:REWRITE M1-FILE-FIX-WHEN-M1-FILE-P))
 )
(HIFAT-SUBSETP-REFLEXIVE
 (2 1 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 (1 1 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (1 1 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (1 1 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 )
(HIFAT-EQUIV)
(HIFAT-EQUIV-IS-AN-EQUIVALENCE
 (34 12 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (26 8 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 )
(CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1
 (5793 71 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (5253 17 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (4397 826 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (3440 224 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1854 6 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (1106 54 (:REWRITE SUBSETP-CAR-MEMBER))
 (1091 21 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (972 27 (:DEFINITION MEMBER-EQUAL))
 (904 553 (:REWRITE DEFAULT-CDR))
 (893 893 (:REWRITE DEFAULT-CAR))
 (776 776 (:REWRITE SUBSETP-TRANS2))
 (776 776 (:REWRITE SUBSETP-TRANS))
 (765 765 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (765 765 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (608 32 (:REWRITE LENGTH-WHEN-STRINGP))
 (352 32 (:DEFINITION LEN))
 (320 32 (:DEFINITION UNSIGNED-BYTE-P))
 (293 32 (:DEFINITION ALISTP))
 (288 32 (:DEFINITION INTEGER-RANGE-P))
 (256 64 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (228 48 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (218 218 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (198 198 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (192 32 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (129 17 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (128 128 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (128 64 (:REWRITE DEFAULT-<-1))
 (128 32 (:DEFINITION STRIP-CARS))
 (126 42 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (110 110 (:TYPE-PRESCRIPTION STRIP-CARS))
 (96 96 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (96 64 (:REWRITE STR::CONSP-OF-EXPLODE))
 (90 90 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (90 90 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (64 64 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (64 64 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (64 32 (:REWRITE DEFAULT-+-2))
 (64 32 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (55 55 (:TYPE-PRESCRIPTION D-E-P))
 (54 54 (:REWRITE SUBSETP-MEMBER . 2))
 (54 54 (:REWRITE SUBSETP-MEMBER . 1))
 (50 50 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (48 16 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (40 20 (:REWRITE SET-EQUIV-ASYM))
 (32 32 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (32 32 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (32 32 (:REWRITE DEFAULT-+-1))
 (20 20 (:TYPE-PRESCRIPTION SET-EQUIV))
 (20 20 (:REWRITE SUBSETP-OF-CDR))
 (17 17 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (17 17 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (12 12 (:REWRITE SUBSETP-MEMBER . 4))
 (12 12 (:REWRITE SUBSETP-MEMBER . 3))
 (12 12 (:REWRITE MEMBER-WHEN-ATOM))
 (12 12 (:REWRITE INTERSECTP-MEMBER . 3))
 (12 12 (:REWRITE INTERSECTP-MEMBER . 2))
 )
(CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV
 (143 143 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (69 23 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (32 8 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (27 7 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (21 21 (:REWRITE DEFAULT-CAR))
 (18 18 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (7 7 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (7 7 (:REWRITE DEFAULT-CDR))
 )
(HIFAT-EQUIV-OF-CONS-LEMMA-1
 (3952 149 (:REWRITE SUBSETP-CAR-MEMBER))
 (3540 734 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (3204 86 (:DEFINITION MEMBER-EQUAL))
 (3057 47 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (2290 229 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (1916 152 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1483 1405 (:REWRITE DEFAULT-CAR))
 (762 42 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (602 30 (:DEFINITION LEN))
 (599 142 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (451 451 (:REWRITE SUBSETP-TRANS2))
 (451 451 (:REWRITE SUBSETP-TRANS))
 (390 49 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (362 60 (:REWRITE STR::CONSP-OF-EXPLODE))
 (343 337 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (343 337 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (314 11 (:REWRITE SUBSETP-OF-CONS))
 (225 18 (:DEFINITION ALISTP))
 (207 34 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (202 34 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (190 95 (:REWRITE SET-EQUIV-ASYM))
 (186 174 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (172 172 (:REWRITE SUBSETP-MEMBER . 2))
 (172 172 (:REWRITE SUBSETP-MEMBER . 1))
 (157 10 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (144 36 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (132 12 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (113 113 (:REWRITE SUBSETP-OF-CDR))
 (106 106 (:TYPE-PRESCRIPTION SET-EQUIV))
 (102 30 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (90 90 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (84 11 (:REWRITE SUBSETP-CONS-2))
 (72 72 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (72 12 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (63 63 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (60 30 (:REWRITE DEFAULT-+-2))
 (53 30 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (48 48 (:REWRITE SUBSETP-MEMBER . 4))
 (48 48 (:REWRITE SUBSETP-MEMBER . 3))
 (48 48 (:REWRITE MEMBER-WHEN-ATOM))
 (48 48 (:REWRITE INTERSECTP-MEMBER . 3))
 (48 48 (:REWRITE INTERSECTP-MEMBER . 2))
 (40 10 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (36 36 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (30 30 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (30 30 (:REWRITE DEFAULT-+-1))
 (30 10 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (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))
 (15 15 (:REWRITE M1-FILE-ALIST-P-OF-HIFAT-FILE-ALIST-FIX))
 (12 12 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 )
(HIFAT-EQUIV-OF-CONS-LEMMA-2
 (8 2 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (6 1 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (5 1 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (3 3 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (2 1 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (1 1 (:TYPE-PRESCRIPTION M1-FILE-P))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 (1 1 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (1 1 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-EQUIV-OF-CONS-LEMMA-3
 (1145 260 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (829 44 (:REWRITE SUBSETP-CAR-MEMBER))
 (757 33 (:DEFINITION MEMBER-EQUAL))
 (578 19 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (508 479 (:REWRITE DEFAULT-CAR))
 (273 91 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (264 20 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (252 231 (:REWRITE DEFAULT-CDR))
 (186 14 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (186 14 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (182 182 (:REWRITE SUBSETP-TRANS2))
 (182 182 (:REWRITE SUBSETP-TRANS))
 (151 151 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (151 151 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (133 133 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (124 42 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (120 7 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (101 6 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (99 23 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (96 6 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (91 91 (:TYPE-PRESCRIPTION ZP))
 (91 91 (:TYPE-PRESCRIPTION LEN))
 (91 4 (:REWRITE SUBSETP-OF-CONS))
 (89 19 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (66 66 (:REWRITE SUBSETP-MEMBER . 2))
 (66 66 (:REWRITE SUBSETP-MEMBER . 1))
 (62 22 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (56 28 (:REWRITE SET-EQUIV-ASYM))
 (46 46 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (45 45 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (38 38 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (34 7 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (34 7 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (33 33 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (32 32 (:TYPE-PRESCRIPTION SET-EQUIV))
 (30 7 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (28 28 (:REWRITE SUBSETP-OF-CDR))
 (28 28 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (28 4 (:REWRITE SUBSETP-CONS-2))
 (27 27 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (19 19 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (18 18 (:REWRITE SUBSETP-MEMBER . 4))
 (18 18 (:REWRITE SUBSETP-MEMBER . 3))
 (18 18 (:REWRITE MEMBER-WHEN-ATOM))
 (18 18 (:REWRITE INTERSECTP-MEMBER . 3))
 (18 18 (:REWRITE INTERSECTP-MEMBER . 2))
 (18 18 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (14 14 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (6 6 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (4 1 (:REWRITE HIFAT-EQUIV-OF-CONS-LEMMA-2))
 )
(HIFAT-EQUIV-OF-CONS-LEMMA-4
 (2922 182 (:DEFINITION MEMBER-EQUAL))
 (2632 112 (:REWRITE SUBSETP-CAR-MEMBER))
 (2321 436 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (2036 218 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (1243 55 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (824 52 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (736 721 (:REWRITE DEFAULT-CDR))
 (660 48 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (632 632 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (579 20 (:REWRITE SUBSETP-OF-CONS))
 (560 146 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (539 49 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (520 72 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (429 53 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (383 383 (:REWRITE SUBSETP-MEMBER . 2))
 (369 123 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (368 368 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (342 15 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (319 319 (:TYPE-PRESCRIPTION M1-FILE-P))
 (294 49 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (294 49 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (287 287 (:REWRITE SUBSETP-TRANS2))
 (287 287 (:REWRITE SUBSETP-TRANS))
 (279 28 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (276 92 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (237 42 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (236 236 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (236 236 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (206 206 (:REWRITE SUBSETP-MEMBER . 4))
 (206 206 (:REWRITE INTERSECTP-MEMBER . 3))
 (206 206 (:REWRITE INTERSECTP-MEMBER . 2))
 (195 10 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (187 51 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (184 184 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (176 176 (:REWRITE MEMBER-WHEN-ATOM))
 (159 12 (:REWRITE M1-FILE-FIX-WHEN-M1-FILE-P))
 (153 53 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (108 54 (:REWRITE SET-EQUIV-ASYM))
 (101 101 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (98 98 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (98 98 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (98 98 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (98 98 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (98 98 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (92 17 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (84 84 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (72 72 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (64 10 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (64 10 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (61 61 (:TYPE-PRESCRIPTION SET-EQUIV))
 (61 11 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE->CONTENTS-OF-HIFAT-FIND-FILE-LEMMA-1))
 (54 54 (:REWRITE SUBSETP-OF-CDR))
 (53 10 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (49 49 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (49 49 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (49 49 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (39 3 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE-FIX))
 (36 6 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (6 6 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (3 3 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 )
(HIFAT-EQUIV-OF-CONS
 (47214 112 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (17747 514 (:DEFINITION MEMBER-EQUAL))
 (17447 4014 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (16728 978 (:REWRITE SUBSETP-CAR-MEMBER))
 (9330 200 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (8834 193 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (8659 204 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (8100 709 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (3474 3282 (:REWRITE DEFAULT-CAR))
 (3234 200 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (2969 244 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (2795 215 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (2526 2526 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (2266 2119 (:REWRITE DEFAULT-CDR))
 (2054 1027 (:REWRITE SET-EQUIV-ASYM))
 (1490 1385 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1490 1385 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1460 132 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (1438 138 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (1399 1399 (:REWRITE SUBSETP-TRANS2))
 (1399 1399 (:REWRITE SUBSETP-TRANS))
 (1341 97 (:REWRITE M1-FILE-FIX-WHEN-M1-FILE-P))
 (1104 99 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (1034 171 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (1028 1028 (:REWRITE SUBSETP-MEMBER . 2))
 (1028 1028 (:REWRITE SUBSETP-MEMBER . 1))
 (1027 1027 (:TYPE-PRESCRIPTION SET-EQUIV))
 (1027 1027 (:REWRITE SUBSETP-OF-CDR))
 (826 730 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (800 132 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (771 49 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (766 258 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (741 247 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (694 640 (:REWRITE MEMBER-WHEN-ATOM))
 (679 227 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (640 640 (:REWRITE SUBSETP-MEMBER . 4))
 (640 640 (:REWRITE SUBSETP-MEMBER . 3))
 (640 640 (:REWRITE INTERSECTP-MEMBER . 3))
 (640 640 (:REWRITE INTERSECTP-MEMBER . 2))
 (404 404 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (389 389 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (356 171 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (352 25 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (342 342 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (321 33 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (312 77 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (264 264 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (264 264 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (264 264 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (250 250 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (171 171 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (132 132 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (59 31 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (40 40 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (36 18 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (4 4 (:REWRITE CONS-CAR-CDR))
 (3 3 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT M1-FILE-FIX-UNDER-M1-FILE-EQUIV))
 )
(HIFAT-EQUIV-IMPLIES-SET-EQUIV-STRIP-CARS-1-LEMMA-1
 (682 6 (:REWRITE MEMBER-EQUAL-OF-STRIP-CARS-WHEN-MEMBER-EQUAL-OF-HONS-DUPLICATED-MEMBERS-AUX))
 (526 6 (:REWRITE MEMBER-EQUAL-OF-HONS-DUPLICATED-MEMBERS-AUX))
 (468 6 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (451 62 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (319 17 (:REWRITE SUBSETP-CAR-MEMBER))
 (261 1 (:REWRITE SUBSETP-OF-CONS))
 (193 12 (:REWRITE FAT32-FILENAME-LIST-P-CORRECTNESS-1))
 (144 9 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (104 68 (:REWRITE DEFAULT-CAR))
 (101 35 (:REWRITE SUBSETP-MEMBER . 3))
 (67 46 (:REWRITE DEFAULT-CDR))
 (65 32 (:REWRITE MEMBER-WHEN-ATOM))
 (60 24 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (56 56 (:REWRITE CONSP-OF-STRIP-CARS))
 (51 5 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (49 49 (:REWRITE SUBSETP-MEMBER . 2))
 (42 24 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (41 5 (:REWRITE MEMBER-EQUAL-OF-STRIP-CARS-WHEN-M1-FILE-ALIST-P))
 (39 19 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (38 38 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (35 35 (:REWRITE SUBSETP-MEMBER . 4))
 (35 35 (:REWRITE INTERSECTP-MEMBER . 3))
 (35 35 (:REWRITE INTERSECTP-MEMBER . 2))
 (30 30 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (30 30 (:TYPE-PRESCRIPTION HONS-DUPLICATED-MEMBERS-AUX))
 (28 28 (:REWRITE SUBSETP-TRANS2))
 (28 28 (:REWRITE SUBSETP-TRANS))
 (27 2 (:REWRITE FAT32-FILENAME-LIST-P-OF-CONS))
 (26 13 (:REWRITE SET-EQUIV-ASYM))
 (24 6 (:REWRITE NO-DUPLICATESP-OF-STRIP-CARS-WHEN-HIFAT-NO-DUPS-P))
 (16 16 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (14 14 (:TYPE-PRESCRIPTION SET-EQUIV))
 (14 14 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (13 13 (:REWRITE SUBSETP-OF-CDR))
 (8 6 (:REWRITE MEMBER-OF-STRIP-CARS))
 (7 7 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (7 7 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (6 2 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (6 1 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (6 1 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (6 1 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (2 2 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (1 1 (:TYPE-PRESCRIPTION NULL))
 (1 1 (:REWRITE FTY::STRIP-CARS-UNDER-IFF))
 )
(HIFAT-EQUIV-IMPLIES-SET-EQUIV-STRIP-CARS-1-LEMMA-2
 (2779 95 (:REWRITE SUBSETP-CAR-MEMBER))
 (2727 434 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (2316 45 (:DEFINITION MEMBER-EQUAL))
 (1318 81 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1014 338 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (898 72 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (577 4 (:REWRITE SET-EQUIV-OF-CONS-SELF))
 (463 370 (:REWRITE SUBSETP-TRANS))
 (455 347 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (452 348 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (435 4 (:REWRITE MEMBER-EQUAL-OF-STRIP-CARS-WHEN-MEMBER-EQUAL-OF-HONS-DUPLICATED-MEMBERS-AUX))
 (327 189 (:REWRITE DEFAULT-CDR))
 (324 18 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (275 3 (:REWRITE MEMBER-EQUAL-OF-HONS-DUPLICATED-MEMBERS-AUX))
 (247 3 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (227 43 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (217 217 (:TYPE-PRESCRIPTION STRIP-CARS))
 (198 18 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (196 196 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (188 96 (:REWRITE SUBSETP-MEMBER . 2))
 (172 172 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (150 22 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (144 24 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (132 22 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (132 19 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (129 43 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (120 41 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (108 18 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (107 107 (:TYPE-PRESCRIPTION M1-FILE-P))
 (105 35 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (98 98 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (80 80 (:REWRITE CONSP-OF-STRIP-CARS))
 (72 12 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (68 4 (:REWRITE MEMBER-EQUAL-OF-STRIP-CARS-WHEN-M1-FILE-ALIST-P))
 (64 8 (:REWRITE SUBSETP-CONS-2))
 (61 46 (:REWRITE MEMBER-WHEN-ATOM))
 (60 10 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (58 29 (:REWRITE SET-EQUIV-ASYM))
 (55 55 (:REWRITE SUBSETP-MEMBER . 4))
 (55 55 (:REWRITE INTERSECTP-MEMBER . 3))
 (55 55 (:REWRITE INTERSECTP-MEMBER . 2))
 (45 45 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (45 45 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (44 44 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (44 44 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (44 44 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (36 36 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (36 36 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (36 36 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (30 30 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (29 29 (:TYPE-PRESCRIPTION SET-EQUIV))
 (24 24 (:TYPE-PRESCRIPTION HONS-DUPLICATED-MEMBERS-AUX))
 (23 23 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (22 22 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (20 20 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (20 20 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (20 20 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (20 20 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (18 18 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (15 15 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (15 3 (:REWRITE NO-DUPLICATESP-OF-STRIP-CARS-WHEN-HIFAT-NO-DUPS-P))
 (14 14 (:REWRITE SUBSETP-OF-CDR))
 (10 10 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (10 1 (:DEFINITION ALISTP))
 (8 2 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (6 2 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (4 4 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (3 3 (:REWRITE FTY::STRIP-CARS-UNDER-IFF))
 (2 2 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-EQUIV-IMPLIES-SET-EQUIV-STRIP-CARS-1
 (72 6 (:REWRITE FAT32-FILENAME-LIST-FIX-WHEN-FAT32-FILENAME-LIST-P))
 (34 34 (:TYPE-PRESCRIPTION STRIP-CARS))
 (30 6 (:DEFINITION STRIP-CARS))
 (24 8 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (24 6 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (16 4 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (12 12 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (12 12 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (12 12 (:REWRITE DEFAULT-CAR))
 (12 4 (:REWRITE CONSP-OF-FAT32-FILENAME-LIST-FIX))
 (12 2 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (12 2 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (10 10 (:REWRITE CONSP-OF-STRIP-CARS))
 (8 8 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-FIX$INLINE))
 (6 6 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (6 6 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (4 4 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (2 2 (:REWRITE SUBSETP-TRANS))
 )
(PUT-ASSOC-UNDER-HIFAT-EQUIV-1
 (16696 3620 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (14590 285 (:REWRITE M1-FILE-FIX-WHEN-M1-FILE-P))
 (14083 331 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (13289 202 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (12056 291 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (11784 237 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (9626 147 (:REWRITE M1-FILE-ALIST-P-OF-PUT-ASSOC))
 (5832 197 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (5392 182 (:REWRITE SUBSETP-CAR-MEMBER))
 (4988 162 (:DEFINITION MEMBER-EQUAL))
 (4700 3600 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (4700 3600 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4463 113 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (4432 464 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (3725 3057 (:REWRITE DEFAULT-CAR))
 (3616 3616 (:REWRITE SUBSETP-TRANS2))
 (3616 3616 (:REWRITE SUBSETP-TRANS))
 (2452 1882 (:REWRITE DEFAULT-CDR))
 (1747 89 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (1599 1403 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (1571 97 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (1432 925 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (1244 291 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (1240 410 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (1134 86 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (1080 126 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (898 302 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (628 628 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (386 92 (:REWRITE MEMBER-WHEN-ATOM))
 (370 370 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (324 324 (:REWRITE SUBSETP-MEMBER . 2))
 (324 324 (:REWRITE SUBSETP-MEMBER . 1))
 (315 315 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (273 126 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (252 252 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (129 101 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (128 64 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (117 117 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (92 92 (:REWRITE SUBSETP-MEMBER . 4))
 (92 92 (:REWRITE SUBSETP-MEMBER . 3))
 (92 92 (:REWRITE INTERSECTP-MEMBER . 3))
 (92 92 (:REWRITE INTERSECTP-MEMBER . 2))
 (74 4 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (70 70 (:REWRITE CONS-CAR-CDR))
 (54 4 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (46 2 (:REWRITE SUBSETP-OF-CONS))
 (19 19 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (14 2 (:REWRITE SUBSETP-CONS-2))
 (8 8 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (8 8 (:REWRITE-QUOTED-CONSTANT TRUE-LIST-LIST-FIX-UNDER-TRUE-LIST-LIST-EQUIV))
 (8 8 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (8 8 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (4 4 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (2 2 (:TYPE-PRESCRIPTION SET-EQUIV))
 (2 2 (:REWRITE FAT32-FILENAME-FIX-UNDER-FAT32-FILENAME-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT M1-FILE-FIX-UNDER-M1-FILE-EQUIV))
 )
(PUT-ASSOC-UNDER-HIFAT-EQUIV-3
 (7068 270 (:REWRITE M1-FILE-FIX-WHEN-M1-FILE-P))
 (6131 379 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (5012 144 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (4831 1926 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (4051 220 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (3403 634 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (3356 157 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (2808 147 (:REWRITE M1-FILE-ALIST-P-OF-PUT-ASSOC))
 (2800 86 (:REWRITE SUBSETP-CAR-MEMBER))
 (2778 2100 (:REWRITE DEFAULT-CAR))
 (2096 49 (:DEFINITION MEMBER-EQUAL))
 (1806 1225 (:REWRITE DEFAULT-CDR))
 (1654 24 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1551 1551 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (1542 197 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (1509 1313 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (1470 963 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (1179 415 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (1134 135 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (1134 86 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (1040 88 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1024 624 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1024 624 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (788 141 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (727 41 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (671 49 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (630 630 (:REWRITE SUBSETP-TRANS2))
 (630 630 (:REWRITE SUBSETP-TRANS))
 (384 384 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (282 135 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (270 270 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (266 44 (:REWRITE MEMBER-WHEN-ATOM))
 (235 235 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (163 139 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (159 159 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (102 102 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (98 98 (:REWRITE SUBSETP-MEMBER . 2))
 (98 98 (:REWRITE SUBSETP-MEMBER . 1))
 (81 53 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (74 4 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (64 32 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (54 4 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (46 2 (:REWRITE SUBSETP-OF-CONS))
 (44 44 (:REWRITE SUBSETP-MEMBER . 4))
 (44 44 (:REWRITE SUBSETP-MEMBER . 3))
 (44 44 (:REWRITE INTERSECTP-MEMBER . 3))
 (44 44 (:REWRITE INTERSECTP-MEMBER . 2))
 (14 2 (:REWRITE SUBSETP-CONS-2))
 (13 13 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (9 9 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-1))
 (8 8 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (8 8 (:REWRITE-QUOTED-CONSTANT TRUE-LIST-LIST-FIX-UNDER-TRUE-LIST-LIST-EQUIV))
 (8 8 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (8 8 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (5 5 (:REWRITE CONS-CAR-CDR))
 (4 4 (:REWRITE SUBSETP-REFL))
 (4 4 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (2 2 (:TYPE-PRESCRIPTION SET-EQUIV))
 (2 2 (:REWRITE FAT32-FILENAME-FIX-UNDER-FAT32-FILENAME-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT M1-FILE-FIX-UNDER-M1-FILE-EQUIV))
 )
(HIFAT-EQUIV-OF-HIFAT-FILE-ALIST-FIX-1
 (13 4 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (4 4 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 )
(HIFAT-EQUIV-OF-HIFAT-FILE-ALIST-FIX-2
 (13 4 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (4 4 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 )
(HIFAT-SUBSETP-OF-PUT-ASSOC-1
 (30657 6342 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (27774 1180 (:REWRITE SUBSETP-CAR-MEMBER))
 (23748 583 (:DEFINITION MEMBER-EQUAL))
 (23104 398 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (22138 1198 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (12903 893 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (12468 539 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (10811 335 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (6954 749 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (5592 5422 (:REWRITE DEFAULT-CAR))
 (4948 4948 (:REWRITE SUBSETP-TRANS2))
 (4948 4948 (:REWRITE SUBSETP-TRANS))
 (4752 4536 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (4752 4536 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4273 23 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (4180 306 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (3832 2739 (:REWRITE DEFAULT-CDR))
 (3624 333 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (3192 3192 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (1888 45 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (1719 581 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (1478 1166 (:REWRITE SUBSETP-MEMBER . 1))
 (1321 449 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (1166 1166 (:REWRITE SUBSETP-MEMBER . 2))
 (1103 53 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (1101 35 (:REWRITE CONSP-OF-REMOVE-ASSOC-1))
 (1040 520 (:REWRITE SET-EQUIV-ASYM))
 (965 149 (:REWRITE ASSOC-AFTER-REMOVE-ASSOC))
 (780 53 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (749 749 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (626 626 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (520 520 (:TYPE-PRESCRIPTION SET-EQUIV))
 (520 520 (:REWRITE SUBSETP-OF-CDR))
 (368 368 (:REWRITE SUBSETP-MEMBER . 4))
 (368 368 (:REWRITE SUBSETP-MEMBER . 3))
 (368 368 (:REWRITE MEMBER-WHEN-ATOM))
 (368 368 (:REWRITE INTERSECTP-MEMBER . 3))
 (368 368 (:REWRITE INTERSECTP-MEMBER . 2))
 (245 25 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (226 78 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (218 71 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (190 190 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (164 13 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE-FIX))
 (120 17 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (120 17 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (50 50 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (50 50 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (34 34 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (34 34 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (26 26 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (17 17 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (17 17 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (13 13 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (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-SUBSETP-OF-PUT-ASSOC-2
 (6037 1045 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (5528 82 (:DEFINITION MEMBER-EQUAL))
 (5107 166 (:REWRITE SUBSETP-CAR-MEMBER))
 (3379 159 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (3276 244 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (3016 112 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (2941 176 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (2285 102 (:REWRITE REMOVE-ASSOC-WHEN-ABSENT-1))
 (1972 56 (:DEFINITION PUT-ASSOC-EQUAL))
 (1933 17 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1848 1823 (:REWRITE DEFAULT-CAR))
 (1791 306 (:DEFINITION ASSOC-EQUAL))
 (1770 34 (:DEFINITION REMOVE-ASSOC-EQUAL))
 (1314 1020 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1314 1020 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1082 60 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (1045 1045 (:REWRITE SUBSETP-TRANS2))
 (1045 1045 (:REWRITE SUBSETP-TRANS))
 (811 788 (:REWRITE DEFAULT-CDR))
 (624 624 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (609 20 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (575 111 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (423 141 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (320 159 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (279 279 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (246 106 (:REWRITE MEMBER-WHEN-ATOM))
 (231 77 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (220 220 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (210 10 (:REWRITE M1-FILE-ALIST-P-OF-REMOVE-ASSOC-EQUAL))
 (165 165 (:REWRITE SUBSETP-MEMBER . 2))
 (143 143 (:REWRITE CONSP-OF-REMOVE-ASSOC-1))
 (123 15 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (108 108 (:REWRITE SUBSETP-MEMBER . 4))
 (108 108 (:REWRITE INTERSECTP-MEMBER . 3))
 (108 108 (:REWRITE INTERSECTP-MEMBER . 2))
 (104 104 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (86 2 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (64 64 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (60 10 (:REWRITE M1-FILE-ALIST-P-OF-REMOVE-ASSOC))
 (48 6 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (48 6 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (42 2 (:REWRITE M1-FILE-ALIST-P-OF-PUT-ASSOC))
 (30 30 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (30 30 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (30 30 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (12 12 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (12 12 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (12 2 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-3))
 (12 2 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE->CONTENTS-OF-HIFAT-FIND-FILE-LEMMA-1))
 (6 6 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (6 6 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (6 2 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (6 1 (:REWRITE HIFAT-SUBSETP-OF-PUT-ASSOC-1))
 (4 4 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 )
(HIFAT-SUBSETP-OF-REMOVE-ASSOC-1
 (8153 162 (:REWRITE REMOVE-ASSOC-WHEN-ABSENT-1))
 (7387 1495 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (6286 54 (:DEFINITION REMOVE-ASSOC-EQUAL))
 (6073 194 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (5082 158 (:REWRITE SUBSETP-CAR-MEMBER))
 (4874 73 (:DEFINITION MEMBER-EQUAL))
 (3535 260 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (2591 192 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (2422 170 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (1630 1426 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1630 1426 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1474 1474 (:REWRITE SUBSETP-TRANS2))
 (1474 1474 (:REWRITE SUBSETP-TRANS))
 (1412 17 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (787 680 (:REWRITE DEFAULT-CDR))
 (686 201 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (670 34 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (644 44 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (504 504 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (432 74 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (324 108 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (322 5 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (291 170 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (271 47 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (215 215 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (177 59 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (172 172 (:REWRITE CONSP-OF-REMOVE-ASSOC-1))
 (156 92 (:REWRITE MEMBER-WHEN-ATOM))
 (150 150 (:REWRITE SUBSETP-MEMBER . 2))
 (98 98 (:REWRITE SUBSETP-MEMBER . 4))
 (98 98 (:REWRITE INTERSECTP-MEMBER . 3))
 (98 98 (:REWRITE INTERSECTP-MEMBER . 2))
 (94 94 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (94 94 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (94 94 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (52 5 (:DEFINITION ALISTP))
 (36 9 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (36 6 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (36 6 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (24 4 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (21 1 (:REWRITE M1-FILE-ALIST-P-OF-REMOVE-ASSOC-EQUAL))
 (18 18 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (16 16 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (12 12 (:REWRITE SUBSETP-OF-CDR))
 (12 12 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (12 12 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (12 6 (:REWRITE SET-EQUIV-ASYM))
 (12 4 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (12 4 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (9 9 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (6 6 (:TYPE-PRESCRIPTION SET-EQUIV))
 (6 6 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (6 6 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (6 1 (:REWRITE M1-FILE-ALIST-P-OF-REMOVE-ASSOC))
 )
(HIFAT-SUBSETP-OF-REMOVE-ASSOC-2
 (7126 276 (:REWRITE SUBSETP-CAR-MEMBER))
 (5978 132 (:DEFINITION MEMBER-EQUAL))
 (5498 994 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (5177 81 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (3301 214 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (3229 209 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (3213 130 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (1896 536 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (1588 51 (:REWRITE CONSP-OF-REMOVE-ASSOC-1))
 (1460 25 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (1072 1072 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (1059 91 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (992 40 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (950 55 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (869 869 (:REWRITE SUBSETP-TRANS2))
 (869 869 (:REWRITE SUBSETP-TRANS))
 (857 857 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (857 857 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (807 67 (:REWRITE M1-FILE-ALIST-P-OF-REMOVE-ASSOC-EQUAL))
 (683 558 (:REWRITE DEFAULT-CDR))
 (663 146 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (611 64 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (565 40 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (540 160 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (478 478 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (417 35 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (416 60 (:REWRITE M1-FILE-ALIST-P-OF-REMOVE-ASSOC))
 (325 325 (:TYPE-PRESCRIPTION M1-FILE-P))
 (324 108 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (273 273 (:REWRITE SUBSETP-MEMBER . 2))
 (267 89 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (263 175 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (261 25 (:REWRITE M1-FILE-FIX-WHEN-M1-FILE-P))
 (242 35 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (242 35 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (175 175 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (130 130 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (126 16 (:REWRITE ASSOC-AFTER-REMOVE-ASSOC))
 (118 118 (:REWRITE SUBSETP-MEMBER . 4))
 (118 118 (:REWRITE INTERSECTP-MEMBER . 3))
 (118 118 (:REWRITE INTERSECTP-MEMBER . 2))
 (106 106 (:REWRITE MEMBER-WHEN-ATOM))
 (100 50 (:REWRITE SET-EQUIV-ASYM))
 (82 82 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (75 75 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (70 70 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (70 70 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (70 70 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (70 70 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (70 70 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (58 6 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (50 50 (:TYPE-PRESCRIPTION SET-EQUIV))
 (50 50 (:REWRITE SUBSETP-OF-CDR))
 (35 35 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (35 35 (:REWRITE FAT32-FILENAME-LIST-P-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))
 (3 1 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (2 2 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 )
(HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-LEMMA-3)
(HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-LEMMA-1
 (459 459 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (90 10 (:DEFINITION ASSOC-EQUAL))
 (72 4 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (64 2 (:DEFINITION PUT-ASSOC-EQUAL))
 (44 44 (:REWRITE DEFAULT-CAR))
 (41 24 (:REWRITE DEFAULT-CDR))
 (38 4 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (34 4 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (28 2 (:REWRITE ZP-OPEN))
 (20 20 (:TYPE-PRESCRIPTION HIFAT-PLACE-FILE-CORRECTNESS-1 . 2))
 (18 8 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (10 8 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (8 4 (:REWRITE DEFAULT-<-2))
 (6 1 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (5 5 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (4 4 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 2 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (2 2 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-3))
 (2 2 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (1 1 (:REWRITE M1-FILE-ALIST-P-OF-HIFAT-FILE-ALIST-FIX))
 (1 1 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (1 1 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 )
(HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3
 (5619 1873 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1523 320 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (1345 63 (:REWRITE SUBSETP-CAR-MEMBER))
 (1162 174 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (1040 27 (:DEFINITION MEMBER-EQUAL))
 (998 200 (:REWRITE DEFAULT-CDR))
 (942 17 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (614 25 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (500 38 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (462 22 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (315 15 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (295 295 (:REWRITE SUBSETP-TRANS2))
 (295 295 (:REWRITE SUBSETP-TRANS))
 (286 286 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (286 286 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (165 15 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (90 15 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (90 15 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (87 87 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (81 11 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (70 22 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (64 64 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (61 61 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (60 60 (:REWRITE SUBSETP-MEMBER . 2))
 (47 7 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (43 43 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (43 15 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (30 30 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (30 30 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (30 30 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (30 30 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (29 29 (:REWRITE SUBSETP-MEMBER . 4))
 (29 29 (:REWRITE INTERSECTP-MEMBER . 3))
 (29 29 (:REWRITE INTERSECTP-MEMBER . 2))
 (28 28 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (28 28 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (20 20 (:REWRITE MEMBER-WHEN-ATOM))
 (20 10 (:REWRITE SET-EQUIV-ASYM))
 (15 15 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (15 15 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (10 10 (:TYPE-PRESCRIPTION SET-EQUIV))
 (10 10 (:REWRITE SUBSETP-OF-CDR))
 )
(HIFAT-FIND-FILE-CORRECTNESS-LEMMA-1)
(ABS-PWRITE-CORRECTNESS-LEMMA-29
 (4902 1634 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1670 118 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (960 44 (:REWRITE SUBSETP-CAR-MEMBER))
 (676 132 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (660 16 (:DEFINITION MEMBER-EQUAL))
 (575 139 (:REWRITE DEFAULT-CDR))
 (409 71 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (366 6 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (346 36 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (272 272 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (256 16 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (220 220 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (203 60 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (201 67 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (178 178 (:TYPE-PRESCRIPTION M1-FILE-P))
 (174 58 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (154 14 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (132 132 (:REWRITE SUBSETP-TRANS2))
 (132 132 (:REWRITE SUBSETP-TRANS))
 (121 21 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (120 120 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (120 120 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (110 110 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (102 17 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (102 17 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (84 14 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (84 14 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (82 2 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (68 68 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (51 3 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (42 42 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (39 39 (:REWRITE SUBSETP-MEMBER . 2))
 (34 34 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (32 32 (:REWRITE SUBSETP-MEMBER . 4))
 (32 32 (:REWRITE INTERSECTP-MEMBER . 3))
 (32 32 (:REWRITE INTERSECTP-MEMBER . 2))
 (30 5 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (29 29 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (29 29 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (28 28 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (28 28 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (28 28 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (24 2 (:REWRITE M1-FILE-FIX-WHEN-M1-FILE-P))
 (23 23 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (20 20 (:REWRITE MEMBER-WHEN-ATOM))
 (17 17 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (14 14 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 )
(HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1
 (20817 568 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (14118 194 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (11404 176 (:REWRITE EQUAL-OF-M1-FILE))
 (8628 284 (:DEFINITION PUT-ASSOC-EQUAL))
 (8588 352 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (7350 914 (:DEFINITION ASSOC-EQUAL))
 (4074 4074 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (3777 3777 (:REWRITE DEFAULT-CAR))
 (2605 2605 (:REWRITE DEFAULT-CDR))
 (2016 144 (:REWRITE ZP-OPEN))
 (1889 183 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (1798 1798 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (1584 176 (:REWRITE M1-FILE-CONTENTS-FIX-WHEN-M1-FILE-CONTENTS-P))
 (1134 143 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (1056 1056 (:TYPE-PRESCRIPTION HIFAT-PLACE-FILE-OF-APPEND-LEMMA-1))
 (1054 261 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (880 176 (:REWRITE M1-FILE-CONTENTS-P-CORRECTNESS-1))
 (577 289 (:REWRITE DEFAULT-<-2))
 (554 190 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (528 528 (:TYPE-PRESCRIPTION M1-FILE))
 (528 176 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (520 520 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (516 516 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (378 378 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (352 176 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (340 340 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (290 289 (:REWRITE DEFAULT-<-1))
 (276 46 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (238 34 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE->CONTENTS-OF-HIFAT-FIND-FILE-LEMMA-1))
 (189 189 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (176 176 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (176 176 (:TYPE-PRESCRIPTION D-E-P))
 (176 176 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-1))
 (176 176 (:REWRITE D-E-P-OF-M1-FILE->D-E))
 (74 74 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (56 56 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (13 4 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (8 8 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-3))
 (8 8 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-1))
 (7 1 (:DEFINITION LEN))
 (4 4 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 (3 1 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (3 1 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2 2 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER))
 (1 1 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(M1-FILE-HIFAT-FILE-ALIST-FIX)
(M1-FILE-HIFAT-FILE-ALIST-FIX-CONGRUENCE-LEMMA-1
 (37505 90 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (17111 3820 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (12412 354 (:DEFINITION MEMBER-EQUAL))
 (12078 668 (:REWRITE SUBSETP-CAR-MEMBER))
 (7214 156 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (6816 158 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (6040 542 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (4876 142 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (4754 200 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (4410 180 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (4396 142 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (2636 2012 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2636 2012 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2446 2348 (:REWRITE DEFAULT-CAR))
 (2136 84 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (2066 2066 (:REWRITE SUBSETP-TRANS2))
 (2066 2066 (:REWRITE SUBSETP-TRANS))
 (1714 1714 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1564 1492 (:REWRITE DEFAULT-CDR))
 (1376 688 (:REWRITE SET-EQUIV-ASYM))
 (1236 84 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (1176 36 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE-FIX))
 (1050 20 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (1020 20 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (746 410 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (708 708 (:REWRITE SUBSETP-MEMBER . 2))
 (708 708 (:REWRITE SUBSETP-MEMBER . 1))
 (688 688 (:TYPE-PRESCRIPTION SET-EQUIV))
 (688 688 (:REWRITE SUBSETP-OF-CDR))
 (658 38 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (642 58 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (582 396 (:REWRITE MEMBER-WHEN-ATOM))
 (574 574 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (564 188 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (556 28 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-29))
 (548 66 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (528 74 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (474 158 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (396 396 (:REWRITE SUBSETP-MEMBER . 4))
 (396 396 (:REWRITE SUBSETP-MEMBER . 3))
 (396 396 (:REWRITE INTERSECTP-MEMBER . 3))
 (396 396 (:REWRITE INTERSECTP-MEMBER . 2))
 (352 54 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (342 114 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (268 130 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (190 190 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (184 184 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (178 178 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (178 178 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (148 148 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (148 148 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (116 116 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (116 116 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (108 108 (:TYPE-PRESCRIPTION NONEMPTY-STRING-LISTP))
 (108 108 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (96 96 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (74 74 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (60 12 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (54 54 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (40 24 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (28 28 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (16 16 (:REWRITE CONS-CAR-CDR))
 (12 12 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (12 12 (:REWRITE M1-FILE->D-E$INLINE-OF-M1-FILE-FIX-X))
 (12 12 (:REWRITE M1-FILE->CONTENTS$INLINE-OF-M1-FILE-FIX-X))
 (4 4 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 )
(M1-FILE-HIFAT-FILE-ALIST-FIX-CONGRUENCE
 (6 2 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (4 4 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 )
(M1-FILE-HIFAT-FILE-ALIST-FIX-NORMALISATION
 (6 2 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (4 4 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 )
(M1-FILE->CONTENTS-OF-M1-FILE-HIFAT-FILE-ALIST-FIX
 (4 2 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (2 2 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (2 1 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 )
(M1-FILE-P-OF-M1-FILE-HIFAT-FILE-ALIST-FIX)
(M1-DIRECTORY-FILE-P-OF-M1-FILE-HIFAT-FILE-ALIST-FIX)
(M1-FILE->D-E-OF-M1-FILE-HIFAT-FILE-ALIST-FIX)
(NOT-M1-REGULAR-FILE-P-OF-M1-FILE-HIFAT-FILE-ALIST-FIX)
(ABS-MKDIR-CORRECTNESS-LEMMA-36
 (79 2 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (76 1 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (32 6 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (26 25 (:REWRITE DEFAULT-CDR))
 (21 20 (:REWRITE DEFAULT-CAR))
 (21 6 (:REWRITE HONS-DUPLICITY-ALIST-P-OF-CONS))
 (15 5 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (12 12 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (10 10 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (7 6 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (6 6 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (5 5 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (4 2 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (3 3 (:TYPE-PRESCRIPTION M1-DIRECTORY-FILE-P))
 (3 3 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (3 1 (:DEFINITION NATP))
 (2 2 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (2 2 (:TYPE-PRESCRIPTION ALISTP))
 (1 1 (:TYPE-PRESCRIPTION M1-FILE-P))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(ABS-PWRITE-CORRECTNESS-LEMMA-13
 (12 2 (:REWRITE M1-FILE-FIX-WHEN-M1-FILE-P))
 (12 2 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (6 6 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (6 2 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (5 1 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (4 4 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (3 3 (:TYPE-PRESCRIPTION M1-FILE-P))
 (3 1 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (2 1 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 )
(ABS-PWRITE-CORRECTNESS-LEMMA-11
 (53312 632 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (50231 2326 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (13956 13956 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (11400 680 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (9726 9726 (:REWRITE DEFAULT-CDR))
 (9360 360 (:REWRITE EQUAL-OF-M1-FILE))
 (9044 952 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (7586 200 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (6993 204 (:DEFINITION STRING-LISTP))
 (5936 424 (:REWRITE ZP-OPEN))
 (3825 492 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (3611 381 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (3240 360 (:REWRITE M1-FILE-CONTENTS-FIX-WHEN-M1-FILE-CONTENTS-P))
 (3076 3076 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (2888 205 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (2888 205 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (2740 376 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (2072 2072 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (1863 205 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (1800 360 (:REWRITE M1-FILE-CONTENTS-P-CORRECTNESS-1))
 (1709 861 (:REWRITE DEFAULT-<-2))
 (1620 540 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (1476 1476 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (1405 1405 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (1320 1320 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (1274 1274 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (1200 200 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (1128 376 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (1080 1080 (:TYPE-PRESCRIPTION M1-FILE))
 (1080 360 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (1068 356 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (1064 1064 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (1000 200 (:REWRITE TRUE-LISTP-WHEN-D-E-P))
 (996 996 (:TYPE-PRESCRIPTION STRING-LISTP))
 (874 861 (:REWRITE DEFAULT-<-1))
 (873 145 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (800 120 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE->CONTENTS-OF-HIFAT-FIND-FILE-LEMMA-1))
 (760 760 (:TYPE-PRESCRIPTION D-E-P))
 (738 738 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (720 360 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (637 637 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (633 105 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (620 620 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (410 410 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (410 410 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (400 400 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (400 400 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (400 200 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (360 360 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (360 360 (:REWRITE M1-FILE->CONTENTS$INLINE-OF-M1-FILE-FIX-X))
 (360 360 (:REWRITE D-E-P-OF-M1-FILE->D-E))
 (310 310 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (242 231 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (234 234 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (200 200 (:TYPE-PRESCRIPTION SET::EMPTYP-TYPE))
 (200 200 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (200 200 (:REWRITE SET::IN-SET))
 (120 120 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (100 100 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-3))
 (100 100 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-1))
 (73 13 (:DEFINITION LEN))
 (52 52 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (39 13 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (39 13 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (26 26 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (26 13 (:REWRITE DEFAULT-+-2))
 (13 13 (:REWRITE DEFAULT-+-1))
 (13 13 (:LINEAR POSITION-WHEN-MEMBER))
 (13 13 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 1 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 )
(HIFAT-TO-LOFAT-INVERSION-LEMMA-6
 (31 8 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (12 12 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (12 2 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (8 8 (:REWRITE SUBSETP-TRANS2))
 (8 8 (:REWRITE SUBSETP-TRANS))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 2 (:REWRITE HIFAT-EQUIV-OF-CONS-LEMMA-2))
 (6 6 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (6 6 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (6 2 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (6 2 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (4 4 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (4 4 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-3
 (13844 148 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (7404 132 (:REWRITE EQUAL-OF-M1-FILE))
 (6588 214 (:DEFINITION PUT-ASSOC-EQUAL))
 (5774 697 (:DEFINITION ASSOC-EQUAL))
 (5392 284 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (3343 3343 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (3053 335 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (2896 2896 (:REWRITE DEFAULT-CAR))
 (1971 1971 (:REWRITE DEFAULT-CDR))
 (1479 163 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (1372 98 (:REWRITE ZP-OPEN))
 (1340 1340 (:TYPE-PRESCRIPTION HIFAT-PLACE-FILE-OF-APPEND-LEMMA-1))
 (1226 1226 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (1206 134 (:REWRITE M1-FILE-CONTENTS-FIX-WHEN-M1-FILE-CONTENTS-P))
 (1028 1028 (:TYPE-PRESCRIPTION HIFAT-PLACE-FILE-CORRECTNESS-1 . 2))
 (930 134 (:REWRITE HIFAT-NO-DUPS-P-OF-HIFAT-PLACE-FILE))
 (852 116 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (670 134 (:REWRITE M1-FILE-CONTENTS-P-CORRECTNESS-1))
 (540 192 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (530 106 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (405 405 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (397 397 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (396 396 (:TYPE-PRESCRIPTION M1-FILE))
 (396 132 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (395 199 (:REWRITE DEFAULT-<-2))
 (284 284 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (268 134 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (263 263 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (240 240 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (202 199 (:REWRITE DEFAULT-<-1))
 (174 6 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 2))
 (156 26 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (142 142 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (134 134 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (134 134 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-1))
 (132 132 (:TYPE-PRESCRIPTION D-E-P))
 (132 132 (:REWRITE D-E-P-OF-M1-FILE->D-E))
 (58 58 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (49 49 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (21 3 (:DEFINITION LEN))
 (20 2 (:REWRITE M1-FILE->CONTENTS-OF-M1-FILE))
 (18 18 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-1))
 (12 12 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (9 3 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (9 3 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (8 4 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (6 6 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-LEMMA-3))
 (6 6 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (6 3 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 (3 3 (:REWRITE DEFAULT-+-1))
 (3 3 (:LINEAR POSITION-WHEN-MEMBER))
 (3 3 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6
 (8799 40 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (8479 1600 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (7569 101 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (7371 24 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (6809 440 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (2293 1032 (:REWRITE DEFAULT-CDR))
 (1587 31 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1520 1520 (:REWRITE SUBSETP-TRANS2))
 (1520 1520 (:REWRITE SUBSETP-TRANS))
 (1520 76 (:REWRITE SUBSETP-CAR-MEMBER))
 (1497 1497 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1497 1497 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1429 1429 (:REWRITE DEFAULT-CAR))
 (1342 38 (:DEFINITION MEMBER-EQUAL))
 (1197 63 (:REWRITE LENGTH-WHEN-STRINGP))
 (693 63 (:DEFINITION LEN))
 (630 63 (:DEFINITION UNSIGNED-BYTE-P))
 (591 63 (:DEFINITION ALISTP))
 (567 63 (:DEFINITION INTEGER-RANGE-P))
 (504 126 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (488 58 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-29))
 (432 432 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (404 84 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (378 63 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (309 1 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (262 24 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (252 252 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (252 126 (:REWRITE DEFAULT-<-1))
 (252 63 (:DEFINITION STRIP-CARS))
 (226 226 (:TYPE-PRESCRIPTION STRIP-CARS))
 (189 189 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (189 126 (:REWRITE STR::CONSP-OF-EXPLODE))
 (168 56 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (160 160 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (160 160 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (126 126 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (126 126 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (126 126 (:REWRITE DEFAULT-<-2))
 (126 126 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (126 63 (:REWRITE DEFAULT-+-2))
 (126 63 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (113 113 (:TYPE-PRESCRIPTION D-E-P))
 (98 98 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (76 76 (:REWRITE SUBSETP-MEMBER . 2))
 (76 76 (:REWRITE SUBSETP-MEMBER . 1))
 (64 32 (:REWRITE SET-EQUIV-ASYM))
 (63 63 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (63 63 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (63 63 (:REWRITE DEFAULT-+-1))
 (63 21 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (55 55 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (53 11 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (32 32 (:TYPE-PRESCRIPTION SET-EQUIV))
 (32 32 (:REWRITE SUBSETP-OF-CDR))
 (23 23 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (23 23 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (14 14 (:REWRITE SUBSETP-MEMBER . 4))
 (14 14 (:REWRITE SUBSETP-MEMBER . 3))
 (14 14 (:REWRITE MEMBER-WHEN-ATOM))
 (14 14 (:REWRITE INTERSECTP-MEMBER . 3))
 (14 14 (:REWRITE INTERSECTP-MEMBER . 2))
 )
(HIFAT-FIND-FILE-CORRECTNESS-LEMMA-8
 (19242 54 (:DEFINITION M1-FILE-ALIST-P))
 (8857 1902 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (6048 162 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (4314 384 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (2710 2710 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (1902 1902 (:REWRITE SUBSETP-TRANS2))
 (1902 1902 (:REWRITE SUBSETP-TRANS))
 (1900 1900 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1900 1900 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1779 167 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (1427 1427 (:REWRITE DEFAULT-CAR))
 (1344 202 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (1323 54 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (1260 1260 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (1026 54 (:REWRITE LENGTH-WHEN-STRINGP))
 (1016 9 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (714 4 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE-FIX))
 (594 54 (:DEFINITION LEN))
 (540 54 (:DEFINITION UNSIGNED-BYTE-P))
 (498 498 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (486 54 (:DEFINITION INTEGER-RANGE-P))
 (448 448 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (432 108 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (381 54 (:DEFINITION ALISTP))
 (358 70 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (295 59 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (268 74 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (224 224 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (216 216 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (216 108 (:REWRITE DEFAULT-<-1))
 (216 54 (:DEFINITION STRIP-CARS))
 (162 162 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (162 108 (:REWRITE STR::CONSP-OF-EXPLODE))
 (132 22 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (118 118 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (118 118 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (118 118 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (110 110 (:TYPE-PRESCRIPTION STRIP-CARS))
 (108 108 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (108 108 (:REWRITE DEFAULT-<-2))
 (108 108 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (108 54 (:REWRITE DEFAULT-+-2))
 (108 54 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (86 9 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (68 68 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (67 23 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (61 61 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (55 55 (:TYPE-PRESCRIPTION D-E-P))
 (54 54 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (54 54 (:REWRITE DEFAULT-+-1))
 (27 9 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (8 8 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (4 4 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (2 2 (:REWRITE M1-FILE-ALIST-P-OF-HIFAT-FILE-ALIST-FIX))
 )
(HIFAT-EQUIV-IMPLIES-EQUAL-M1-REGULAR-FILE-P-MV-NTH-0-HIFAT-FIND-FILE-2
 (165 15 (:DEFINITION LEN))
 (152 4 (:DEFINITION UNSIGNED-BYTE-P))
 (148 4 (:DEFINITION INTEGER-RANGE-P))
 (119 43 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (116 14 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (94 4 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (84 4 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (60 15 (:REWRITE DEFAULT-CDR))
 (57 21 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (45 45 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (45 30 (:REWRITE STR::CONSP-OF-EXPLODE))
 (44 28 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (39 39 (:TYPE-PRESCRIPTION LEN))
 (38 38 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (38 38 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (36 9 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (30 15 (:REWRITE DEFAULT-+-2))
 (16 16 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (15 15 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (15 15 (:REWRITE DEFAULT-+-1))
 (12 4 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (12 4 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (8 8 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (8 8 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (8 8 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (8 4 (:LINEAR M1-REGULAR-FILE-P-CORRECTNESS-2))
 (4 4 (:TYPE-PRESCRIPTION M1-FILE-P))
 (4 4 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (4 4 (:REWRITE M1-FILE-CONTENTS-P-OF-M1-FILE->CONTENTS))
 (4 4 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 )
(HIFAT-FIND-FILE-CORRECTNESS-LEMMA-9
 (9520 28 (:DEFINITION M1-FILE-ALIST-P))
 (8279 1803 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (5509 117 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (4666 172 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (3196 262 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (2900 399 (:DEFINITION ASSOC-EQUAL))
 (2828 84 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (2785 2785 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (2239 172 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (2212 196 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (2118 274 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (2112 2112 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (1803 1803 (:REWRITE SUBSETP-TRANS2))
 (1803 1803 (:REWRITE SUBSETP-TRANS))
 (1802 1802 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1802 1802 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1711 1711 (:REWRITE DEFAULT-CAR))
 (706 706 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (700 700 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (616 28 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (550 110 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (544 544 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (532 28 (:REWRITE LENGTH-WHEN-STRINGP))
 (474 79 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (353 353 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (348 36 (:DEFINITION LEN))
 (340 114 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (280 28 (:DEFINITION UNSIGNED-BYTE-P))
 (252 28 (:DEFINITION INTEGER-RANGE-P))
 (246 82 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (224 56 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (220 220 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (208 19 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (196 28 (:DEFINITION ALISTP))
 (140 28 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (112 112 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (112 56 (:REWRITE DEFAULT-<-1))
 (112 28 (:DEFINITION STRIP-CARS))
 (107 107 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (84 84 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (84 56 (:REWRITE STR::CONSP-OF-EXPLODE))
 (72 36 (:REWRITE DEFAULT-+-2))
 (56 56 (:TYPE-PRESCRIPTION STRIP-CARS))
 (56 56 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (56 56 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (56 56 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (56 56 (:REWRITE DEFAULT-<-2))
 (56 56 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (56 28 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (36 36 (:REWRITE DEFAULT-+-1))
 (28 28 (:TYPE-PRESCRIPTION D-E-P))
 (28 28 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (24 24 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (9 3 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 )
(HIFAT-FIND-FILE-CORRECTNESS-LEMMA-10
 (242 22 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (203 22 (:DEFINITION ASSOC-EQUAL))
 (162 162 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (132 22 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (98 7 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (88 88 (:REWRITE DEFAULT-CAR))
 (86 86 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (75 25 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (54 54 (:REWRITE DEFAULT-CDR))
 (44 44 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (35 7 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (35 7 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (28 28 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (22 22 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (21 7 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (10 2 (:DEFINITION LEN))
 (8 8 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (7 7 (:TYPE-PRESCRIPTION M1-FILE-P))
 (7 7 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (5 5 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (5 5 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (5 5 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 )
(HIFAT-EQUIV-IMPLIES-EQUAL-MV-NTH-1-HIFAT-FIND-FILE-2
 (54 12 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (12 12 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (6 2 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (4 1 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 )
(HIFAT-FIND-FILE-CORRECTNESS-3
 (84 10 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (57 21 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (36 9 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (30 6 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (30 6 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (18 6 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (12 12 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (12 12 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (12 12 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (12 12 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 )
(HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-1
 (91607 128 (:DEFINITION HIFAT-SUBSETP))
 (62904 648 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (51182 250 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (41279 5556 (:DEFINITION ASSOC-EQUAL))
 (34920 1164 (:DEFINITION PUT-ASSOC-EQUAL))
 (33121 7166 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (26279 26279 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (22230 22222 (:REWRITE DEFAULT-CAR))
 (15774 13788 (:REWRITE DEFAULT-CDR))
 (13281 571 (:REWRITE SUBSETP-CAR-MEMBER))
 (11316 280 (:DEFINITION MEMBER-EQUAL))
 (9622 78 (:DEFINITION REMOVE-ASSOC-EQUAL))
 (9281 234 (:REWRITE REMOVE-ASSOC-WHEN-ABSENT-1))
 (8473 153 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (6998 6998 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (6860 6860 (:REWRITE SUBSETP-TRANS2))
 (6860 6860 (:REWRITE SUBSETP-TRANS))
 (6856 6600 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (6856 6600 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (6272 448 (:REWRITE ZP-OPEN))
 (5216 574 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (4938 328 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (3492 3492 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (3306 409 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (2509 490 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (2087 729 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (1860 1860 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (1792 896 (:REWRITE DEFAULT-<-2))
 (1479 708 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (1098 1098 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (1088 1088 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (1068 1068 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (912 152 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (896 896 (:REWRITE DEFAULT-<-1))
 (587 128 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (560 560 (:REWRITE SUBSETP-MEMBER . 2))
 (560 560 (:REWRITE SUBSETP-MEMBER . 1))
 (549 549 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (423 18 (:REWRITE MEMBER-OF-PUT-ASSOC))
 (244 244 (:TYPE-PRESCRIPTION PUT-ASSOC-EQUAL))
 (240 120 (:REWRITE SET-EQUIV-ASYM))
 (222 222 (:REWRITE CONSP-OF-REMOVE-ASSOC-1))
 (216 168 (:REWRITE MEMBER-WHEN-ATOM))
 (209 14 (:REWRITE M1-FILE-ALIST-P-OF-PUT-ASSOC))
 (168 168 (:REWRITE SUBSETP-MEMBER . 4))
 (168 168 (:REWRITE SUBSETP-MEMBER . 3))
 (168 168 (:REWRITE INTERSECTP-MEMBER . 3))
 (168 168 (:REWRITE INTERSECTP-MEMBER . 2))
 (132 72 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (126 126 (:REWRITE SUBSETP-OF-CDR))
 (120 120 (:TYPE-PRESCRIPTION SET-EQUIV))
 (110 10 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (60 10 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (44 28 (:DEFINITION NULL))
 (40 4 (:DEFINITION ALISTP))
 (36 36 (:REWRITE M1-FILE-ALIST-P-OF-HIFAT-FILE-ALIST-FIX))
 (32 8 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (28 28 (:TYPE-PRESCRIPTION NULL))
 (20 20 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (20 20 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (20 20 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (16 16 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (10 10 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (10 10 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (8 8 (:REWRITE M1-FILE-P-OF-M1-FILE-HIFAT-FILE-ALIST-FIX))
 (8 8 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-PLACE-FILE-CORRECTNESS-4
 (14645 18 (:DEFINITION HIFAT-PLACE-FILE))
 (5485 60 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (4194 216 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (3771 414 (:DEFINITION ASSOC-EQUAL))
 (3456 108 (:DEFINITION PUT-ASSOC-EQUAL))
 (3096 684 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (2286 36 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (1926 1926 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (1674 126 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (1584 1584 (:REWRITE DEFAULT-CAR))
 (1440 207 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (1359 1017 (:REWRITE DEFAULT-CDR))
 (954 63 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (864 54 (:REWRITE M1-FILE-HIFAT-FILE-ALIST-FIX-NORMALISATION))
 (744 744 (:TYPE-PRESCRIPTION ZP))
 (684 684 (:TYPE-PRESCRIPTION LEN))
 (684 36 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (666 54 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (588 42 (:REWRITE ZP-OPEN))
 (576 54 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE-FIX))
 (495 99 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (456 456 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (432 432 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (414 54 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (396 54 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (396 36 (:REWRITE M1-FILE-FIX-WHEN-M1-FILE-P))
 (270 54 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (261 261 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (234 234 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (225 45 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-29))
 (216 216 (:TYPE-PRESCRIPTION M1-FILE-HIFAT-FILE-ALIST-FIX))
 (198 198 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (198 198 (:REWRITE FAT32-FILENAME-P-OF-FAT32-FILENAME-FIX))
 (198 18 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (180 180 (:TYPE-PRESCRIPTION M1-FILE-P))
 (171 57 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (168 84 (:REWRITE DEFAULT-<-2))
 (162 54 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (108 108 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (108 36 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (108 18 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (102 102 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (84 84 (:REWRITE DEFAULT-<-1))
 (54 54 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (54 54 (:REWRITE M1-FILE->CONTENTS$INLINE-OF-M1-FILE-FIX-X))
 (41 11 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (36 36 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (36 36 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (36 36 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (18 18 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (18 18 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-EQUIV-IMPLIES-EQUAL-M1-DIRECTORY-FILE-P-MV-NTH-0-HIFAT-FIND-FILE-2
 (2488 46 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (2378 57 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (2268 16 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (1445 152 (:DEFINITION ASSOC-EQUAL))
 (1303 51 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (1202 1202 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (833 320 (:REWRITE DEFAULT-CDR))
 (532 532 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (500 500 (:REWRITE DEFAULT-CAR))
 (454 44 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (272 16 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (246 41 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (208 208 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (175 35 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (168 16 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (82 82 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (77 77 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (66 18 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (43 43 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (41 41 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (40 8 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (18 18 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (16 16 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (16 16 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (16 16 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (12 4 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (8 8 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (8 8 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (8 8 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (5 1 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (4 4 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (3 1 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 )
(ABS-PWRITE-CORRECTNESS-LEMMA-22
 (6280 405 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (6175 1217 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (5075 160 (:REWRITE SUBSETP-CAR-MEMBER))
 (4523 215 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (3284 102 (:DEFINITION MEMBER-EQUAL))
 (2892 172 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (2881 48 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (2291 69 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (1790 111 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1351 185 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-29))
 (1307 21 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1160 1160 (:REWRITE SUBSETP-TRANS2))
 (1160 1160 (:REWRITE SUBSETP-TRANS))
 (1045 35 (:REWRITE SUBSETP-OF-CONS))
 (996 996 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (977 977 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (977 977 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (961 733 (:REWRITE DEFAULT-CDR))
 (945 69 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (824 196 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (600 10 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (549 183 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (544 68 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (243 81 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (226 90 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (222 222 (:REWRITE SUBSETP-MEMBER . 2))
 (215 215 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (208 208 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (178 70 (:REWRITE HIFAT-EQUIV-OF-CONS-LEMMA-4))
 (146 22 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (132 132 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (102 9 (:DEFINITION ALISTP))
 (99 99 (:REWRITE SUBSETP-MEMBER . 4))
 (99 99 (:REWRITE INTERSECTP-MEMBER . 3))
 (99 99 (:REWRITE INTERSECTP-MEMBER . 2))
 (80 80 (:REWRITE MEMBER-WHEN-ATOM))
 (68 17 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (67 67 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (53 5 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (44 44 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (44 44 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (36 6 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (36 6 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (34 34 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (22 22 (:TYPE-PRESCRIPTION SET-EQUIV))
 (22 8 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (17 17 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (17 5 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (16 16 (:REWRITE SUBSETP-OF-CDR))
 (13 3 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE->CONTENTS-OF-HIFAT-FIND-FILE-LEMMA-1))
 (12 12 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (12 12 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (12 6 (:REWRITE SET-EQUIV-ASYM))
 (6 6 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (6 6 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (6 1 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-3))
 (4 4 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-FIX-UNDER-FAT32-FILENAME-EQUIV))
 )
(ABS-PWRITE-CORRECTNESS-LEMMA-23
 (7189 201 (:REWRITE M1-FILE-HIFAT-FILE-ALIST-FIX-NORMALISATION))
 (6645 2130 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (6543 353 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE->CONTENTS))
 (5574 178 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (4535 884 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (4479 266 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (4250 12 (:REWRITE HIFAT-EQUIV-OF-CONS-LEMMA-4))
 (4083 260 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (3291 2523 (:REWRITE DEFAULT-CAR))
 (3144 100 (:REWRITE SUBSETP-CAR-MEMBER))
 (3066 156 (:REWRITE M1-FILE-ALIST-P-OF-PUT-ASSOC))
 (2809 403 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (2636 73 (:DEFINITION MEMBER-EQUAL))
 (2580 26 (:DEFINITION UNSIGNED-BYTE-P))
 (2554 26 (:DEFINITION INTEGER-RANGE-P))
 (2515 1607 (:REWRITE DEFAULT-CDR))
 (2179 2179 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (2161 45 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1641 12 (:REWRITE M1-FILE-ALIST-P-OF-CONS))
 (1605 1065 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (1565 155 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (1533 1325 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (1426 151 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (1426 12 (:DEFINITION HIFAT-NO-DUPS-P))
 (1374 38 (:LINEAR LEN-OF-EXPLODE-OF-M1-FILE-CONTENTS-FIX))
 (1350 157 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (1308 884 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1308 884 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1296 112 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1211 90 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (1126 50 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (968 88 (:DEFINITION LEN))
 (950 50 (:REWRITE LENGTH-WHEN-STRINGP))
 (884 884 (:REWRITE SUBSETP-TRANS2))
 (884 884 (:REWRITE SUBSETP-TRANS))
 (858 858 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (857 171 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (834 62 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 (690 74 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-29))
 (629 50 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (605 203 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (576 24 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (530 118 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (314 314 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (313 157 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (286 52 (:REWRITE MEMBER-WHEN-ATOM))
 (276 276 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (264 264 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (264 176 (:REWRITE STR::CONSP-OF-EXPLODE))
 (261 261 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (211 163 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (190 38 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (176 88 (:REWRITE DEFAULT-+-2))
 (172 172 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (172 172 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (152 152 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (146 146 (:REWRITE SUBSETP-MEMBER . 2))
 (146 146 (:REWRITE SUBSETP-MEMBER . 1))
 (115 115 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (114 38 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (114 38 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (106 106 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-FIX))
 (100 50 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (88 88 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (88 88 (:REWRITE DEFAULT-+-1))
 (86 62 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (76 76 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (68 6 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (52 52 (:REWRITE SUBSETP-MEMBER . 4))
 (52 52 (:REWRITE SUBSETP-MEMBER . 3))
 (52 52 (:REWRITE INTERSECTP-MEMBER . 3))
 (52 52 (:REWRITE INTERSECTP-MEMBER . 2))
 (48 48 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (48 24 (:REWRITE DEFAULT-<-1))
 (24 24 (:REWRITE DEFAULT-<-2))
 (24 24 (:LINEAR POSITION-WHEN-MEMBER))
 (24 24 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (23 23 (:REWRITE CONS-CAR-CDR))
 (12 12 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (12 12 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (10 10 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-3))
 (10 10 (:REWRITE PUT-ASSOC-UNDER-HIFAT-EQUIV-1))
 (6 6 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (2 2 (:REWRITE-QUOTED-CONSTANT M1-FILE-FIX-UNDER-M1-FILE-EQUIV))
 )
(HIFAT-PWRITE-CORRECTNESS-LEMMA-1
 (5994 16 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 2))
 (5452 160 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (4738 436 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (3350 742 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (3146 286 (:DEFINITION LEN))
 (2854 317 (:DEFINITION ASSOC-EQUAL))
 (2650 74 (:REWRITE EQUAL-OF-M1-FILE))
 (2560 80 (:DEFINITION PUT-ASSOC-EQUAL))
 (1992 456 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (1934 1076 (:REWRITE DEFAULT-CDR))
 (1932 112 (:REWRITE M1-FILE-HIFAT-FILE-ALIST-FIX-NORMALISATION))
 (1716 1716 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (1489 175 (:REWRITE HIFAT-FILE-ALIST-FIX-WHEN-HIFAT-NO-DUPS-P))
 (1323 1323 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (1276 1276 (:REWRITE DEFAULT-CAR))
 (1200 60 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (1164 44 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (964 60 (:REWRITE HIFAT-NO-DUPS-P-OF-HIFAT-PLACE-FILE))
 (935 85 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (858 858 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (858 572 (:REWRITE STR::CONSP-OF-EXPLODE))
 (840 60 (:REWRITE ZP-OPEN))
 (768 768 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (768 768 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (600 600 (:TYPE-PRESCRIPTION HIFAT-PLACE-FILE-OF-APPEND-LEMMA-1))
 (572 286 (:REWRITE DEFAULT-+-2))
 (526 86 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-2))
 (510 85 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (472 472 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (430 86 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (400 400 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-FIX))
 (360 360 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (354 118 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (354 118 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (328 208 (:REWRITE DEFAULT-<-2))
 (292 208 (:REWRITE DEFAULT-<-1))
 (286 286 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (286 286 (:REWRITE DEFAULT-+-1))
 (250 74 (:REWRITE D-E-FIX-WHEN-D-E-P))
 (236 236 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (170 170 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (161 161 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (152 152 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (152 152 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-4))
 (91 91 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (88 88 (:TYPE-PRESCRIPTION D-E-P))
 (85 85 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (76 76 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (60 60 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-1))
 (60 60 (:REWRITE D-E-P-OF-M1-FILE->D-E))
 (58 20 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (56 56 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-D-E-FIX))
 (56 56 (:TYPE-PRESCRIPTION M1-FILE->D-E$INLINE))
 (44 44 (:LINEAR POSITION-WHEN-MEMBER))
 (44 44 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (32 32 (:TYPE-PRESCRIPTION HIFAT-EQUIV))
 (31 31 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (28 28 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (11 11 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (8 4 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )