(FETCH-BLOCKS-BY-INDICES
 (30 6 (:DEFINITION LEN))
 (15 15 (:REWRITE DEFAULT-CAR))
 (15 1 (:DEFINITION BLOCK-LISTP))
 (12 6 (:REWRITE DEFAULT-+-2))
 (11 7 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-<-1))
 (7 7 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (6 6 (:REWRITE DEFAULT-+-1))
 (3 1 (:DEFINITION CHARACTER-LISTP))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER))
 (2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1 1 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 )
(FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1
 (2730 30 (:REWRITE CONSP-OF-NTH-WHEN-ALISTP))
 (2246 102 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1620 60 (:REWRITE ALISTP-L2-FS-P))
 (1440 60 (:DEFINITION L2-FS-P))
 (1410 30 (:DEFINITION ALISTP))
 (900 900 (:TYPE-PRESCRIPTION L2-FS-P))
 (856 834 (:REWRITE DEFAULT-CDR))
 (840 60 (:REWRITE ALISTP-L1-FS-P))
 (813 769 (:REWRITE DEFAULT-CAR))
 (666 100 (:REWRITE NFIX-WHEN-ZP))
 (660 60 (:DEFINITION L1-FS-P))
 (621 515 (:REWRITE DEFAULT-<-2))
 (598 141 (:REWRITE ZP-OPEN))
 (589 318 (:REWRITE DEFAULT-+-2))
 (541 515 (:REWRITE DEFAULT-<-1))
 (480 480 (:TYPE-PRESCRIPTION L1-FS-P))
 (318 318 (:REWRITE DEFAULT-+-1))
 (164 92 (:REWRITE NFIX-WHEN-NATP))
 (150 150 (:TYPE-PRESCRIPTION ALISTP))
 (134 134 (:LINEAR POSITION-WHEN-MEMBER))
 (134 134 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (120 60 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (54 18 (:DEFINITION NFIX))
 (43 43 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (26 26 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2
 (416 16 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (272 8 (:DEFINITION NTH))
 (128 24 (:REWRITE ZP-OPEN))
 (128 16 (:REWRITE NFIX-WHEN-ZP))
 (114 61 (:REWRITE DEFAULT-+-2))
 (105 7 (:DEFINITION BLOCK-LISTP))
 (104 85 (:REWRITE DEFAULT-<-2))
 (99 92 (:REWRITE DEFAULT-CDR))
 (91 85 (:REWRITE DEFAULT-<-1))
 (61 61 (:REWRITE DEFAULT-+-1))
 (56 56 (:REWRITE DEFAULT-CAR))
 (40 16 (:REWRITE NFIX-WHEN-NATP))
 (38 38 (:LINEAR POSITION-WHEN-MEMBER))
 (38 38 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (21 7 (:DEFINITION CHARACTER-LISTP))
 (18 6 (:DEFINITION NFIX))
 (16 16 (:TYPE-PRESCRIPTION ZP))
 (11 11 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (7 7 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (6 6 (:TYPE-PRESCRIPTION NATP))
 (6 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FETCH-BLOCKS-BY-INDICES-CORRECTNESS-3
 (605 19 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (292 8 (:DEFINITION NTH))
 (270 54 (:DEFINITION LEN))
 (174 22 (:REWRITE NFIX-WHEN-ZP))
 (166 26 (:REWRITE ZP-OPEN))
 (146 106 (:REWRITE DEFAULT-<-2))
 (132 70 (:REWRITE DEFAULT-+-2))
 (116 106 (:REWRITE DEFAULT-<-1))
 (105 7 (:DEFINITION BLOCK-LISTP))
 (97 88 (:REWRITE DEFAULT-CDR))
 (78 70 (:REWRITE DEFAULT-+-1))
 (72 63 (:REWRITE DEFAULT-CAR))
 (34 10 (:DEFINITION NFIX))
 (27 27 (:LINEAR POSITION-WHEN-MEMBER))
 (27 27 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (21 7 (:DEFINITION CHARACTER-LISTP))
 (19 19 (:TYPE-PRESCRIPTION NFIX))
 (18 18 (:TYPE-PRESCRIPTION ZP))
 (12 4 (:DEFINITION BINARY-APPEND))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (8 8 (:TYPE-PRESCRIPTION NATP))
 (7 7 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(L3-REGULAR-FILE-ENTRY-P)
(L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1)
(L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-2)
(L3-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))
 )
(L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3
 (305 38 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (97 97 (:REWRITE DEFAULT-CAR))
 (90 90 (:REWRITE DEFAULT-CDR))
 (56 56 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (55 11 (:DEFINITION LEN))
 (31 31 (:REWRITE DEFAULT-<-2))
 (31 31 (:REWRITE DEFAULT-<-1))
 (22 11 (:REWRITE DEFAULT-+-2))
 (11 11 (:TYPE-PRESCRIPTION LEN))
 (11 11 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE CDR-CONS))
 (2 2 (:REWRITE CAR-CONS))
 )
(ALISTP-L3-FS-P
 (282 6 (:REWRITE ALISTP-L2-FS-P))
 (266 10 (:DEFINITION L2-FS-P))
 (136 136 (:TYPE-PRESCRIPTION L2-FS-P))
 (136 6 (:REWRITE ALISTP-L1-FS-P))
 (125 125 (:REWRITE DEFAULT-CAR))
 (120 10 (:DEFINITION L1-FS-P))
 (88 88 (:REWRITE DEFAULT-CDR))
 (74 74 (:TYPE-PRESCRIPTION L1-FS-P))
 (41 15 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (25 9 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (24 8 (:DEFINITION NATP))
 (20 10 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (8 8 (:REWRITE DEFAULT-<-2))
 (8 8 (:REWRITE DEFAULT-<-1))
 )
(L3-FS-P-ASSOC
 (428 428 (:REWRITE DEFAULT-CAR))
 (391 229 (:REWRITE DEFAULT-CDR))
 (257 119 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 )
(L3-BOUNDED-FS-P
 (996 454 (:REWRITE DEFAULT-+-2))
 (629 454 (:REWRITE DEFAULT-+-1))
 (320 80 (:DEFINITION INTEGER-ABS))
 (312 39 (:REWRITE LENGTH-WHEN-STRINGP))
 (215 43 (:DEFINITION LEN))
 (148 113 (:REWRITE DEFAULT-<-2))
 (141 113 (:REWRITE DEFAULT-<-1))
 (80 80 (:REWRITE DEFAULT-UNARY-MINUS))
 (41 41 (:REWRITE DEFAULT-REALPART))
 (41 41 (:REWRITE DEFAULT-NUMERATOR))
 (41 41 (:REWRITE DEFAULT-IMAGPART))
 (41 41 (:REWRITE DEFAULT-DENOMINATOR))
 (39 39 (:REWRITE DEFAULT-COERCE-2))
 (39 39 (:REWRITE DEFAULT-COERCE-1))
 (12 4 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (8 8 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (7 7 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L3-BOUNDED-FS-P-CORRECTNESS-1
 (392 392 (:REWRITE DEFAULT-CAR))
 (359 359 (:REWRITE DEFAULT-CDR))
 (335 67 (:DEFINITION LEN))
 (264 12 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (190 19 (:DEFINITION BOUNDED-NAT-LISTP))
 (140 121 (:REWRITE DEFAULT-<-2))
 (134 67 (:REWRITE DEFAULT-+-2))
 (121 121 (:REWRITE DEFAULT-<-1))
 (67 67 (:TYPE-PRESCRIPTION LEN))
 (67 67 (:REWRITE DEFAULT-+-1))
 (19 19 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L3-BOUNDED-FS-P-CORRECTNESS-2)
(L3-BOUNDED-FS-P-ASSOC
 (25200 1310 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 (8639 8198 (:REWRITE DEFAULT-CDR))
 (8327 159 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (7765 1553 (:DEFINITION LEN))
 (7207 152 (:DEFINITION L3-FS-P))
 (3106 1553 (:REWRITE DEFAULT-+-2))
 (2869 2594 (:REWRITE DEFAULT-<-2))
 (2597 2594 (:REWRITE DEFAULT-<-1))
 (1817 49 (:REWRITE L3-FS-P-ASSOC))
 (1553 1553 (:REWRITE DEFAULT-+-1))
 (278 278 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (26 2 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (16 2 (:DEFINITION MEMBER-EQUAL))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 )
(L3-TO-L2-FS-GUARD-LEMMA-1
 (182 12 (:REWRITE TAKE-OF-LEN-FREE))
 (167 95 (:REWRITE DEFAULT-+-2))
 (149 107 (:REWRITE DEFAULT-CDR))
 (144 6 (:DEFINITION TAKE))
 (118 76 (:REWRITE DEFAULT-CAR))
 (100 95 (:REWRITE DEFAULT-+-1))
 (73 15 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (69 9 (:REWRITE CONSP-OF-APPEND))
 (67 47 (:REWRITE DEFAULT-<-1))
 (62 31 (:REWRITE DEFAULT-*-2))
 (61 47 (:REWRITE DEFAULT-<-2))
 (58 20 (:DEFINITION NATP))
 (54 6 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (45 24 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (42 3 (:DEFINITION TRUE-LISTP))
 (37 37 (:LINEAR POSITION-WHEN-MEMBER))
 (37 37 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (36 6 (:DEFINITION STRING-LISTP))
 (31 31 (:REWRITE DEFAULT-*-1))
 (30 30 (:TYPE-PRESCRIPTION STRING-LISTP))
 (28 6 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-1))
 (27 9 (:DEFINITION BINARY-APPEND))
 (24 24 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (24 24 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (20 20 (:TYPE-PRESCRIPTION NATP))
 (15 15 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (13 7 (:REWRITE ZP-OPEN))
 (9 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (6 6 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (4 1 (:REWRITE NFIX-WHEN-ZP))
 (3 1 (:REWRITE NFIX-WHEN-NATP))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 )
(L3-TO-L2-FS
 (246 3 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (244 117 (:REWRITE DEFAULT-+-2))
 (171 6 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (155 117 (:REWRITE DEFAULT-+-1))
 (140 28 (:DEFINITION LEN))
 (102 3 (:DEFINITION NTH))
 (72 18 (:DEFINITION INTEGER-ABS))
 (72 9 (:REWRITE LENGTH-WHEN-STRINGP))
 (71 54 (:REWRITE DEFAULT-<-2))
 (70 13 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (68 68 (:REWRITE DEFAULT-CAR))
 (61 54 (:REWRITE DEFAULT-<-1))
 (52 10 (:REWRITE ZP-OPEN))
 (52 1 (:DEFINITION UNMAKE-BLOCKS))
 (48 6 (:REWRITE NFIX-WHEN-ZP))
 (26 12 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (26 2 (:REWRITE TAKE-OF-LEN-FREE))
 (25 1 (:DEFINITION TAKE))
 (18 18 (:REWRITE DEFAULT-UNARY-MINUS))
 (18 6 (:REWRITE NFIX-WHEN-NATP))
 (18 6 (:DEFINITION CHARACTER-LISTP))
 (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))
 (9 3 (:DEFINITION NFIX))
 (9 3 (:DEFINITION NATP))
 (8 8 (:LINEAR POSITION-WHEN-MEMBER))
 (8 8 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 6 (:TYPE-PRESCRIPTION ZP))
 (6 6 (:TYPE-PRESCRIPTION NFIX))
 (5 5 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 1 (:DEFINITION BINARY-APPEND))
 )
(L3-TO-L2-FS-CORRECTNESS-1
 (328 4 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (232 4 (:DEFINITION UNMAKE-BLOCKS))
 (228 8 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (150 30 (:DEFINITION LEN))
 (146 146 (:TYPE-PRESCRIPTION LEN))
 (136 4 (:DEFINITION NTH))
 (128 8 (:REWRITE TAKE-OF-LEN-FREE))
 (123 119 (:REWRITE DEFAULT-CDR))
 (107 103 (:REWRITE DEFAULT-CAR))
 (100 4 (:REWRITE DEFAULT-COERCE-3))
 (100 4 (:DEFINITION TAKE))
 (96 20 (:REWRITE ZP-OPEN))
 (90 6 (:DEFINITION BLOCK-LISTP))
 (88 4 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (80 46 (:REWRITE DEFAULT-+-2))
 (66 54 (:REWRITE DEFAULT-<-2))
 (64 8 (:REWRITE NFIX-WHEN-ZP))
 (58 54 (:REWRITE DEFAULT-<-1))
 (50 46 (:REWRITE DEFAULT-+-1))
 (32 4 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (30 10 (:DEFINITION NATP))
 (29 11 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (24 24 (:LINEAR POSITION-WHEN-MEMBER))
 (24 24 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (24 8 (:REWRITE NFIX-WHEN-NATP))
 (18 6 (:DEFINITION CHARACTER-LISTP))
 (16 4 (:REWRITE COMMUTATIVITY-OF-+))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (12 4 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (12 4 (:DEFINITION NFIX))
 (12 4 (:DEFINITION BINARY-APPEND))
 (8 8 (:TYPE-PRESCRIPTION ZP))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (8 8 (:TYPE-PRESCRIPTION NATP))
 (8 8 (:TYPE-PRESCRIPTION NAT-LISTP))
 (8 8 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (6 6 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (4 4 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (4 4 (:REWRITE DEFAULT-COERCE-2))
 )
(L3-STAT
 (282 3 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (247 87 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (207 6 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (120 3 (:DEFINITION NTH))
 (109 19 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (106 7 (:DEFINITION L3-FS-P))
 (95 19 (:DEFINITION LEN))
 (81 81 (:REWRITE DEFAULT-CDR))
 (73 73 (:REWRITE DEFAULT-CAR))
 (70 10 (:REWRITE ZP-OPEN))
 (66 6 (:REWRITE NFIX-WHEN-ZP))
 (58 1 (:DEFINITION UNMAKE-BLOCKS))
 (45 25 (:REWRITE DEFAULT-+-2))
 (40 31 (:REWRITE DEFAULT-<-2))
 (34 31 (:REWRITE DEFAULT-<-1))
 (32 2 (:REWRITE TAKE-OF-LEN-FREE))
 (28 12 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (28 1 (:DEFINITION TAKE))
 (27 6 (:REWRITE NFIX-WHEN-NATP))
 (26 25 (:REWRITE DEFAULT-+-1))
 (26 2 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (20 4 (:DEFINITION ASSOC-EQUAL))
 (18 6 (:DEFINITION CHARACTER-LISTP))
 (18 3 (:DEFINITION NATP))
 (16 2 (:DEFINITION MEMBER-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (9 3 (:DEFINITION NFIX))
 (8 8 (:LINEAR POSITION-WHEN-MEMBER))
 (8 8 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 6 (:TYPE-PRESCRIPTION NFIX))
 (5 5 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 1 (:DEFINITION EQLABLE-ALISTP))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 (4 1 (:REWRITE COMMUTATIVITY-OF-+))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 1 (:DEFINITION BINARY-APPEND))
 )
(L3-STAT-CORRECTNESS-1-LEMMA-2
 (492 6 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (348 6 (:DEFINITION UNMAKE-BLOCKS))
 (342 12 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (210 42 (:DEFINITION LEN))
 (204 6 (:DEFINITION NTH))
 (192 12 (:REWRITE TAKE-OF-LEN-FREE))
 (168 161 (:REWRITE DEFAULT-CAR))
 (150 6 (:REWRITE DEFAULT-COERCE-3))
 (150 6 (:DEFINITION TAKE))
 (144 141 (:REWRITE DEFAULT-CDR))
 (144 30 (:REWRITE ZP-OPEN))
 (132 6 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (114 66 (:REWRITE DEFAULT-+-2))
 (96 12 (:REWRITE NFIX-WHEN-ZP))
 (90 72 (:REWRITE DEFAULT-<-2))
 (90 6 (:DEFINITION BLOCK-LISTP))
 (78 72 (:REWRITE DEFAULT-<-1))
 (72 66 (:REWRITE DEFAULT-+-1))
 (48 6 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (36 36 (:LINEAR POSITION-WHEN-MEMBER))
 (36 36 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (36 12 (:REWRITE NFIX-WHEN-NATP))
 (29 11 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (24 24 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (24 6 (:REWRITE COMMUTATIVITY-OF-+))
 (18 18 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (18 6 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (18 6 (:DEFINITION NFIX))
 (18 6 (:DEFINITION NATP))
 (18 6 (:DEFINITION CHARACTER-LISTP))
 (18 6 (:DEFINITION BINARY-APPEND))
 (12 12 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (12 12 (:TYPE-PRESCRIPTION NFIX))
 (12 12 (:TYPE-PRESCRIPTION NATP))
 (12 12 (:TYPE-PRESCRIPTION NAT-LISTP))
 (12 12 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (6 6 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (6 6 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (6 6 (:REWRITE DEFAULT-COERCE-2))
 )
(L3-STAT-CORRECTNESS-1-LEMMA-3
 (6190 73 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (4744 73 (:DEFINITION UNMAKE-BLOCKS))
 (4317 146 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (2560 73 (:DEFINITION NTH))
 (2534 146 (:REWRITE TAKE-OF-LEN-FREE))
 (2305 461 (:DEFINITION LEN))
 (2269 73 (:REWRITE DEFAULT-COERCE-3))
 (2038 73 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1960 73 (:DEFINITION TAKE))
 (1867 1417 (:REWRITE DEFAULT-CDR))
 (1839 1473 (:REWRITE DEFAULT-CAR))
 (1830 353 (:REWRITE ZP-OPEN))
 (1359 753 (:REWRITE DEFAULT-+-2))
 (1246 146 (:REWRITE NFIX-WHEN-ZP))
 (1095 876 (:REWRITE DEFAULT-<-2))
 (970 753 (:REWRITE DEFAULT-+-1))
 (949 876 (:REWRITE DEFAULT-<-1))
 (729 35 (:DEFINITION BLOCK-LISTP))
 (488 61 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (477 146 (:REWRITE NFIX-WHEN-NATP))
 (462 462 (:LINEAR POSITION-WHEN-MEMBER))
 (462 462 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (459 73 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (364 73 (:REWRITE COMMUTATIVITY-OF-+))
 (318 85 (:DEFINITION NATP))
 (291 219 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (280 256 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (219 73 (:DEFINITION NFIX))
 (219 73 (:DEFINITION BINARY-APPEND))
 (192 12 (:DEFINITION NAT-LISTP))
 (182 182 (:TYPE-PRESCRIPTION NAT-LISTP))
 (170 170 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (146 146 (:TYPE-PRESCRIPTION NFIX))
 (141 35 (:DEFINITION CHARACTER-LISTP))
 (134 134 (:TYPE-PRESCRIPTION NATP))
 (83 83 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (73 73 (:REWRITE DEFAULT-COERCE-2))
 (65 23 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (61 61 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (46 10 (:REWRITE L3-FS-P-ASSOC))
 (39 13 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-2))
 (24 24 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 )
(L3-STAT-CORRECTNESS-1-LEMMA-4
 (2288 26 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1638 52 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1586 26 (:DEFINITION UNMAKE-BLOCKS))
 (1138 643 (:REWRITE DEFAULT-CDR))
 (962 26 (:DEFINITION NTH))
 (910 52 (:REWRITE TAKE-OF-LEN-FREE))
 (845 169 (:DEFINITION LEN))
 (702 130 (:REWRITE ZP-OPEN))
 (689 26 (:DEFINITION TAKE))
 (650 26 (:REWRITE DEFAULT-COERCE-3))
 (629 596 (:REWRITE DEFAULT-CAR))
 (572 26 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (494 52 (:REWRITE NFIX-WHEN-ZP))
 (468 273 (:REWRITE DEFAULT-+-2))
 (390 312 (:REWRITE DEFAULT-<-2))
 (338 312 (:REWRITE DEFAULT-<-1))
 (299 273 (:REWRITE DEFAULT-+-1))
 (208 26 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (195 52 (:REWRITE NFIX-WHEN-NATP))
 (195 13 (:DEFINITION BLOCK-LISTP))
 (170 70 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (156 156 (:LINEAR POSITION-WHEN-MEMBER))
 (156 156 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (117 26 (:DEFINITION NATP))
 (104 104 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (104 26 (:REWRITE COMMUTATIVITY-OF-+))
 (78 78 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (78 26 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (78 26 (:DEFINITION NFIX))
 (78 26 (:DEFINITION BINARY-APPEND))
 (63 11 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-2))
 (52 52 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (52 52 (:TYPE-PRESCRIPTION NFIX))
 (52 52 (:TYPE-PRESCRIPTION NATP))
 (52 52 (:TYPE-PRESCRIPTION NAT-LISTP))
 (52 52 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (48 8 (:REWRITE L3-FS-P-ASSOC))
 (39 13 (:DEFINITION CHARACTER-LISTP))
 (26 26 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (26 26 (:REWRITE DEFAULT-COERCE-2))
 (13 13 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 )
(L3-STAT-CORRECTNESS-1-LEMMA-5
 (210 1 (:DEFINITION L3-TO-L2-FS))
 (96 32 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (94 1 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (69 2 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (64 1 (:DEFINITION UNMAKE-BLOCKS))
 (49 4 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (44 3 (:DEFINITION L3-FS-P))
 (40 1 (:DEFINITION NTH))
 (38 2 (:REWRITE TAKE-OF-LEN-FREE))
 (35 32 (:REWRITE DEFAULT-CAR))
 (35 7 (:DEFINITION LEN))
 (32 32 (:REWRITE DEFAULT-CDR))
 (30 5 (:REWRITE ZP-OPEN))
 (28 1 (:DEFINITION TAKE))
 (25 1 (:REWRITE DEFAULT-COERCE-3))
 (22 2 (:REWRITE NFIX-WHEN-ZP))
 (22 1 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (20 4 (:DEFINITION ASSOC-EQUAL))
 (19 11 (:REWRITE DEFAULT-+-2))
 (15 12 (:REWRITE DEFAULT-<-2))
 (15 1 (:DEFINITION BLOCK-LISTP))
 (13 12 (:REWRITE DEFAULT-<-1))
 (12 11 (:REWRITE DEFAULT-+-1))
 (9 2 (:REWRITE NFIX-WHEN-NATP))
 (8 1 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (7 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (6 6 (:LINEAR POSITION-WHEN-MEMBER))
 (6 6 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 1 (:DEFINITION NATP))
 (4 4 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (4 1 (:REWRITE COMMUTATIVITY-OF-+))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 1 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (3 1 (:DEFINITION NFIX))
 (3 1 (:DEFINITION CHARACTER-LISTP))
 (3 1 (:DEFINITION BINARY-APPEND))
 (2 2 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:TYPE-PRESCRIPTION NAT-LISTP))
 (2 2 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (1 1 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (1 1 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (1 1 (:REWRITE DEFAULT-COERCE-2))
 )
(L3-STAT-CORRECTNESS-1
 (11892 138 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (8442 276 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (8202 138 (:DEFINITION UNMAKE-BLOCKS))
 (4980 138 (:DEFINITION NTH))
 (4614 276 (:REWRITE TAKE-OF-LEN-FREE))
 (4325 865 (:DEFINITION LEN))
 (3594 138 (:DEFINITION TAKE))
 (3568 682 (:REWRITE ZP-OPEN))
 (3258 138 (:REWRITE DEFAULT-COERCE-3))
 (2860 130 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (2496 276 (:REWRITE NFIX-WHEN-ZP))
 (2420 1417 (:REWRITE DEFAULT-+-2))
 (2072 1658 (:REWRITE DEFAULT-<-2))
 (1938 386 (:DEFINITION ASSOC-EQUAL))
 (1796 1658 (:REWRITE DEFAULT-<-1))
 (1649 40 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (1555 1417 (:REWRITE DEFAULT-+-1))
 (1040 130 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (972 276 (:REWRITE NFIX-WHEN-NATP))
 (798 798 (:LINEAR POSITION-WHEN-MEMBER))
 (798 798 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (675 45 (:DEFINITION BLOCK-LISTP))
 (618 148 (:DEFINITION NATP))
 (552 138 (:REWRITE COMMUTATIVITY-OF-+))
 (550 530 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (536 40 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (445 10 (:REWRITE L2-FS-P-ASSOC))
 (427 10 (:DEFINITION L2-FS-P))
 (414 414 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (414 138 (:DEFINITION NFIX))
 (414 138 (:DEFINITION BINARY-APPEND))
 (413 12 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (390 130 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (354 10 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (336 40 (:DEFINITION MEMBER-EQUAL))
 (325 139 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (276 276 (:TYPE-PRESCRIPTION NFIX))
 (276 276 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (268 268 (:TYPE-PRESCRIPTION NATP))
 (260 260 (:TYPE-PRESCRIPTION NAT-LISTP))
 (200 200 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (138 138 (:REWRITE DEFAULT-COERCE-2))
 (135 45 (:DEFINITION CHARACTER-LISTP))
 (130 130 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (80 80 (:REWRITE SUBSETP-MEMBER . 2))
 (80 80 (:REWRITE SUBSETP-MEMBER . 1))
 (45 45 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 )
(L3-STAT-CORRECTNESS-2-LEMMA-1
 (328 4 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (288 4 (:REWRITE DEFAULT-COERCE-3))
 (272 4 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (248 8 (:DEFINITION BLOCK-LISTP))
 (232 4 (:DEFINITION UNMAKE-BLOCKS))
 (228 8 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (180 180 (:TYPE-PRESCRIPTION LEN))
 (140 28 (:DEFINITION LEN))
 (136 4 (:DEFINITION NTH))
 (132 4 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (128 8 (:REWRITE TAKE-OF-LEN-FREE))
 (100 4 (:DEFINITION TAKE))
 (99 99 (:REWRITE DEFAULT-CDR))
 (84 84 (:REWRITE DEFAULT-CAR))
 (80 16 (:REWRITE ZP-OPEN))
 (76 44 (:REWRITE DEFAULT-+-2))
 (64 8 (:REWRITE NFIX-WHEN-ZP))
 (56 44 (:REWRITE DEFAULT-<-2))
 (48 44 (:REWRITE DEFAULT-<-1))
 (48 44 (:REWRITE DEFAULT-+-1))
 (48 8 (:DEFINITION CHARACTER-LISTP))
 (40 40 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (40 40 (:TYPE-PRESCRIPTION BLOCK-LISTP))
 (40 40 (:LINEAR POSITION-WHEN-MEMBER))
 (40 40 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (29 11 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (24 8 (:REWRITE NFIX-WHEN-NATP))
 (16 16 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (16 4 (:REWRITE COMMUTATIVITY-OF-+))
 (12 12 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (12 4 (:DEFINITION NFIX))
 (12 4 (:DEFINITION NATP))
 (12 4 (:DEFINITION BINARY-APPEND))
 (8 8 (:TYPE-PRESCRIPTION ZP))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE DEFAULT-COERCE-2))
 )
(L3-STAT-CORRECTNESS-2
 (8212 94 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (5862 188 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (5704 94 (:DEFINITION UNMAKE-BLOCKS))
 (3448 94 (:DEFINITION NTH))
 (3260 188 (:REWRITE TAKE-OF-LEN-FREE))
 (3198 2395 (:REWRITE DEFAULT-CAR))
 (3014 336 (:DEFINITION ASSOC-EQUAL))
 (2993 2332 (:REWRITE DEFAULT-CDR))
 (2875 575 (:DEFINITION LEN))
 (2603 40 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (2508 470 (:REWRITE ZP-OPEN))
 (2476 94 (:DEFINITION TAKE))
 (2350 94 (:REWRITE DEFAULT-COERCE-3))
 (2068 94 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1756 188 (:REWRITE NFIX-WHEN-ZP))
 (1620 951 (:REWRITE DEFAULT-+-2))
 (1420 1138 (:REWRITE DEFAULT-<-2))
 (1232 1138 (:REWRITE DEFAULT-<-1))
 (1045 951 (:REWRITE DEFAULT-+-1))
 (930 19 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (769 10 (:REWRITE L2-FS-P-ASSOC))
 (755 12 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (752 94 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (690 188 (:REWRITE NFIX-WHEN-NATP))
 (633 10 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (564 564 (:LINEAR POSITION-WHEN-MEMBER))
 (564 564 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (477 104 (:DEFINITION NATP))
 (454 10 (:DEFINITION L2-FS-P))
 (406 386 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (376 94 (:REWRITE COMMUTATIVITY-OF-+))
 (304 23 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (282 282 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (282 94 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (282 94 (:DEFINITION NFIX))
 (282 94 (:DEFINITION BINARY-APPEND))
 (189 23 (:DEFINITION MEMBER-EQUAL))
 (188 188 (:TYPE-PRESCRIPTION NFIX))
 (188 188 (:TYPE-PRESCRIPTION NATP))
 (188 188 (:TYPE-PRESCRIPTION NAT-LISTP))
 (188 188 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (165 11 (:DEFINITION BLOCK-LISTP))
 (146 62 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (115 115 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (94 94 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (94 94 (:REWRITE DEFAULT-COERCE-2))
 (46 46 (:REWRITE SUBSETP-MEMBER . 2))
 (46 46 (:REWRITE SUBSETP-MEMBER . 1))
 (33 11 (:DEFINITION CHARACTER-LISTP))
 (29 29 (:REWRITE L3-TO-L2-FS-CORRECTNESS-1))
 (11 11 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 )
(L3-STAT-OF-STAT
 (1246 13 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1050 334 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (921 26 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (820 13 (:DEFINITION UNMAKE-BLOCKS))
 (532 13 (:DEFINITION NTH))
 (482 26 (:REWRITE TAKE-OF-LEN-FREE))
 (425 393 (:REWRITE DEFAULT-CDR))
 (415 83 (:DEFINITION LEN))
 (413 396 (:REWRITE DEFAULT-CAR))
 (398 64 (:REWRITE ZP-OPEN))
 (370 13 (:DEFINITION TAKE))
 (346 24 (:DEFINITION L3-FS-P))
 (301 13 (:REWRITE DEFAULT-COERCE-3))
 (298 26 (:REWRITE NFIX-WHEN-ZP))
 (264 12 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (259 47 (:DEFINITION ASSOC-EQUAL))
 (231 135 (:REWRITE DEFAULT-+-2))
 (194 155 (:REWRITE DEFAULT-<-2))
 (187 13 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (168 155 (:REWRITE DEFAULT-<-1))
 (148 135 (:REWRITE DEFAULT-+-1))
 (123 26 (:REWRITE NFIX-WHEN-NATP))
 (122 13 (:DEFINITION MEMBER-EQUAL))
 (96 12 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (84 13 (:DEFINITION NATP))
 (70 70 (:LINEAR POSITION-WHEN-MEMBER))
 (70 70 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (65 65 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (52 13 (:REWRITE COMMUTATIVITY-OF-+))
 (48 48 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (39 39 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (39 13 (:DEFINITION NFIX))
 (36 12 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (35 15 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (26 26 (:TYPE-PRESCRIPTION NFIX))
 (26 26 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (26 26 (:REWRITE SUBSETP-MEMBER . 2))
 (26 26 (:REWRITE SUBSETP-MEMBER . 1))
 (25 25 (:TYPE-PRESCRIPTION NATP))
 (24 24 (:TYPE-PRESCRIPTION NAT-LISTP))
 (18 6 (:DEFINITION CHARACTER-LISTP))
 (13 13 (:REWRITE DEFAULT-COERCE-2))
 (12 12 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (12 12 (:REWRITE CONSP-OF-APPEND))
 (4 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (2 1 (:DEFINITION STRING-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 )
(L3-RDCHS
 (238 1 (:DEFINITION L3-STAT))
 (94 1 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (69 2 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (58 1 (:DEFINITION UNMAKE-BLOCKS))
 (45 9 (:DEFINITION LEN))
 (40 1 (:DEFINITION NTH))
 (39 29 (:REWRITE DEFAULT-+-2))
 (37 26 (:REWRITE DEFAULT-<-1))
 (32 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (32 2 (:REWRITE TAKE-OF-LEN-FREE))
 (30 30 (:REWRITE DEFAULT-CDR))
 (30 29 (:REWRITE DEFAULT-+-1))
 (30 5 (:REWRITE ZP-OPEN))
 (30 2 (:DEFINITION L3-FS-P))
 (29 26 (:REWRITE DEFAULT-<-2))
 (28 1 (:DEFINITION TAKE))
 (25 1 (:REWRITE DEFAULT-COERCE-3))
 (24 24 (:REWRITE DEFAULT-CAR))
 (24 8 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (22 2 (:REWRITE NFIX-WHEN-ZP))
 (22 1 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (15 1 (:DEFINITION BLOCK-LISTP))
 (13 1 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (12 12 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (11 1 (:REWRITE L3-FS-P-ASSOC))
 (10 10 (:TYPE-PRESCRIPTION ZP))
 (10 2 (:DEFINITION ASSOC-EQUAL))
 (9 2 (:REWRITE NFIX-WHEN-NATP))
 (8 1 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (8 1 (:DEFINITION MEMBER-EQUAL))
 (7 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (5 5 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (4 4 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (4 4 (:LINEAR POSITION-WHEN-MEMBER))
 (4 4 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:REWRITE DEFAULT-COERCE-2))
 (3 1 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (3 1 (:DEFINITION SYMBOL-LISTP))
 (3 1 (:DEFINITION NFIX))
 (3 1 (:DEFINITION CHARACTER-LISTP))
 (3 1 (:DEFINITION BINARY-APPEND))
 (2 2 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:TYPE-PRESCRIPTION NAT-LISTP))
 (2 2 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:REWRITE DEFAULT-COERCE-1))
 (1 1 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (1 1 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 )
(L3-RDCHS-CORRECTNESS-1-LEMMA-1
 (1690 19 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1215 38 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1168 19 (:DEFINITION UNMAKE-BLOCKS))
 (744 595 (:REWRITE DEFAULT-CAR))
 (712 19 (:DEFINITION NTH))
 (674 38 (:REWRITE TAKE-OF-LEN-FREE))
 (657 559 (:REWRITE DEFAULT-CDR))
 (613 81 (:DEFINITION ASSOC-EQUAL))
 (610 122 (:DEFINITION LEN))
 (548 8 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (522 95 (:REWRITE ZP-OPEN))
 (508 19 (:DEFINITION TAKE))
 (475 19 (:REWRITE DEFAULT-COERCE-3))
 (418 19 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (370 38 (:REWRITE NFIX-WHEN-ZP))
 (339 198 (:REWRITE DEFAULT-+-2))
 (287 230 (:REWRITE DEFAULT-<-2))
 (249 230 (:REWRITE DEFAULT-<-1))
 (217 198 (:REWRITE DEFAULT-+-1))
 (182 14 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (160 2 (:REWRITE L2-FS-P-ASSOC))
 (152 19 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (148 2 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (147 38 (:REWRITE NFIX-WHEN-NATP))
 (138 2 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (120 8 (:DEFINITION BLOCK-LISTP))
 (114 114 (:LINEAR POSITION-WHEN-MEMBER))
 (114 114 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (112 14 (:DEFINITION MEMBER-EQUAL))
 (104 21 (:DEFINITION NATP))
 (96 2 (:DEFINITION L2-FS-P))
 (82 78 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (76 19 (:REWRITE COMMUTATIVITY-OF-+))
 (70 70 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (58 10 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (57 57 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (57 19 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (57 19 (:DEFINITION NFIX))
 (57 19 (:DEFINITION BINARY-APPEND))
 (55 23 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (45 6 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (38 38 (:TYPE-PRESCRIPTION NFIX))
 (38 38 (:TYPE-PRESCRIPTION NATP))
 (38 38 (:TYPE-PRESCRIPTION NAT-LISTP))
 (38 38 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (28 28 (:REWRITE SUBSETP-MEMBER . 2))
 (28 28 (:REWRITE SUBSETP-MEMBER . 1))
 (24 8 (:DEFINITION CHARACTER-LISTP))
 (19 19 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (19 19 (:REWRITE DEFAULT-COERCE-2))
 (8 8 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (5 5 (:REWRITE L3-TO-L2-FS-CORRECTNESS-1))
 )
(L3-RDCHS-CORRECTNESS-1
 (5076 21 (:DEFINITION L3-STAT))
 (2384 26 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1914 60 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1580 26 (:DEFINITION UNMAKE-BLOCKS))
 (1258 60 (:REWRITE TAKE-OF-LEN-FREE))
 (1243 5 (:REWRITE L3-STAT-CORRECTNESS-2))
 (1173 30 (:DEFINITION TAKE))
 (1134 30 (:DEFINITION NTH))
 (1070 194 (:DEFINITION LEN))
 (954 5 (:DEFINITION L3-TO-L2-FS))
 (873 170 (:REWRITE ZP-OPEN))
 (829 667 (:REWRITE DEFAULT-CDR))
 (719 85 (:REWRITE NFIX-WHEN-ZP))
 (691 52 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (675 30 (:REWRITE DEFAULT-COERCE-3))
 (638 202 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (596 530 (:REWRITE DEFAULT-CAR))
 (572 26 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (567 344 (:REWRITE DEFAULT-+-2))
 (487 380 (:REWRITE DEFAULT-<-2))
 (460 36 (:DEFINITION L3-FS-P))
 (429 1 (:DEFINITION L2-STAT))
 (416 380 (:REWRITE DEFAULT-<-1))
 (386 59 (:DEFINITION ASSOC-EQUAL))
 (373 344 (:REWRITE DEFAULT-+-1))
 (290 290 (:TYPE-PRESCRIPTION ZP))
 (288 85 (:REWRITE NFIX-WHEN-NATP))
 (286 22 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (277 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (274 4 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (251 12 (:REWRITE DEFAULT-COERCE-1))
 (242 22 (:REWRITE L3-FS-P-ASSOC))
 (208 26 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (208 4 (:REWRITE CAR-OF-NTHCDR))
 (186 186 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (178 178 (:LINEAR POSITION-WHEN-MEMBER))
 (178 178 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (176 22 (:DEFINITION MEMBER-EQUAL))
 (162 8 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (159 3 (:REWRITE LEN-OF-NTHCDR))
 (132 4 (:DEFINITION NTHCDR))
 (110 110 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (107 105 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (105 105 (:TYPE-PRESCRIPTION L3-TO-L2-FS))
 (92 28 (:DEFINITION NFIX))
 (80 1 (:REWRITE L2-FS-P-ASSOC))
 (78 78 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (78 26 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (78 26 (:DEFINITION BINARY-APPEND))
 (76 8 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (74 1 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (69 1 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (67 67 (:TYPE-PRESCRIPTION NFIX))
 (60 4 (:REWRITE CONSP-OF-NTHCDR))
 (60 4 (:DEFINITION BLOCK-LISTP))
 (55 55 (:TYPE-PRESCRIPTION NATP))
 (52 52 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (52 52 (:TYPE-PRESCRIPTION NAT-LISTP))
 (52 52 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (48 1 (:DEFINITION L2-FS-P))
 (46 5 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-2))
 (44 44 (:REWRITE SUBSETP-MEMBER . 2))
 (44 44 (:REWRITE SUBSETP-MEMBER . 1))
 (42 42 (:REWRITE DEFAULT-COERCE-2))
 (37 4 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-4))
 (29 5 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (28 12 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (26 26 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (23 23 (:REWRITE L3-STAT-CORRECTNESS-2-LEMMA-1))
 (20 20 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (19 19 (:TYPE-PRESCRIPTION L2-FS-P))
 (15 3 (:REWRITE CONSP-OF-TAKE))
 (12 4 (:DEFINITION SYMBOL-LISTP))
 (12 4 (:DEFINITION CHARACTER-LISTP))
 (5 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE L3-TO-L2-FS-CORRECTNESS-1))
 (2 2 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(L3-UNLINK
 (151 55 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (62 4 (:DEFINITION L3-FS-P))
 (44 9 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (29 29 (:REWRITE DEFAULT-CAR))
 (27 27 (:REWRITE DEFAULT-CDR))
 (26 2 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (21 9 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (16 2 (:DEFINITION MEMBER-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (10 2 (:DEFINITION ASSOC-EQUAL))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 )
(L3-UNLINK-RETURNS-FS-LEMMA-1
 (1389 463 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (42 16 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (31 31 (:REWRITE DEFAULT-CDR))
 )
(L3-UNLINK-RETURNS-FS
 (4071 4071 (:REWRITE DEFAULT-CAR))
 (3303 1101 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (3221 3221 (:REWRITE DEFAULT-CDR))
 (2184 728 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (872 62 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (735 147 (:DEFINITION ASSOC-EQUAL))
 (728 728 (:TYPE-PRESCRIPTION NULL))
 (728 728 (:DEFINITION NULL))
 (562 62 (:DEFINITION MEMBER-EQUAL))
 (310 310 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (124 124 (:REWRITE SUBSETP-MEMBER . 2))
 (124 124 (:REWRITE SUBSETP-MEMBER . 1))
 )
(L3-UNLINK-CORRECTNESS-1-LEMMA-1
 (3587 44 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (2552 44 (:DEFINITION UNMAKE-BLOCKS))
 (2496 88 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1487 44 (:DEFINITION NTH))
 (1432 1432 (:TYPE-PRESCRIPTION LEN))
 (1408 88 (:REWRITE TAKE-OF-LEN-FREE))
 (1340 268 (:DEFINITION LEN))
 (1100 44 (:DEFINITION TAKE))
 (1008 214 (:REWRITE ZP-OPEN))
 (997 949 (:REWRITE DEFAULT-CDR))
 (956 44 (:REWRITE DEFAULT-COERCE-3))
 (836 38 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (806 757 (:REWRITE DEFAULT-CAR))
 (756 444 (:REWRITE DEFAULT-+-2))
 (692 88 (:REWRITE NFIX-WHEN-ZP))
 (645 513 (:REWRITE DEFAULT-<-2))
 (557 513 (:REWRITE DEFAULT-<-1))
 (488 444 (:REWRITE DEFAULT-+-1))
 (304 38 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (264 264 (:LINEAR POSITION-WHEN-MEMBER))
 (264 264 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (264 88 (:REWRITE NFIX-WHEN-NATP))
 (191 77 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (176 44 (:REWRITE COMMUTATIVITY-OF-+))
 (152 152 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (150 10 (:DEFINITION BLOCK-LISTP))
 (132 132 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (132 44 (:DEFINITION NFIX))
 (132 44 (:DEFINITION NATP))
 (132 44 (:DEFINITION BINARY-APPEND))
 (114 38 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (91 91 (:TYPE-PRESCRIPTION ZP))
 (88 88 (:TYPE-PRESCRIPTION NFIX))
 (88 88 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (82 82 (:TYPE-PRESCRIPTION NATP))
 (76 76 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (76 76 (:TYPE-PRESCRIPTION NAT-LISTP))
 (57 57 (:TYPE-PRESCRIPTION NULL))
 (57 57 (:DEFINITION NULL))
 (57 33 (:REWRITE L3-STAT-CORRECTNESS-2-LEMMA-1))
 (44 44 (:REWRITE DEFAULT-COERCE-2))
 (38 38 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (30 10 (:DEFINITION CHARACTER-LISTP))
 (10 10 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 )
(L3-UNLINK-CORRECTNESS-1-LEMMA-2
 (1242 414 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1040 725 (:REWRITE DEFAULT-CDR))
 (892 892 (:REWRITE DEFAULT-CAR))
 (686 58 (:REWRITE L3-FS-P-ASSOC))
 (366 24 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (309 103 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (246 24 (:DEFINITION MEMBER-EQUAL))
 (142 54 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (125 25 (:DEFINITION LEN))
 (120 120 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (103 103 (:TYPE-PRESCRIPTION NULL))
 (103 103 (:DEFINITION NULL))
 (75 25 (:DEFINITION CHARACTER-LISTP))
 (50 25 (:REWRITE DEFAULT-+-2))
 (48 48 (:REWRITE SUBSETP-MEMBER . 2))
 (48 48 (:REWRITE SUBSETP-MEMBER . 1))
 (25 25 (:REWRITE DEFAULT-+-1))
 (24 24 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 )
(L3-UNLINK-CORRECTNESS-1
 (1910 23 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1346 23 (:DEFINITION UNMAKE-BLOCKS))
 (1335 46 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (794 23 (:DEFINITION NTH))
 (792 643 (:REWRITE DEFAULT-CAR))
 (766 643 (:REWRITE DEFAULT-CDR))
 (748 46 (:REWRITE TAKE-OF-LEN-FREE))
 (730 146 (:DEFINITION LEN))
 (610 70 (:DEFINITION ASSOC-EQUAL))
 (581 23 (:DEFINITION TAKE))
 (575 23 (:REWRITE DEFAULT-COERCE-3))
 (564 115 (:REWRITE ZP-OPEN))
 (548 8 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (506 23 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (407 238 (:REWRITE DEFAULT-+-2))
 (380 46 (:REWRITE NFIX-WHEN-ZP))
 (347 278 (:REWRITE DEFAULT-<-2))
 (301 278 (:REWRITE DEFAULT-<-1))
 (261 238 (:REWRITE DEFAULT-+-1))
 (184 23 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (160 2 (:REWRITE L2-FS-P-ASSOC))
 (148 2 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (144 46 (:REWRITE NFIX-WHEN-NATP))
 (138 138 (:LINEAR POSITION-WHEN-MEMBER))
 (138 138 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (138 2 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (120 8 (:DEFINITION BLOCK-LISTP))
 (117 13 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (117 9 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (98 94 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (96 2 (:DEFINITION L2-FS-P))
 (92 23 (:REWRITE COMMUTATIVITY-OF-+))
 (89 25 (:DEFINITION NATP))
 (78 26 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (72 9 (:DEFINITION MEMBER-EQUAL))
 (69 69 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (69 23 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (69 23 (:DEFINITION NFIX))
 (69 23 (:DEFINITION BINARY-APPEND))
 (52 22 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (46 46 (:TYPE-PRESCRIPTION NFIX))
 (46 46 (:TYPE-PRESCRIPTION NATP))
 (46 46 (:TYPE-PRESCRIPTION NAT-LISTP))
 (46 46 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (45 45 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (26 26 (:TYPE-PRESCRIPTION NULL))
 (26 26 (:DEFINITION NULL))
 (24 8 (:DEFINITION CHARACTER-LISTP))
 (23 23 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (23 23 (:REWRITE DEFAULT-COERCE-2))
 (18 18 (:REWRITE SUBSETP-MEMBER . 2))
 (18 18 (:REWRITE SUBSETP-MEMBER . 1))
 (8 8 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (4 4 (:REWRITE L3-TO-L2-FS-CORRECTNESS-1))
 )
(INDUCTION-SCHEME)
(GENERATE-INDEX-LIST-CORRECTNESS-3
 (267 136 (:REWRITE DEFAULT-+-2))
 (176 3 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-3))
 (164 20 (:REWRITE ZP-OPEN))
 (160 149 (:REWRITE DEFAULT-CDR))
 (155 136 (:REWRITE DEFAULT-+-1))
 (155 20 (:REWRITE NFIX-WHEN-ZP))
 (153 4 (:DEFINITION BOUNDED-NAT-LISTP))
 (111 74 (:REWRITE DEFAULT-<-2))
 (94 81 (:REWRITE DEFAULT-CAR))
 (85 74 (:REWRITE DEFAULT-<-1))
 (44 9 (:DEFINITION NATP))
 (28 8 (:DEFINITION NFIX))
 (17 17 (:TYPE-PRESCRIPTION BOUNDED-NAT-LISTP))
 (12 12 (:TYPE-PRESCRIPTION ZP))
 (12 12 (:LINEAR POSITION-WHEN-MEMBER))
 (12 12 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 6 (:TYPE-PRESCRIPTION NATP))
 (6 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:TYPE-PRESCRIPTION INDUCTION-SCHEME))
 )
(L3-WRCHS
 (337 117 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (282 3 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (207 6 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (173 28 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (170 22 (:DEFINITION LEN))
 (150 10 (:DEFINITION L3-FS-P))
 (135 102 (:REWRITE DEFAULT-CDR))
 (120 3 (:DEFINITION NTH))
 (101 101 (:REWRITE DEFAULT-CAR))
 (73 13 (:REWRITE ZP-OPEN))
 (66 6 (:REWRITE NFIX-WHEN-ZP))
 (58 1 (:DEFINITION UNMAKE-BLOCKS))
 (54 2 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (51 28 (:REWRITE DEFAULT-+-2))
 (49 38 (:REWRITE DEFAULT-<-2))
 (48 2 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (41 38 (:REWRITE DEFAULT-<-1))
 (35 15 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (32 2 (:REWRITE TAKE-OF-LEN-FREE))
 (30 6 (:DEFINITION ASSOC-EQUAL))
 (29 28 (:REWRITE DEFAULT-+-1))
 (28 1 (:DEFINITION TAKE))
 (27 6 (:REWRITE NFIX-WHEN-NATP))
 (26 2 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (21 7 (:DEFINITION CHARACTER-LISTP))
 (20 4 (:DEFINITION EQLABLE-ALISTP))
 (18 2 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (16 2 (:DEFINITION MEMBER-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (9 9 (:LINEAR POSITION-WHEN-MEMBER))
 (9 9 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (9 3 (:DEFINITION NFIX))
 (6 6 (:TYPE-PRESCRIPTION NFIX))
 (5 5 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 (4 1 (:REWRITE COMMUTATIVITY-OF-+))
 (3 1 (:DEFINITION BINARY-APPEND))
 (2 2 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE DEFAULT-COERCE-1))
 (1 1 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 )
(L3-WRCHS-RETURNS-FS-LEMMA-1
 (161 65 (:REWRITE L3-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))
 )
(L3-WRCHS-RETURNS-FS-LEMMA-3
 (279 1 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (277 3 (:DEFINITION L3-FS-P))
 (156 4 (:DEFINITION GENERATE-INDEX-LIST))
 (112 9 (:REWRITE ZP-OPEN))
 (100 5 (:REWRITE NFIX-WHEN-ZP))
 (80 12 (:DEFINITION LEN))
 (42 27 (:REWRITE DEFAULT-CDR))
 (36 20 (:REWRITE DEFAULT-+-2))
 (31 17 (:REWRITE DEFAULT-<-2))
 (22 2 (:DEFINITION NAT-LISTP))
 (20 20 (:REWRITE DEFAULT-+-1))
 (19 16 (:REWRITE DEFAULT-CAR))
 (17 17 (:REWRITE DEFAULT-<-1))
 (16 4 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (15 1 (:DEFINITION BLOCK-LISTP))
 (14 14 (:TYPE-PRESCRIPTION L3-FS-P))
 (12 12 (:TYPE-PRESCRIPTION NAT-LISTP))
 (12 12 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (12 3 (:DEFINITION NATP))
 (11 11 (:TYPE-PRESCRIPTION GENERATE-INDEX-LIST))
 (8 8 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (6 2 (:DEFINITION CHARACTER-LISTP))
 (5 5 (:TYPE-PRESCRIPTION ZP))
 (5 5 (:LINEAR POSITION-WHEN-MEMBER))
 (5 5 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (4 4 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (4 4 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (3 3 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 )
(L3-WRCHS-RETURNS-FS
 (1052 70 (:DEFINITION LEN))
 (736 334 (:REWRITE DEFAULT-CDR))
 (594 198 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (576 24 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (564 6 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (414 12 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (373 361 (:REWRITE DEFAULT-CAR))
 (372 6 (:DEFINITION UNMAKE-BLOCKS))
 (336 72 (:REWRITE ZP-OPEN))
 (324 12 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (252 18 (:REWRITE NFIX-WHEN-ZP))
 (240 6 (:DEFINITION NTH))
 (234 6 (:DEFINITION GENERATE-INDEX-LIST))
 (216 24 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (216 12 (:REWRITE TAKE-OF-LEN-FREE))
 (188 106 (:REWRITE DEFAULT-+-2))
 (180 120 (:REWRITE DEFAULT-<-2))
 (168 6 (:DEFINITION TAKE))
 (162 18 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (127 53 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (126 120 (:REWRITE DEFAULT-<-1))
 (125 25 (:DEFINITION ASSOC-EQUAL))
 (117 9 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (112 106 (:REWRITE DEFAULT-+-1))
 (108 36 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (78 78 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (72 24 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (72 9 (:DEFINITION MEMBER-EQUAL))
 (66 22 (:DEFINITION CHARACTER-LISTP))
 (66 18 (:REWRITE NFIX-WHEN-NATP))
 (60 30 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (50 50 (:LINEAR POSITION-WHEN-MEMBER))
 (50 50 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (48 48 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (48 48 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (45 45 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (36 36 (:TYPE-PRESCRIPTION NULL))
 (36 36 (:DEFINITION NULL))
 (36 12 (:DEFINITION BINARY-APPEND))
 (36 6 (:DEFINITION NATP))
 (30 30 (:TYPE-PRESCRIPTION NATP))
 (24 24 (:TYPE-PRESCRIPTION NAT-LISTP))
 (24 24 (:REWRITE DEFAULT-COERCE-2))
 (24 24 (:REWRITE DEFAULT-COERCE-1))
 (24 6 (:REWRITE COMMUTATIVITY-OF-+))
 (18 18 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (18 18 (:REWRITE SUBSETP-MEMBER . 2))
 (18 18 (:REWRITE SUBSETP-MEMBER . 1))
 (18 18 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (18 6 (:DEFINITION NFIX))
 (12 12 (:TYPE-PRESCRIPTION NFIX))
 (12 12 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (6 6 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 )
(L3-WRCHS-CORRECTNESS-1-LEMMA-3
 (5 5 (:REWRITE DEFAULT-CAR))
 (5 1 (:DEFINITION LEN))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(L3-WRCHS-CORRECTNESS-1-LEMMA-4
 (944 184 (:DEFINITION LEN))
 (820 10 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (738 10 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (708 10 (:DEFINITION L3-FS-P))
 (598 598 (:REWRITE DEFAULT-CDR))
 (592 10 (:REWRITE DEFAULT-COERCE-3))
 (570 20 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (562 10 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (560 10 (:DEFINITION UNMAKE-BLOCKS))
 (537 17 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 (504 504 (:TYPE-PRESCRIPTION LEN))
 (474 474 (:REWRITE DEFAULT-CAR))
 (416 228 (:REWRITE DEFAULT-+-2))
 (340 10 (:DEFINITION NTH))
 (320 20 (:REWRITE TAKE-OF-LEN-FREE))
 (304 263 (:REWRITE DEFAULT-<-2))
 (273 263 (:REWRITE DEFAULT-<-1))
 (250 10 (:DEFINITION TAKE))
 (240 50 (:REWRITE ZP-OPEN))
 (228 228 (:REWRITE DEFAULT-+-1))
 (160 20 (:REWRITE NFIX-WHEN-ZP))
 (143 11 (:DEFINITION BOUNDED-NAT-LISTP))
 (136 10 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (90 6 (:DEFINITION BLOCK-LISTP))
 (86 10 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (60 60 (:LINEAR POSITION-WHEN-MEMBER))
 (60 60 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (60 20 (:REWRITE NFIX-WHEN-NATP))
 (48 16 (:DEFINITION BINARY-APPEND))
 (30 10 (:REWRITE COMMUTATIVITY-OF-+))
 (30 10 (:DEFINITION NFIX))
 (20 20 (:TYPE-PRESCRIPTION ZP))
 (20 20 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (20 20 (:TYPE-PRESCRIPTION NFIX))
 (20 20 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (18 6 (:DEFINITION CHARACTER-LISTP))
 (10 10 (:TYPE-PRESCRIPTION NATP))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (10 10 (:REWRITE DEFAULT-COERCE-2))
 (6 6 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 )
(L3-WRCHS-CORRECTNESS-1-LEMMA-6
 (1305 437 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 (1190 1190 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (953 953 (:REWRITE DEFAULT-CAR))
 (795 795 (:REWRITE DEFAULT-CDR))
 (483 161 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (430 86 (:DEFINITION LEN))
 (425 310 (:REWRITE DEFAULT-<-2))
 (311 310 (:REWRITE DEFAULT-<-1))
 (207 69 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (172 86 (:REWRITE DEFAULT-+-2))
 (116 116 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (86 86 (:TYPE-PRESCRIPTION LEN))
 (86 86 (:REWRITE DEFAULT-+-1))
 (69 69 (:TYPE-PRESCRIPTION NULL))
 (69 69 (:DEFINITION NULL))
 )
(L3-WRCHS-CORRECTNESS-1-LEMMA-8
 (4106 47 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (3260 47 (:DEFINITION UNMAKE-BLOCKS))
 (2883 94 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1726 94 (:REWRITE TAKE-OF-LEN-FREE))
 (1700 47 (:DEFINITION NTH))
 (1526 1067 (:REWRITE DEFAULT-CDR))
 (1515 303 (:DEFINITION LEN))
 (1495 47 (:REWRITE DEFAULT-COERCE-3))
 (1346 47 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1322 47 (:DEFINITION TAKE))
 (1246 227 (:REWRITE ZP-OPEN))
 (1210 1050 (:REWRITE DEFAULT-CAR))
 (913 491 (:REWRITE DEFAULT-+-2))
 (854 94 (:REWRITE NFIX-WHEN-ZP))
 (705 564 (:REWRITE DEFAULT-<-2))
 (682 491 (:REWRITE DEFAULT-+-1))
 (611 564 (:REWRITE DEFAULT-<-1))
 (571 29 (:DEFINITION BLOCK-LISTP))
 (333 94 (:REWRITE NFIX-WHEN-NATP))
 (325 47 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (312 39 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (298 298 (:LINEAR POSITION-WHEN-MEMBER))
 (298 298 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (260 47 (:REWRITE COMMUTATIVITY-OF-+))
 (240 55 (:DEFINITION NATP))
 (213 141 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (205 17 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-4))
 (180 164 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (152 8 (:DEFINITION NAT-LISTP))
 (141 47 (:DEFINITION NFIX))
 (141 47 (:DEFINITION BINARY-APPEND))
 (118 118 (:TYPE-PRESCRIPTION NAT-LISTP))
 (111 29 (:DEFINITION CHARACTER-LISTP))
 (110 110 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (102 102 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (94 94 (:TYPE-PRESCRIPTION NFIX))
 (86 86 (:TYPE-PRESCRIPTION NATP))
 (86 30 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (83 31 (:REWRITE L3-FS-P-ASSOC))
 (61 61 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (51 35 (:REWRITE L3-STAT-CORRECTNESS-2-LEMMA-1))
 (47 47 (:REWRITE DEFAULT-COERCE-2))
 (43 17 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-2))
 (39 39 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (16 16 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 )
(L3-WRCHS-CORRECTNESS-1-LEMMA-9
 (1852 22 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1302 44 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1300 22 (:DEFINITION UNMAKE-BLOCKS))
 (830 157 (:DEFINITION LEN))
 (772 22 (:DEFINITION NTH))
 (740 18 (:REWRITE DEFAULT-COERCE-3))
 (728 44 (:REWRITE TAKE-OF-LEN-FREE))
 (682 18 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (592 108 (:REWRITE ZP-OPEN))
 (578 26 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (567 551 (:REWRITE DEFAULT-CDR))
 (562 22 (:DEFINITION TAKE))
 (560 40 (:DEFINITION L3-FS-P))
 (468 156 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (452 449 (:REWRITE DEFAULT-CAR))
 (436 47 (:REWRITE NFIX-WHEN-ZP))
 (433 251 (:REWRITE DEFAULT-+-2))
 (368 16 (:DEFINITION BLOCK-LISTP))
 (340 265 (:REWRITE DEFAULT-<-2))
 (287 265 (:REWRITE DEFAULT-<-1))
 (276 18 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (273 251 (:REWRITE DEFAULT-+-1))
 (170 10 (:REWRITE L3-FS-P-ASSOC))
 (151 151 (:LINEAR POSITION-WHEN-MEMBER))
 (151 151 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (150 47 (:REWRITE NFIX-WHEN-NATP))
 (117 3 (:DEFINITION GENERATE-INDEX-LIST))
 (112 14 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (102 4 (:REWRITE L3-WRCHS-RETURNS-FS))
 (88 22 (:REWRITE COMMUTATIVITY-OF-+))
 (81 9 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (78 26 (:DEFINITION BINARY-APPEND))
 (78 22 (:DEFINITION NATP))
 (78 6 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (75 15 (:DEFINITION ASSOC-EQUAL))
 (72 16 (:DEFINITION CHARACTER-LISTP))
 (66 66 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (66 22 (:DEFINITION NFIX))
 (56 56 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (54 18 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (52 52 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (52 52 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (48 48 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (48 6 (:DEFINITION MEMBER-EQUAL))
 (44 44 (:TYPE-PRESCRIPTION NFIX))
 (36 36 (:TYPE-PRESCRIPTION NATP))
 (30 30 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (28 28 (:TYPE-PRESCRIPTION NAT-LISTP))
 (24 12 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (24 8 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 (18 18 (:TYPE-PRESCRIPTION NULL))
 (18 18 (:REWRITE DEFAULT-COERCE-2))
 (18 18 (:DEFINITION NULL))
 (15 6 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (14 14 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (12 12 (:REWRITE SUBSETP-MEMBER . 2))
 (12 12 (:REWRITE SUBSETP-MEMBER . 1))
 (9 9 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (6 6 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (3 3 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 )
(L3-WRCHS-CORRECTNESS-1
 (6512 74 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (4685 519 (:DEFINITION LEN))
 (4658 148 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (4542 74 (:DEFINITION UNMAKE-BLOCKS))
 (3642 2139 (:REWRITE DEFAULT-CDR))
 (2736 74 (:DEFINITION NTH))
 (2625 2175 (:REWRITE DEFAULT-CAR))
 (2592 148 (:REWRITE TAKE-OF-LEN-FREE))
 (2412 511 (:REWRITE ZP-OPEN))
 (2209 267 (:DEFINITION ASSOC-EQUAL))
 (2009 85 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (1968 74 (:DEFINITION TAKE))
 (1828 119 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1704 163 (:REWRITE NFIX-WHEN-ZP))
 (1624 64 (:REWRITE DEFAULT-COERCE-3))
 (1459 845 (:REWRITE DEFAULT-+-2))
 (1366 1014 (:REWRITE DEFAULT-<-2))
 (1182 84 (:DEFINITION L3-FS-P))
 (1161 20 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (1088 1014 (:REWRITE DEFAULT-<-1))
 (931 845 (:REWRITE DEFAULT-+-1))
 (810 30 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (603 67 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (585 15 (:DEFINITION GENERATE-INDEX-LIST))
 (584 163 (:REWRITE NFIX-WHEN-NATP))
 (504 504 (:LINEAR POSITION-WHEN-MEMBER))
 (504 504 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (402 134 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (355 25 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (351 5 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (318 5 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (317 5 (:REWRITE L2-FS-P-ASSOC))
 (302 74 (:REWRITE COMMUTATIVITY-OF-+))
 (273 91 (:DEFINITION BINARY-APPEND))
 (230 25 (:DEFINITION MEMBER-EQUAL))
 (228 222 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (222 74 (:DEFINITION NFIX))
 (209 117 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (193 193 (:TYPE-PRESCRIPTION NATP))
 (160 5 (:DEFINITION L2-FS-P))
 (154 154 (:REWRITE DEFAULT-COERCE-2))
 (148 148 (:TYPE-PRESCRIPTION NFIX))
 (148 148 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (134 134 (:TYPE-PRESCRIPTION NULL))
 (134 134 (:DEFINITION NULL))
 (125 125 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (113 25 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (90 90 (:REWRITE DEFAULT-COERCE-1))
 (50 50 (:REWRITE SUBSETP-MEMBER . 2))
 (50 50 (:REWRITE SUBSETP-MEMBER . 1))
 (45 45 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (36 16 (:REWRITE L3-WRCHS-RETURNS-FS))
 (33 11 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 (33 11 (:DEFINITION CHARACTER-LISTP))
 (18 10 (:REWRITE L3-TO-L2-FS-CORRECTNESS-1))
 (15 15 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 )
(L3-CREATE
 (472 162 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (208 16 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (154 10 (:DEFINITION L3-FS-P))
 (128 16 (:DEFINITION MEMBER-EQUAL))
 (118 19 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (97 97 (:REWRITE DEFAULT-CAR))
 (93 90 (:REWRITE DEFAULT-CDR))
 (80 80 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (60 11 (:DEFINITION LEN))
 (49 21 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (32 32 (:REWRITE SUBSETP-MEMBER . 2))
 (32 32 (:REWRITE SUBSETP-MEMBER . 1))
 (27 9 (:DEFINITION CHARACTER-LISTP))
 (22 11 (:REWRITE DEFAULT-+-2))
 (20 4 (:DEFINITION ASSOC-EQUAL))
 (15 3 (:DEFINITION EQLABLE-ALISTP))
 (11 11 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (1 1 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (1 1 (:REWRITE DEFAULT-COERCE-2))
 (1 1 (:REWRITE DEFAULT-COERCE-1))
 )
(L3-CREATE-RETURNS-FS
 (552 184 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (341 321 (:REWRITE DEFAULT-CAR))
 (308 270 (:REWRITE DEFAULT-CDR))
 (240 42 (:DEFINITION LEN))
 (234 6 (:DEFINITION GENERATE-INDEX-LIST))
 (150 62 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (144 12 (:REWRITE ZP-OPEN))
 (120 6 (:REWRITE NFIX-WHEN-ZP))
 (117 9 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (115 23 (:DEFINITION ASSOC-EQUAL))
 (108 12 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (102 54 (:REWRITE DEFAULT-+-2))
 (72 24 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (72 24 (:DEFINITION CHARACTER-LISTP))
 (72 9 (:DEFINITION MEMBER-EQUAL))
 (54 54 (:REWRITE DEFAULT-+-1))
 (45 45 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (36 18 (:REWRITE DEFAULT-<-2))
 (24 24 (:TYPE-PRESCRIPTION NULL))
 (24 24 (:DEFINITION NULL))
 (18 18 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (18 18 (:REWRITE SUBSETP-MEMBER . 2))
 (18 18 (:REWRITE SUBSETP-MEMBER . 1))
 (18 18 (:REWRITE DEFAULT-<-1))
 (18 6 (:DEFINITION BINARY-APPEND))
 (12 12 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (12 12 (:REWRITE DEFAULT-COERCE-2))
 (12 12 (:REWRITE DEFAULT-COERCE-1))
 (12 6 (:REWRITE NFIX-WHEN-NATP))
 (6 6 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (6 6 (:LINEAR POSITION-WHEN-MEMBER))
 (6 6 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(L3-CREATE-CORRECTNESS-1-LEMMA-2
 (1476 18 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1044 18 (:DEFINITION UNMAKE-BLOCKS))
 (1026 36 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (876 292 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (700 137 (:DEFINITION LEN))
 (612 18 (:DEFINITION NTH))
 (576 36 (:REWRITE TAKE-OF-LEN-FREE))
 (575 18 (:REWRITE DEFAULT-COERCE-3))
 (522 501 (:REWRITE DEFAULT-CDR))
 (519 18 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (496 94 (:REWRITE ZP-OPEN))
 (480 33 (:DEFINITION L3-FS-P))
 (450 18 (:DEFINITION TAKE))
 (436 430 (:REWRITE DEFAULT-CAR))
 (373 215 (:REWRITE DEFAULT-+-2))
 (348 39 (:REWRITE NFIX-WHEN-ZP))
 (286 223 (:REWRITE DEFAULT-<-2))
 (259 13 (:DEFINITION BLOCK-LISTP))
 (241 223 (:REWRITE DEFAULT-<-1))
 (233 215 (:REWRITE DEFAULT-+-1))
 (139 16 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (134 18 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (119 119 (:LINEAR POSITION-WHEN-MEMBER))
 (119 119 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (117 9 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (117 3 (:DEFINITION GENERATE-INDEX-LIST))
 (115 23 (:DEFINITION ASSOC-EQUAL))
 (114 39 (:REWRITE NFIX-WHEN-NATP))
 (72 18 (:REWRITE COMMUTATIVITY-OF-+))
 (72 9 (:DEFINITION MEMBER-EQUAL))
 (66 22 (:DEFINITION BINARY-APPEND))
 (64 64 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (63 27 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (54 54 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (54 18 (:DEFINITION NFIX))
 (54 18 (:DEFINITION NATP))
 (54 6 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (51 13 (:DEFINITION CHARACTER-LISTP))
 (45 45 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (40 40 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (38 38 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (36 36 (:TYPE-PRESCRIPTION NFIX))
 (36 12 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (34 34 (:TYPE-PRESCRIPTION NATP))
 (32 32 (:TYPE-PRESCRIPTION NAT-LISTP))
 (29 29 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (27 9 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 (25 25 (:REWRITE DEFAULT-COERCE-2))
 (23 10 (:REWRITE L3-CREATE-RETURNS-FS))
 (18 18 (:REWRITE SUBSETP-MEMBER . 2))
 (18 18 (:REWRITE SUBSETP-MEMBER . 1))
 (16 16 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (12 12 (:TYPE-PRESCRIPTION NULL))
 (12 12 (:DEFINITION NULL))
 (9 9 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (7 7 (:REWRITE DEFAULT-COERCE-1))
 (6 6 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (3 3 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 )
(L3-CREATE-CORRECTNESS-1
 (5456 64 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (3918 64 (:DEFINITION UNMAKE-BLOCKS))
 (3844 128 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (2977 558 (:DEFINITION LEN))
 (2732 2247 (:REWRITE DEFAULT-CDR))
 (2653 2180 (:REWRITE DEFAULT-CAR))
 (2482 386 (:REWRITE ZP-OPEN))
 (2274 64 (:DEFINITION NTH))
 (2176 128 (:REWRITE TAKE-OF-LEN-FREE))
 (1829 245 (:DEFINITION ASSOC-EQUAL))
 (1822 163 (:REWRITE NFIX-WHEN-ZP))
 (1808 65 (:REWRITE DEFAULT-COERCE-3))
 (1673 64 (:DEFINITION TAKE))
 (1617 62 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1559 884 (:REWRITE DEFAULT-+-2))
 (1365 35 (:DEFINITION GENERATE-INDEX-LIST))
 (1310 92 (:DEFINITION L3-FS-P))
 (1171 874 (:REWRITE DEFAULT-<-2))
 (984 884 (:REWRITE DEFAULT-+-1))
 (938 874 (:REWRITE DEFAULT-<-1))
 (834 15 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (544 60 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (503 163 (:REWRITE NFIX-WHEN-NATP))
 (450 50 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (446 32 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (427 427 (:LINEAR POSITION-WHEN-MEMBER))
 (427 427 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (318 5 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (317 5 (:REWRITE L2-FS-P-ASSOC))
 (307 62 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (303 101 (:DEFINITION BINARY-APPEND))
 (300 100 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (286 32 (:DEFINITION MEMBER-EQUAL))
 (276 69 (:DEFINITION NATP))
 (274 64 (:REWRITE COMMUTATIVITY-OF-+))
 (255 245 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (210 192 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (192 64 (:DEFINITION NFIX))
 (160 160 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (160 5 (:DEFINITION L2-FS-P))
 (153 153 (:REWRITE DEFAULT-COERCE-2))
 (132 132 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (128 128 (:TYPE-PRESCRIPTION NFIX))
 (124 124 (:TYPE-PRESCRIPTION NATP))
 (120 120 (:TYPE-PRESCRIPTION NAT-LISTP))
 (105 105 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (100 100 (:TYPE-PRESCRIPTION NULL))
 (100 100 (:DEFINITION NULL))
 (88 88 (:REWRITE DEFAULT-COERCE-1))
 (79 36 (:REWRITE L3-CREATE-RETURNS-FS))
 (75 21 (:DEFINITION CHARACTER-LISTP))
 (70 70 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (64 64 (:REWRITE SUBSETP-MEMBER . 2))
 (64 64 (:REWRITE SUBSETP-MEMBER . 1))
 (60 60 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (59 15 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (56 20 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 (35 35 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (24 5 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (9 5 (:REWRITE L3-TO-L2-FS-CORRECTNESS-1))
 )
(L3-READ-AFTER-WRITE-1-LEMMA-2
 (690 230 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (470 5 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (345 10 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (320 5 (:DEFINITION UNMAKE-BLOCKS))
 (245 245 (:REWRITE DEFAULT-CAR))
 (219 219 (:REWRITE DEFAULT-CDR))
 (200 5 (:DEFINITION NTH))
 (195 39 (:DEFINITION LEN))
 (190 10 (:REWRITE TAKE-OF-LEN-FREE))
 (160 32 (:DEFINITION ASSOC-EQUAL))
 (150 25 (:REWRITE ZP-OPEN))
 (140 5 (:DEFINITION TAKE))
 (135 9 (:DEFINITION BLOCK-LISTP))
 (130 10 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (125 5 (:REWRITE DEFAULT-COERCE-3))
 (110 10 (:REWRITE NFIX-WHEN-ZP))
 (110 5 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (103 59 (:REWRITE DEFAULT-+-2))
 (94 40 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (80 10 (:DEFINITION MEMBER-EQUAL))
 (75 60 (:REWRITE DEFAULT-<-2))
 (65 60 (:REWRITE DEFAULT-<-1))
 (64 59 (:REWRITE DEFAULT-+-1))
 (50 50 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (45 10 (:REWRITE NFIX-WHEN-NATP))
 (40 5 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (30 30 (:LINEAR POSITION-WHEN-MEMBER))
 (30 30 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (30 5 (:DEFINITION NATP))
 (27 9 (:DEFINITION CHARACTER-LISTP))
 (20 20 (:REWRITE SUBSETP-MEMBER . 2))
 (20 20 (:REWRITE SUBSETP-MEMBER . 1))
 (20 20 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (20 5 (:REWRITE COMMUTATIVITY-OF-+))
 (15 15 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (15 5 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (15 5 (:DEFINITION NFIX))
 (15 5 (:DEFINITION BINARY-APPEND))
 (10 10 (:TYPE-PRESCRIPTION NFIX))
 (10 10 (:TYPE-PRESCRIPTION NATP))
 (10 10 (:TYPE-PRESCRIPTION NAT-LISTP))
 (10 10 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (9 9 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (5 5 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (5 5 (:REWRITE DEFAULT-COERCE-2))
 )
(L3-READ-AFTER-WRITE-1-LEMMA-3
 (19240 44 (:DEFINITION L3-WRCHS))
 (7868 544 (:DEFINITION LEN))
 (6386 69 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (5359 2334 (:REWRITE DEFAULT-CDR))
 (4661 138 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (4224 176 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (3976 69 (:DEFINITION UNMAKE-BLOCKS))
 (3765 15 (:DEFINITION L3-STAT))
 (3128 644 (:REWRITE ZP-OPEN))
 (2710 69 (:DEFINITION NTH))
 (2548 201 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (2493 2289 (:REWRITE DEFAULT-CAR))
 (2376 88 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (2348 182 (:REWRITE NFIX-WHEN-ZP))
 (2188 10 (:DEFINITION L3-TO-L2-FS))
 (2182 138 (:REWRITE TAKE-OF-LEN-FREE))
 (1940 151 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (1907 69 (:DEFINITION TAKE))
 (1716 44 (:DEFINITION GENERATE-INDEX-LIST))
 (1624 1109 (:REWRITE DEFAULT-<-2))
 (1565 908 (:REWRITE DEFAULT-+-2))
 (1188 132 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (1178 1109 (:REWRITE DEFAULT-<-1))
 (1142 28 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (1048 25 (:REWRITE DEFAULT-COERCE-3))
 (1005 163 (:DEFINITION ASSOC-EQUAL))
 (977 908 (:REWRITE DEFAULT-+-1))
 (928 69 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (873 201 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (792 264 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (689 61 (:REWRITE L3-FS-P-ASSOC))
 (684 182 (:REWRITE NFIX-WHEN-NATP))
 (631 631 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (583 69 (:DEFINITION MEMBER-EQUAL))
 (516 14 (:DEFINITION L2-FS-P))
 (458 430 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (452 452 (:LINEAR POSITION-WHEN-MEMBER))
 (452 452 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (440 220 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (368 368 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (350 6 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (345 345 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (339 113 (:DEFINITION BINARY-APPEND))
 (290 26 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (290 6 (:REWRITE L2-FS-P-ASSOC))
 (276 69 (:REWRITE COMMUTATIVITY-OF-+))
 (264 264 (:TYPE-PRESCRIPTION NULL))
 (264 264 (:DEFINITION NULL))
 (261 261 (:TYPE-PRESCRIPTION NATP))
 (208 208 (:TYPE-PRESCRIPTION NAT-LISTP))
 (207 207 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (207 69 (:DEFINITION NFIX))
 (201 201 (:REWRITE DEFAULT-COERCE-2))
 (192 6 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (177 41 (:DEFINITION CHARACTER-LISTP))
 (176 176 (:REWRITE DEFAULT-COERCE-1))
 (176 16 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-8))
 (168 72 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (156 156 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (154 16 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-4))
 (138 138 (:TYPE-PRESCRIPTION NFIX))
 (138 138 (:REWRITE SUBSETP-MEMBER . 2))
 (138 138 (:REWRITE SUBSETP-MEMBER . 1))
 (132 132 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (132 132 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (128 16 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (56 7 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-9))
 (44 44 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (12 12 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (9 3 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 )
(L3-STAT-AFTER-WRITE
 (14906 34 (:DEFINITION L3-WRCHS))
 (9514 105 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (7728 750 (:DEFINITION LEN))
 (6889 210 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (6395 3435 (:REWRITE DEFAULT-CDR))
 (6247 32 (:DEFINITION L3-TO-L2-FS))
 (6068 105 (:DEFINITION UNMAKE-BLOCKS))
 (4854 85 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (4568 3518 (:REWRITE DEFAULT-CAR))
 (4022 105 (:DEFINITION NTH))
 (3850 775 (:REWRITE ZP-OPEN))
 (3525 430 (:DEFINITION ASSOC-EQUAL))
 (3462 145 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (3338 210 (:REWRITE TAKE-OF-LEN-FREE))
 (3030 207 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (2851 105 (:DEFINITION TAKE))
 (2812 244 (:REWRITE NFIX-WHEN-ZP))
 (2696 210 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (2250 80 (:REWRITE DEFAULT-COERCE-3))
 (2127 1238 (:REWRITE DEFAULT-+-2))
 (2073 1511 (:REWRITE DEFAULT-<-2))
 (1836 68 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (1616 1511 (:REWRITE DEFAULT-<-1))
 (1375 20 (:REWRITE L2-FS-P-ASSOC))
 (1357 20 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (1343 1238 (:REWRITE DEFAULT-+-1))
 (1326 34 (:DEFINITION GENERATE-INDEX-LIST))
 (1313 98 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1227 30 (:DEFINITION L2-FS-P))
 (1115 20 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (974 88 (:REWRITE L3-FS-P-ASSOC))
 (924 244 (:REWRITE NFIX-WHEN-NATP))
 (918 102 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (823 98 (:DEFINITION MEMBER-EQUAL))
 (769 207 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (671 95 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (637 70 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-4))
 (622 562 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (612 204 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (605 605 (:LINEAR POSITION-WHEN-MEMBER))
 (605 605 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (590 590 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (520 65 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (490 490 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (420 105 (:REWRITE COMMUTATIVITY-OF-+))
 (417 139 (:DEFINITION BINARY-APPEND))
 (370 70 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-8))
 (337 337 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (315 315 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (315 105 (:DEFINITION NFIX))
 (306 306 (:TYPE-PRESCRIPTION NATP))
 (266 266 (:TYPE-PRESCRIPTION NAT-LISTP))
 (234 234 (:REWRITE DEFAULT-COERCE-2))
 (222 222 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (210 210 (:TYPE-PRESCRIPTION NFIX))
 (204 204 (:TYPE-PRESCRIPTION NULL))
 (204 204 (:DEFINITION NULL))
 (196 196 (:REWRITE SUBSETP-MEMBER . 2))
 (196 196 (:REWRITE SUBSETP-MEMBER . 1))
 (154 154 (:REWRITE DEFAULT-COERCE-1))
 (135 34 (:DEFINITION CHARACTER-LISTP))
 (126 54 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (102 102 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (102 102 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (72 9 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-9))
 (40 40 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (34 34 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (18 6 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 )
(L3-READ-AFTER-WRITE-1
 (1311 3 (:DEFINITION L3-WRCHS))
 (1087 90 (:DEFINITION LEN))
 (940 10 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (690 20 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (660 289 (:REWRITE DEFAULT-CDR))
 (580 10 (:DEFINITION UNMAKE-BLOCKS))
 (550 32 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (417 105 (:REWRITE ZP-OPEN))
 (400 10 (:DEFINITION NTH))
 (320 20 (:REWRITE TAKE-OF-LEN-FREE))
 (300 27 (:REWRITE NFIX-WHEN-ZP))
 (298 17 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (280 10 (:DEFINITION TAKE))
 (274 19 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (264 150 (:REWRITE DEFAULT-+-2))
 (242 236 (:REWRITE DEFAULT-CAR))
 (240 80 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (236 163 (:REWRITE DEFAULT-<-2))
 (213 9 (:REWRITE DEFAULT-COERCE-3))
 (212 1 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (188 2 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (182 13 (:DEFINITION L3-FS-P))
 (174 163 (:REWRITE DEFAULT-<-1))
 (162 6 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (161 150 (:REWRITE DEFAULT-+-1))
 (133 10 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (128 10 (:REWRITE L3-FS-P-ASSOC))
 (126 126 (:TYPE-PRESCRIPTION ZP))
 (117 3 (:DEFINITION GENERATE-INDEX-LIST))
 (110 2 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 1))
 (100 27 (:REWRITE NFIX-WHEN-NATP))
 (85 17 (:DEFINITION ASSOC-EQUAL))
 (83 10 (:DEFINITION MEMBER-EQUAL))
 (81 9 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (63 19 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (62 62 (:LINEAR POSITION-WHEN-MEMBER))
 (62 62 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (62 7 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (54 18 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (53 53 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (52 52 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (50 50 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (49 49 (:REWRITE DEFAULT-COERCE-2))
 (40 40 (:REWRITE DEFAULT-COERCE-1))
 (39 13 (:DEFINITION BINARY-APPEND))
 (39 1 (:DEFINITION NTHCDR))
 (31 31 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (30 30 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (30 10 (:DEFINITION NFIX))
 (29 29 (:TYPE-PRESCRIPTION NATP))
 (26 26 (:TYPE-PRESCRIPTION NAT-LISTP))
 (22 22 (:TYPE-PRESCRIPTION NFIX))
 (20 20 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (20 20 (:REWRITE SUBSETP-MEMBER . 2))
 (20 20 (:REWRITE SUBSETP-MEMBER . 1))
 (18 18 (:TYPE-PRESCRIPTION NULL))
 (18 18 (:DEFINITION NULL))
 (9 9 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (9 9 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (9 3 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 (9 3 (:DEFINITION CHARACTER-LISTP))
 (6 6 (:REWRITE L3-WRCHS-RETURNS-FS))
 (3 3 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(L3-READ-AFTER-WRITE-2
 (1748 4 (:DEFINITION L3-WRCHS))
 (1222 13 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1078 112 (:DEFINITION LEN))
 (989 30 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (754 13 (:DEFINITION UNMAKE-BLOCKS))
 (710 382 (:REWRITE DEFAULT-CDR))
 (640 30 (:REWRITE TAKE-OF-LEN-FREE))
 (598 15 (:DEFINITION TAKE))
 (582 15 (:DEFINITION NTH))
 (566 115 (:REWRITE ZP-OPEN))
 (468 48 (:REWRITE NFIX-WHEN-ZP))
 (388 22 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (384 16 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (358 25 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (335 204 (:REWRITE DEFAULT-+-2))
 (320 312 (:REWRITE DEFAULT-CAR))
 (312 104 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (303 220 (:REWRITE DEFAULT-<-2))
 (257 11 (:REWRITE DEFAULT-COERCE-3))
 (239 220 (:REWRITE DEFAULT-<-1))
 (238 17 (:DEFINITION L3-FS-P))
 (219 204 (:REWRITE DEFAULT-+-1))
 (216 8 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (173 48 (:REWRITE NFIX-WHEN-NATP))
 (173 13 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (167 13 (:REWRITE L3-FS-P-ASSOC))
 (162 162 (:TYPE-PRESCRIPTION ZP))
 (156 4 (:DEFINITION GENERATE-INDEX-LIST))
 (118 2 (:REWRITE LEN-OF-NTHCDR))
 (110 22 (:DEFINITION ASSOC-EQUAL))
 (108 13 (:DEFINITION MEMBER-EQUAL))
 (108 12 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (106 2 (:REWRITE CAR-OF-NTHCDR))
 (92 4 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (88 88 (:LINEAR POSITION-WHEN-MEMBER))
 (88 88 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (83 25 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (80 9 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (72 24 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (70 70 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (68 68 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (66 2 (:DEFINITION NTHCDR))
 (65 65 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (53 15 (:DEFINITION NFIX))
 (51 17 (:DEFINITION BINARY-APPEND))
 (41 41 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (40 40 (:TYPE-PRESCRIPTION NATP))
 (39 39 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (38 4 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (38 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (34 34 (:TYPE-PRESCRIPTION NFIX))
 (34 34 (:TYPE-PRESCRIPTION NAT-LISTP))
 (33 33 (:REWRITE DEFAULT-COERCE-2))
 (32 2 (:REWRITE CONSP-OF-NTHCDR))
 (26 26 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (26 26 (:REWRITE SUBSETP-MEMBER . 2))
 (26 26 (:REWRITE SUBSETP-MEMBER . 1))
 (24 24 (:TYPE-PRESCRIPTION NULL))
 (24 24 (:DEFINITION NULL))
 (22 22 (:REWRITE DEFAULT-COERCE-1))
 (12 12 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (12 12 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (12 4 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 (12 4 (:DEFINITION CHARACTER-LISTP))
 (10 10 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (10 2 (:REWRITE CONSP-OF-TAKE))
 (8 8 (:REWRITE L3-WRCHS-RETURNS-FS))
 (4 4 (:TYPE-PRESCRIPTION TRUE-LISTP-TAKE))
 (4 4 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (4 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(L3-READ-AFTER-CREATE-1
 (5190 30 (:DEFINITION L3-CREATE))
 (4137 4 (:DEFINITION L2-CREATE))
 (3394 39 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (2419 78 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (2388 12 (:REWRITE L3-UNLINK-CORRECTNESS-1-LEMMA-1))
 (2194 1865 (:REWRITE DEFAULT-CDR))
 (2169 1892 (:REWRITE DEFAULT-CAR))
 (2126 39 (:DEFINITION UNMAKE-BLOCKS))
 (2085 387 (:DEFINITION LEN))
 (1784 142 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (1762 253 (:REWRITE ZP-OPEN))
 (1424 39 (:DEFINITION NTH))
 (1325 187 (:DEFINITION ASSOC-EQUAL))
 (1322 108 (:REWRITE NFIX-WHEN-ZP))
 (1307 41 (:REWRITE DEFAULT-COERCE-3))
 (1196 82 (:REWRITE TAKE-OF-LEN-FREE))
 (1170 30 (:DEFINITION GENERATE-INDEX-LIST))
 (1134 39 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1094 41 (:DEFINITION TAKE))
 (1075 613 (:REWRITE DEFAULT-+-2))
 (956 34 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (848 262 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (794 577 (:REWRITE DEFAULT-<-2))
 (706 53 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (654 613 (:REWRITE DEFAULT-+-1))
 (648 72 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (618 577 (:REWRITE DEFAULT-<-1))
 (595 53 (:REWRITE L3-FS-P-ASSOC))
 (491 4 (:DEFINITION L2-STAT))
 (484 15 (:DEFINITION L2-FS-P))
 (456 72 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (441 53 (:DEFINITION MEMBER-EQUAL))
 (432 144 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (370 370 (:TYPE-PRESCRIPTION ZP))
 (343 108 (:REWRITE NFIX-WHEN-NATP))
 (297 39 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (283 19 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-4))
 (272 8 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (272 8 (:REWRITE L2-FS-P-ASSOC))
 (265 265 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (264 33 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (245 54 (:DEFINITION NATP))
 (238 238 (:LINEAR POSITION-WHEN-MEMBER))
 (238 238 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (226 27 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-2))
 (207 69 (:DEFINITION BINARY-APPEND))
 (177 147 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (154 66 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (144 144 (:TYPE-PRESCRIPTION NULL))
 (144 144 (:DEFINITION NULL))
 (144 36 (:DEFINITION CHARACTER-LISTP))
 (128 8 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (118 118 (:REWRITE DEFAULT-COERCE-2))
 (117 117 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (117 39 (:DEFINITION NFIX))
 (109 109 (:REWRITE L3-STAT-CORRECTNESS-2-LEMMA-1))
 (106 106 (:REWRITE SUBSETP-MEMBER . 2))
 (106 106 (:REWRITE SUBSETP-MEMBER . 1))
 (90 90 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (90 90 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (84 84 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (83 19 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-8))
 (80 80 (:TYPE-PRESCRIPTION NFIX))
 (77 77 (:REWRITE DEFAULT-COERCE-1))
 (72 72 (:TYPE-PRESCRIPTION NATP))
 (66 66 (:TYPE-PRESCRIPTION NAT-LISTP))
 (60 60 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (52 2 (:REWRITE THEN-SUBSEQ-SAME-2))
 (52 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (51 8 (:REWRITE L2-CREATE-RETURNS-FS))
 (44 12 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (44 2 (:REWRITE CONSP-OF-TAKE))
 (33 33 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (32 4 (:REWRITE L3-CREATE-CORRECTNESS-1-LEMMA-2))
 (32 2 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (30 30 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (24 8 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 (8 8 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 )
(L3-READ-AFTER-CREATE-2
 (28708 164 (:DEFINITION L3-CREATE))
 (27308 310 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (21678 716 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (21371 26 (:DEFINITION L2-CREATE))
 (18913 14579 (:REWRITE DEFAULT-CDR))
 (17902 14635 (:REWRITE DEFAULT-CAR))
 (17808 310 (:DEFINITION UNMAKE-BLOCKS))
 (16935 2983 (:DEFINITION LEN))
 (15750 425 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (14307 716 (:REWRITE TAKE-OF-LEN-FREE))
 (13852 2392 (:REWRITE ZP-OPEN))
 (13681 358 (:DEFINITION TAKE))
 (13330 1718 (:DEFINITION ASSOC-EQUAL))
 (12972 358 (:DEFINITION NTH))
 (12498 892 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (11420 1213 (:REWRITE NFIX-WHEN-ZP))
 (10350 78 (:REWRITE L3-UNLINK-CORRECTNESS-1-LEMMA-1))
 (8766 5281 (:REWRITE DEFAULT-+-2))
 (8503 358 (:REWRITE DEFAULT-COERCE-3))
 (7188 310 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (6855 5147 (:REWRITE DEFAULT-<-2))
 (6396 164 (:DEFINITION GENERATE-INDEX-LIST))
 (6306 457 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (5619 5281 (:REWRITE DEFAULT-+-1))
 (5563 5147 (:REWRITE DEFAULT-<-1))
 (4551 375 (:REWRITE L3-FS-P-ASSOC))
 (4224 406 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (4108 107 (:REWRITE L2-FS-P-ASSOC))
 (4021 457 (:DEFINITION MEMBER-EQUAL))
 (3812 107 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (3597 1213 (:REWRITE NFIX-WHEN-NATP))
 (3315 107 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (3010 315 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-4))
 (2456 48 (:REWRITE CAR-OF-NTHCDR))
 (2436 812 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (2416 302 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (2285 2285 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (2252 2252 (:LINEAR POSITION-WHEN-MEMBER))
 (2252 2252 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (2246 47 (:REWRITE LEN-OF-NTHCDR))
 (2238 318 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (2096 96 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (1942 406 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (1881 315 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-8))
 (1616 1344 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (1584 48 (:DEFINITION NTHCDR))
 (1422 474 (:DEFINITION BINARY-APPEND))
 (1170 310 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (1148 352 (:DEFINITION NFIX))
 (930 930 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (914 914 (:REWRITE SUBSETP-MEMBER . 2))
 (914 914 (:REWRITE SUBSETP-MEMBER . 1))
 (912 96 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (862 862 (:REWRITE DEFAULT-COERCE-2))
 (812 812 (:TYPE-PRESCRIPTION NULL))
 (812 812 (:DEFINITION NULL))
 (811 811 (:TYPE-PRESCRIPTION NFIX))
 (730 342 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (722 42 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (699 48 (:REWRITE CONSP-OF-NTHCDR))
 (659 659 (:TYPE-PRESCRIPTION NATP))
 (636 636 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (628 628 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (604 604 (:TYPE-PRESCRIPTION NAT-LISTP))
 (504 504 (:REWRITE DEFAULT-COERCE-1))
 (492 492 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (384 112 (:DEFINITION CHARACTER-LISTP))
 (328 328 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (302 302 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (240 240 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (235 47 (:REWRITE CONSP-OF-TAKE))
 (224 28 (:REWRITE L3-CREATE-CORRECTNESS-1-LEMMA-2))
 (164 164 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (162 162 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (113 64 (:REWRITE L2-CREATE-RETURNS-FS))
 (111 37 (:REWRITE L3-BOUNDED-FS-P-CORRECTNESS-2))
 (89 89 (:REWRITE DEFAULT-UNARY-MINUS))
 (42 42 (:REWRITE FOLD-CONSTS-IN-+))
 (18 2 (:REWRITE L3-RDCHS-CORRECTNESS-1-LEMMA-1))
 )
(WC-LEN)