(L5-REGULAR-FILE-ENTRY-P
 (70 70 (:REWRITE DEFAULT-CDR))
 (40 25 (:REWRITE DEFAULT-+-2))
 (25 25 (:REWRITE DEFAULT-+-1))
 (6 6 (:LINEAR POSITION-WHEN-MEMBER))
 (6 6 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(L5-REGULAR-FILE-CONTENTS)
(L5-REGULAR-FILE-LENGTH)
(L5-REGULAR-FILE-USER-READ)
(L5-REGULAR-FILE-USER-WRITE)
(L5-REGULAR-FILE-OTHER-READ)
(L5-REGULAR-FILE-OTHER-WRITE)
(L5-REGULAR-FILE-USER)
(L5-MAKE-REGULAR-FILE)
(L5-MAKE-REGULAR-FILE-CORRECTNESS-1
 (32 32 (:REWRITE DEFAULT-CDR))
 (16 8 (:REWRITE DEFAULT-+-2))
 (10 10 (:REWRITE DEFAULT-CAR))
 (8 8 (:TYPE-PRESCRIPTION LEN))
 (8 8 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 )
(L5-MAKE-REGULAR-FILE-CORRECTNESS-2)
(L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-1)
(L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-2)
(L5-FS-P
 (140 66 (:REWRITE DEFAULT-+-2))
 (92 66 (:REWRITE DEFAULT-+-1))
 (48 12 (:DEFINITION INTEGER-ABS))
 (48 6 (:REWRITE LENGTH-WHEN-STRINGP))
 (30 6 (:DEFINITION LEN))
 (26 26 (:REWRITE DEFAULT-CAR))
 (23 23 (:REWRITE DEFAULT-CDR))
 (21 16 (:REWRITE DEFAULT-<-2))
 (20 16 (:REWRITE DEFAULT-<-1))
 (12 12 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 6 (:TYPE-PRESCRIPTION LEN))
 (6 6 (:REWRITE DEFAULT-REALPART))
 (6 6 (:REWRITE DEFAULT-NUMERATOR))
 (6 6 (:REWRITE DEFAULT-IMAGPART))
 (6 6 (:REWRITE DEFAULT-DENOMINATOR))
 (6 6 (:REWRITE DEFAULT-COERCE-2))
 (6 6 (:REWRITE DEFAULT-COERCE-1))
 )
(L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3
 (303 303 (:REWRITE DEFAULT-CDR))
 (88 88 (:REWRITE DEFAULT-CAR))
 (63 9 (:DEFINITION NAT-LISTP))
 (45 25 (:REWRITE DEFAULT-+-2))
 (27 9 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (25 25 (:REWRITE DEFAULT-+-1))
 (23 23 (:REWRITE DEFAULT-<-2))
 (23 23 (:REWRITE DEFAULT-<-1))
 (18 18 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (18 18 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER))
 (1 1 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(ALISTP-L5-FS-P
 (312 6 (:REWRITE ALISTP-L2-FS-P))
 (296 12 (:DEFINITION L2-FS-P))
 (176 6 (:REWRITE ALISTP-L3-FS-P))
 (160 10 (:DEFINITION L3-FS-P))
 (156 156 (:REWRITE DEFAULT-CAR))
 (143 143 (:TYPE-PRESCRIPTION L2-FS-P))
 (138 6 (:REWRITE ALISTP-L1-FS-P))
 (122 122 (:REWRITE DEFAULT-CDR))
 (122 10 (:DEFINITION L1-FS-P))
 (74 74 (:TYPE-PRESCRIPTION L3-FS-P))
 (74 74 (:TYPE-PRESCRIPTION L1-FS-P))
 (54 54 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (41 15 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (27 9 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (27 9 (:DEFINITION NATP))
 (22 11 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (10 10 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE DEFAULT-<-1))
 )
(L5-FS-P-ASSOC
 (428 428 (:REWRITE DEFAULT-CAR))
 (391 229 (:REWRITE DEFAULT-CDR))
 (257 119 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 )
(L5-REGULAR-FILE-READABLE-P)
(L5-STAT
 (271 95 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (212 18 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (162 11 (:DEFINITION L5-FS-P))
 (104 8 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (79 79 (:REWRITE DEFAULT-CAR))
 (75 75 (:REWRITE DEFAULT-CDR))
 (64 8 (:DEFINITION MEMBER-EQUAL))
 (40 40 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (40 8 (:DEFINITION ASSOC-EQUAL))
 (28 12 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (25 5 (:DEFINITION LEN))
 (16 16 (:REWRITE SUBSETP-MEMBER . 2))
 (16 16 (:REWRITE SUBSETP-MEMBER . 1))
 (15 5 (:DEFINITION CHARACTER-LISTP))
 (10 5 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-+-1))
 (5 1 (:DEFINITION EQLABLE-ALISTP))
 )
(L5-REGULAR-FILE-WRITABLE-P)
(L5-RDCHS
 (328 4 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (228 8 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (209 20 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (170 12 (:DEFINITION L5-FS-P))
 (147 25 (:DEFINITION LEN))
 (136 4 (:DEFINITION NTH))
 (104 2 (:DEFINITION UNMAKE-BLOCKS))
 (79 79 (:REWRITE DEFAULT-CDR))
 (78 51 (:REWRITE DEFAULT-+-2))
 (76 15 (:REWRITE ZP-OPEN))
 (72 58 (:REWRITE DEFAULT-<-1))
 (70 58 (:REWRITE DEFAULT-<-2))
 (64 8 (:REWRITE NFIX-WHEN-ZP))
 (60 1 (:DEFINITION L5-STAT))
 (59 59 (:REWRITE DEFAULT-CAR))
 (53 51 (:REWRITE DEFAULT-+-1))
 (52 4 (:REWRITE TAKE-OF-LEN-FREE))
 (50 2 (:DEFINITION TAKE))
 (40 3 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (25 1 (:REWRITE DEFAULT-COERCE-3))
 (24 8 (:REWRITE NFIX-WHEN-NATP))
 (13 1 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (12 12 (:LINEAR POSITION-WHEN-MEMBER))
 (12 12 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (12 4 (:DEFINITION NFIX))
 (11 1 (:REWRITE L5-FS-P-ASSOC))
 (10 10 (:TYPE-PRESCRIPTION ZP))
 (10 2 (:DEFINITION ASSOC-EQUAL))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (8 8 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (8 1 (:DEFINITION MEMBER-EQUAL))
 (7 3 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (6 2 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (6 2 (:DEFINITION CHARACTER-LISTP))
 (6 2 (:DEFINITION BINARY-APPEND))
 (5 5 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (3 1 (:DEFINITION SYMBOL-LISTP))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (1 1 (:REWRITE DEFAULT-COERCE-2))
 )
(L5-WRCHS
 (1320 48 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1316 20 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (1306 484 (:REWRITE DEFAULT-CDR))
 (1260 18 (:DEFINITION INDICES-MARKED-P))
 (1200 50 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (1188 44 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (878 298 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (816 24 (:DEFINITION NTH))
 (747 168 (:REWRITE ZP-OPEN))
 (726 67 (:REWRITE NFIX-WHEN-ZP))
 (643 56 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (499 341 (:REWRITE DEFAULT-<-2))
 (484 33 (:DEFINITION L5-FS-P))
 (480 6 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (450 50 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (367 341 (:REWRITE DEFAULT-<-1))
 (360 360 (:REWRITE DEFAULT-CAR))
 (352 202 (:REWRITE DEFAULT-+-2))
 (260 20 (:DEFINITION COUNT-FREE-BLOCKS))
 (226 202 (:REWRITE DEFAULT-+-1))
 (226 4 (:DEFINITION UNMAKE-BLOCKS))
 (155 31 (:DEFINITION ASSOC-EQUAL))
 (122 8 (:REWRITE TAKE-OF-LEN-FREE))
 (106 106 (:LINEAR POSITION-WHEN-MEMBER))
 (106 106 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (100 4 (:DEFINITION TAKE))
 (96 24 (:REWRITE COMMUTATIVITY-OF-+))
 (90 90 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (77 33 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (72 24 (:DEFINITION NFIX))
 (50 50 (:REWRITE DEFAULT-COERCE-2))
 (50 50 (:REWRITE DEFAULT-COERCE-1))
 (48 48 (:TYPE-PRESCRIPTION NFIX))
 (39 13 (:DEFINITION CHARACTER-LISTP))
 (39 3 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (25 5 (:DEFINITION EQLABLE-ALISTP))
 (24 3 (:DEFINITION MEMBER-EQUAL))
 (22 22 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (15 15 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (14 14 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (12 4 (:DEFINITION BINARY-APPEND))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 (1 1 (:TYPE-PRESCRIPTION SET-INDICES))
 )
(L5-TO-L4-FS
 (199 92 (:REWRITE DEFAULT-+-2))
 (129 92 (:REWRITE DEFAULT-+-1))
 (72 18 (:DEFINITION INTEGER-ABS))
 (72 9 (:REWRITE LENGTH-WHEN-STRINGP))
 (45 9 (:DEFINITION LEN))
 (31 23 (:REWRITE DEFAULT-<-2))
 (30 5 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (29 29 (:REWRITE DEFAULT-CAR))
 (27 23 (:REWRITE DEFAULT-<-1))
 (26 12 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (18 18 (:REWRITE DEFAULT-UNARY-MINUS))
 (9 9 (:TYPE-PRESCRIPTION LEN))
 (9 9 (:REWRITE DEFAULT-REALPART))
 (9 9 (:REWRITE DEFAULT-NUMERATOR))
 (9 9 (:REWRITE DEFAULT-IMAGPART))
 (9 9 (:REWRITE DEFAULT-DENOMINATOR))
 (9 9 (:REWRITE DEFAULT-COERCE-2))
 (9 9 (:REWRITE DEFAULT-COERCE-1))
 )
(L5-TO-L4-FS-CORRECTNESS-1
 (670 26 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (354 36 (:DEFINITION NAT-LISTP))
 (249 67 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (191 185 (:REWRITE DEFAULT-CAR))
 (186 50 (:DEFINITION NATP))
 (162 159 (:REWRITE DEFAULT-CDR))
 (152 152 (:TYPE-PRESCRIPTION NAT-LISTP))
 (129 129 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (90 18 (:DEFINITION LEN))
 (70 70 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (50 50 (:REWRITE DEFAULT-<-2))
 (50 50 (:REWRITE DEFAULT-<-1))
 (41 15 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (36 18 (:REWRITE DEFAULT-+-2))
 (24 24 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (18 18 (:TYPE-PRESCRIPTION LEN))
 (18 18 (:REWRITE DEFAULT-+-1))
 )
(L5-STAT-CORRECTNESS-1-LEMMA-1
 (258 234 (:REWRITE DEFAULT-CAR))
 (83 80 (:REWRITE DEFAULT-CDR))
 (59 21 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 )
(L5-STAT-CORRECTNESS-1-LEMMA-2
 (74 6 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (58 6 (:DEFINITION L5-FS-P))
 (34 34 (:TYPE-PRESCRIPTION L5-FS-P))
 (22 22 (:REWRITE DEFAULT-CAR))
 (20 20 (:REWRITE DEFAULT-CDR))
 )
(L5-STAT-CORRECTNESS-1-LEMMA-3
 (2901 23 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (2608 33 (:DEFINITION L3-FS-P))
 (1371 1061 (:REWRITE DEFAULT-CDR))
 (968 173 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (608 59 (:DEFINITION NAT-LISTP))
 (484 10 (:REWRITE L3-FS-P-ASSOC))
 (411 79 (:DEFINITION LEN))
 (258 258 (:TYPE-PRESCRIPTION L3-FS-P))
 (158 79 (:REWRITE DEFAULT-+-2))
 (118 118 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (114 114 (:REWRITE DEFAULT-<-2))
 (114 114 (:REWRITE DEFAULT-<-1))
 (109 41 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (99 14 (:REWRITE L5-FS-P-ASSOC))
 (79 79 (:REWRITE DEFAULT-+-1))
 (77 77 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 (18 10 (:REWRITE L5-TO-L4-FS-CORRECTNESS-1 . 1))
 (13 1 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (8 1 (:DEFINITION MEMBER-EQUAL))
 (5 5 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 )
(L5-STAT-CORRECTNESS-1-LEMMA-4
 (827 239 (:REWRITE DEFAULT-CDR))
 (404 379 (:REWRITE DEFAULT-CAR))
 (164 66 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (110 10 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-3))
 (80 10 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-1))
 (70 9 (:REWRITE L5-FS-P-ASSOC))
 (12 12 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 )
(L5-STAT-CORRECTNESS-1
 (2704 180 (:DEFINITION L5-FS-P))
 (2554 372 (:DEFINITION ASSOC-EQUAL))
 (2326 2266 (:REWRITE DEFAULT-CAR))
 (1954 178 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1863 62 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1846 31 (:DEFINITION UNMAKE-BLOCKS))
 (1256 132 (:DEFINITION MEMBER-EQUAL))
 (1102 31 (:DEFINITION NTH))
 (1040 62 (:REWRITE TAKE-OF-LEN-FREE))
 (985 197 (:DEFINITION LEN))
 (806 31 (:REWRITE DEFAULT-COERCE-3))
 (799 31 (:DEFINITION TAKE))
 (788 154 (:REWRITE ZP-OPEN))
 (781 17 (:DEFINITION L3-FS-P))
 (712 31 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (684 684 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (549 321 (:REWRITE DEFAULT-+-2))
 (544 62 (:REWRITE NFIX-WHEN-ZP))
 (465 372 (:REWRITE DEFAULT-<-2))
 (403 372 (:REWRITE DEFAULT-<-1))
 (352 321 (:REWRITE DEFAULT-+-1))
 (272 272 (:REWRITE SUBSETP-MEMBER . 2))
 (272 272 (:REWRITE SUBSETP-MEMBER . 1))
 (240 30 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (210 62 (:REWRITE NFIX-WHEN-NATP))
 (197 12 (:DEFINITION BLOCK-LISTP))
 (188 188 (:LINEAR POSITION-WHEN-MEMBER))
 (188 188 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (124 31 (:REWRITE COMMUTATIVITY-OF-+))
 (107 31 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (93 93 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (93 31 (:DEFINITION NFIX))
 (93 31 (:DEFINITION BINARY-APPEND))
 (91 89 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (84 36 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (65 65 (:TYPE-PRESCRIPTION NAT-LISTP))
 (64 64 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (62 62 (:TYPE-PRESCRIPTION NFIX))
 (61 61 (:TYPE-PRESCRIPTION NATP))
 (39 12 (:DEFINITION CHARACTER-LISTP))
 (32 32 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (31 31 (:REWRITE DEFAULT-COERCE-2))
 (30 30 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (16 16 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (10 1 (:DEFINITION NAT-LISTP))
 (2 2 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 )
(L5-STAT-CORRECTNESS-2-LEMMA-1
 (4032 48 (:DEFINITION L3-FS-P))
 (2349 95 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-4))
 (1900 381 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-3))
 (675 99 (:REWRITE L5-FS-P-ASSOC))
 (545 109 (:DEFINITION LEN))
 (339 117 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (218 109 (:REWRITE DEFAULT-+-2))
 (190 190 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (170 170 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 (166 166 (:REWRITE DEFAULT-<-2))
 (166 166 (:REWRITE DEFAULT-<-1))
 (132 25 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-1))
 (109 109 (:REWRITE DEFAULT-+-1))
 )
(L5-STAT-CORRECTNESS-2
 (1153 1141 (:REWRITE DEFAULT-CAR))
 (958 184 (:DEFINITION ASSOC-EQUAL))
 (742 74 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (452 54 (:DEFINITION MEMBER-EQUAL))
 (422 15 (:REWRITE L5-STAT-CORRECTNESS-1 . 1))
 (376 4 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (329 32 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-3))
 (276 8 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (270 270 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (256 4 (:DEFINITION UNMAKE-BLOCKS))
 (192 4 (:REWRITE DEFAULT-COERCE-3))
 (180 4 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (170 34 (:DEFINITION LEN))
 (160 4 (:DEFINITION NTH))
 (152 8 (:REWRITE TAKE-OF-LEN-FREE))
 (150 10 (:DEFINITION BLOCK-LISTP))
 (145 63 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (120 20 (:REWRITE ZP-OPEN))
 (112 4 (:DEFINITION TAKE))
 (108 108 (:REWRITE SUBSETP-MEMBER . 2))
 (108 108 (:REWRITE SUBSETP-MEMBER . 1))
 (108 16 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (88 50 (:REWRITE DEFAULT-+-2))
 (88 8 (:REWRITE NFIX-WHEN-ZP))
 (70 58 (:REWRITE DEFAULT-<-2))
 (68 4 (:REWRITE L3-FS-P-ASSOC))
 (62 58 (:REWRITE DEFAULT-<-1))
 (54 50 (:REWRITE DEFAULT-+-1))
 (50 4 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (50 4 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (36 8 (:REWRITE NFIX-WHEN-NATP))
 (30 10 (:DEFINITION CHARACTER-LISTP))
 (28 2 (:DEFINITION L3-FS-P))
 (24 24 (:LINEAR POSITION-WHEN-MEMBER))
 (24 24 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (16 4 (:REWRITE COMMUTATIVITY-OF-+))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (12 4 (:DEFINITION NFIX))
 (12 4 (:DEFINITION BINARY-APPEND))
 (10 10 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (8 8 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (8 8 (:TYPE-PRESCRIPTION NATP))
 (8 8 (:TYPE-PRESCRIPTION NAT-LISTP))
 (8 8 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (4 4 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (4 4 (:REWRITE DEFAULT-COERCE-2))
 )
(L5-WRCHS-RETURNS-FS-LEMMA-1
 (161 65 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (143 143 (:REWRITE DEFAULT-CAR))
 (88 88 (:REWRITE DEFAULT-CDR))
 (51 17 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (17 17 (:TYPE-PRESCRIPTION NULL))
 (17 17 (:DEFINITION NULL))
 )
(L5-WRCHS-RETURNS-FS-LEMMA-2
 (1278 105 (:DEFINITION LEN))
 (1210 44 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1040 13 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (834 410 (:REWRITE DEFAULT-CDR))
 (748 22 (:DEFINITION NTH))
 (724 13 (:DEFINITION UNMAKE-BLOCKS))
 (660 12 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (630 9 (:DEFINITION INDICES-MARKED-P))
 (624 26 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (457 119 (:REWRITE ZP-OPEN))
 (429 143 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (394 390 (:REWRITE DEFAULT-CAR))
 (390 78 (:DEFINITION ASSOC-EQUAL))
 (386 26 (:REWRITE TAKE-OF-LEN-FREE))
 (370 45 (:REWRITE NFIX-WHEN-ZP))
 (342 256 (:REWRITE DEFAULT-<-2))
 (325 13 (:DEFINITION TAKE))
 (320 190 (:REWRITE DEFAULT-+-2))
 (270 256 (:REWRITE DEFAULT-<-1))
 (234 26 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (216 8 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (215 190 (:REWRITE DEFAULT-+-1))
 (192 13 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (174 10 (:DEFINITION L5-FS-P))
 (156 12 (:DEFINITION COUNT-FREE-BLOCKS))
 (100 25 (:REWRITE COMMUTATIVITY-OF-+))
 (88 88 (:LINEAR POSITION-WHEN-MEMBER))
 (88 88 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (87 87 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (78 26 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (70 35 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (66 22 (:DEFINITION NFIX))
 (66 22 (:DEFINITION NATP))
 (48 48 (:TYPE-PRESCRIPTION NATP))
 (45 45 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (45 3 (:DEFINITION BLOCK-LISTP))
 (44 44 (:TYPE-PRESCRIPTION NFIX))
 (39 39 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (39 13 (:DEFINITION BINARY-APPEND))
 (33 3 (:REWRITE L5-FS-P-ASSOC))
 (28 28 (:TYPE-PRESCRIPTION L5-MAKE-REGULAR-FILE))
 (26 26 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (26 26 (:REWRITE DEFAULT-COERCE-2))
 (26 26 (:REWRITE DEFAULT-COERCE-1))
 (24 24 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (21 9 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (15 3 (:DEFINITION BOOLEAN-LISTP))
 (12 12 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (9 3 (:DEFINITION CHARACTER-LISTP))
 (4 4 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 )
(L5-WRCHS-RETURNS-FS
 (1319 535 (:REWRITE DEFAULT-CDR))
 (1269 423 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (935 34 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (720 9 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (680 478 (:REWRITE DEFAULT-CAR))
 (585 9 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (578 17 (:DEFINITION NTH))
 (560 8 (:DEFINITION INDICES-MARKED-P))
 (530 149 (:REWRITE ZP-OPEN))
 (500 44 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (480 9 (:DEFINITION UNMAKE-BLOCKS))
 (468 4 (:DEFINITION SET-INDICES))
 (405 42 (:REWRITE NFIX-WHEN-ZP))
 (381 273 (:REWRITE DEFAULT-<-2))
 (340 194 (:REWRITE DEFAULT-+-2))
 (290 273 (:REWRITE DEFAULT-<-1))
 (246 18 (:REWRITE TAKE-OF-LEN-FREE))
 (225 9 (:DEFINITION TAKE))
 (215 43 (:DEFINITION ASSOC-EQUAL))
 (212 194 (:REWRITE DEFAULT-+-1))
 (165 11 (:DEFINITION BLOCK-LISTP))
 (153 17 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (136 56 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (132 44 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (117 9 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (117 9 (:DEFINITION COUNT-FREE-BLOCKS))
 (102 34 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (92 92 (:LINEAR POSITION-WHEN-MEMBER))
 (92 92 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (72 18 (:REWRITE COMMUTATIVITY-OF-+))
 (72 9 (:DEFINITION MEMBER-EQUAL))
 (64 8 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (55 11 (:DEFINITION BOOLEAN-LISTP))
 (51 17 (:DEFINITION NFIX))
 (51 17 (:DEFINITION NATP))
 (45 45 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (44 44 (:REWRITE DEFAULT-COERCE-2))
 (44 44 (:REWRITE DEFAULT-COERCE-1))
 (40 40 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (40 4 (:DEFINITION UPDATE-NTH))
 (34 34 (:TYPE-PRESCRIPTION NULL))
 (34 34 (:DEFINITION NULL))
 (33 11 (:DEFINITION CHARACTER-LISTP))
 (27 27 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (27 9 (:DEFINITION BINARY-APPEND))
 (18 18 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (18 18 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (18 18 (:REWRITE SUBSETP-MEMBER . 2))
 (18 18 (:REWRITE SUBSETP-MEMBER . 1))
 (14 14 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (8 8 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 )
(L5-WRCHS-CORRECTNESS-1-LEMMA-1
 (285 280 (:REWRITE DEFAULT-CAR))
 (209 205 (:REWRITE DEFAULT-CDR))
 (126 50 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (62 24 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (38 38 (:TYPE-PRESCRIPTION NULL))
 (38 38 (:DEFINITION NULL))
 (10 10 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 )
(L5-WRCHS-CORRECTNESS-1-LEMMA-2
 (9850 134 (:DEFINITION INDICES-MARKED-P))
 (8242 268 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (7584 2528 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (4858 134 (:DEFINITION NTH))
 (2813 2529 (:REWRITE DEFAULT-CDR))
 (2622 179 (:DEFINITION L3-FS-P))
 (2446 402 (:REWRITE ZP-OPEN))
 (2446 268 (:REWRITE NFIX-WHEN-ZP))
 (1474 1206 (:REWRITE DEFAULT-<-2))
 (1340 268 (:DEFINITION LEN))
 (1206 1206 (:REWRITE DEFAULT-<-1))
 (955 268 (:REWRITE NFIX-WHEN-NATP))
 (670 402 (:REWRITE DEFAULT-+-2))
 (553 134 (:DEFINITION NATP))
 (432 108 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (402 402 (:REWRITE DEFAULT-+-1))
 (402 134 (:DEFINITION NFIX))
 (268 268 (:TYPE-PRESCRIPTION NFIX))
 (268 268 (:LINEAR POSITION-WHEN-MEMBER))
 (268 268 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (241 142 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 (230 46 (:DEFINITION BOOLEAN-LISTP))
 (209 22 (:REWRITE L5-FS-P-ASSOC))
 (134 134 (:TYPE-PRESCRIPTION NATP))
 )
(L5-WRCHS-CORRECTNESS-1-LEMMA-3
 (2076 134 (:DEFINITION L5-FS-P))
 (1987 1372 (:REWRITE DEFAULT-CDR))
 (1797 120 (:DEFINITION L3-FS-P))
 (1496 1403 (:REWRITE DEFAULT-CAR))
 (1191 397 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (690 126 (:DEFINITION BINARY-APPEND))
 (398 92 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 (272 16 (:REWRITE L5-FS-P-ASSOC))
 (175 75 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (120 30 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (85 85 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (85 85 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (85 85 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (85 85 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (85 85 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (85 85 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (85 85 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (84 4 (:DEFINITION MEMBER-INTERSECTP-EQUAL))
 (36 12 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (32 8 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (12 12 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (12 12 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (10 10 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-7))
 (10 10 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-6))
 (8 8 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 )
(L5-WRCHS-CORRECTNESS-1-LEMMA-4
 (5418 1806 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (3000 125 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (2381 2102 (:REWRITE DEFAULT-CDR))
 (2354 161 (:DEFINITION L3-FS-P))
 (1375 125 (:DEFINITION MEMBER-EQUAL))
 (1356 228 (:DEFINITION BINARY-APPEND))
 (1000 250 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (392 98 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (250 250 (:REWRITE SUBSETP-MEMBER . 4))
 (250 250 (:REWRITE SUBSETP-MEMBER . 3))
 (250 250 (:REWRITE SUBSETP-MEMBER . 2))
 (250 250 (:REWRITE SUBSETP-MEMBER . 1))
 (235 136 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 (153 18 (:REWRITE L5-FS-P-ASSOC))
 (125 125 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (44 12 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (12 12 (:TYPE-PRESCRIPTION BINARY-APPEND))
 )
(L5-WRCHS-CORRECTNESS-1-LEMMA-5
 (192 6 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (111 37 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (108 6 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (102 7 (:DEFINITION L5-FS-P))
 (102 6 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (95 7 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (92 4 (:DEFINITION L5-TO-L4-FS))
 (84 6 (:DEFINITION L3-FS-P))
 (79 1 (:DEFINITION INDICES-MARKED-LISTP))
 (74 74 (:REWRITE DEFAULT-CAR))
 (73 1 (:DEFINITION INDICES-MARKED-P))
 (72 72 (:REWRITE DEFAULT-CDR))
 (61 2 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (36 1 (:DEFINITION NTH))
 (34 34 (:TYPE-PRESCRIPTION L5-REGULAR-FILE-ENTRY-P))
 (30 6 (:DEFINITION BINARY-APPEND))
 (30 1 (:DEFINITION NO-DUPLICATES-LISTP))
 (28 2 (:REWRITE L5-FS-P-ASSOC))
 (24 24 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (24 1 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (20 20 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (20 4 (:DEFINITION ASSOC-EQUAL))
 (18 3 (:REWRITE ZP-OPEN))
 (18 2 (:REWRITE NFIX-WHEN-ZP))
 (14 6 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (12 12 (:TYPE-PRESCRIPTION L5-TO-L4-FS))
 (11 9 (:REWRITE DEFAULT-<-2))
 (11 1 (:DEFINITION MEMBER-EQUAL))
 (10 2 (:DEFINITION LEN))
 (9 9 (:REWRITE DEFAULT-<-1))
 (8 2 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (7 2 (:REWRITE NFIX-WHEN-NATP))
 (6 6 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 (5 3 (:REWRITE DEFAULT-+-2))
 (4 1 (:DEFINITION NATP))
 (3 3 (:REWRITE DEFAULT-+-1))
 (3 1 (:DEFINITION NFIX))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (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 (:LINEAR POSITION-WHEN-MEMBER))
 (2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 )
(L5-WRCHS-CORRECTNESS-1-LEMMA-6
 (790 316 (:REWRITE DEFAULT-CDR))
 (290 14 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-4))
 (123 21 (:REWRITE L5-FS-P-ASSOC))
 (95 14 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-3))
 (83 29 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (53 9 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-1))
 (15 15 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 )
(L5-WRCHS-CORRECTNESS-1-LEMMA-7
 (148 143 (:REWRITE DEFAULT-CAR))
 (80 7 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-3))
 (57 55 (:REWRITE DEFAULT-CDR))
 (57 7 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-1))
 (41 15 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (9 9 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 )
(L5-WRCHS-CORRECTNESS-1-LEMMA-8
 (87 3 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (79 1 (:DEFINITION INDICES-MARKED-LISTP))
 (73 1 (:DEFINITION INDICES-MARKED-P))
 (61 2 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (58 4 (:DEFINITION L3-FS-P))
 (55 4 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (54 3 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (36 1 (:DEFINITION NTH))
 (31 31 (:REWRITE DEFAULT-CDR))
 (30 1 (:DEFINITION NO-DUPLICATES-LISTP))
 (27 27 (:REWRITE DEFAULT-CAR))
 (24 1 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (18 18 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (18 3 (:REWRITE ZP-OPEN))
 (18 2 (:REWRITE NFIX-WHEN-ZP))
 (15 3 (:DEFINITION LEN))
 (15 3 (:DEFINITION BINARY-APPEND))
 (14 14 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (13 13 (:TYPE-PRESCRIPTION LEN))
 (11 9 (:REWRITE DEFAULT-<-2))
 (11 1 (:DEFINITION MEMBER-EQUAL))
 (9 9 (:REWRITE DEFAULT-<-1))
 (8 2 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (7 4 (:REWRITE DEFAULT-+-2))
 (7 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (7 2 (:REWRITE NFIX-WHEN-NATP))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION NATP))
 (3 1 (:DEFINITION NFIX))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (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 (:LINEAR POSITION-WHEN-MEMBER))
 (2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 )
(L5-WRCHS-CORRECTNESS-1
 (43625 15211 (:REWRITE DEFAULT-CDR))
 (24001 14981 (:REWRITE DEFAULT-CAR))
 (20955 762 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (20826 178 (:DEFINITION SET-INDICES))
 (17642 1446 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (16080 201 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (14308 4526 (:REWRITE ZP-OPEN))
 (13500 180 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (12954 381 (:DEFINITION NTH))
 (12600 180 (:DEFINITION INDICES-MARKED-P))
 (11550 201 (:DEFINITION UNMAKE-BLOCKS))
 (9800 6654 (:REWRITE DEFAULT-<-2))
 (9595 937 (:REWRITE NFIX-WHEN-ZP))
 (9465 1867 (:DEFINITION ASSOC-EQUAL))
 (7637 4410 (:REWRITE DEFAULT-+-2))
 (7479 831 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (7074 6654 (:REWRITE DEFAULT-<-1))
 (6324 402 (:REWRITE TAKE-OF-LEN-FREE))
 (5025 201 (:DEFINITION TAKE))
 (4974 1662 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (4833 4410 (:REWRITE DEFAULT-+-1))
 (4338 1446 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (3795 55 (:REWRITE L5-STAT-CORRECTNESS-2-LEMMA-1))
 (3479 221 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (2848 356 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (2802 222 (:DEFINITION COUNT-FREE-BLOCKS))
 (2428 2428 (:LINEAR POSITION-WHEN-MEMBER))
 (2428 2428 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (2374 221 (:DEFINITION MEMBER-EQUAL))
 (1780 178 (:DEFINITION UPDATE-NTH))
 (1692 423 (:REWRITE COMMUTATIVITY-OF-+))
 (1656 1656 (:TYPE-PRESCRIPTION NULL))
 (1530 1530 (:REWRITE DEFAULT-COERCE-2))
 (1530 1530 (:REWRITE DEFAULT-COERCE-1))
 (1485 165 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-3))
 (1143 381 (:DEFINITION NFIX))
 (1105 1105 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (900 900 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (762 762 (:TYPE-PRESCRIPTION NFIX))
 (674 6 (:DEFINITION L3-FS-P))
 (603 603 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (603 201 (:DEFINITION BINARY-APPEND))
 (442 442 (:REWRITE SUBSETP-MEMBER . 2))
 (442 442 (:REWRITE SUBSETP-MEMBER . 1))
 (407 407 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (402 402 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (360 360 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (356 356 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (290 124 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (198 32 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (126 42 (:DEFINITION CHARACTER-LISTP))
 (120 12 (:DEFINITION NAT-LISTP))
 (68 68 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (24 24 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (11 11 (:TYPE-PRESCRIPTION L5-MAKE-REGULAR-FILE))
 )
(L5-RDCHS-CORRECTNESS-1-LEMMA-1
 (517 505 (:REWRITE DEFAULT-CAR))
 (443 415 (:REWRITE DEFAULT-CDR))
 (426 80 (:DEFINITION ASSOC-EQUAL))
 (337 3 (:DEFINITION L3-FS-P))
 (253 11 (:DEFINITION L5-TO-L4-FS))
 (246 3 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (182 14 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (179 4 (:REWRITE L5-STAT-CORRECTNESS-1 . 1))
 (174 3 (:DEFINITION UNMAKE-BLOCKS))
 (171 6 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (165 33 (:DEFINITION LEN))
 (130 2 (:REWRITE L5-STAT-CORRECTNESS-2-LEMMA-1))
 (120 8 (:DEFINITION BLOCK-LISTP))
 (112 14 (:DEFINITION MEMBER-EQUAL))
 (102 3 (:DEFINITION NTH))
 (99 16 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (96 6 (:REWRITE TAKE-OF-LEN-FREE))
 (81 45 (:REWRITE DEFAULT-+-2))
 (75 3 (:REWRITE DEFAULT-COERCE-3))
 (75 3 (:DEFINITION TAKE))
 (72 15 (:REWRITE ZP-OPEN))
 (70 70 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (66 3 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (64 55 (:REWRITE DEFAULT-<-2))
 (60 6 (:DEFINITION NAT-LISTP))
 (58 55 (:REWRITE DEFAULT-<-1))
 (52 22 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (48 45 (:REWRITE DEFAULT-+-1))
 (48 6 (:REWRITE NFIX-WHEN-ZP))
 (42 42 (:TYPE-PRESCRIPTION NAT-LISTP))
 (39 13 (:DEFINITION NATP))
 (34 34 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (28 28 (:REWRITE SUBSETP-MEMBER . 2))
 (28 28 (:REWRITE SUBSETP-MEMBER . 1))
 (28 4 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-3))
 (24 8 (:DEFINITION CHARACTER-LISTP))
 (24 3 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (18 18 (:LINEAR POSITION-WHEN-MEMBER))
 (18 18 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (18 6 (:REWRITE NFIX-WHEN-NATP))
 (17 17 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (12 12 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (12 3 (:REWRITE COMMUTATIVITY-OF-+))
 (9 9 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (9 3 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (9 3 (:DEFINITION NFIX))
 (9 3 (:DEFINITION BINARY-APPEND))
 (8 8 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (6 6 (:TYPE-PRESCRIPTION NFIX))
 (6 6 (:TYPE-PRESCRIPTION NATP))
 (6 6 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (3 3 (:REWRITE DEFAULT-COERCE-2))
 )
(L5-RDCHS-CORRECTNESS-1
 (2820 47 (:DEFINITION L5-STAT))
 (1663 121 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (1450 6 (:REWRITE L5-STAT-CORRECTNESS-2 . 1))
 (1282 91 (:DEFINITION L5-FS-P))
 (1236 864 (:REWRITE DEFAULT-CDR))
 (1015 13 (:DEFINITION TAKE))
 (924 111 (:DEFINITION LEN))
 (784 733 (:REWRITE DEFAULT-CAR))
 (738 9 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (732 26 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (727 26 (:REWRITE TAKE-OF-LEN-FREE))
 (672 2 (:DEFINITION L3-STAT))
 (640 43 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (637 49 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (607 13 (:DEFINITION NTH))
 (580 116 (:DEFINITION ASSOC-EQUAL))
 (578 9 (:DEFINITION UNMAKE-BLOCKS))
 (541 51 (:REWRITE L5-FS-P-ASSOC))
 (418 4 (:REWRITE CAR-OF-NTHCDR))
 (392 49 (:DEFINITION MEMBER-EQUAL))
 (355 89 (:REWRITE ZP-OPEN))
 (324 108 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (321 51 (:REWRITE NFIX-WHEN-ZP))
 (316 193 (:REWRITE DEFAULT-+-2))
 (245 245 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (240 184 (:REWRITE DEFAULT-<-2))
 (213 4 (:DEFINITION NTHCDR))
 (205 193 (:REWRITE DEFAULT-+-1))
 (203 184 (:REWRITE DEFAULT-<-1))
 (200 11 (:REWRITE DEFAULT-COERCE-3))
 (195 8 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (184 8 (:DEFINITION L5-TO-L4-FS))
 (181 3 (:REWRITE LEN-OF-NTHCDR))
 (162 162 (:TYPE-PRESCRIPTION ZP))
 (148 8 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (130 2 (:REWRITE L5-STAT-CORRECTNESS-2-LEMMA-1))
 (128 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (123 51 (:REWRITE NFIX-WHEN-NATP))
 (120 6 (:DEFINITION BLOCK-LISTP))
 (98 98 (:REWRITE SUBSETP-MEMBER . 2))
 (98 98 (:REWRITE SUBSETP-MEMBER . 1))
 (93 4 (:REWRITE CONSP-OF-NTHCDR))
 (92 92 (:LINEAR POSITION-WHEN-MEMBER))
 (92 92 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (82 3 (:REWRITE DEFAULT-COERCE-1))
 (74 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (68 6 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-7))
 (68 2 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-4))
 (64 9 (:DEFINITION BINARY-APPEND))
 (47 47 (:TYPE-PRESCRIPTION NATP))
 (41 11 (:DEFINITION NFIX))
 (35 20 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (33 33 (:TYPE-PRESCRIPTION NFIX))
 (28 12 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (28 4 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-3))
 (27 27 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (24 6 (:DEFINITION CHARACTER-LISTP))
 (18 18 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (18 2 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-6))
 (15 3 (:REWRITE CONSP-OF-TAKE))
 (14 14 (:REWRITE DEFAULT-COERCE-2))
 (12 4 (:DEFINITION SYMBOL-LISTP))
 (5 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 4 (:TYPE-PRESCRIPTION L5-TO-L4-FS))
 (2 2 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(L5-WRCHS-RETURNS-DISK-LEMMA-1
 (242 10 (:DEFINITION BOUNDED-NAT-LISTP))
 (120 60 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (64 36 (:REWRITE DEFAULT-CAR))
 (60 60 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (57 29 (:REWRITE DEFAULT-CDR))
 (54 10 (:DEFINITION NATP))
 (54 6 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (51 3 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (42 3 (:DEFINITION L5-FS-P))
 (36 6 (:DEFINITION STRING-LISTP))
 (33 3 (:DEFINITION TRUE-LISTP))
 (30 30 (:TYPE-PRESCRIPTION STRING-LISTP))
 (30 20 (:REWRITE DEFAULT-<-2))
 (24 24 (:TYPE-PRESCRIPTION L5-FS-P))
 (20 20 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (20 20 (:REWRITE DEFAULT-<-1))
 (12 12 (:REWRITE CONSP-OF-APPEND))
 (12 4 (:DEFINITION BINARY-APPEND))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L5-WRCHS-RETURNS-DISK-LEMMA-2
 (738 47 (:DEFINITION L3-FS-P))
 (518 464 (:REWRITE DEFAULT-CAR))
 (473 417 (:REWRITE DEFAULT-CDR))
 (320 42 (:DEFINITION BINARY-APPEND))
 (84 56 (:REWRITE DEFAULT-<-2))
 (73 29 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (72 18 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (62 62 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (56 56 (:REWRITE DEFAULT-<-1))
 (56 3 (:REWRITE CONSP-OF-APPEND))
 (44 1 (:DEFINITION TRUE-LISTP))
 (42 42 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-8))
 (30 2 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (28 28 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (28 28 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 (24 2 (:DEFINITION STRING-LISTP))
 (10 10 (:TYPE-PRESCRIPTION STRING-LISTP))
 )
(L5-WRCHS-RETURNS-DISK-LEMMA-3
 (7509 2503 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (2200 1870 (:REWRITE DEFAULT-CDR))
 (2168 152 (:DEFINITION L3-FS-P))
 (1704 240 (:DEFINITION BINARY-APPEND))
 (400 100 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (393 262 (:REWRITE DEFAULT-<-2))
 (308 308 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (262 262 (:REWRITE DEFAULT-<-1))
 (247 43 (:REWRITE L5-FS-P-ASSOC))
 (241 142 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 (203 29 (:DEFINITION BOOLEAN-LISTP))
 (157 40 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (131 131 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (87 87 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-8))
 (56 3 (:REWRITE CONSP-OF-APPEND))
 (44 1 (:DEFINITION TRUE-LISTP))
 (40 40 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (30 2 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (24 2 (:DEFINITION STRING-LISTP))
 (16 16 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (10 10 (:TYPE-PRESCRIPTION STRING-LISTP))
 (5 5 (:TYPE-PRESCRIPTION TRUE-LISTP))
 )
(L5-WRCHS-RETURNS-DISK-LEMMA-4
 (6861 2287 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (4800 65 (:DEFINITION L3-FS-P))
 (1981 388 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (1666 1443 (:REWRITE DEFAULT-CDR))
 (1290 136 (:DEFINITION NAT-LISTP))
 (994 994 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (725 145 (:DEFINITION LEN))
 (508 72 (:DEFINITION BINARY-APPEND))
 (462 395 (:REWRITE DEFAULT-<-2))
 (395 395 (:REWRITE DEFAULT-<-1))
 (360 360 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (290 145 (:REWRITE DEFAULT-+-2))
 (272 272 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (187 34 (:REWRITE L5-WRCHS-RETURNS-DISK-LEMMA-2))
 (145 145 (:REWRITE DEFAULT-+-1))
 (142 142 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (113 39 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (91 14 (:REWRITE L5-FS-P-ASSOC))
 (67 67 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (64 16 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (38 38 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 )
(L5-WRCHS-RETURNS-DISK
 (2656 1164 (:REWRITE DEFAULT-CDR))
 (2437 86 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (2236 17 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-25))
 (2170 30 (:DEFINITION INDICES-MARKED-P))
 (1496 43 (:DEFINITION NTH))
 (1453 993 (:REWRITE DEFAULT-CAR))
 (1428 17 (:DEFINITION INDICES-MARKED-LISTP))
 (1302 434 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1180 306 (:REWRITE ZP-OPEN))
 (1042 13 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (953 99 (:REWRITE NFIX-WHEN-ZP))
 (952 14 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (936 8 (:DEFINITION SET-INDICES))
 (928 80 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (856 624 (:REWRITE DEFAULT-<-2))
 (712 13 (:DEFINITION UNMAKE-BLOCKS))
 (699 395 (:REWRITE DEFAULT-+-2))
 (674 17 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (650 624 (:REWRITE DEFAULT-<-1))
 (460 20 (:DEFINITION L5-TO-L4-FS))
 (422 395 (:REWRITE DEFAULT-+-1))
 (374 26 (:REWRITE TAKE-OF-LEN-FREE))
 (342 38 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (326 17 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (325 13 (:DEFINITION TAKE))
 (309 17 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (280 56 (:DEFINITION ASSOC-EQUAL))
 (258 17 (:DEFINITION L3-FS-P))
 (240 80 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (228 76 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (198 60 (:DEFINITION NATP))
 (192 192 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (182 14 (:DEFINITION COUNT-FREE-BLOCKS))
 (166 166 (:LINEAR POSITION-WHEN-MEMBER))
 (166 166 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (163 1 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-2))
 (156 12 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (153 153 (:TYPE-PRESCRIPTION L3-FS-P))
 (150 150 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (144 144 (:TYPE-PRESCRIPTION L5-TO-L4-FS))
 (139 71 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-8))
 (136 136 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (129 43 (:DEFINITION NFIX))
 (128 16 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (124 30 (:DEFINITION BINARY-APPEND))
 (123 123 (:TYPE-PRESCRIPTION NATP))
 (115 49 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (108 27 (:REWRITE COMMUTATIVITY-OF-+))
 (96 32 (:DEFINITION CHARACTER-LISTP))
 (96 12 (:DEFINITION MEMBER-EQUAL))
 (85 85 (:TYPE-PRESCRIPTION INDICES-MARKED-LISTP))
 (80 80 (:REWRITE DEFAULT-COERCE-2))
 (80 80 (:REWRITE DEFAULT-COERCE-1))
 (80 8 (:DEFINITION UPDATE-NTH))
 (76 76 (:TYPE-PRESCRIPTION NULL))
 (76 76 (:DEFINITION NULL))
 (68 68 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (39 39 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (37 37 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 (37 37 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (36 36 (:TYPE-PRESCRIPTION L4-STRICTER-FS-P))
 (34 1 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-5))
 (28 28 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (26 26 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (24 24 (:REWRITE SUBSETP-MEMBER . 2))
 (24 24 (:REWRITE SUBSETP-MEMBER . 1))
 (24 24 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (19 17 (:REWRITE L5-TO-L4-FS-CORRECTNESS-1 . 1))
 (18 1 (:REWRITE L5-WRCHS-RETURNS-DISK-LEMMA-2))
 (16 16 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 )
(L5-READ-AFTER-WRITE-1-LEMMA-1
 (15884 5574 (:REWRITE DEFAULT-CDR))
 (10175 370 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (7933 4960 (:REWRITE DEFAULT-CAR))
 (7600 95 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (6903 59 (:DEFINITION SET-INDICES))
 (6700 574 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (6587 107 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (6300 90 (:DEFINITION INDICES-MARKED-P))
 (6290 185 (:DEFINITION NTH))
 (6022 1815 (:REWRITE ZP-OPEN))
 (5510 95 (:DEFINITION UNMAKE-BLOCKS))
 (4301 453 (:REWRITE NFIX-WHEN-ZP))
 (4123 2880 (:REWRITE DEFAULT-<-2))
 (3345 1943 (:REWRITE DEFAULT-+-2))
 (3058 2880 (:REWRITE DEFAULT-<-1))
 (3040 190 (:REWRITE TAKE-OF-LEN-FREE))
 (2529 281 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (2375 95 (:DEFINITION TAKE))
 (2145 1943 (:REWRITE DEFAULT-+-1))
 (1763 134 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1722 574 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (1674 562 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (1391 107 (:DEFINITION COUNT-FREE-BLOCKS))
 (1093 134 (:DEFINITION MEMBER-EQUAL))
 (992 992 (:LINEAR POSITION-WHEN-MEMBER))
 (992 992 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (944 118 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (808 202 (:REWRITE COMMUTATIVITY-OF-+))
 (670 670 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (590 59 (:DEFINITION UPDATE-NTH))
 (574 574 (:REWRITE DEFAULT-COERCE-2))
 (574 574 (:REWRITE DEFAULT-COERCE-1))
 (556 556 (:TYPE-PRESCRIPTION NULL))
 (555 185 (:DEFINITION NFIX))
 (555 185 (:DEFINITION NATP))
 (450 450 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (405 27 (:DEFINITION BLOCK-LISTP))
 (370 370 (:TYPE-PRESCRIPTION NFIX))
 (285 285 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (285 95 (:DEFINITION BINARY-APPEND))
 (268 268 (:REWRITE SUBSETP-MEMBER . 2))
 (268 268 (:REWRITE SUBSETP-MEMBER . 1))
 (214 214 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (196 28 (:DEFINITION BOOLEAN-LISTP))
 (192 82 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (190 190 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (155 155 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (118 118 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (84 84 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-8))
 (81 27 (:DEFINITION CHARACTER-LISTP))
 )
(L5-READ-AFTER-WRITE-1-LEMMA-2
 (22819 8037 (:REWRITE DEFAULT-CDR))
 (13750 500 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (11470 7046 (:REWRITE DEFAULT-CAR))
 (10320 129 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (10296 88 (:DEFINITION SET-INDICES))
 (9668 820 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (8856 144 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (8500 250 (:DEFINITION NTH))
 (8470 121 (:DEFINITION INDICES-MARKED-P))
 (8380 2557 (:REWRITE ZP-OPEN))
 (6882 129 (:DEFINITION UNMAKE-BLOCKS))
 (5891 613 (:REWRITE NFIX-WHEN-ZP))
 (5695 3958 (:REWRITE DEFAULT-<-2))
 (4588 2664 (:REWRITE DEFAULT-+-2))
 (4200 3958 (:REWRITE DEFAULT-<-1))
 (3636 404 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (3528 258 (:REWRITE TAKE-OF-LEN-FREE))
 (3225 129 (:DEFINITION TAKE))
 (2937 2664 (:REWRITE DEFAULT-+-1))
 (2460 820 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (2388 808 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (2208 165 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1872 144 (:DEFINITION COUNT-FREE-BLOCKS))
 (1408 176 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (1383 165 (:DEFINITION MEMBER-EQUAL))
 (1177 1177 (:LINEAR POSITION-WHEN-MEMBER))
 (1177 1177 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1092 273 (:REWRITE COMMUTATIVITY-OF-+))
 (880 88 (:DEFINITION UPDATE-NTH))
 (825 825 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (820 820 (:REWRITE DEFAULT-COERCE-2))
 (820 820 (:REWRITE DEFAULT-COERCE-1))
 (790 790 (:TYPE-PRESCRIPTION NULL))
 (750 250 (:DEFINITION NFIX))
 (750 250 (:DEFINITION NATP))
 (605 605 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (500 500 (:TYPE-PRESCRIPTION NFIX))
 (387 387 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (387 129 (:DEFINITION BINARY-APPEND))
 (330 330 (:REWRITE SUBSETP-MEMBER . 2))
 (330 330 (:REWRITE SUBSETP-MEMBER . 1))
 (288 288 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (258 258 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (218 218 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (206 88 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (176 176 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (93 93 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-8))
 (90 30 (:DEFINITION CHARACTER-LISTP))
 )
(L5-READ-AFTER-WRITE-1-LEMMA-3
 (1454 2 (:DEFINITION L5-WRCHS))
 (509 31 (:DEFINITION LEN))
 (488 196 (:REWRITE DEFAULT-CDR))
 (468 16 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (408 12 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (362 6 (:DEFINITION L5-STAT))
 (256 156 (:REWRITE DEFAULT-CAR))
 (247 18 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (240 2 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-2))
 (234 2 (:DEFINITION SET-INDICES))
 (220 8 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (196 16 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (160 2 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (154 48 (:REWRITE ZP-OPEN))
 (146 2 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (142 10 (:DEFINITION L5-FS-P))
 (140 2 (:DEFINITION INDICES-MARKED-P))
 (136 4 (:DEFINITION NTH))
 (116 2 (:DEFINITION UNMAKE-BLOCKS))
 (104 10 (:REWRITE NFIX-WHEN-ZP))
 (104 8 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (103 71 (:REWRITE DEFAULT-<-2))
 (90 10 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (90 8 (:REWRITE L5-FS-P-ASSOC))
 (82 47 (:REWRITE DEFAULT-+-2))
 (80 16 (:DEFINITION ASSOC-EQUAL))
 (75 71 (:REWRITE DEFAULT-<-1))
 (64 8 (:DEFINITION MEMBER-EQUAL))
 (64 4 (:REWRITE TAKE-OF-LEN-FREE))
 (60 20 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (51 47 (:REWRITE DEFAULT-+-1))
 (50 2 (:DEFINITION TAKE))
 (48 16 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (48 16 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (46 46 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (40 40 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (40 40 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (36 36 (:TYPE-PRESCRIPTION ZP))
 (36 18 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (32 4 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (28 28 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (28 28 (:TYPE-PRESCRIPTION COUNT-FREE-BLOCKS))
 (28 10 (:REWRITE NFIX-WHEN-NATP))
 (26 26 (:LINEAR POSITION-WHEN-MEMBER))
 (26 26 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (26 2 (:DEFINITION COUNT-FREE-BLOCKS))
 (22 2 (:DEFINITION MIN))
 (20 20 (:TYPE-PRESCRIPTION NULL))
 (20 20 (:TYPE-PRESCRIPTION NATP))
 (20 20 (:TYPE-PRESCRIPTION NAT-LISTP))
 (20 20 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (20 20 (:DEFINITION NULL))
 (20 2 (:DEFINITION UPDATE-NTH))
 (16 16 (:REWRITE SUBSETP-MEMBER . 2))
 (16 16 (:REWRITE SUBSETP-MEMBER . 1))
 (16 16 (:REWRITE DEFAULT-COERCE-2))
 (16 16 (:REWRITE DEFAULT-COERCE-1))
 (16 4 (:REWRITE COMMUTATIVITY-OF-+))
 (15 1 (:DEFINITION BLOCK-LISTP))
 (12 4 (:DEFINITION NFIX))
 (12 4 (:DEFINITION NATP))
 (10 10 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (10 10 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (7 3 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (7 1 (:DEFINITION BOOLEAN-LISTP))
 (6 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 2 (:DEFINITION BINARY-APPEND))
 (4 4 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (4 4 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (4 4 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (4 4 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (3 3 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-8))
 (3 1 (:DEFINITION SYMBOL-LISTP))
 (3 1 (:DEFINITION CHARACTER-LISTP))
 (1 1 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (1 1 (:REWRITE L5-WRCHS-RETURNS-FS))
 )
(L5-READ-AFTER-WRITE-1
 (114051 157 (:DEFINITION L5-WRCHS))
 (65653 24546 (:REWRITE DEFAULT-CDR))
 (52404 53 (:DEFINITION L4-WRCHS))
 (49202 1706 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (48054 1853 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (43044 1286 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (34610 22023 (:REWRITE DEFAULT-CAR))
 (34016 2289 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (33798 553 (:DEFINITION L5-STAT))
 (29971 1030 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (25749 515 (:DEFINITION NTH))
 (25592 210 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-2))
 (24931 305 (:DEFINITION TAKE))
 (24390 210 (:DEFINITION SET-INDICES))
 (22566 277 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (19277 5691 (:REWRITE ZP-OPEN))
 (16726 277 (:DEFINITION UNMAKE-BLOCKS))
 (16464 46 (:DEFINITION L3-STAT))
 (16282 610 (:REWRITE TAKE-OF-LEN-FREE))
 (15722 210 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (15318 666 (:DEFINITION L5-TO-L4-FS))
 (14700 210 (:DEFINITION INDICES-MARKED-P))
 (13895 2779 (:DEFINITION ASSOC-EQUAL))
 (13488 1436 (:REWRITE NFIX-WHEN-ZP))
 (12480 8529 (:REWRITE DEFAULT-<-2))
 (11143 28 (:REWRITE CAR-OF-NTHCDR))
 (10847 6234 (:REWRITE DEFAULT-+-2))
 (10517 809 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (9430 862 (:REWRITE L5-FS-P-ASSOC))
 (9070 8529 (:REWRITE DEFAULT-<-1))
 (8973 997 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (7680 2560 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (7632 212 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-1))
 (7341 25 (:REWRITE L5-STAT-CORRECTNESS-2 . 1))
 (6765 6234 (:REWRITE DEFAULT-+-1))
 (6472 809 (:DEFINITION MEMBER-EQUAL))
 (5982 1994 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (5646 1806 (:REWRITE DEFAULT-COERCE-1))
 (5120 76 (:REWRITE L5-STAT-CORRECTNESS-2-LEMMA-1))
 (5093 79 (:REWRITE DEFAULT-COERCE-3))
 (5049 5049 (:TYPE-PRESCRIPTION ZP))
 (4601 997 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (4126 440 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-7))
 (4107 28 (:DEFINITION NTHCDR))
 (4045 4045 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (3889 1436 (:REWRITE NFIX-WHEN-NATP))
 (3806 1916 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (3598 56 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (3002 3002 (:LINEAR POSITION-WHEN-MEMBER))
 (3002 3002 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (2873 223 (:DEFINITION COUNT-FREE-BLOCKS))
 (2783 56 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (2764 76 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-4))
 (2760 28 (:REWRITE LEN-OF-NTHCDR))
 (2332 2332 (:TYPE-PRESCRIPTION NATP))
 (2310 210 (:DEFINITION MIN))
 (2139 2139 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (2100 210 (:DEFINITION UPDATE-NTH))
 (1994 1994 (:TYPE-PRESCRIPTION NULL))
 (1994 1994 (:DEFINITION NULL))
 (1923 28 (:REWRITE CONSP-OF-NTHCDR))
 (1885 1885 (:REWRITE DEFAULT-COERCE-2))
 (1618 1618 (:REWRITE SUBSETP-MEMBER . 2))
 (1618 1618 (:REWRITE SUBSETP-MEMBER . 1))
 (1615 205 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-3))
 (1492 492 (:DEFINITION NFIX))
 (1166 5 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (1164 277 (:DEFINITION BINARY-APPEND))
 (1086 1086 (:TYPE-PRESCRIPTION NFIX))
 (1050 1050 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (831 831 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (778 46 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (684 76 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-6))
 (666 18 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (612 28 (:REWRITE CONSP-OF-TAKE))
 (554 554 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (544 46 (:REWRITE L4-WRCHS-RETURNS-DISK))
 (433 433 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (420 420 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (420 420 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (387 23 (:REWRITE L3-FS-P-ASSOC))
 (322 23 (:DEFINITION L3-FS-P))
 (299 299 (:TYPE-PRESCRIPTION L3-FS-P))
 (185 140 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (147 31 (:DEFINITION CHARACTER-LISTP))
 (138 138 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (111 23 (:REWRITE L4-WRCHS-RETURNS-FS))
 (92 92 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (77 33 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (76 76 (:REWRITE L5-STAT-CORRECTNESS-1-LEMMA-2))
 (69 69 (:REWRITE L5-TO-L4-FS-CORRECTNESS-1 . 1))
 (61 61 (:REWRITE FOLD-CONSTS-IN-+))
 (56 56 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(L5-READ-AFTER-WRITE-2-LEMMA-6
 (451 451 (:REWRITE DEFAULT-CAR))
 (435 87 (:DEFINITION ASSOC-EQUAL))
 (420 140 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (388 388 (:REWRITE DEFAULT-CDR))
 (286 22 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (176 22 (:DEFINITION MEMBER-EQUAL))
 (110 110 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (73 31 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (44 44 (:REWRITE SUBSETP-MEMBER . 2))
 (44 44 (:REWRITE SUBSETP-MEMBER . 1))
 )
(INDUCTION-SCHEME
 (18 6 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (6 6 (:TYPE-PRESCRIPTION ZP))
 (6 6 (:TYPE-PRESCRIPTION LEN))
 )
(L5-READ-AFTER-WRITE-2-LEMMA-5
 (84620 29789 (:REWRITE DEFAULT-CDR))
 (50325 1830 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (44080 551 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (41732 25583 (:REWRITE DEFAULT-CAR))
 (37882 332 (:DEFINITION SET-INDICES))
 (33622 2776 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (32060 554 (:DEFINITION UNMAKE-BLOCKS))
 (31110 915 (:DEFINITION NTH))
 (30044 9467 (:REWRITE ZP-OPEN))
 (27308 376 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (25480 364 (:DEFINITION INDICES-MARKED-P))
 (21868 15122 (:REWRITE DEFAULT-<-2))
 (20165 2119 (:REWRITE NFIX-WHEN-ZP))
 (17885 10385 (:REWRITE DEFAULT-+-2))
 (17680 1108 (:REWRITE TAKE-OF-LEN-FREE))
 (16154 15122 (:REWRITE DEFAULT-<-1))
 (14283 1587 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (13832 554 (:DEFINITION TAKE))
 (11469 10385 (:REWRITE DEFAULT-+-1))
 (9486 3174 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (8376 2770 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (6582 530 (:DEFINITION COUNT-FREE-BLOCKS))
 (5871 5871 (:LINEAR POSITION-WHEN-MEMBER))
 (5871 5871 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (5189 356 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (5104 638 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (4336 1084 (:REWRITE COMMUTATIVITY-OF-+))
 (3409 356 (:DEFINITION MEMBER-EQUAL))
 (3320 332 (:DEFINITION UPDATE-NTH))
 (3156 3156 (:TYPE-PRESCRIPTION NULL))
 (3066 3066 (:REWRITE DEFAULT-COERCE-2))
 (3066 3066 (:REWRITE DEFAULT-COERCE-1))
 (2745 915 (:DEFINITION NFIX))
 (1830 1830 (:TYPE-PRESCRIPTION NFIX))
 (1820 1820 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (1780 1780 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1662 554 (:DEFINITION BINARY-APPEND))
 (1659 1659 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (902 902 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (754 754 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (712 712 (:REWRITE SUBSETP-MEMBER . 2))
 (712 712 (:REWRITE SUBSETP-MEMBER . 1))
 (664 664 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (498 154 (:DEFINITION CHARACTER-LISTP))
 (396 44 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (264 44 (:DEFINITION STRING-LISTP))
 (242 22 (:DEFINITION TRUE-LISTP))
 (220 220 (:TYPE-PRESCRIPTION STRING-LISTP))
 (60 6 (:DEFINITION NAT-LISTP))
 (12 12 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (3 3 (:TYPE-PRESCRIPTION INDUCTION-SCHEME))
 )
(L5-READ-AFTER-WRITE-2-LEMMA-7
 (547957 193455 (:REWRITE DEFAULT-CDR))
 (335720 12208 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (324560 4057 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (300303 173443 (:REWRITE DEFAULT-CAR))
 (296649 2467 (:DEFINITION SET-INDICES))
 (246176 18266 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (232024 4057 (:DEFINITION UNMAKE-BLOCKS))
 (207536 6104 (:DEFINITION NTH))
 (200062 61766 (:REWRITE ZP-OPEN))
 (153471 2057 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (143290 2047 (:DEFINITION INDICES-MARKED-P))
 (137101 96154 (:REWRITE DEFAULT-<-2))
 (131504 13900 (:REWRITE NFIX-WHEN-ZP))
 (126542 8114 (:REWRITE TAKE-OF-LEN-FREE))
 (115392 67185 (:REWRITE DEFAULT-+-2))
 (102299 96154 (:REWRITE DEFAULT-<-1))
 (101425 4057 (:DEFINITION TAKE))
 (83700 9300 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (73535 67185 (:REWRITE DEFAULT-+-1))
 (61638 18266 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (55550 18600 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (50303 3365 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (45680 45320 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (38013 38013 (:LINEAR POSITION-WHEN-MEMBER))
 (38013 38013 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (37312 4664 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (33706 3308 (:DEFINITION MEMBER-EQUAL))
 (30788 30788 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (29337 2293 (:DEFINITION COUNT-FREE-BLOCKS))
 (25400 6350 (:REWRITE COMMUTATIVITY-OF-+))
 (25090 25090 (:TYPE-PRESCRIPTION NAT-LISTP))
 (24670 2467 (:DEFINITION UPDATE-NTH))
 (23830 23830 (:TYPE-PRESCRIPTION NATP))
 (18738 18738 (:REWRITE DEFAULT-COERCE-2))
 (18738 18738 (:REWRITE DEFAULT-COERCE-1))
 (18475 18475 (:TYPE-PRESCRIPTION NULL))
 (18475 18475 (:DEFINITION NULL))
 (18312 6104 (:DEFINITION NFIX))
 (16540 16540 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (12208 12208 (:TYPE-PRESCRIPTION NFIX))
 (12171 12171 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (12171 4057 (:DEFINITION BINARY-APPEND))
 (10235 10235 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (9194 9194 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (6616 6616 (:REWRITE SUBSETP-MEMBER . 2))
 (6616 6616 (:REWRITE SUBSETP-MEMBER . 1))
 (5400 540 (:DEFINITION NAT-LISTP))
 (5055 5055 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (4934 4934 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (4114 4114 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (3948 776 (:DEFINITION CHARACTER-LISTP))
 (1080 1080 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (45 45 (:TYPE-PRESCRIPTION L5-MAKE-REGULAR-FILE))
 (3 3 (:TYPE-PRESCRIPTION INDUCTION-SCHEME))
 )
(L5-READ-AFTER-WRITE-2-LEMMA-8
 (10593 4011 (:REWRITE DEFAULT-CDR))
 (10428 366 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (9228 282 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (5366 3266 (:REWRITE DEFAULT-CAR))
 (5120 42 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-2))
 (4914 42 (:DEFINITION SET-INDICES))
 (4620 168 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (4116 336 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (3360 42 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (3279 1053 (:REWRITE ZP-OPEN))
 (3146 42 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (2940 42 (:DEFINITION INDICES-MARKED-P))
 (2856 84 (:DEFINITION NTH))
 (2350 1603 (:REWRITE DEFAULT-<-2))
 (2232 42 (:DEFINITION UNMAKE-BLOCKS))
 (2184 210 (:REWRITE NFIX-WHEN-ZP))
 (1890 210 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (1873 152 (:REWRITE L5-FS-P-ASSOC))
 (1761 1014 (:REWRITE DEFAULT-+-2))
 (1702 1603 (:REWRITE DEFAULT-<-1))
 (1625 325 (:DEFINITION ASSOC-EQUAL))
 (1260 420 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (1140 84 (:REWRITE TAKE-OF-LEN-FREE))
 (1113 1014 (:REWRITE DEFAULT-+-1))
 (1050 42 (:DEFINITION TAKE))
 (1008 336 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (966 966 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (840 840 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (786 408 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (711 57 (:DEFINITION COUNT-FREE-BLOCKS))
 (672 84 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (613 46 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (588 588 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (588 210 (:REWRITE NFIX-WHEN-NATP))
 (487 487 (:LINEAR POSITION-WHEN-MEMBER))
 (487 487 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (465 465 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (462 42 (:DEFINITION MIN))
 (420 420 (:TYPE-PRESCRIPTION NULL))
 (420 420 (:TYPE-PRESCRIPTION NATP))
 (420 420 (:TYPE-PRESCRIPTION NAT-LISTP))
 (420 420 (:DEFINITION NULL))
 (420 42 (:DEFINITION UPDATE-NTH))
 (396 99 (:REWRITE COMMUTATIVITY-OF-+))
 (383 46 (:DEFINITION MEMBER-EQUAL))
 (366 366 (:REWRITE DEFAULT-COERCE-2))
 (366 366 (:REWRITE DEFAULT-COERCE-1))
 (252 84 (:DEFINITION NFIX))
 (230 230 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (210 210 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (210 210 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (168 168 (:TYPE-PRESCRIPTION NFIX))
 (168 21 (:REWRITE L5-WRCHS-RETURNS-FS))
 (126 126 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (126 42 (:DEFINITION BINARY-APPEND))
 (122 52 (:REWRITE L5-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (103 4 (:REWRITE L5-WRCHS-CORRECTNESS-1-LEMMA-5))
 (99 99 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (92 92 (:REWRITE SUBSETP-MEMBER . 2))
 (92 92 (:REWRITE SUBSETP-MEMBER . 1))
 (84 84 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (84 84 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (84 84 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (45 15 (:DEFINITION CHARACTER-LISTP))
 (3 3 (:TYPE-PRESCRIPTION INDUCTION-SCHEME))
 )
(L5-READ-AFTER-WRITE-2
 (3478 126 (:REWRITE TAKE-OF-LEN-FREE))
 (2718 63 (:DEFINITION TAKE))
 (2578 172 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1815 63 (:REWRITE LEN-OF-NTHCDR))
 (1420 63 (:REWRITE CAR-OF-NTHCDR))
 (1357 63 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1347 63 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (822 315 (:REWRITE NFIX-WHEN-ZP))
 (692 315 (:REWRITE NFIX-WHEN-NATP))
 (653 15 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (330 330 (:TYPE-PRESCRIPTION ZP))
 (306 306 (:LINEAR POSITION-WHEN-MEMBER))
 (306 306 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (189 63 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (147 21 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (126 126 (:TYPE-PRESCRIPTION NFIX))
 (105 21 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (101 63 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (48 15 (:DEFINITION NFIX))
 (21 21 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 )