(DIRNAME
 (204 2 (:DEFINITION TAKE))
 (140 4 (:REWRITE TAKE-OF-TOO-MANY))
 (104 4 (:REWRITE TAKE-OF-LEN-FREE))
 (60 12 (:DEFINITION LEN))
 (55 5 (:REWRITE NFIX-WHEN-ZP))
 (54 6 (:REWRITE ZP-OPEN))
 (52 52 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (31 19 (:REWRITE DEFAULT-+-2))
 (30 10 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (30 10 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (20 20 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (20 16 (:REWRITE DEFAULT-<-2))
 (20 3 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (19 19 (:REWRITE DEFAULT-+-1))
 (18 6 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (16 16 (:REWRITE DEFAULT-<-1))
 (14 14 (:REWRITE DEFAULT-CDR))
 (12 3 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (11 2 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (11 2 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (10 10 (:LINEAR POSITION-WHEN-MEMBER))
 (10 10 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (4 4 (:TYPE-PRESCRIPTION ZP))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:REWRITE TAKE-WHEN-ATOM))
 (3 3 (:REWRITE SUBSETP-TRANS2))
 (3 3 (:REWRITE SUBSETP-TRANS))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 2 (:DEFINITION NATP))
 )
(FAT32-FILENAME-LIST-P-OF-DIRNAME)
(FAT32-FILENAME-LIST-EQUIV-IMPLIES-EQUAL-DIRNAME-1
 (226 2 (:DEFINITION TAKE))
 (162 4 (:REWRITE TAKE-OF-TOO-MANY))
 (114 4 (:REWRITE TAKE-OF-LEN-FREE))
 (76 6 (:REWRITE ZP-OPEN))
 (76 4 (:REWRITE NFIX-WHEN-ZP))
 (60 60 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (50 10 (:DEFINITION LEN))
 (36 12 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (36 12 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (28 18 (:REWRITE DEFAULT-+-2))
 (25 2 (:REWRITE FAT32-FILENAME-LIST-FIX-WHEN-FAT32-FILENAME-LIST-P))
 (24 24 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (20 16 (:REWRITE DEFAULT-<-2))
 (18 18 (:REWRITE DEFAULT-+-1))
 (18 6 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (16 16 (:REWRITE DEFAULT-<-1))
 (12 12 (:REWRITE DEFAULT-CDR))
 (12 12 (:LINEAR POSITION-WHEN-MEMBER))
 (12 12 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (10 1 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (8 4 (:REWRITE NFIX-WHEN-NATP))
 (6 6 (:TYPE-PRESCRIPTION TRUE-LISTP-TAKE))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (4 4 (:TYPE-PRESCRIPTION ZP))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (4 4 (:REWRITE TAKE-WHEN-ATOM))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 2 (:DEFINITION NATP))
 (1 1 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 )
(LEN-OF-DIRNAME
 (113 1 (:DEFINITION TAKE))
 (81 2 (:REWRITE TAKE-OF-TOO-MANY))
 (73 4 (:REWRITE NFIX-WHEN-ZP))
 (67 5 (:REWRITE ZP-OPEN))
 (61 11 (:DEFINITION LEN))
 (57 2 (:REWRITE TAKE-OF-LEN-FREE))
 (46 46 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (31 19 (:REWRITE DEFAULT-+-2))
 (30 10 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (30 10 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (22 2 (:DEFINITION NATP))
 (20 20 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (19 19 (:REWRITE DEFAULT-+-1))
 (19 15 (:REWRITE DEFAULT-<-2))
 (17 15 (:REWRITE DEFAULT-<-1))
 (12 12 (:REWRITE DEFAULT-CDR))
 (10 10 (:LINEAR POSITION-WHEN-MEMBER))
 (10 10 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (9 3 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (4 4 (:TYPE-PRESCRIPTION ZP))
 (4 4 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:TYPE-PRESCRIPTION TRUE-LISTP-TAKE))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (2 2 (:REWRITE TAKE-WHEN-ATOM))
 (1 1 (:REWRITE DEFAULT-CAR))
 )
(CONSP-OF-DIRNAME
 (275 6 (:REWRITE TAKE-OF-TOO-MANY))
 (200 2 (:REWRITE TAKE-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (164 4 (:REWRITE ABS-PLACE-FILE-HELPER-OF-CTX-APP-LEMMA-1))
 (145 6 (:REWRITE TAKE-OF-LEN-FREE))
 (144 75 (:REWRITE DEFAULT-+-2))
 (126 2 (:DEFINITION FAT32-FILENAME-LIST-PREFIXP))
 (104 6 (:REWRITE NFIX-WHEN-ZP))
 (100 7 (:REWRITE ZP-OPEN))
 (83 83 (:REWRITE DEFAULT-CDR))
 (76 75 (:REWRITE DEFAULT-+-1))
 (42 42 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (39 24 (:REWRITE DEFAULT-<-2))
 (31 24 (:REWRITE DEFAULT-<-1))
 (21 7 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (21 7 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (21 7 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (14 14 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (12 12 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-PREFIXP))
 (11 6 (:REWRITE NFIX-WHEN-NATP))
 (8 8 (:REWRITE DEFAULT-CAR))
 (7 7 (:LINEAR POSITION-WHEN-MEMBER))
 (7 7 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 6 (:TYPE-PRESCRIPTION NFIX))
 (6 6 (:REWRITE TAKE-WHEN-ATOM))
 (5 5 (:TYPE-PRESCRIPTION ZP))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 2))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (4 2 (:REWRITE LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (3 3 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:DEFINITION NATP))
 )
(PREFIXP-OF-DIRNAME
 (3946 36 (:REWRITE LEN-WHEN-PREFIXP))
 (1913 40 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (1718 40 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (1356 45 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (1107 34 (:REWRITE TAKE-OF-TOO-MANY))
 (785 34 (:REWRITE TAKE-OF-LEN-FREE))
 (696 696 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (661 36 (:REWRITE LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (650 75 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (547 56 (:REWRITE NFIX-WHEN-ZP))
 (428 6 (:DEFINITION TRUE-LISTP))
 (424 12 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (423 237 (:REWRITE DEFAULT-+-2))
 (394 9 (:DEFINITION STRING-LISTP))
 (384 128 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (384 128 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (334 227 (:REWRITE DEFAULT-<-2))
 (316 287 (:REWRITE DEFAULT-CDR))
 (313 227 (:REWRITE DEFAULT-<-1))
 (313 7 (:REWRITE LEN-OF-DIRNAME))
 (303 2 (:REWRITE TAKE-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (276 92 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (256 256 (:LINEAR LEN-WHEN-PREFIXP))
 (237 237 (:REWRITE DEFAULT-+-1))
 (235 3 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (176 176 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (175 9 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (165 9 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (163 22 (:DEFINITION NATP))
 (151 76 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (142 88 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (130 9 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (128 128 (:LINEAR POSITION-WHEN-MEMBER))
 (128 128 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (126 3 (:REWRITE TAKE-WHEN-PREFIXP))
 (120 9 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (115 46 (:REWRITE CONSP-OF-FAT32-FILENAME-LIST-FIX))
 (97 17 (:REWRITE CONSP-OF-TAKE))
 (93 76 (:REWRITE DEFAULT-CAR))
 (83 37 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (80 37 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (78 3 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (76 12 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (75 12 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (68 34 (:REWRITE CDR-OF-FAT32-FILENAME-LIST-FIX-X-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (48 12 (:REWRITE TRUE-LISTP-WHEN-D-E-P))
 (45 45 (:TYPE-PRESCRIPTION STRING-LISTP))
 (42 42 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (40 40 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (40 40 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (40 40 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (40 40 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (37 37 (:TYPE-PRESCRIPTION ZP))
 (36 18 (:REWRITE CAR-OF-FAT32-FILENAME-LIST-FIX-X-UNDER-FAT32-FILENAME-EQUIV))
 (36 3 (:REWRITE FAT32-FILENAME-LIST-FIX-WHEN-FAT32-FILENAME-LIST-P))
 (35 35 (:TYPE-PRESCRIPTION NFIX))
 (34 34 (:REWRITE TAKE-WHEN-ATOM))
 (34 5 (:REWRITE FAT32-FILENAME-LIST-P-OF-TAKE))
 (32 16 (:REWRITE CONSP-OF-DIRNAME))
 (32 5 (:REWRITE CAR-OF-TAKE))
 (30 30 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (22 22 (:TYPE-PRESCRIPTION NATP))
 (21 21 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (21 4 (:REWRITE FAT32-FILENAME-LIST-P-OF-LIST-FIX))
 (18 18 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (18 18 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (18 18 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (18 18 (:TYPE-PRESCRIPTION D-E-P))
 (18 18 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (18 18 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (18 18 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (18 9 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (18 9 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (17 17 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 (14 14 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (13 2 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 (12 12 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 (12 12 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (9 9 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (9 9 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (9 9 (:REWRITE SET::IN-SET))
 (3 3 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (3 3 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (3 3 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (3 3 (:REWRITE CONSP-OF-LIST-FIX))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-OF-SELF))
 )
(BASENAME
 (319 10 (:REWRITE LAST-WHEN-EQUAL-LEN-1))
 (205 5 (:DEFINITION LAST))
 (162 80 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (92 92 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (63 63 (:TYPE-PRESCRIPTION LEN))
 (58 2 (:REWRITE SUBSETP-CAR-MEMBER))
 (54 18 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (54 18 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (46 1 (:DEFINITION MEMBER-EQUAL))
 (45 9 (:DEFINITION LEN))
 (42 7 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (36 36 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (30 10 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (20 20 (:REWRITE DEFAULT-CDR))
 (18 18 (:LINEAR POSITION-WHEN-MEMBER))
 (18 18 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (18 9 (:REWRITE DEFAULT-+-2))
 (18 1 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (17 17 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (15 9 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (15 1 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (13 6 (:REWRITE DEFAULT-CAR))
 (11 6 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (11 6 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 1 (:REWRITE FAT32-FILENAME-LIST-P-OF-LAST))
 (7 7 (:REWRITE SUBSETP-TRANS2))
 (7 7 (:REWRITE SUBSETP-TRANS))
 (4 4 (:REWRITE CONSP-OF-LAST))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (1 1 (:REWRITE SUBSETP-REFL))
 )
(FAT32-FILENAME-P-OF-BASENAME)
(FAT32-FILENAME-LIST-EQUIV-IMPLIES-EQUAL-BASENAME-1
 (36 18 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (18 18 (:TYPE-PRESCRIPTION LAST))
 )
(APPEND-NTHCDR-DIRNAME-BASENAME-LEMMA-1
 (8479 76 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (7111 154 (:REWRITE FAT32-FILENAME-LIST-FIX-WHEN-FAT32-FILENAME-LIST-P))
 (6812 270 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (5985 140 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (5602 155 (:DEFINITION STRING-LISTP))
 (4720 78 (:DEFINITION TRUE-LISTP))
 (3967 265 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (2962 84 (:REWRITE TAKE-OF-TOO-MANY))
 (2394 142 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (2394 142 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (2172 2172 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (2003 197 (:REWRITE NFIX-WHEN-ZP))
 (1920 84 (:REWRITE TAKE-OF-LEN-FREE))
 (1684 142 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (1679 738 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (1577 1126 (:REWRITE DEFAULT-CDR))
 (1476 1476 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (1167 389 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (1167 389 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (1131 717 (:REWRITE DEFAULT-+-2))
 (1120 140 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (924 308 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (832 133 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (778 778 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (768 614 (:REWRITE DEFAULT-<-2))
 (717 717 (:REWRITE DEFAULT-+-1))
 (700 140 (:REWRITE TRUE-LISTP-WHEN-D-E-P))
 (683 614 (:REWRITE DEFAULT-<-1))
 (635 390 (:REWRITE DEFAULT-CAR))
 (618 618 (:TYPE-PRESCRIPTION STRING-LISTP))
 (554 554 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (550 550 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (472 40 (:REWRITE CONSP-OF-NTHCDR))
 (431 9 (:REWRITE CAR-OF-NTHCDR))
 (390 13 (:REWRITE ABS-PLACE-FILE-HELPER-OF-CTX-APP-LEMMA-1))
 (389 389 (:LINEAR POSITION-WHEN-MEMBER))
 (389 389 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (385 22 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (342 18 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (313 49 (:DEFINITION NATP))
 (309 40 (:REWRITE FAT32-FILENAME-LIST-P-OF-LAST))
 (284 284 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (284 284 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (280 280 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (280 280 (:TYPE-PRESCRIPTION D-E-P))
 (280 280 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (280 140 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (280 140 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (277 9 (:DEFINITION NTH))
 (275 275 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (166 24 (:REWRITE FAT32-FILENAME-LIST-P-OF-TAKE))
 (140 140 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (140 140 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (140 140 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (140 140 (:REWRITE SET::IN-SET))
 (121 121 (:TYPE-PRESCRIPTION ZP))
 (114 19 (:REWRITE FAT32-FILENAME-LIST-P-OF-NTHCDR))
 (85 55 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (84 84 (:REWRITE TAKE-WHEN-ATOM))
 (77 12 (:REWRITE CAR-OF-TAKE))
 (54 9 (:REWRITE FAT32-FILENAME-P-OF-NTH-WHEN-FAT32-FILENAME-LIST-P))
 (49 49 (:TYPE-PRESCRIPTION NATP))
 (42 42 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (13 13 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (13 13 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 2))
 (13 13 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (12 6 (:REWRITE LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (8 8 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (7 7 (:REWRITE CONSP-OF-LAST))
 (6 6 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 (5 5 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(APPEND-NTHCDR-DIRNAME-BASENAME
 (265 1 (:DEFINITION BINARY-APPEND))
 (248 32 (:REWRITE NFIX-WHEN-ZP))
 (202 4 (:REWRITE NTHCDR-WHEN->=-N-LEN-L-UNDER-LIST-EQUIV))
 (174 4 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (162 4 (:DEFINITION STRING-LISTP))
 (146 1 (:REWRITE CAR-OF-NTHCDR))
 (138 2 (:DEFINITION TRUE-LISTP))
 (128 2 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (126 4 (:REWRITE CONSP-OF-NTHCDR))
 (116 8 (:DEFINITION NATP))
 (101 2 (:REWRITE APPEND-NTHCDR-DIRNAME-BASENAME-LEMMA-1 . 3))
 (98 71 (:REWRITE DEFAULT-<-2))
 (88 71 (:REWRITE DEFAULT-<-1))
 (86 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (81 39 (:REWRITE DEFAULT-CDR))
 (78 78 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (69 38 (:REWRITE DEFAULT-+-2))
 (69 4 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (69 4 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (55 2 (:REWRITE FAT32-FILENAME-LIST-FIX-WHEN-FAT32-FILENAME-LIST-P))
 (55 1 (:DEFINITION NTH))
 (51 17 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (51 17 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (49 4 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (49 4 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (42 11 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (39 38 (:REWRITE DEFAULT-+-1))
 (37 1 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (35 1 (:DEFINITION NAT-EQUIV$INLINE))
 (34 34 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (32 4 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (25 4 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (25 4 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (22 22 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (20 20 (:TYPE-PRESCRIPTION STRING-LISTP))
 (20 4 (:REWRITE TRUE-LISTP-WHEN-D-E-P))
 (17 17 (:TYPE-PRESCRIPTION ZP))
 (17 17 (:LINEAR POSITION-WHEN-MEMBER))
 (17 17 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (16 16 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (15 15 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 5 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (10 10 (:TYPE-PRESCRIPTION NATP))
 (10 5 (:REWRITE CONSP-OF-DIRNAME))
 (9 5 (:REWRITE DEFAULT-CAR))
 (8 8 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (8 8 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (8 8 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (8 8 (:TYPE-PRESCRIPTION D-E-P))
 (8 8 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (8 8 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (8 8 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (8 8 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (8 4 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (8 4 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (6 1 (:REWRITE FAT32-FILENAME-LIST-P-OF-NTHCDR))
 (4 4 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (4 4 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (4 4 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (4 4 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (4 4 (:REWRITE SET::IN-SET))
 (4 1 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 (1 1 (:TYPE-PRESCRIPTION NAT-EQUIV$INLINE))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1 1 (:REWRITE NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(ABS-PWRITE-CORRECTNESS-LEMMA-37
 (200 52 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (44 22 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (22 22 (:TYPE-PRESCRIPTION LAST))
 (10 2 (:DEFINITION ASSOC-EQUAL))
 (8 8 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (2 1 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 (1 1 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-LSTAT)
(STRUCT-STAT-P-OF-HIFAT-LSTAT
 (24 5 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (19 3 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (18 2 (:DEFINITION LEN))
 (16 4 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (15 1 (:REWRITE LENGTH-WHEN-STRINGP))
 (13 2 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (11 3 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (9 2 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (9 2 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (7 7 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (6 6 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (6 6 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (5 2 (:REWRITE DEFAULT-CDR))
 (4 4 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (4 4 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (4 2 (:REWRITE DEFAULT-+-2))
 (3 3 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (3 3 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (3 3 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (3 2 (:REWRITE STR::CONSP-OF-EXPLODE))
 (2 2 (:TYPE-PRESCRIPTION LEN))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (1 1 (:TYPE-PRESCRIPTION M1-FILE-P))
 (1 1 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (1 1 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (1 1 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (1 1 (:DEFINITION NOT))
 )
(HIFAT-LSTAT-CORRECTNESS-3
 (48 10 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (38 6 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (36 4 (:DEFINITION LEN))
 (32 8 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (30 2 (:REWRITE LENGTH-WHEN-STRINGP))
 (26 4 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (22 6 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (18 4 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (18 4 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (14 14 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (12 12 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (12 12 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (10 4 (:REWRITE DEFAULT-CDR))
 (8 8 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (8 8 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (6 6 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (6 6 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (6 6 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (6 4 (:REWRITE STR::CONSP-OF-EXPLODE))
 (4 4 (:TYPE-PRESCRIPTION LEN))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (2 2 (:TYPE-PRESCRIPTION M1-FILE-P))
 (2 2 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (2 2 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (2 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1 1 (:REWRITE DEFAULT-<-2))
 )
(HIFAT-OPEN
 (66 6 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (60 3 (:DEFINITION ALISTP))
 (25 5 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (25 5 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (21 6 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (21 6 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (20 20 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (11 3 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (10 10 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (10 10 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (10 10 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (10 5 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (10 5 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (8 2 (:DEFINITION STRIP-CARS))
 (7 7 (:REWRITE DEFAULT-CAR))
 (5 5 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (5 5 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (3 3 (:REWRITE SUBSETP-TRANS2))
 (3 3 (:REWRITE SUBSETP-TRANS))
 (3 3 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2 2 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-OPEN-CORRECTNESS-1
 (26 2 (:DEFINITION STRIP-CARS))
 (22 6 (:REWRITE DEFAULT-CAR))
 (12 2 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (12 2 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (7 1 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (7 1 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (6 4 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (4 4 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 )
(HIFAT-OPEN-CORRECTNESS-2
 (56 15 (:REWRITE DEFAULT-CAR))
 (38 8 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (37 1 (:DEFINITION MEMBER-EQUAL))
 (32 2 (:REWRITE SUBSETP-CAR-MEMBER))
 (30 7 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (28 4 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (20 1 (:REWRITE HIFAT-EQUIV-IMPLIES-SET-EQUIV-STRIP-CARS-1-LEMMA-2))
 (17 11 (:REWRITE DEFAULT-CDR))
 (15 1 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (12 12 (:TYPE-PRESCRIPTION FD-TABLE-P))
 (12 12 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (12 2 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (12 1 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (7 1 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (6 6 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (6 2 (:REWRITE NO-DUPLICATESP-OF-STRIP-CARS-WHEN-HIFAT-NO-DUPS-P))
 (5 4 (:REWRITE CONSP-OF-STRIP-CARS))
 (5 2 (:REWRITE MEMBER-WHEN-ATOM))
 (4 4 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (4 4 (:TYPE-PRESCRIPTION FILE-TABLE-P))
 (4 4 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (4 2 (:REWRITE SET-EQUIV-ASYM))
 (4 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4 1 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (4 1 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (2 2 (:TYPE-PRESCRIPTION SET-EQUIV))
 (2 2 (:TYPE-PRESCRIPTION M1-FILE-ALIST-P))
 (2 2 (:TYPE-PRESCRIPTION HIFAT-SUBSETP))
 (2 2 (:TYPE-PRESCRIPTION FILE-TABLE-FIX$INLINE))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 (2 2 (:REWRITE SUBSETP-OF-CDR))
 (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 M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 3))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 2))
 (2 2 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (1 1 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1 1 (:TYPE-PRESCRIPTION FIND-NEW-INDEX-CORRECTNESS-LEMMA-1))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 )
(HIFAT-OPEN-CORRECTNESS-3
 (56 15 (:REWRITE DEFAULT-CAR))
 (38 8 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (37 1 (:DEFINITION MEMBER-EQUAL))
 (32 2 (:REWRITE SUBSETP-CAR-MEMBER))
 (30 7 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (28 4 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (20 1 (:REWRITE HIFAT-EQUIV-IMPLIES-SET-EQUIV-STRIP-CARS-1-LEMMA-2))
 (17 11 (:REWRITE DEFAULT-CDR))
 (15 1 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (12 12 (:TYPE-PRESCRIPTION FILE-TABLE-P))
 (12 12 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (12 2 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (12 1 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (7 1 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (6 6 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (6 2 (:REWRITE NO-DUPLICATESP-OF-STRIP-CARS-WHEN-HIFAT-NO-DUPS-P))
 (5 4 (:REWRITE CONSP-OF-STRIP-CARS))
 (5 2 (:REWRITE MEMBER-WHEN-ATOM))
 (4 4 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (4 4 (:TYPE-PRESCRIPTION FD-TABLE-P))
 (4 4 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (4 2 (:REWRITE SET-EQUIV-ASYM))
 (4 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4 1 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (4 1 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (2 2 (:TYPE-PRESCRIPTION SET-EQUIV))
 (2 2 (:TYPE-PRESCRIPTION M1-FILE-ALIST-P))
 (2 2 (:TYPE-PRESCRIPTION HIFAT-SUBSETP))
 (2 2 (:TYPE-PRESCRIPTION FD-TABLE-FIX$INLINE))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 (2 2 (:REWRITE SUBSETP-OF-CDR))
 (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 M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 3))
 (2 2 (:REWRITE INTERSECTP-MEMBER . 2))
 (2 2 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (1 1 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1 1 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 )
(HIFAT-OPEN-CORRECTNESS-4
 (104 8 (:DEFINITION STRIP-CARS))
 (72 16 (:REWRITE DEFAULT-CAR))
 (48 8 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (48 8 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (28 4 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (28 4 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (16 16 (:TYPE-PRESCRIPTION FILE-TABLE-P))
 (16 16 (:TYPE-PRESCRIPTION FD-TABLE-P))
 (16 16 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (16 16 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (8 8 (:TYPE-PRESCRIPTION FILE-TABLE-FIX$INLINE))
 (8 8 (:TYPE-PRESCRIPTION FD-TABLE-FIX$INLINE))
 (8 8 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (8 8 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (2 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE DEFAULT-<-2))
 )
(FAT32-FILENAME-LIST-EQUIV-IMPLIES-EQUAL-HIFAT-OPEN-1
 (52 4 (:DEFINITION STRIP-CARS))
 (36 8 (:REWRITE DEFAULT-CAR))
 (19 4 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (19 4 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (14 2 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (14 2 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (6 6 (:TYPE-PRESCRIPTION FILE-TABLE-P))
 (6 6 (:TYPE-PRESCRIPTION FD-TABLE-P))
 (6 6 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (6 6 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (4 4 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (3 3 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 )
(HIFAT-PREAD
 (841 36 (:DEFINITION LEN))
 (563 131 (:REWRITE DEFAULT-CDR))
 (557 73 (:REWRITE STR::CONSP-OF-EXPLODE))
 (526 92 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (400 8 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (376 8 (:DEFINITION STRING-LISTP))
 (340 4 (:DEFINITION TRUE-LISTP))
 (283 47 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (214 42 (:DEFINITION ASSOC-EQUAL))
 (186 62 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (179 11 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (145 37 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (136 136 (:REWRITE DEFAULT-CAR))
 (124 62 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (124 8 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (124 8 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (117 113 (:TYPE-PRESCRIPTION STRINGP-SUBSEQ-TYPE-PRESCRIPTION))
 (110 110 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (79 43 (:REWRITE DEFAULT-+-2))
 (76 4 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (76 4 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (64 8 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (63 1 (:REWRITE THEN-SUBSEQ-EMPTY-1))
 (62 62 (:TYPE-PRESCRIPTION M1-FILE-P))
 (60 36 (:REWRITE DEFAULT-<-2))
 (56 56 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (56 56 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (54 36 (:REWRITE DEFAULT-<-1))
 (54 12 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (52 4 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (48 48 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (43 43 (:REWRITE DEFAULT-+-1))
 (40 40 (:TYPE-PRESCRIPTION STRING-LISTP))
 (40 8 (:REWRITE TRUE-LISTP-WHEN-D-E-P))
 (40 2 (:DEFINITION ALISTP))
 (27 6 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (24 24 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (24 24 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (24 24 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (22 22 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (22 22 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (20 4 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (20 4 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (16 16 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (16 16 (:TYPE-PRESCRIPTION D-E-P))
 (16 16 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (16 8 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (16 8 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (16 4 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (15 6 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (12 12 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (12 12 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (12 12 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (9 3 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (9 3 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (8 8 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (8 8 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (8 8 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (8 8 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (8 8 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (8 8 (:REWRITE SET::IN-SET))
 (8 8 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (8 8 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (8 8 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (8 8 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (8 4 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (8 4 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (7 1 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 (6 6 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (5 5 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (4 4 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (4 4 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (4 4 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (4 4 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (3 3 (:LINEAR POSITION-WHEN-MEMBER))
 (3 3 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (3 3 (:DEFINITION SUBSEQ-LIST))
 (2 1 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 )
(HIFAT-PREAD-CORRECTNESS-1
 (3296 138 (:DEFINITION LEN))
 (2689 481 (:REWRITE DEFAULT-CDR))
 (2276 161 (:DEFINITION ASSOC-EQUAL))
 (2016 252 (:REWRITE STR::CONSP-OF-EXPLODE))
 (1805 307 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (1675 488 (:REWRITE DEFAULT-CAR))
 (1014 14 (:REWRITE TAKE-OF-LEN-FREE))
 (997 172 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (890 25 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (865 150 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (838 13 (:REWRITE LEN-OF-NTHCDR))
 (728 8 (:DEFINITION NTHCDR))
 (680 5 (:REWRITE CAR-OF-NTHCDR))
 (642 214 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (602 86 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (575 13 (:REWRITE TAKE-WHEN-ATOM))
 (560 16 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (550 64 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (531 531 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (525 75 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (490 13 (:REWRITE CONSP-OF-NTHCDR))
 (465 10 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (434 309 (:REWRITE DEFAULT-<-2))
 (428 214 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (400 5 (:DEFINITION NTH))
 (399 222 (:REWRITE DEFAULT-+-2))
 (398 114 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (346 346 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (343 309 (:REWRITE DEFAULT-<-1))
 (330 330 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (286 286 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (249 222 (:REWRITE DEFAULT-+-1))
 (214 214 (:TYPE-PRESCRIPTION M1-FILE-P))
 (214 214 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (192 24 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (183 61 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (183 61 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (172 35 (:DEFINITION NATP))
 (165 165 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (153 51 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (143 143 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (142 142 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (142 142 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (132 66 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (122 122 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (112 26 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (65 65 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (65 26 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (61 61 (:LINEAR POSITION-WHEN-MEMBER))
 (61 61 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (60 12 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (56 1 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (49 49 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (39 39 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT->FID$INLINE))
 (37 37 (:TYPE-PRESCRIPTION NATP))
 (33 11 (:TYPE-PRESCRIPTION TRUE-LISTP-SUBSEQ-TYPE-PRESCRIPTION))
 (32 23 (:REWRITE DEFAULT-UNARY-MINUS))
 (24 24 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (24 24 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (24 24 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (24 24 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (22 22 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (17 17 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 (13 13 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (11 11 (:TYPE-PRESCRIPTION STRINGP-SUBSEQ-TYPE-PRESCRIPTION))
 (4 4 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (2 1 (:REWRITE FIX-WHEN-ACL2-NUMBERP))
 )
(NATP-OF-HIFAT-PREAD
 (3412 136 (:DEFINITION LEN))
 (2806 6 (:DEFINITION TAKE))
 (2798 464 (:REWRITE DEFAULT-CDR))
 (2120 150 (:DEFINITION ASSOC-EQUAL))
 (2066 254 (:REWRITE STR::CONSP-OF-EXPLODE))
 (1834 308 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (1578 456 (:REWRITE DEFAULT-CAR))
 (1216 14 (:REWRITE TAKE-OF-LEN-FREE))
 (1068 30 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (920 160 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (816 6 (:REWRITE CAR-OF-NTHCDR))
 (800 140 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (732 12 (:REWRITE LEN-OF-NTHCDR))
 (654 218 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (560 80 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (558 12 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (546 12 (:REWRITE TAKE-WHEN-ATOM))
 (546 6 (:DEFINITION NTHCDR))
 (534 534 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (534 66 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (490 70 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (480 6 (:DEFINITION NTH))
 (462 12 (:REWRITE CONSP-OF-NTHCDR))
 (438 316 (:REWRITE DEFAULT-<-2))
 (436 218 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (420 12 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (404 226 (:REWRITE DEFAULT-+-2))
 (392 112 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (364 364 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (352 316 (:REWRITE DEFAULT-<-1))
 (304 304 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (264 264 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (262 226 (:REWRITE DEFAULT-+-1))
 (218 218 (:TYPE-PRESCRIPTION M1-FILE-P))
 (192 64 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (192 64 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (192 24 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (162 54 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (152 152 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (144 72 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (140 140 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (140 140 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (132 132 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (128 128 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (112 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (108 24 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (66 66 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (64 64 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (64 64 (:LINEAR POSITION-WHEN-MEMBER))
 (64 64 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (60 24 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (60 12 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (36 36 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT->FID$INLINE))
 (28 20 (:REWRITE DEFAULT-UNARY-MINUS))
 (24 24 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (24 24 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (24 24 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (24 24 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (22 22 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (20 20 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (16 16 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 (6 6 (:REWRITE FOLD-CONSTS-IN-+))
 (4 4 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (4 2 (:REWRITE FIX-WHEN-ACL2-NUMBERP))
 (2 2 (:TYPE-PRESCRIPTION LENGTH))
 )
(FD-TABLE-EQUIV-IMPLIES-EQUAL-HIFAT-PREAD-5
 (132 6 (:DEFINITION LEN))
 (120 40 (:TYPE-PRESCRIPTION TRUE-LISTP-SUBSEQ-TYPE-PRESCRIPTION))
 (112 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (86 14 (:REWRITE DEFAULT-CDR))
 (84 12 (:REWRITE STR::CONSP-OF-EXPLODE))
 (72 16 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (56 4 (:DEFINITION ASSOC-EQUAL))
 (40 40 (:TYPE-PRESCRIPTION STRINGP-SUBSEQ-TYPE-PRESCRIPTION))
 (40 12 (:REWRITE DEFAULT-CAR))
 (32 4 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (31 6 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (26 8 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (24 8 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (24 8 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (20 10 (:REWRITE DEFAULT-+-2))
 (19 4 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (18 18 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (18 4 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (16 8 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (14 10 (:REWRITE DEFAULT-+-1))
 (14 2 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (14 2 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (10 10 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (10 4 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (10 2 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (8 8 (:TYPE-PRESCRIPTION M1-FILE-P))
 (8 8 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (8 8 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (8 8 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (8 8 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (8 4 (:REWRITE DEFAULT-<-2))
 (6 6 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT->FID$INLINE))
 (6 6 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (6 4 (:REWRITE DEFAULT-<-1))
 (5 5 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (4 4 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (4 4 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (4 4 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (3 3 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (2 2 (:DEFINITION SUBSEQ-LIST))
 )
(FILE-TABLE-EQUIV-IMPLIES-EQUAL-HIFAT-PREAD-6
 (132 6 (:DEFINITION LEN))
 (120 40 (:TYPE-PRESCRIPTION TRUE-LISTP-SUBSEQ-TYPE-PRESCRIPTION))
 (112 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (86 14 (:REWRITE DEFAULT-CDR))
 (84 12 (:REWRITE STR::CONSP-OF-EXPLODE))
 (72 16 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (56 4 (:DEFINITION ASSOC-EQUAL))
 (40 40 (:TYPE-PRESCRIPTION STRINGP-SUBSEQ-TYPE-PRESCRIPTION))
 (40 12 (:REWRITE DEFAULT-CAR))
 (32 4 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (31 6 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (26 8 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (24 8 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (24 8 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (20 10 (:REWRITE DEFAULT-+-2))
 (19 4 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (18 18 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (18 4 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (16 8 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (14 10 (:REWRITE DEFAULT-+-1))
 (14 2 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (14 2 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (10 10 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (10 4 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (10 2 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (8 8 (:TYPE-PRESCRIPTION M1-FILE-P))
 (8 8 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (8 8 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (8 8 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (8 8 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (8 4 (:REWRITE DEFAULT-<-2))
 (6 6 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT->FID$INLINE))
 (6 6 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (6 4 (:REWRITE DEFAULT-<-1))
 (5 5 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (4 4 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (4 4 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (4 4 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (3 3 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (2 2 (:DEFINITION SUBSEQ-LIST))
 )
(HIFAT-EQUIV-IMPLIES-EQUAL-HIFAT-PREAD-4
 (3856 273 (:DEFINITION ASSOC-EQUAL))
 (2778 825 (:REWRITE DEFAULT-CAR))
 (2152 131 (:DEFINITION LEN))
 (1802 677 (:REWRITE DEFAULT-CDR))
 (1650 290 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (1450 4 (:DEFINITION TAKE))
 (1446 256 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (1015 145 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (896 128 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (761 244 (:REWRITE STR::CONSP-OF-EXPLODE))
 (704 10 (:REWRITE TAKE-OF-LEN-FREE))
 (688 112 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (544 544 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (532 20 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (476 476 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (468 468 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (455 135 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (400 8 (:REWRITE LEN-OF-NTHCDR))
 (379 82 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (378 208 (:REWRITE DEFAULT-+-2))
 (364 4 (:REWRITE CAR-OF-NTHCDR))
 (338 233 (:REWRITE DEFAULT-<-2))
 (328 4 (:DEFINITION NTHCDR))
 (300 8 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (284 8 (:REWRITE TAKE-WHEN-ATOM))
 (276 76 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (272 272 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (268 233 (:REWRITE DEFAULT-<-1))
 (264 264 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (243 208 (:REWRITE DEFAULT-+-1))
 (238 238 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (236 8 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (212 4 (:DEFINITION NTH))
 (192 8 (:REWRITE CONSP-OF-NTHCDR))
 (174 49 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (160 160 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (160 160 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (148 76 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (144 48 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (144 48 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (133 49 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (112 24 (:DEFINITION NATP))
 (108 36 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (107 31 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (96 96 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (96 48 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (84 84 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT->FID$INLINE))
 (76 76 (:TYPE-PRESCRIPTION M1-FILE-P))
 (76 76 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (73 73 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (48 48 (:LINEAR POSITION-WHEN-MEMBER))
 (48 48 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (38 38 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (38 38 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (38 38 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (38 38 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (34 34 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (28 28 (:TYPE-PRESCRIPTION NATP))
 (22 15 (:REWRITE DEFAULT-UNARY-MINUS))
 (16 16 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (10 10 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 (6 6 (:REWRITE FOLD-CONSTS-IN-+))
 (4 2 (:REWRITE FIX-WHEN-ACL2-NUMBERP))
 (3 3 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 )
(HIFAT-PWRITE
 (9174 3066 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1204 84 (:DEFINITION LEN))
 (1082 50 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (920 36 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (782 12 (:REWRITE M1-REGULAR-FILE-P-OF-M1-FILE))
 (660 276 (:REWRITE DEFAULT-CDR))
 (590 12 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (516 98 (:DEFINITION ASSOC-EQUAL))
 (508 168 (:REWRITE STR::CONSP-OF-EXPLODE))
 (436 116 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (364 28 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (362 24 (:REWRITE M1-FILE-CONTENTS-FIX-WHEN-M1-FILE-CONTENTS-P))
 (322 322 (:REWRITE DEFAULT-CAR))
 (272 136 (:REWRITE DEFAULT-+-2))
 (216 84 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (192 96 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-FIX))
 (192 24 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (160 160 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (160 160 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (160 32 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (140 28 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (140 28 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (136 136 (:REWRITE DEFAULT-+-1))
 (112 112 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (112 28 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (72 16 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (68 54 (:REWRITE DEFAULT-<-2))
 (64 64 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (64 64 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (60 54 (:REWRITE DEFAULT-<-1))
 (60 30 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (56 56 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (56 56 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (56 56 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (56 28 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (56 28 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (48 12 (:REWRITE NFIX-WHEN-ZP))
 (40 40 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (40 40 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (40 16 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (35 35 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (35 35 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (28 28 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (28 28 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (26 26 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (24 24 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (20 20 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (20 20 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (18 6 (:REWRITE M1-FILE-HIFAT-FILE-ALIST-FIX-NORMALISATION))
 (16 16 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (16 8 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (14 2 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LISTP))
 (12 12 (:REWRITE ZP-OPEN))
 (12 6 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE))
 (12 4 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (12 4 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (8 8 (:REWRITE SUBSETP-TRANS2))
 (8 8 (:REWRITE SUBSETP-TRANS))
 (8 8 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (6 6 (:TYPE-PRESCRIPTION HIFAT-FILE-ALIST-FIX))
 (4 4 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (4 4 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-SUBSETP-EQUAL))
 (4 4 (:LINEAR POSITION-WHEN-MEMBER))
 (4 4 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (4 2 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-NOT-CONSP))
 )
(HIFAT-PWRITE-CORRECTNESS-1
 (5862 144 (:REWRITE M1-FILE-CONTENTS-FIX-WHEN-M1-FILE-CONTENTS-P))
 (5798 75 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (5447 255 (:DEFINITION LEN))
 (2580 860 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (2429 663 (:REWRITE DEFAULT-CDR))
 (2204 140 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (2002 30 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 1))
 (1230 294 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (1226 276 (:REWRITE STR::CONSP-OF-EXPLODE))
 (1153 223 (:DEFINITION ASSOC-EQUAL))
 (1088 30 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (680 355 (:REWRITE DEFAULT-+-2))
 (669 669 (:REWRITE DEFAULT-CAR))
 (546 228 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (541 353 (:REWRITE DEFAULT-<-2))
 (468 468 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (468 468 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (468 468 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (458 172 (:REWRITE ZP-OPEN))
 (410 355 (:REWRITE DEFAULT-+-1))
 (388 353 (:REWRITE DEFAULT-<-1))
 (372 310 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (340 84 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (320 320 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (261 41 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (240 80 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (240 80 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (224 70 (:REWRITE STR::EXPLODE-OF-IMPLODE))
 (180 60 (:DEFINITION NATP))
 (172 42 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (160 160 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (160 5 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (150 30 (:REWRITE NFIX-WHEN-NATP))
 (150 30 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 2))
 (130 30 (:REWRITE COMMUTATIVITY-OF-+))
 (128 128 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (128 128 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (120 30 (:REWRITE NFIX-WHEN-ZP))
 (108 42 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (101 33 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (90 30 (:REWRITE M1-FILE-HIFAT-FILE-ALIST-FIX-NORMALISATION))
 (90 30 (:DEFINITION NFIX))
 (80 80 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (75 75 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (74 74 (:TYPE-PRESCRIPTION M1-DIRECTORY-FILE-P))
 (70 70 (:REWRITE STR::MAKE-CHARACTER-LIST-IS-IDENTITY-UNDER-CHARLISTEQV))
 (66 66 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT->FID$INLINE))
 (60 60 (:TYPE-PRESCRIPTION NATP))
 (52 52 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (48 48 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (42 42 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (42 42 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (41 21 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (40 40 (:LINEAR POSITION-WHEN-MEMBER))
 (40 40 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (35 35 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (30 30 (:TYPE-PRESCRIPTION HIFAT-FILE-ALIST-FIX))
 (24 12 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE))
 (21 21 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (20 20 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (20 20 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-3 . 1))
 (20 10 (:REWRITE UNICITY-OF-0))
 (16 16 (:REWRITE-QUOTED-CONSTANT D-E-FIX-UNDER-D-E-EQUIV))
 (10 10 (:REWRITE FIX-WHEN-ACL2-NUMBERP))
 )
(HIFAT-PWRITE-CORRECTNESS-2
 (1220 10 (:REWRITE M1-FILE-CONTENTS-FIX-WHEN-M1-FILE-CONTENTS-P))
 (1200 10 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (1008 336 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (840 10 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (674 10 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 1))
 (658 50 (:DEFINITION LEN))
 (543 105 (:DEFINITION ASSOC-EQUAL))
 (315 315 (:REWRITE DEFAULT-CAR))
 (310 86 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (306 20 (:REWRITE LENGTH-WHEN-STRINGP))
 (302 242 (:REWRITE DEFAULT-CDR))
 (250 66 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (220 20 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (160 80 (:REWRITE DEFAULT-+-2))
 (154 24 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (150 20 (:REWRITE ZP-OPEN))
 (112 112 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (112 112 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (100 80 (:REWRITE DEFAULT-<-2))
 (100 26 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (95 80 (:REWRITE DEFAULT-+-1))
 (92 92 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (92 92 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (90 80 (:REWRITE DEFAULT-<-1))
 (80 40 (:REWRITE STR::CONSP-OF-EXPLODE))
 (70 70 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (68 26 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (60 50 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (60 20 (:DEFINITION NATP))
 (50 10 (:REWRITE NFIX-WHEN-NATP))
 (50 10 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 2))
 (42 42 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT->FID$INLINE))
 (40 40 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (40 10 (:REWRITE NFIX-WHEN-ZP))
 (40 10 (:REWRITE COMMUTATIVITY-OF-+))
 (32 10 (:REWRITE STR::EXPLODE-OF-IMPLODE))
 (30 10 (:REWRITE M1-FILE-HIFAT-FILE-ALIST-FIX-NORMALISATION))
 (30 10 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (30 10 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (30 10 (:DEFINITION NFIX))
 (25 3 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (22 22 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (22 22 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (20 20 (:TYPE-PRESCRIPTION NATP))
 (20 20 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (20 20 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (18 18 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (11 3 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (10 10 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (10 10 (:TYPE-PRESCRIPTION HIFAT-FILE-ALIST-FIX))
 (10 10 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (10 10 (:REWRITE STR::MAKE-CHARACTER-LIST-IS-IDENTITY-UNDER-CHARLISTEQV))
 (10 10 (:LINEAR POSITION-WHEN-MEMBER))
 (10 10 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (8 8 (:TYPE-PRESCRIPTION M1-DIRECTORY-FILE-P))
 (5 5 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 3 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (3 3 (:TYPE-PRESCRIPTION M1-FILE-P))
 (3 3 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 )
(HIFAT-PWRITE-CORRECTNESS-3
 (624 208 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (302 58 (:DEFINITION ASSOC-EQUAL))
 (174 174 (:REWRITE DEFAULT-CAR))
 (134 116 (:REWRITE DEFAULT-CDR))
 (120 6 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (96 24 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (96 12 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (96 12 (:DEFINITION LEN))
 (84 6 (:REWRITE ZP-OPEN))
 (66 18 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (66 6 (:REWRITE LENGTH-WHEN-STRINGP))
 (54 12 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (46 10 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (42 18 (:REWRITE DEFAULT-+-2))
 (40 28 (:REWRITE DEFAULT-<-2))
 (36 36 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (36 36 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (32 28 (:REWRITE DEFAULT-<-1))
 (32 4 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (30 12 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (28 10 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (24 24 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (24 24 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (24 18 (:REWRITE DEFAULT-+-1))
 (18 18 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (18 18 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT->FID$INLINE))
 (18 12 (:REWRITE STR::CONSP-OF-EXPLODE))
 (18 6 (:REWRITE M1-FILE-HIFAT-FILE-ALIST-FIX-NORMALISATION))
 (16 16 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (16 16 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (12 12 (:TYPE-PRESCRIPTION M1-DIRECTORY-FILE-P))
 (12 12 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (12 12 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (12 12 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-4))
 (12 4 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (10 10 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (8 4 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (6 6 (:TYPE-PRESCRIPTION STRINGP-OF-IMPLODE))
 (6 6 (:TYPE-PRESCRIPTION HIFAT-FILE-ALIST-FIX))
 (6 6 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (4 4 (:TYPE-PRESCRIPTION M1-FILE-P))
 (4 4 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 )
(HIFAT-PWRITE-CORRECTNESS-4
 (1220 10 (:REWRITE M1-FILE-CONTENTS-FIX-WHEN-M1-FILE-CONTENTS-P))
 (1200 10 (:REWRITE M1-FILE-CONTENTS-P-WHEN-STRINGP))
 (1008 336 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (840 10 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (674 10 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 1))
 (658 50 (:DEFINITION LEN))
 (543 105 (:DEFINITION ASSOC-EQUAL))
 (315 315 (:REWRITE DEFAULT-CAR))
 (310 86 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (306 20 (:REWRITE LENGTH-WHEN-STRINGP))
 (302 242 (:REWRITE DEFAULT-CDR))
 (250 66 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (220 20 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (160 80 (:REWRITE DEFAULT-+-2))
 (154 24 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (150 20 (:REWRITE ZP-OPEN))
 (112 112 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (112 112 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (100 80 (:REWRITE DEFAULT-<-2))
 (100 26 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (95 80 (:REWRITE DEFAULT-+-1))
 (92 92 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (92 92 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (90 80 (:REWRITE DEFAULT-<-1))
 (80 40 (:REWRITE STR::CONSP-OF-EXPLODE))
 (70 70 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (68 26 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (60 50 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (60 20 (:DEFINITION NATP))
 (50 10 (:REWRITE NFIX-WHEN-NATP))
 (50 10 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 2))
 (42 42 (:TYPE-PRESCRIPTION FILE-TABLE-ELEMENT->FID$INLINE))
 (40 40 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (40 10 (:REWRITE NFIX-WHEN-ZP))
 (40 10 (:REWRITE COMMUTATIVITY-OF-+))
 (32 10 (:REWRITE STR::EXPLODE-OF-IMPLODE))
 (30 10 (:REWRITE M1-FILE-HIFAT-FILE-ALIST-FIX-NORMALISATION))
 (30 10 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (30 10 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (30 10 (:DEFINITION NFIX))
 (25 3 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (22 22 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (22 22 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (20 20 (:TYPE-PRESCRIPTION NATP))
 (20 20 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (20 20 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (18 18 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (11 3 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (10 10 (:TYPE-PRESCRIPTION M1-FILE-CONTENTS-P))
 (10 10 (:TYPE-PRESCRIPTION HIFAT-FILE-ALIST-FIX))
 (10 10 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (10 10 (:REWRITE STR::MAKE-CHARACTER-LIST-IS-IDENTITY-UNDER-CHARLISTEQV))
 (10 10 (:LINEAR POSITION-WHEN-MEMBER))
 (10 10 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (8 8 (:TYPE-PRESCRIPTION M1-DIRECTORY-FILE-P))
 (5 5 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 3 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (3 3 (:TYPE-PRESCRIPTION M1-FILE-P))
 (3 3 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 )
(HIFAT-MKDIR)
(HIFAT-MKDIR-CORRECTNESS-1
 (234 57 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (184 11 (:REWRITE ZP-OPEN))
 (175 22 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (166 29 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (126 11 (:REWRITE NFIX-WHEN-ZP))
 (126 8 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (118 19 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (111 11 (:REWRITE NFIX-WHEN-NATP))
 (85 5 (:DEFINITION NATP))
 (66 40 (:REWRITE DEFAULT-<-2))
 (66 33 (:REWRITE DEFAULT-+-2))
 (65 1 (:DEFINITION FAT32-FILENAME-LIST-PREFIXP))
 (64 61 (:REWRITE DEFAULT-CDR))
 (58 40 (:REWRITE DEFAULT-<-1))
 (55 55 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (45 9 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (33 33 (:REWRITE DEFAULT-+-1))
 (30 30 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (25 5 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 (22 21 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (21 7 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (21 7 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (18 18 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (18 18 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (18 18 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (16 4 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (14 14 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (14 14 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (12 12 (:TYPE-PRESCRIPTION M1-FILE-P))
 (12 12 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (11 11 (:TYPE-PRESCRIPTION ZP))
 (9 2 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (7 7 (:LINEAR POSITION-WHEN-MEMBER))
 (7 7 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 2 (:REWRITE DEFAULT-CAR))
 (5 5 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE-QUOTED-CONSTANT M1-FILE-FIX-UNDER-M1-FILE-EQUIV))
 (4 4 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (4 4 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-3 . 1))
 (4 2 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-3 . 2))
 (3 1 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 2))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (2 1 (:REWRITE LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 )
(HIFAT-MKDIR-CORRECTNESS-2
 (198 46 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (157 20 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (147 26 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (132 8 (:REWRITE ZP-OPEN))
 (109 17 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (97 9 (:REWRITE NFIX-WHEN-ZP))
 (85 9 (:REWRITE NFIX-WHEN-NATP))
 (84 4 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (65 1 (:DEFINITION FAT32-FILENAME-LIST-PREFIXP))
 (64 4 (:DEFINITION NATP))
 (58 55 (:REWRITE DEFAULT-CDR))
 (58 29 (:REWRITE DEFAULT-+-2))
 (51 31 (:REWRITE DEFAULT-<-2))
 (48 48 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (46 31 (:REWRITE DEFAULT-<-1))
 (40 8 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (29 29 (:REWRITE DEFAULT-+-1))
 (22 22 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (20 19 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (20 4 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 (16 16 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (16 16 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (16 16 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (16 4 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (15 5 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (15 5 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (12 12 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (11 11 (:TYPE-PRESCRIPTION M1-FILE-P))
 (11 11 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (10 10 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (9 2 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (8 8 (:TYPE-PRESCRIPTION ZP))
 (6 2 (:REWRITE DEFAULT-CAR))
 (5 5 (:LINEAR POSITION-WHEN-MEMBER))
 (5 5 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE-QUOTED-CONSTANT M1-FILE-FIX-UNDER-M1-FILE-EQUIV))
 (4 4 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (3 1 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 2))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (2 1 (:REWRITE LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 )
(HIFAT-MKDIR-CORRECTNESS-3
 (120 6 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (84 6 (:REWRITE ZP-OPEN))
 (81 18 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (57 9 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (54 6 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (39 6 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (30 18 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (27 6 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (25 13 (:REWRITE DEFAULT-<-2))
 (24 6 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (15 15 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (15 3 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (14 13 (:REWRITE DEFAULT-<-1))
 (12 12 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (12 12 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-4))
 (6 6 (:TYPE-PRESCRIPTION ZP))
 (6 6 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (6 6 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (6 6 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (6 6 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (6 6 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (6 6 (:REWRITE DEFAULT-CDR))
 (3 3 (:TYPE-PRESCRIPTION M1-FILE-P))
 (3 3 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(HIFAT-MKDIR-CORRECTNESS-4
 (375 47 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (366 64 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (358 82 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (242 38 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (208 12 (:REWRITE ZP-OPEN))
 (194 18 (:REWRITE NFIX-WHEN-ZP))
 (170 18 (:REWRITE NFIX-WHEN-NATP))
 (130 2 (:DEFINITION FAT32-FILENAME-LIST-PREFIXP))
 (128 8 (:DEFINITION NATP))
 (125 119 (:REWRITE DEFAULT-CDR))
 (116 58 (:REWRITE DEFAULT-+-2))
 (113 113 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (95 19 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (86 54 (:REWRITE DEFAULT-<-2))
 (84 54 (:REWRITE DEFAULT-<-1))
 (84 4 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-3))
 (58 58 (:REWRITE DEFAULT-+-1))
 (47 46 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (44 44 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (40 8 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 (38 38 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (38 38 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (38 38 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (30 10 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (30 10 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (27 27 (:TYPE-PRESCRIPTION M1-FILE-P))
 (27 27 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (20 20 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (18 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-WHEN-ATOM-1))
 (16 4 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (12 12 (:TYPE-PRESCRIPTION ZP))
 (12 12 (:REWRITE HIFAT-PLACE-FILE-WHEN-HIFAT-EQUIV-1 . 1))
 (12 4 (:REWRITE DEFAULT-CAR))
 (10 10 (:LINEAR POSITION-WHEN-MEMBER))
 (10 10 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (8 8 (:TYPE-PRESCRIPTION NATP))
 (6 2 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (4 4 (:REWRITE-QUOTED-CONSTANT M1-FILE-FIX-UNDER-M1-FILE-EQUIV))
 (4 4 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 2))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-PREFIXP-TRANSITIVE . 1))
 (4 2 (:REWRITE LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-EQUIV$INLINE))
 )
(HIFAT-MKNOD)
(HIFAT-UNLINK)
(HIFAT-UNLINK-RECURSIVE)
(HIFAT-RMDIR)
(HIFAT-RENAME)
(HIFAT-CLOSE
 (106 106 (:REWRITE DEFAULT-CAR))
 (104 8 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (80 4 (:DEFINITION ALISTP))
 (44 33 (:REWRITE DEFAULT-CDR))
 (40 8 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (40 8 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (32 32 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (32 8 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (20 20 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (16 16 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (16 16 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (16 16 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (16 8 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (16 8 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (12 2 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-37))
 (10 10 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (10 10 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (8 8 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (6 3 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (3 3 (:REWRITE SUBSETP-TRANS2))
 (3 3 (:REWRITE SUBSETP-TRANS))
 (2 2 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-CLOSE-CORRECTNESS-1
 (324 4 (:DEFINITION REMOVE-ASSOC-EQUAL))
 (268 12 (:REWRITE REMOVE-ASSOC-WHEN-ABSENT-1))
 (186 17 (:DEFINITION ASSOC-EQUAL))
 (156 65 (:REWRITE DEFAULT-CAR))
 (97 17 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (86 2 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (78 13 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (58 4 (:REWRITE SUBSETP-CAR-MEMBER))
 (58 2 (:DEFINITION MEMBER-EQUAL))
 (56 8 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (50 12 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (49 7 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (46 32 (:REWRITE DEFAULT-CDR))
 (32 32 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (28 2 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-37))
 (26 26 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (24 2 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (20 20 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (16 16 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (16 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (15 15 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (15 15 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (13 13 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (12 12 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (8 4 (:REWRITE SET-EQUIV-ASYM))
 (6 2 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (4 4 (:TYPE-PRESCRIPTION SET-EQUIV))
 (4 4 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (4 4 (:REWRITE SUBSETP-OF-CDR))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (2 2 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 )
(HIFAT-CLOSE-CORRECTNESS-2
 (153 2 (:DEFINITION REMOVE-ASSOC-EQUAL))
 (138 2 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (134 6 (:REWRITE REMOVE-ASSOC-WHEN-ABSENT-1))
 (103 3 (:DEFINITION MEMBER-EQUAL))
 (93 6 (:REWRITE SUBSETP-CAR-MEMBER))
 (81 18 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (53 33 (:REWRITE DEFAULT-CAR))
 (43 6 (:DEFINITION ASSOC-EQUAL))
 (43 1 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (42 3 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (30 30 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (27 21 (:REWRITE DEFAULT-CDR))
 (24 4 (:REWRITE FILE-TABLE-FIX-WHEN-FILE-TABLE-P))
 (21 3 (:REWRITE CONSP-CAR-OF-FILE-TABLE-FIX))
 (14 1 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-37))
 (12 6 (:REWRITE SET-EQUIV-ASYM))
 (10 4 (:REWRITE MEMBER-WHEN-ATOM))
 (9 3 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (8 8 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (8 8 (:REWRITE CONSP-OF-STRIP-CARS))
 (8 2 (:DEFINITION STRIP-CARS))
 (8 1 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (7 7 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (6 6 (:TYPE-PRESCRIPTION SET-EQUIV))
 (6 6 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (6 6 (:REWRITE SUBSETP-OF-CDR))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 (6 6 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (6 6 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (6 2 (:REWRITE NO-DUPLICATESP-OF-STRIP-CARS-WHEN-HIFAT-NO-DUPS-P))
 (4 4 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (4 4 (:REWRITE SUBSETP-MEMBER . 4))
 (4 4 (:REWRITE SUBSETP-MEMBER . 3))
 (4 4 (:REWRITE INTERSECTP-MEMBER . 3))
 (4 4 (:REWRITE INTERSECTP-MEMBER . 2))
 (4 4 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (3 3 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (3 3 (:REWRITE SUBSETP-TRANS2))
 (3 3 (:REWRITE SUBSETP-TRANS))
 (3 1 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (2 2 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (1 1 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 )
(HIFAT-CLOSE-CORRECTNESS-3
 (144 2 (:DEFINITION REMOVE-ASSOC-EQUAL))
 (138 2 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (125 6 (:REWRITE REMOVE-ASSOC-WHEN-ABSENT-1))
 (102 3 (:DEFINITION MEMBER-EQUAL))
 (93 6 (:REWRITE SUBSETP-CAR-MEMBER))
 (81 18 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (53 33 (:REWRITE DEFAULT-CAR))
 (43 6 (:DEFINITION ASSOC-EQUAL))
 (42 3 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (42 1 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (30 30 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (27 21 (:REWRITE DEFAULT-CDR))
 (18 3 (:REWRITE FD-TABLE-FIX-WHEN-FD-TABLE-P))
 (14 2 (:REWRITE CONSP-CAR-OF-FD-TABLE-FIX))
 (12 6 (:REWRITE SET-EQUIV-ASYM))
 (10 4 (:REWRITE MEMBER-WHEN-ATOM))
 (9 3 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (8 8 (:REWRITE CONSP-OF-STRIP-CARS))
 (8 2 (:DEFINITION STRIP-CARS))
 (7 7 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (6 6 (:TYPE-PRESCRIPTION SET-EQUIV))
 (6 6 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (6 6 (:REWRITE SUBSETP-OF-CDR))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 (6 6 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (6 6 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (6 6 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (6 2 (:REWRITE NO-DUPLICATESP-OF-STRIP-CARS-WHEN-HIFAT-NO-DUPS-P))
 (6 1 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-37))
 (4 4 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (4 4 (:REWRITE SUBSETP-MEMBER . 4))
 (4 4 (:REWRITE SUBSETP-MEMBER . 3))
 (4 4 (:REWRITE INTERSECTP-MEMBER . 3))
 (4 4 (:REWRITE INTERSECTP-MEMBER . 2))
 (3 3 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (3 3 (:REWRITE SUBSETP-TRANS2))
 (3 3 (:REWRITE SUBSETP-TRANS))
 (3 3 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (3 1 (:REWRITE HIFAT-FILE-ALIST-FIX-GUARD-LEMMA-1))
 (2 2 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (1 1 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (1 1 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 )
(HIFAT-TRUNCATE
 (1122 90 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (1041 132 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (963 18 (:REWRITE TAKE-OF-LEN-FREE))
 (822 102 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (792 6 (:DEFINITION TAKE))
 (702 42 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (672 63 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (630 90 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (579 45 (:REWRITE STR::CONSP-OF-EXPLODE))
 (489 27 (:DEFINITION LEN))
 (486 9 (:LINEAR LEN-OF-EXPLODE-WHEN-M1-FILE-CONTENTS-P-1))
 (477 159 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (360 45 (:DEFINITION MEMBER-EQUAL))
 (297 87 (:REWRITE DEFAULT-CAR))
 (291 87 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (261 9 (:LINEAR M1-REGULAR-FILE-P-CORRECTNESS-2))
 (225 225 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (201 36 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (191 98 (:REWRITE DEFAULT-CDR))
 (144 144 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (141 81 (:REWRITE NFIX-WHEN-ZP))
 (108 24 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (104 8 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (102 102 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (102 102 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (102 15 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (90 90 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (90 90 (:REWRITE SUBSETP-MEMBER . 2))
 (90 90 (:REWRITE SUBSETP-MEMBER . 1))
 (90 12 (:REWRITE TAKE-WHEN-ATOM))
 (81 27 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (81 27 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (80 4 (:DEFINITION ALISTP))
 (78 78 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (72 45 (:REWRITE DEFAULT-+-2))
 (54 54 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (54 18 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (51 21 (:REWRITE ZP-OPEN))
 (45 45 (:REWRITE DEFAULT-+-1))
 (44 8 (:DEFINITION ASSOC-EQUAL))
 (40 8 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (40 8 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (39 30 (:REWRITE DEFAULT-<-2))
 (32 32 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (32 8 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (30 30 (:REWRITE DEFAULT-<-1))
 (27 27 (:LINEAR POSITION-WHEN-MEMBER))
 (27 27 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (24 24 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (24 12 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (18 18 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (18 6 (:REWRITE M1-FILE-HIFAT-FILE-ALIST-FIX-NORMALISATION))
 (16 16 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (16 16 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (16 16 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (16 8 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (16 8 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (15 6 (:REWRITE REPEAT-WHEN-ZP))
 (12 12 (:REWRITE SUBSETP-TRANS2))
 (12 12 (:REWRITE SUBSETP-TRANS))
 (12 12 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (12 6 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE))
 (9 9 (:REWRITE M1-FILE-CONTENTS-P-OF-M1-FILE->CONTENTS))
 (8 8 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (6 6 (:TYPE-PRESCRIPTION HIFAT-FILE-ALIST-FIX))
 (4 4 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (4 4 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (4 4 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 )
(HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7
 (12531 32 (:DEFINITION M1-FILE-ALIST-P))
 (10973 702 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (6255 1352 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (3760 96 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (3368 76 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (3281 3281 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (2924 14 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (2576 230 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1929 71 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (1697 77 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (1435 975 (:REWRITE DEFAULT-CDR))
 (1396 1396 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (1352 1352 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1352 1352 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1352 1352 (:REWRITE SUBSETP-TRANS2))
 (1352 1352 (:REWRITE SUBSETP-TRANS))
 (1303 107 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (1258 172 (:DEFINITION ASSOC-EQUAL))
 (984 133 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (944 944 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (911 911 (:REWRITE DEFAULT-CAR))
 (888 10 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (842 32 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (832 64 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (710 4 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE-FIX))
 (643 32 (:DEFINITION ALISTP))
 (608 32 (:REWRITE LENGTH-WHEN-STRINGP))
 (449 9 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (393 393 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (352 32 (:DEFINITION LEN))
 (351 351 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (328 328 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (320 64 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (320 64 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (320 32 (:DEFINITION UNSIGNED-BYTE-P))
 (288 32 (:DEFINITION INTEGER-RANGE-P))
 (260 52 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (256 256 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (256 64 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (197 63 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (195 39 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (186 31 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (164 164 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (128 128 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (128 128 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (128 128 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (128 64 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (128 64 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (128 64 (:REWRITE DEFAULT-<-1))
 (128 32 (:DEFINITION STRIP-CARS))
 (96 96 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (96 64 (:REWRITE STR::CONSP-OF-EXPLODE))
 (93 33 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (90 90 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (86 9 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (78 78 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (78 78 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (66 66 (:TYPE-PRESCRIPTION STRIP-CARS))
 (64 64 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (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))
 (52 52 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (34 34 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (34 34 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (33 33 (:TYPE-PRESCRIPTION D-E-P))
 (32 32 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (32 32 (:REWRITE DEFAULT-+-1))
 (27 9 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (14 14 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (10 10 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (8 8 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (7 7 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (4 4 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (2 2 (:REWRITE M1-FILE-ALIST-P-OF-HIFAT-FILE-ALIST-FIX))
 )
(HIFAT-FIND-FILE-CORRECTNESS-LEMMA-5
 (46621 115 (:DEFINITION M1-FILE-ALIST-P))
 (37908 1726 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (27777 5589 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (19625 49 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (18330 390 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (16917 1163 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (13758 13758 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (9511 259 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (8607 465 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (6986 292 (:REWRITE SUBSETP-CAR-MEMBER))
 (6397 78 (:REWRITE M1-FILE-P-OF-CDAR-WHEN-M1-FILE-ALIST-P))
 (6341 345 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (5872 145 (:DEFINITION MEMBER-EQUAL))
 (5593 5587 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (5593 5587 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (5589 5589 (:REWRITE SUBSETP-TRANS2))
 (5589 5589 (:REWRITE SUBSETP-TRANS))
 (4280 70 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (3857 26 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (3350 3350 (:REWRITE DEFAULT-CAR))
 (2990 230 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (2805 9 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE-FIX))
 (2692 2692 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (2507 115 (:DEFINITION ALISTP))
 (2211 187 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (2146 115 (:REWRITE LENGTH-WHEN-STRINGP))
 (2100 2100 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (2090 306 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (1897 277 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (1630 35 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (1540 1540 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (1265 115 (:DEFINITION LEN))
 (1240 210 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-37))
 (1150 230 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (1150 230 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (1150 115 (:DEFINITION UNSIGNED-BYTE-P))
 (1108 1108 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (1035 115 (:DEFINITION INTEGER-RANGE-P))
 (920 920 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (920 230 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (863 863 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (815 215 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (655 125 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (554 554 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (489 465 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (460 460 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (460 460 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (460 460 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (460 230 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (460 230 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (460 230 (:REWRITE DEFAULT-<-1))
 (460 115 (:DEFINITION STRIP-CARS))
 (420 1 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE-CONTENTS-OF-CDAR))
 (414 1 (:REWRITE HIFAT-SUBSETP-REFLEXIVE-LEMMA-3))
 (368 368 (:TYPE-PRESCRIPTION STRIP-CARS))
 (345 345 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (345 230 (:REWRITE STR::CONSP-OF-EXPLODE))
 (290 290 (:REWRITE SUBSETP-MEMBER . 2))
 (290 290 (:REWRITE SUBSETP-MEMBER . 1))
 (264 44 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (250 250 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (250 250 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (230 230 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (230 230 (:REWRITE DEFAULT-<-2))
 (230 230 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (230 115 (:REWRITE DEFAULT-+-2))
 (230 115 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (196 196 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (192 77 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (184 184 (:TYPE-PRESCRIPTION D-E-P))
 (115 115 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (115 115 (:REWRITE DEFAULT-+-1))
 (114 114 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (96 32 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (64 64 (:REWRITE SUBSETP-MEMBER . 4))
 (64 64 (:REWRITE SUBSETP-MEMBER . 3))
 (64 64 (:REWRITE MEMBER-WHEN-ATOM))
 (64 64 (:REWRITE INTERSECTP-MEMBER . 3))
 (64 64 (:REWRITE INTERSECTP-MEMBER . 2))
 (49 49 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (39 39 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (30 5 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (24 24 (:REWRITE M1-FILE-ALIST-P-OF-HIFAT-FILE-ALIST-FIX))
 (18 18 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (10 10 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (9 9 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (5 5 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (2 2 (:REWRITE SUBSETP-REFL))
 (1 1 (:REWRITE HIFAT-NO-DUPS-P-OF-M1-FILE->CONTENTS-OF-HIFAT-FIND-FILE))
 )
(HIFAT-FIND-FILE-CORRECTNESS-LEMMA-2
 (280 70 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (88 88 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (56 4 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (38 5 (:DEFINITION ASSOC-EQUAL))
 (34 4 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (33 3 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (25 1 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (24 7 (:REWRITE DEFAULT-CDR))
 (20 20 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (20 4 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (18 18 (:REWRITE DEFAULT-CAR))
 (18 4 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (18 3 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (14 1 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (6 6 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (5 1 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (4 4 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (4 4 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (4 4 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 (3 3 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (3 3 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (3 1 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (2 2 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (2 2 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (2 2 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (1 1 (:TYPE-PRESCRIPTION M1-FILE-P))
 (1 1 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1-LEMMA-1))
 )
(HIFAT-FIND-FILE-CORRECTNESS-LEMMA-3
 (316 79 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (117 117 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (98 8 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (89 12 (:DEFINITION ASSOC-EQUAL))
 (54 12 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (53 19 (:REWRITE DEFAULT-CDR))
 (53 2 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (52 2 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (40 40 (:REWRITE DEFAULT-CAR))
 (34 34 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (34 4 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (30 30 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (22 2 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (18 3 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (14 14 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (12 12 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (12 12 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (12 12 (:REWRITE SUBSETP-TRANS2))
 (12 12 (:REWRITE SUBSETP-TRANS))
 (10 2 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (6 6 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (6 2 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (5 5 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (5 5 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-2))
 (4 4 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (4 4 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (4 4 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (3 3 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (3 3 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (3 1 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 )
(HIFAT-FIND-FILE-CORRECTNESS-LEMMA-4
 (248 62 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (64 64 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (34 4 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (18 4 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (11 1 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (8 1 (:DEFINITION ASSOC-EQUAL))
 (6 1 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (4 4 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (4 4 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (2 2 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (2 2 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (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 FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(LEMMA
 (7809 21 (:DEFINITION M1-FILE-ALIST-P))
 (7060 436 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (4093 93 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (4083 870 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (2847 16 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (2563 337 (:DEFINITION ASSOC-EQUAL))
 (2118 2118 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (2114 2114 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (2098 294 (:REWRITE FAT32-FILENAME-FIX-WHEN-FAT32-FILENAME-P))
 (2037 6 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (1899 156 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1836 63 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (1543 69 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-6))
 (1488 1488 (:REWRITE DEFAULT-CAR))
 (1487 1046 (:REWRITE DEFAULT-CDR))
 (1445 76 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (1254 190 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (872 28 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (870 870 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (870 870 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (870 870 (:REWRITE SUBSETP-TRANS2))
 (870 870 (:REWRITE SUBSETP-TRANS))
 (824 824 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (546 42 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (429 21 (:DEFINITION ALISTP))
 (419 1 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE-FIX))
 (418 418 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (402 21 (:REWRITE FAT32-FILENAME-P-OF-CAAR-WHEN-M1-FILE-ALIST-P))
 (399 21 (:REWRITE LENGTH-WHEN-STRINGP))
 (380 76 (:REWRITE HIFAT-PLACE-FILE-CORRECTNESS-LEMMA-3))
 (348 348 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (250 50 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (231 21 (:DEFINITION LEN))
 (218 218 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (210 42 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (210 42 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (210 21 (:DEFINITION UNSIGNED-BYTE-P))
 (209 209 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (202 202 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (189 21 (:DEFINITION INTEGER-RANGE-P))
 (168 168 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (168 42 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (145 29 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (114 19 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (99 99 (:REWRITE-QUOTED-CONSTANT M1-FILE-CONTENTS-FIX-UNDER-M1-FILE-CONTENTS-EQUIV))
 (84 84 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (84 84 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (84 84 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (84 84 (:REWRITE HIFAT-SUBSETP-TRANSITIVE-LEMMA-1))
 (84 42 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (84 42 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (84 42 (:REWRITE DEFAULT-<-1))
 (84 21 (:DEFINITION STRIP-CARS))
 (82 82 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (63 63 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (63 42 (:REWRITE STR::CONSP-OF-EXPLODE))
 (60 24 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (59 51 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (58 58 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (58 58 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (48 48 (:TYPE-PRESCRIPTION STRIP-CARS))
 (42 42 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (42 42 (:REWRITE DEFAULT-<-2))
 (42 42 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (42 21 (:REWRITE DEFAULT-+-2))
 (42 21 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (31 3 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (24 24 (:TYPE-PRESCRIPTION D-E-P))
 (21 21 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (21 21 (:REWRITE DEFAULT-+-1))
 (16 16 (:TYPE-PRESCRIPTION ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (14 11 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (11 11 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (9 3 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (6 6 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 (6 6 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (6 2 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (2 2 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (2 2 (:REWRITE M1-FILE-ALIST-P-OF-HIFAT-FILE-ALIST-FIX))
 (2 2 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (1 1 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 )
(HIFAT-FIND-FILE-CORRECTNESS-4
 (118211 393 (:REWRITE M1-DIRECTORY-FILE-P-CORRECTNESS-1))
 (102540 7344 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (92189 343 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (74064 12288 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (61266 4422 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (59356 1859 (:REWRITE M1-FILE-ALIST-P-OF-CDR-WHEN-M1-FILE-ALIST-P))
 (29100 29100 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (24824 162 (:REWRITE M1-DIRECTORY-FILE-P-OF-M1-FILE-FIX))
 (13882 1262 (:DEFINITION LEN))
 (13050 1050 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (12405 12288 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (12405 12288 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (12288 12288 (:REWRITE SUBSETP-TRANS2))
 (12288 12288 (:REWRITE SUBSETP-TRANS))
 (10933 2761 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (8237 8075 (:REWRITE DEFAULT-CAR))
 (5000 1000 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (5000 1000 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (4992 4992 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (4647 1499 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (4248 4248 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (4147 393 (:REWRITE M1-FILE-P-WHEN-M1-REGULAR-FILE-P))
 (4050 1050 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (4000 4000 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (3915 3672 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (3786 3786 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (3786 2524 (:REWRITE STR::CONSP-OF-EXPLODE))
 (3744 1248 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (3744 1248 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (3465 1745 (:REWRITE DEFAULT-<-1))
 (3079 33 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (2524 1262 (:REWRITE DEFAULT-+-2))
 (2496 2496 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (2000 2000 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (2000 2000 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (2000 1000 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (2000 1000 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (1988 1988 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (1745 1745 (:REWRITE DEFAULT-<-2))
 (1574 1574 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (1574 1574 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (1352 200 (:REWRITE M1-FILE-ALIST-P-OF-M1-FILE-CONTENTS-FIX))
 (1262 1262 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (1262 1262 (:REWRITE DEFAULT-+-1))
 (1248 1248 (:LINEAR POSITION-WHEN-MEMBER))
 (1248 1248 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1122 120 (:DEFINITION ASSOC-EQUAL))
 (1110 1110 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (1012 1000 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (1008 224 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (997 333 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (808 808 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (729 81 (:REWRITE M1-FILE->CONTENTS$INLINE-OF-M1-FILE-FIX-X))
 (663 39 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (648 648 (:TYPE-PRESCRIPTION M1-FILE-FIX$INLINE))
 (524 524 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (505 81 (:REWRITE FAT32-FILENAME-P-OF-CAR-WHEN-FAT32-FILENAME-LIST-P))
 (468 39 (:DEFINITION MEMBER-EQUAL))
 (404 131 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (324 324 (:TYPE-PRESCRIPTION FAT32-FILENAME-FIX))
 (243 243 (:REWRITE CDR-CONS))
 (240 240 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (234 39 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-37))
 (224 224 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (195 195 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (162 162 (:REWRITE CAR-CONS))
 (120 120 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (120 120 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (120 120 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (120 120 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (81 81 (:REWRITE M1-FILE-P-OF-M1-FILE-FIX))
 (81 81 (:REWRITE M1-FILE->D-E$INLINE-OF-M1-FILE-FIX-X))
 (81 81 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-4))
 (78 78 (:REWRITE SUBSETP-MEMBER . 2))
 (78 78 (:REWRITE SUBSETP-MEMBER . 1))
 (44 44 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (27 22 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (22 22 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 )
(DIR-STREAM-P
 (234 18 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (90 18 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (90 18 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (76 18 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (72 72 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (36 36 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (36 36 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (36 18 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (36 18 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (31 31 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (28 28 (:REWRITE DEFAULT-CAR))
 (27 18 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (23 23 (:REWRITE DEFAULT-CDR))
 )
(CONSP-WHEN-DIR-STREAM-P)
(DIR-STREAM-FIX$INLINE)
(DIR-STREAM-P-OF-DIR-STREAM-FIX
 (31 7 (:REWRITE FAT32-FILENAME-LIST-FIX-WHEN-FAT32-FILENAME-LIST-P))
 (16 16 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (13 1 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (8 1 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (7 1 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (6 1 (:REWRITE HONS-DUPLICITY-ALIST-P-OF-CONS))
 (5 1 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (5 1 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (4 4 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (4 4 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (4 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-CAR))
 (2 2 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (2 2 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (2 1 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (2 1 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (1 1 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 )
(DIR-STREAM-FIX-WHEN-DIR-STREAM-P
 (2 2 (:DEFINITION STRIP-CARS))
 )
(DIR-STREAM-FIX$INLINE
 (2 2 (:DEFINITION STRIP-CARS))
 )
(FTY::TMP-DEFFIXTYPE-IDEMPOTENT)
(DIR-STREAM-EQUIV$INLINE)
(DIR-STREAM-EQUIV-IS-AN-EQUIVALENCE)
(DIR-STREAM-EQUIV-IMPLIES-EQUAL-DIR-STREAM-FIX-1)
(DIR-STREAM-FIX-UNDER-DIR-STREAM-EQUIV)
(EQUAL-OF-DIR-STREAM-FIX-1-FORWARD-TO-DIR-STREAM-EQUIV)
(EQUAL-OF-DIR-STREAM-FIX-2-FORWARD-TO-DIR-STREAM-EQUIV)
(DIR-STREAM-EQUIV-OF-DIR-STREAM-FIX-1-FORWARD)
(DIR-STREAM-EQUIV-OF-DIR-STREAM-FIX-2-FORWARD)
(DIR-STREAM->FILE-LIST$INLINE
 (2 2 (:DEFINITION STRIP-CARS))
 )
(FAT32-FILENAME-LIST-P-OF-DIR-STREAM->FILE-LIST)
(DIR-STREAM->FILE-LIST$INLINE-OF-DIR-STREAM-FIX-X
 (9 3 (:REWRITE DIR-STREAM-FIX-WHEN-DIR-STREAM-P))
 (6 6 (:TYPE-PRESCRIPTION DIR-STREAM-P))
 )
(DIR-STREAM->FILE-LIST$INLINE-DIR-STREAM-EQUIV-CONGRUENCE-ON-X)
(DIR-STREAM)
(DIR-STREAM-P-OF-DIR-STREAM
 (15 4 (:REWRITE FAT32-FILENAME-LIST-FIX-WHEN-FAT32-FILENAME-LIST-P))
 (13 1 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (8 8 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (8 1 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (6 1 (:REWRITE HONS-DUPLICITY-ALIST-P-OF-CONS))
 (5 1 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (5 1 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (4 4 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (3 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (2 2 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (2 2 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (2 1 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (2 1 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (1 1 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (1 1 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (1 1 (:REWRITE DEFAULT-CAR))
 )
(DIR-STREAM->FILE-LIST-OF-DIR-STREAM)
(DIR-STREAM-OF-FIELDS
 (3 1 (:REWRITE DIR-STREAM-FIX-WHEN-DIR-STREAM-P))
 (2 2 (:TYPE-PRESCRIPTION DIR-STREAM-P))
 )
(DIR-STREAM-FIX-WHEN-DIR-STREAM
 (3 1 (:REWRITE DIR-STREAM-FIX-WHEN-DIR-STREAM-P))
 (2 2 (:TYPE-PRESCRIPTION DIR-STREAM-P))
 )
(EQUAL-OF-DIR-STREAM)
(DIR-STREAM-OF-FAT32-FILENAME-LIST-FIX-FILE-LIST)
(DIR-STREAM-FAT32-FILENAME-LIST-EQUIV-CONGRUENCE-ON-FILE-LIST)
(DIR-STREAM-FIX-REDEF)
(TMP-DEFTYPES-NATP-OF-NFIX)
(DIR-STREAM-TABLE-P)
(BOOLEANP-OF-NATP-FOR-DIR-STREAM-TABLE-P-KEY-LEMMA)
(BOOLEANP-OF-DIR-STREAM-P-FOR-DIR-STREAM-TABLE-P-VAL-LEMMA)
(BOOLEANP-OF-NATP-FOR-DIR-STREAM-TABLE-P-KEY)
(BOOLEANP-OF-DIR-STREAM-P-FOR-DIR-STREAM-TABLE-P-VAL)
(DIR-STREAM-TABLE-P-OF-REVAPPEND)
(DIR-STREAM-TABLE-P-OF-REMOVE)
(DIR-STREAM-TABLE-P-OF-LAST)
(DIR-STREAM-TABLE-P-OF-NTHCDR)
(DIR-STREAM-TABLE-P-OF-BUTLAST)
(DIR-STREAM-TABLE-P-OF-UPDATE-NTH)
(DIR-STREAM-TABLE-P-OF-REPEAT)
(DIR-STREAM-TABLE-P-OF-TAKE)
(DIR-STREAM-TABLE-P-OF-UNION-EQUAL)
(DIR-STREAM-TABLE-P-OF-INTERSECTION-EQUAL-2)
(DIR-STREAM-TABLE-P-OF-INTERSECTION-EQUAL-1)
(DIR-STREAM-TABLE-P-OF-SET-DIFFERENCE-EQUAL)
(DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL)
(DIR-STREAM-TABLE-P-OF-RCONS)
(DIR-STREAM-TABLE-P-OF-APPEND)
(DIR-STREAM-TABLE-P-OF-REV)
(DIR-STREAM-TABLE-P-OF-DUPLICATED-MEMBERS)
(DIR-STREAM-TABLE-P-OF-DIFFERENCE)
(DIR-STREAM-TABLE-P-OF-INTERSECT-2)
(DIR-STREAM-TABLE-P-OF-INTERSECT-1)
(DIR-STREAM-TABLE-P-OF-UNION)
(DIR-STREAM-TABLE-P-OF-MERGESORT)
(DIR-STREAM-TABLE-P-OF-DELETE)
(DIR-STREAM-TABLE-P-OF-INSERT)
(DIR-STREAM-TABLE-P-OF-SFIX)
(DIR-STREAM-TABLE-P-OF-LIST-FIX)
(TRUE-LISTP-WHEN-DIR-STREAM-TABLE-P)
(DIR-STREAM-TABLE-P-WHEN-NOT-CONSP)
(DIR-STREAM-TABLE-P-OF-CDR-WHEN-DIR-STREAM-TABLE-P)
(DIR-STREAM-TABLE-P-OF-CONS)
(DIR-STREAM-TABLE-P-OF-REMOVE-ASSOC
 (76 10 (:REWRITE DIR-STREAM-TABLE-P-OF-CDR-WHEN-DIR-STREAM-TABLE-P))
 (32 32 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (16 16 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 )
(DIR-STREAM-TABLE-P-OF-PUT-ASSOC)
(DIR-STREAM-TABLE-P-OF-HONS-SHRINK-ALIST)
(DIR-STREAM-TABLE-P-OF-HONS-ACONS)
(DIR-STREAM-P-OF-CDR-OF-HONS-ASSOC-EQUAL-WHEN-DIR-STREAM-TABLE-P)
(ALISTP-WHEN-DIR-STREAM-TABLE-P-REWRITE)
(ALISTP-WHEN-DIR-STREAM-TABLE-P)
(DIR-STREAM-P-OF-CDAR-WHEN-DIR-STREAM-TABLE-P)
(NATP-OF-CAAR-WHEN-DIR-STREAM-TABLE-P)
(DIR-STREAM-TABLE-FIX$INLINE)
(DIR-STREAM-TABLE-P-OF-DIR-STREAM-TABLE-FIX
 (434 7 (:REWRITE NFIX-WHEN-NATP))
 (334 20 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (304 15 (:REWRITE NATP-OF-CAAR-WHEN-DIR-STREAM-TABLE-P))
 (291 8 (:DEFINITION DIR-STREAM-TABLE-P))
 (256 4 (:REWRITE NFIX-WHEN-ZP))
 (248 4 (:REWRITE ZP-OPEN))
 (244 6 (:DEFINITION INTEGER-LISTP))
 (236 12 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (230 12 (:REWRITE DIR-STREAM-TABLE-P-OF-CDR-WHEN-DIR-STREAM-TABLE-P))
 (134 24 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (124 6 (:DEFINITION NATP))
 (103 7 (:REWRITE DIR-STREAM-FIX-WHEN-DIR-STREAM-P))
 (100 15 (:REWRITE DIR-STREAM-P-OF-CDAR-WHEN-DIR-STREAM-TABLE-P))
 (90 80 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (75 40 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (74 6 (:REWRITE NAT-LISTP-OF-CDR-WHEN-NAT-LISTP))
 (50 6 (:REWRITE NATP-OF-CAR-WHEN-NAT-LISTP))
 (48 6 (:REWRITE NATP-OF-CAAR-WHEN-FILE-TABLE-P))
 (48 6 (:REWRITE NATP-OF-CAAR-WHEN-FD-TABLE-P))
 (44 44 (:REWRITE DEFAULT-CAR))
 (38 6 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (28 28 (:TYPE-PRESCRIPTION DIR-STREAM-P))
 (28 28 (:REWRITE DEFAULT-CDR))
 (24 24 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (24 24 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (24 24 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (24 24 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (24 24 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (18 18 (:REWRITE DEFAULT-<-2))
 (18 18 (:REWRITE DEFAULT-<-1))
 (16 16 (:TYPE-PRESCRIPTION NATP))
 (16 16 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (16 16 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (16 4 (:DEFINITION NFIX))
 (12 12 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (12 6 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (12 2 (:REWRITE FILE-TABLE-P-OF-CDR-WHEN-FILE-TABLE-P))
 (12 2 (:REWRITE FD-TABLE-P-OF-CDR-WHEN-FD-TABLE-P))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (8 8 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (8 8 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION ZP))
 )
(DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P
 (459 12 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (417 6 (:DEFINITION INTEGER-LISTP))
 (357 12 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (237 26 (:REWRITE DIR-STREAM-P-OF-CDAR-WHEN-DIR-STREAM-TABLE-P))
 (206 113 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (198 24 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (168 23 (:REWRITE DIR-STREAM-TABLE-P-OF-CDR-WHEN-DIR-STREAM-TABLE-P))
 (150 12 (:REWRITE NAT-LISTP-OF-CDR-WHEN-NAT-LISTP))
 (98 94 (:REWRITE DEFAULT-CAR))
 (78 15 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (69 10 (:REWRITE NATP-OF-CAAR-WHEN-DIR-STREAM-TABLE-P))
 (49 45 (:REWRITE DEFAULT-CDR))
 (48 48 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (48 15 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (36 36 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (36 36 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (27 3 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (24 24 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (24 24 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (24 24 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (18 9 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (12 12 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (12 6 (:REWRITE SET-EQUIV-ASYM))
 (6 6 (:TYPE-PRESCRIPTION SET-EQUIV))
 (6 6 (:REWRITE SUBSETP-OF-CDR))
 (5 5 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE SUBSETP-TRANS2))
 (3 3 (:REWRITE SUBSETP-TRANS))
 (3 3 (:REWRITE SUBSETP-REFL))
 )
(DIR-STREAM-TABLE-FIX$INLINE
 (10 10 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (6 1 (:REWRITE NATP-OF-CAAR-WHEN-DIR-STREAM-TABLE-P))
 (6 1 (:REWRITE DIR-STREAM-TABLE-P-OF-CDR-WHEN-DIR-STREAM-TABLE-P))
 (6 1 (:REWRITE DIR-STREAM-P-OF-CDAR-WHEN-DIR-STREAM-TABLE-P))
 (5 5 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 )
(FTY::TMP-DEFFIXTYPE-IDEMPOTENT
 (2 2 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (1 1 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 )
(DIR-STREAM-TABLE-EQUIV$INLINE)
(DIR-STREAM-TABLE-EQUIV-IS-AN-EQUIVALENCE)
(DIR-STREAM-TABLE-EQUIV-IMPLIES-EQUAL-DIR-STREAM-TABLE-FIX-1)
(DIR-STREAM-TABLE-FIX-UNDER-DIR-STREAM-TABLE-EQUIV)
(EQUAL-OF-DIR-STREAM-TABLE-FIX-1-FORWARD-TO-DIR-STREAM-TABLE-EQUIV)
(EQUAL-OF-DIR-STREAM-TABLE-FIX-2-FORWARD-TO-DIR-STREAM-TABLE-EQUIV)
(DIR-STREAM-TABLE-EQUIV-OF-DIR-STREAM-TABLE-FIX-1-FORWARD)
(DIR-STREAM-TABLE-EQUIV-OF-DIR-STREAM-TABLE-FIX-2-FORWARD)
(CONS-OF-NFIX-K-UNDER-DIR-STREAM-TABLE-EQUIV
 (31 4 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (20 2 (:REWRITE DIR-STREAM-TABLE-P-OF-CONS))
 (6 6 (:TYPE-PRESCRIPTION DIR-STREAM-TABLE-P))
 (6 6 (:TYPE-PRESCRIPTION DIR-STREAM-P))
 (6 6 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (4 2 (:REWRITE DIR-STREAM-FIX-WHEN-DIR-STREAM-P))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 )
(CONS-NAT-EQUIV-CONGRUENCE-ON-K-UNDER-DIR-STREAM-TABLE-EQUIV)
(CONS-OF-DIR-STREAM-FIX-V-UNDER-DIR-STREAM-TABLE-EQUIV
 (33 4 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (22 2 (:REWRITE DIR-STREAM-TABLE-P-OF-CONS))
 (6 6 (:TYPE-PRESCRIPTION NATP))
 (6 6 (:TYPE-PRESCRIPTION DIR-STREAM-TABLE-P))
 (6 6 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (4 2 (:REWRITE NFIX-WHEN-NATP))
 (3 3 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 )
(CONS-DIR-STREAM-EQUIV-CONGRUENCE-ON-V-UNDER-DIR-STREAM-TABLE-EQUIV)
(CONS-OF-DIR-STREAM-TABLE-FIX-Y-UNDER-DIR-STREAM-TABLE-EQUIV
 (15 2 (:REWRITE DIR-STREAM-TABLE-P-OF-CONS))
 (9 9 (:TYPE-PRESCRIPTION DIR-STREAM-P))
 (8 8 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (6 6 (:TYPE-PRESCRIPTION NATP))
 (6 2 (:REWRITE NFIX-WHEN-NATP))
 (6 2 (:REWRITE DIR-STREAM-FIX-WHEN-DIR-STREAM-P))
 (4 4 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 )
(CONS-DIR-STREAM-TABLE-EQUIV-CONGRUENCE-ON-Y-UNDER-DIR-STREAM-TABLE-EQUIV)
(DIR-STREAM-TABLE-FIX-OF-ACONS
 (19 3 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (10 1 (:REWRITE DIR-STREAM-TABLE-P-OF-CONS))
 (4 4 (:TYPE-PRESCRIPTION DIR-STREAM-TABLE-P))
 (4 4 (:TYPE-PRESCRIPTION DIR-STREAM-P))
 (4 4 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (4 2 (:REWRITE NFIX-WHEN-NATP))
 (4 2 (:REWRITE DIR-STREAM-FIX-WHEN-DIR-STREAM-P))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 )
(DIR-STREAM-TABLE-FIX-OF-APPEND
 (324 19 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (174 6 (:REWRITE DIR-STREAM-TABLE-P-OF-APPEND))
 (102 90 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (88 52 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (85 85 (:TYPE-PRESCRIPTION DIR-STREAM-TABLE-P))
 (72 6 (:REWRITE DIR-STREAM-TABLE-P-OF-LIST-FIX))
 (51 11 (:REWRITE DIR-STREAM-TABLE-P-OF-CDR-WHEN-DIR-STREAM-TABLE-P))
 (50 1 (:REWRITE DIR-STREAM-TABLE-P-OF-CONS))
 (36 36 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 (28 4 (:REWRITE NFIX-WHEN-NATP))
 (28 4 (:REWRITE DIR-STREAM-FIX-WHEN-DIR-STREAM-P))
 (24 4 (:REWRITE NATP-OF-CAAR-WHEN-DIR-STREAM-TABLE-P))
 (24 4 (:REWRITE DIR-STREAM-P-OF-CDAR-WHEN-DIR-STREAM-TABLE-P))
 (12 12 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (8 8 (:TYPE-PRESCRIPTION DIR-STREAM-P))
 (7 7 (:TYPE-PRESCRIPTION NATP))
 )
(CONSP-CAR-OF-DIR-STREAM-TABLE-FIX
 (72 10 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (31 31 (:TYPE-PRESCRIPTION DIR-STREAM-TABLE-P))
 (30 30 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (30 5 (:REWRITE DIR-STREAM-TABLE-P-OF-CDR-WHEN-DIR-STREAM-TABLE-P))
 (18 2 (:REWRITE NFIX-WHEN-NATP))
 (18 2 (:REWRITE DIR-STREAM-FIX-WHEN-DIR-STREAM-P))
 (16 16 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (12 2 (:REWRITE NATP-OF-CAAR-WHEN-DIR-STREAM-TABLE-P))
 (12 2 (:REWRITE DIR-STREAM-P-OF-CDAR-WHEN-DIR-STREAM-TABLE-P))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:TYPE-PRESCRIPTION DIR-STREAM-P))
 )
(FAT32-FILENAME-LIST-P-OF-STRIP-CARS-WHEN-M1-FILE-ALIST-P
 (132 14 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (95 1 (:REWRITE SET-EQUIV-OF-CONS-SELF))
 (83 1 (:REWRITE MEMBER-OF-STRIP-CARS))
 (43 2 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (29 2 (:REWRITE SUBSETP-CAR-MEMBER))
 (29 1 (:REWRITE SUBSETP-CONS-2))
 (28 1 (:DEFINITION MEMBER-EQUAL))
 (25 1 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-37))
 (23 2 (:REWRITE HIFAT-EQUIV-IMPLIES-SET-EQUIV-STRIP-CARS-1-LEMMA-2))
 (17 1 (:REWRITE HIFAT-SUBSETP-REFLEXIVE))
 (15 5 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (15 5 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (12 1 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (10 10 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE SUBSETP-TRANS2))
 (7 7 (:REWRITE SUBSETP-TRANS))
 (6 1 (:DEFINITION ASSOC-EQUAL))
 (5 5 (:TYPE-PRESCRIPTION ZP))
 (5 5 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (5 5 (:TYPE-PRESCRIPTION LEN))
 (5 5 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE CONSP-OF-STRIP-CARS))
 (5 3 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (5 3 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (4 4 (:TYPE-PRESCRIPTION HIFAT-NO-DUPS-P))
 (4 2 (:REWRITE SET-EQUIV-ASYM))
 (3 1 (:REWRITE HIFAT-NO-DUPS-P-OF-CDR))
 (2 2 (:TYPE-PRESCRIPTION SET-EQUIV))
 (2 2 (:TYPE-PRESCRIPTION HIFAT-SUBSETP))
 (2 2 (:REWRITE SUBSETP-OF-CDR))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (1 1 (:TYPE-PRESCRIPTION NULL))
 (1 1 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (1 1 (:REWRITE HIFAT-SUBSETP-WHEN-ATOM))
 (1 1 (:REWRITE HIFAT-SUBSETP-TRANSITIVE))
 (1 1 (:DEFINITION NULL))
 )
(NAT-LISTP-OF-STRIP-CARS-WHEN-DIR-STREAM-TABLE-P
 (60 5 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (36 4 (:REWRITE FILE-TABLE-P-CORRECTNESS-1))
 (36 4 (:REWRITE FD-TABLE-P-CORRECTNESS-1))
 (19 7 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (15 4 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (14 1 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CONS))
 (12 12 (:REWRITE FILE-TABLE-P-WHEN-SUBSETP-EQUAL))
 (12 12 (:REWRITE FD-TABLE-P-WHEN-SUBSETP-EQUAL))
 (12 2 (:REWRITE FILE-TABLE-P-OF-CDR-WHEN-FILE-TABLE-P))
 (12 2 (:REWRITE FD-TABLE-P-OF-CDR-WHEN-FD-TABLE-P))
 (8 8 (:REWRITE CONSP-OF-STRIP-CARS))
 (7 7 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (6 6 (:REWRITE FILE-TABLE-P-WHEN-NOT-CONSP))
 (6 6 (:REWRITE FD-TABLE-P-WHEN-NOT-CONSP))
 (6 6 (:REWRITE DEFAULT-CAR))
 (5 5 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (5 5 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (5 1 (:REWRITE FAT32-MASKED-ENTRY-P-OF-CAR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (3 3 (:REWRITE DEFAULT-CDR))
 (2 2 (:TYPE-PRESCRIPTION FAT32-MASKED-ENTRY-P))
 (2 1 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 )
(FAT32-FILENAME-LIST-P-OF-<<-MERGE
 (656 122 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (204 5 (:DEFINITION MEMBER-EQUAL))
 (200 4 (:REWRITE SUBSETP-OF-CONS))
 (136 35 (:REWRITE <<-TRICHOTOMY))
 (133 100 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (115 115 (:REWRITE SUBSETP-TRANS2))
 (115 115 (:REWRITE SUBSETP-TRANS))
 (112 2 (:REWRITE SET-EQUIV-OF-CONS-SELF))
 (96 6 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (86 6 (:REWRITE SUBSETP-CONS-2))
 (37 33 (:REWRITE <<-TRANSITIVE))
 (30 16 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (27 27 (:REWRITE DEFAULT-CAR))
 (16 2 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (11 11 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE SUBSETP-MEMBER . 2))
 (10 10 (:REWRITE SUBSETP-MEMBER . 1))
 (10 2 (:REWRITE TRUE-LISTP-WHEN-D-E-P))
 (6 2 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (4 4 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (4 4 (:TYPE-PRESCRIPTION D-E-P))
 (4 4 (:REWRITE D-E-P-WHEN-MEMBER-EQUAL-OF-D-E-LIST-P))
 (4 2 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (4 2 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (2 2 (:TYPE-PRESCRIPTION STRING-LISTP))
 (2 2 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (2 2 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (2 2 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (2 2 (:REWRITE SET::IN-SET))
 (2 2 (:DEFINITION STRING-LISTP))
 (1 1 (:REWRITE SUBSETP-NIL))
 (1 1 (:REWRITE SET-EQUIV-OF-NIL))
 (1 1 (:REWRITE <<-IRREFLEXIVE))
 )
(FAT32-FILENAME-LIST-P-OF-<<-SORT-WHEN-FAT32-FILENAME-LIST-P
 (4203 33 (:REWRITE <<-SORT-CONSP))
 (3516 4 (:DEFINITION TAKE))
 (3387 14 (:REWRITE CONSP-OF-NTHCDR))
 (3188 8 (:REWRITE TAKE-OF-TOO-MANY))
 (3184 8 (:REWRITE TAKE-OF-LEN-FREE))
 (2897 8 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (2690 33 (:REWRITE ZP-OPEN))
 (2261 32 (:REWRITE NFIX-WHEN-ZP))
 (2160 41 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (2080 4 (:DEFINITION NTHCDR))
 (1913 31 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1807 32 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1513 62 (:LINEAR FLOOR-TYPE-2 . 1))
 (1425 162 (:REWRITE FLOOR-=-X/Y . 3))
 (1425 162 (:REWRITE FLOOR-=-X/Y . 2))
 (1025 810 (:REWRITE DEFAULT-*-2))
 (1025 810 (:REWRITE DEFAULT-*-1))
 (888 162 (:REWRITE FLOOR-TYPE-3 . 2))
 (826 491 (:REWRITE DEFAULT-<-1))
 (816 491 (:REWRITE DEFAULT-<-2))
 (777 162 (:REWRITE FLOOR-TYPE-3 . 3))
 (728 728 (:TYPE-PRESCRIPTION HIFAT-BOUNDED-FILE-ALIST-P))
 (703 13 (:REWRITE CONSP-OF-TAKE))
 (700 25 (:REWRITE FLOOR-TYPE-2))
 (687 687 (:TYPE-PRESCRIPTION PAINFUL-DEBUGGING-LEMMA-15))
 (687 687 (:TYPE-PRESCRIPTION FLOOR-TYPE-1 . 2))
 (687 687 (:TYPE-PRESCRIPTION FLOOR-TYPE-1 . 1))
 (632 138 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 (541 162 (:REWRITE FLOOR-TYPE-4 . 2))
 (522 174 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 2))
 (522 174 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 1))
 (448 7 (:REWRITE NATP-POSP--1))
 (441 50 (:LINEAR PAINFUL-DEBUGGING-LEMMA-15))
 (399 7 (:REWRITE NATP-POSP))
 (348 348 (:LINEAR LEN-WHEN-FAT32-FILENAME-LIST-PREFIXP))
 (337 62 (:LINEAR FLOOR-TYPE-2 . 2))
 (296 296 (:REWRITE INTEGERP-+-MINUS-*))
 (244 24 (:REWRITE FLOOR-RECURSION))
 (240 162 (:REWRITE FLOOR-TYPE-4 . 3))
 (236 4 (:REWRITE FLOOR-=-X/Y . 4))
 (226 55 (:LINEAR FLOOR-TYPE-1 . 2))
 (174 174 (:LINEAR POSITION-WHEN-MEMBER))
 (174 174 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (132 62 (:REWRITE DEFAULT-+-2))
 (132 4 (:REWRITE CANCEL-EQUAL-+-*))
 (88 55 (:LINEAR FLOOR-TYPE-1 . 1))
 (80 62 (:REWRITE DEFAULT-+-1))
 (66 8 (:REWRITE <-0-+-NEGATIVE-1))
 (48 16 (:LINEAR LEN-WHEN-HIFAT-BOUNDED-FILE-ALIST-P . 3))
 (40 40 (:REWRITE SUBSETP-TRANS2))
 (40 40 (:REWRITE SUBSETP-TRANS))
 (30 9 (:LINEAR X*Y>1-POSITIVE))
 (30 4 (:REWRITE COMMUTATIVITY-OF-+))
 (18 18 (:REWRITE DEFAULT-CDR))
 (16 16 (:TYPE-PRESCRIPTION ZP))
 (10 1 (:REWRITE SUBSETP-CONS-2))
 (8 8 (:REWRITE TAKE-WHEN-ATOM))
 (7 7 (:TYPE-PRESCRIPTION NATP))
 (7 7 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE EQUAL-CONSTANT-+))
 (1 1 (:REWRITE SET-EQUIV-OF-NIL))
 )
(STRING-LISTP-WHEN-FAT32-FILENAME-LIST-P
 (21 8 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (7 7 (:REWRITE SUBSETP-TRANS2))
 (7 7 (:REWRITE SUBSETP-TRANS))
 (6 6 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 )
(HIFAT-OPENDIR
 (188 19 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (184 13 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (130 10 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (102 6 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (84 12 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (68 19 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (61 14 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (55 19 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (50 10 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (50 10 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (48 6 (:DEFINITION MEMBER-EQUAL))
 (40 40 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (40 10 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (32 32 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (30 30 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (30 6 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (21 21 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (20 20 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (20 20 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (20 20 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (20 10 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (20 10 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (19 19 (:REWRITE DEFAULT-CAR))
 (18 10 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (18 10 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (18 4 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (16 4 (:DEFINITION STRIP-CARS))
 (15 15 (:REWRITE DEFAULT-CDR))
 (14 14 (:REWRITE SUBSETP-TRANS2))
 (14 14 (:REWRITE SUBSETP-TRANS))
 (14 6 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (12 12 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (12 12 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (12 12 (:REWRITE SUBSETP-MEMBER . 2))
 (12 12 (:REWRITE SUBSETP-MEMBER . 1))
 (12 12 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (10 10 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (10 10 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (9 3 (:REWRITE <<-SORT-CONSP))
 (8 8 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (6 6 (:REWRITE CONSP-OF-STRIP-CARS))
 (4 4 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (4 4 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 )
(DIR-STREAM-TABLE-P-OF-HIFAT-OPENDIR
 (38 6 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (36 4 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (34 4 (:DEFINITION STRIP-CARS))
 (28 4 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (25 5 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (24 9 (:REWRITE DEFAULT-CAR))
 (18 4 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (18 4 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (14 2 (:REWRITE CONSP-CAR-OF-DIR-STREAM-TABLE-FIX))
 (10 10 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (10 10 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (10 2 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (10 2 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (6 6 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (6 5 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (4 4 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (4 4 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (4 4 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (4 4 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (4 4 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (2 2 (:TYPE-PRESCRIPTION M1-FILE-P))
 (2 2 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 )
(HIFAT-OPENDIR-CORRECTNESS-2
 (19 3 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (18 2 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (17 2 (:DEFINITION STRIP-CARS))
 (14 2 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (12 2 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (11 4 (:REWRITE DEFAULT-CAR))
 (9 2 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (9 2 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (7 1 (:REWRITE CONSP-CAR-OF-DIR-STREAM-TABLE-FIX))
 (5 5 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (5 1 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (5 1 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (4 4 (:TYPE-PRESCRIPTION DIR-STREAM-TABLE-P))
 (4 4 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (3 3 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (2 2 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (2 2 (:TYPE-PRESCRIPTION DIR-STREAM-TABLE-FIX$INLINE))
 (2 2 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (2 2 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (2 2 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (2 2 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (1 1 (:TYPE-PRESCRIPTION M1-FILE-P))
 (1 1 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 )
(DIR-STREAM-TABLE-EQUIV-IMPLIES-EQUAL-HIFAT-OPENDIR-3
 (38 6 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (36 4 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (34 4 (:DEFINITION STRIP-CARS))
 (31 6 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (28 4 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (22 8 (:REWRITE DEFAULT-CAR))
 (18 4 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (14 2 (:REWRITE CONSP-CAR-OF-DIR-STREAM-TABLE-FIX))
 (10 10 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (10 10 (:TYPE-PRESCRIPTION DIR-STREAM-TABLE-P))
 (10 10 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (10 3 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (10 2 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (10 2 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (6 6 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (5 5 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (4 4 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (4 4 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (4 4 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (4 4 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (4 4 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (2 2 (:TYPE-PRESCRIPTION M1-FILE-P))
 (2 2 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 )
(HIFAT-OPENDIR-CORRECTNESS-LEMMA-1)
(HIFAT-OPENDIR-CORRECTNESS-LEMMA-2
 (10 2 (:DEFINITION STRIP-CARS))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(HIFAT-OPENDIR-CORRECTNESS-1
 (19 3 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (18 2 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (17 2 (:DEFINITION STRIP-CARS))
 (14 2 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-51))
 (12 2 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (11 4 (:REWRITE DEFAULT-CAR))
 (9 2 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (9 2 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (7 1 (:REWRITE CONSP-CAR-OF-DIR-STREAM-TABLE-FIX))
 (5 5 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (5 1 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (5 1 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (4 4 (:TYPE-PRESCRIPTION DIR-STREAM-TABLE-P))
 (4 4 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (3 3 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (2 2 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (2 2 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (2 2 (:TYPE-PRESCRIPTION DIR-STREAM-TABLE-FIX$INLINE))
 (2 2 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (2 2 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (2 2 (:REWRITE FAT32-FILENAME-P-WHEN-MEMBER-EQUAL-OF-FAT32-FILENAME-LIST-P))
 (2 2 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (1 1 (:TYPE-PRESCRIPTION M1-FILE-P))
 (1 1 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-1))
 )
(HIFAT-EQUIV-IMPLIES-EQUAL-HIFAT-OPENDIR-1
 (819 93 (:REWRITE ABS-LSTAT-REFINEMENT-LEMMA-1))
 (540 98 (:REWRITE M1-REGULAR-FILE-P-CORRECTNESS-1))
 (490 90 (:REWRITE M1-DIRECTORY-FILE-P-WHEN-M1-FILE-P))
 (312 4 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (250 50 (:DEFINITION LEN))
 (246 61 (:REWRITE ABS-FIND-FILE-CORRECTNESS-1-LEMMA-40))
 (235 47 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (235 47 (:REWRITE FAT32-FILENAME-P-CORRECTNESS-1))
 (231 231 (:TYPE-PRESCRIPTION M1-REGULAR-FILE-P))
 (223 108 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-3))
 (190 108 (:REWRITE DEFAULT-CAR))
 (190 34 (:DEFINITION STRIP-CARS))
 (168 128 (:REWRITE DEFAULT-CDR))
 (168 4 (:DEFINITION MEMBER-EQUAL))
 (144 12 (:REWRITE M1-READ-AFTER-WRITE-LEMMA-1))
 (128 8 (:REWRITE SUBSETP-CAR-MEMBER))
 (115 115 (:REWRITE HIFAT-FIND-FILE-CORRECTNESS-LEMMA-7))
 (112 24 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (100 50 (:REWRITE DEFAULT-+-2))
 (94 94 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (94 94 (:TYPE-PRESCRIPTION FAT32-FILENAME-P))
 (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))
 (82 82 (:REWRITE M1-FILE-ALIST-P-WHEN-SUBSETP-EQUAL))
 (61 61 (:REWRITE ABS-MKDIR-CORRECTNESS-LEMMA-49))
 (60 4 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (54 14 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (50 50 (:REWRITE DEFAULT-+-1))
 (45 13 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (42 6 (:REWRITE CONSP-CAR-OF-DIR-STREAM-TABLE-FIX))
 (41 41 (:REWRITE M1-FILE-ALIST-P-WHEN-NOT-CONSP))
 (40 40 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (26 26 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (26 26 (:REWRITE CONSP-OF-STRIP-CARS))
 (25 25 (:REWRITE FAT32-FILENAME-LIST-EQUIV-WHEN-ATOM-RIGHT))
 (20 20 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (20 8 (:REWRITE MEMBER-WHEN-ATOM))
 (16 16 (:TYPE-PRESCRIPTION DIR-STREAM-TABLE-P))
 (16 16 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (16 4 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (12 12 (:TYPE-PRESCRIPTION SET-EQUIV))
 (12 12 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (8 8 (:REWRITE SUBSETP-OF-CDR))
 (8 8 (:REWRITE SUBSETP-MEMBER . 4))
 (8 8 (:REWRITE SUBSETP-MEMBER . 3))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (8 8 (:REWRITE INTERSECTP-MEMBER . 3))
 (8 8 (:REWRITE INTERSECTP-MEMBER . 2))
 (8 8 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (4 4 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 (3 1 (:REWRITE <<-SORT-CONSP))
 )
(HIFAT-READDIR
 (55 2 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (52 4 (:REWRITE OMAP::ALISTP-WHEN-MAPP))
 (49 49 (:REWRITE DEFAULT-CAR))
 (40 2 (:REWRITE INTEGER-LISTP-WHEN-NAT-LISTP))
 (40 2 (:DEFINITION ALISTP))
 (40 1 (:DEFINITION INTEGER-LISTP))
 (34 23 (:REWRITE DEFAULT-CDR))
 (21 3 (:REWRITE NAT-LISTP-IF-FAT32-MASKED-ENTRY-LIST-P))
 (20 4 (:REWRITE OMAP::MFIX-IMPLIES-MAPP))
 (20 4 (:REWRITE OMAP::MAPP-WHEN-NOT-EMPTY))
 (16 16 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (16 4 (:REWRITE ALISTP-WHEN-HONS-DUPLICITY-ALIST-P))
 (12 2 (:REWRITE ABS-PWRITE-CORRECTNESS-LEMMA-37))
 (12 1 (:REWRITE NAT-LISTP-OF-CDR-WHEN-NAT-LISTP))
 (9 9 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (9 9 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (8 8 (:TYPE-PRESCRIPTION OMAP::MFIX))
 (8 8 (:TYPE-PRESCRIPTION HONS-DUPLICITY-ALIST-P))
 (8 8 (:TYPE-PRESCRIPTION OMAP::EMPTY))
 (8 8 (:REWRITE DEFAULT-<-2))
 (8 8 (:REWRITE DEFAULT-<-1))
 (8 4 (:REWRITE OMAP::MFIX-WHEN-MAPP))
 (8 4 (:REWRITE OMAP::MAPP-NON-NIL-IMPLIES-NON-EMPTY))
 (8 2 (:REWRITE NFIX-WHEN-ZP))
 (6 6 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (6 1 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-OF-CDR-WHEN-FAT32-MASKED-ENTRY-LIST-P))
 (4 4 (:REWRITE HONS-DUPLICITY-ALIST-P-WHEN-NOT-CONSP))
 (4 4 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-NOT-CONSP))
 (4 4 (:REWRITE FAT32-MASKED-ENTRY-LIST-P-WHEN-BOUNDED-NAT-LISTP))
 (3 3 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (3 3 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (3 3 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (3 3 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (2 2 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (2 2 (:REWRITE ZP-OPEN))
 (2 2 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 (2 1 (:REWRITE SUBSETP-WHEN-SUBSETP))
 (2 1 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 )
(DIR-STREAM-TABLE-P-OF-HIFAT-READDIR
 (441 12 (:REWRITE PUT-ASSOC-EQUAL-WITHOUT-CHANGE . 2))
 (375 30 (:DEFINITION ASSOC-EQUAL))
 (321 111 (:REWRITE DEFAULT-CAR))
 (297 52 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (225 6 (:REWRITE EQUAL-OF-DIR-STREAM))
 (210 30 (:REWRITE CONSP-CAR-OF-DIR-STREAM-TABLE-FIX))
 (192 6 (:DEFINITION PUT-ASSOC-EQUAL))
 (177 6 (:REWRITE FAT32-FILENAME-LIST-FIX-WHEN-FAT32-FILENAME-LIST-P))
 (144 6 (:REWRITE FAT32-FILENAME-LIST-P-OF-CDR-WHEN-FAT32-FILENAME-LIST-P))
 (106 106 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (75 75 (:REWRITE DEFAULT-CDR))
 (53 53 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (12 12 (:TYPE-PRESCRIPTION FAT32-FILENAME-LIST-P))
 (12 12 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (12 12 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-SUBSETP-EQUAL))
 (9 9 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 (8 6 (:REWRITE DEFAULT-<-1))
 (6 6 (:TYPE-PRESCRIPTION DIR-STREAM-P))
 (6 6 (:REWRITE FAT32-FILENAME-LIST-P-WHEN-NOT-CONSP))
 (6 6 (:REWRITE FAT32-FILENAME-LIST-P-OF-DIR-STREAM->FILE-LIST))
 (6 6 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (5 1 (:REWRITE NFIX-WHEN-NATP))
 (4 1 (:REWRITE NFIX-WHEN-ZP))
 (3 1 (:DEFINITION NATP))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE ZP-OPEN))
 )
(HIFAT-CLOSEDIR
 (24 12 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (2 2 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (1 1 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 )
(DIR-STREAM-TABLE-P-OF-HIFAT-CLOSEDIR
 (51 1 (:DEFINITION REMOVE-ASSOC-EQUAL))
 (37 3 (:REWRITE REMOVE-ASSOC-WHEN-ABSENT-1))
 (26 12 (:REWRITE DEFAULT-CAR))
 (26 3 (:DEFINITION ASSOC-EQUAL))
 (18 3 (:REWRITE DIR-STREAM-TABLE-FIX-WHEN-DIR-STREAM-TABLE-P))
 (14 2 (:REWRITE CONSP-CAR-OF-DIR-STREAM-TABLE-FIX))
 (8 8 (:REWRITE DIR-STREAM-TABLE-P-WHEN-SUBSETP-EQUAL))
 (5 5 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DIR-STREAM-TABLE-P-WHEN-NOT-CONSP))
 (3 3 (:REWRITE HIFAT-SUBSETP-PRESERVES-ASSOC))
 (3 3 (:REWRITE CONSP-OF-ASSOC-WHEN-HIFAT-EQUIV-LEMMA-1))
 (2 2 (:REWRITE-QUOTED-CONSTANT FAT32-FILENAME-LIST-FIX-UNDER-FAT32-FILENAME-LIST-EQUIV))
 )