File: file-system-4%40useless-runes.lsp

package info (click to toggle)
acl2 8.5dfsg-5
links: PTS
area: main
in suites: bookworm
size: 991,452 kB
sloc: lisp: 15,567,759; javascript: 22,820; cpp: 13,929; ansic: 12,092; perl: 7,150; java: 4,405; xml: 3,884; makefile: 3,507; sh: 3,187; ruby: 2,633; ml: 763; python: 746; yacc: 723; awk: 295; csh: 186; php: 171; lex: 154; tcl: 49; asm: 23; haskell: 17
file content (4268 lines) | stat: -rw-r--r-- 175,374 bytes
(INDICES-MARKED-P
 (15 3 (:DEFINITION BOOLEAN-LISTP))
 (14 1 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
 (10 10 (:REWRITE DEFAULT-CAR))
 (8 8 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 )
(INDICES-MARKED-P-CORRECTNESS-1
 (130 26 (:DEFINITION LEN))
 (108 17 (:REWRITE NFIX-WHEN-ZP))
 (102 19 (:REWRITE ZP-OPEN))
 (93 73 (:REWRITE DEFAULT-<-2))
 (73 73 (:REWRITE DEFAULT-<-1))
 (58 32 (:REWRITE DEFAULT-+-2))
 (49 49 (:REWRITE DEFAULT-CAR))
 (41 41 (:REWRITE DEFAULT-CDR))
 (32 32 (:REWRITE DEFAULT-+-1))
 (17 17 (:LINEAR POSITION-WHEN-MEMBER))
 (17 17 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (13 13 (:TYPE-PRESCRIPTION ZP))
 (11 11 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (9 3 (:DEFINITION NFIX))
 )
(INDICES-MARKED-P-CORRECTNESS-2
 (2073 58 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (611 58 (:REWRITE NFIX-WHEN-ZP))
 (422 211 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (320 262 (:REWRITE DEFAULT-<-2))
 (300 58 (:REWRITE NFIX-WHEN-NATP))
 (290 58 (:DEFINITION LEN))
 (283 262 (:REWRITE DEFAULT-<-1))
 (211 211 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (211 211 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (174 30 (:DEFINITION NATP))
 (172 117 (:REWRITE DEFAULT-CDR))
 (145 87 (:REWRITE DEFAULT-+-2))
 (129 29 (:DEFINITION NFIX))
 (127 69 (:REWRITE DEFAULT-CAR))
 (87 87 (:REWRITE DEFAULT-+-1))
 (58 58 (:TYPE-PRESCRIPTION ZP))
 (58 58 (:LINEAR POSITION-WHEN-MEMBER))
 (58 58 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (29 29 (:TYPE-PRESCRIPTION NATP))
 (21 21 (:REWRITE CONSP-OF-APPEND))
 (14 1 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
 (10 1 (:DEFINITION NAT-LISTP))
 (5 5 (:TYPE-PRESCRIPTION NAT-LISTP))
 (2 2 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 )
(INDICES-MARKED-P-CORRECTNESS-3
 (1465 40 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (336 12 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-2))
 (334 62 (:DEFINITION LEN))
 (320 40 (:REWRITE NFIX-WHEN-ZP))
 (292 238 (:REWRITE DEFAULT-<-2))
 (238 238 (:REWRITE DEFAULT-<-1))
 (159 159 (:REWRITE DEFAULT-CDR))
 (144 82 (:REWRITE DEFAULT-+-2))
 (140 140 (:REWRITE DEFAULT-CAR))
 (117 9 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-3))
 (113 14 (:DEFINITION MEMBER-EQUAL))
 (100 40 (:REWRITE NFIX-WHEN-NATP))
 (93 6 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
 (82 82 (:REWRITE DEFAULT-+-1))
 (73 34 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (69 9 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-4))
 (52 52 (:LINEAR POSITION-WHEN-MEMBER))
 (52 52 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (45 15 (:DEFINITION NFIX))
 (40 40 (:TYPE-PRESCRIPTION ZP))
 (28 28 (:REWRITE SUBSETP-MEMBER . 2))
 (28 28 (:REWRITE SUBSETP-MEMBER . 1))
 (22 22 (:TYPE-PRESCRIPTION NATP))
 (10 10 (:REWRITE SUBSETP-MEMBER . 4))
 (10 10 (:REWRITE SUBSETP-MEMBER . 3))
 )
(INDUCTION-SCHEME)
(INDICES-MARKED-P-CORRECTNESS-4
 (301 8 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (176 34 (:DEFINITION LEN))
 (138 4 (:DEFINITION NTH))
 (136 3 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-2))
 (117 43 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (98 76 (:REWRITE DEFAULT-<-2))
 (95 95 (:REWRITE DEFAULT-CDR))
 (90 90 (:REWRITE DEFAULT-CAR))
 (76 76 (:REWRITE DEFAULT-<-1))
 (72 38 (:REWRITE DEFAULT-+-2))
 (64 12 (:REWRITE ZP-OPEN))
 (64 8 (:REWRITE NFIX-WHEN-ZP))
 (63 2 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-4))
 (38 38 (:REWRITE DEFAULT-+-1))
 (19 4 (:REWRITE SUBSETP-MEMBER . 3))
 (18 18 (:LINEAR POSITION-WHEN-MEMBER))
 (18 18 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (16 8 (:REWRITE NFIX-WHEN-NATP))
 (15 15 (:REWRITE SUBSETP-MEMBER . 2))
 (15 15 (:REWRITE SUBSETP-MEMBER . 1))
 (12 1 (:DEFINITION SUBSETP-EQUAL))
 (8 8 (:TYPE-PRESCRIPTION ZP))
 (8 8 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (6 2 (:DEFINITION NFIX))
 (4 4 (:REWRITE SUBSETP-MEMBER . 4))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:TYPE-PRESCRIPTION INDUCTION-SCHEME))
 (1 1 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 )
(INDICES-MARKED-P-CORRECTNESS-5
 (115 4 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (89 2 (:REWRITE INDICES-MARKED-P-CORRECTNESS-3))
 (70 2 (:DEFINITION NTH))
 (35 7 (:DEFINITION LEN))
 (32 6 (:REWRITE ZP-OPEN))
 (32 4 (:REWRITE NFIX-WHEN-ZP))
 (29 23 (:REWRITE DEFAULT-<-2))
 (24 23 (:REWRITE DEFAULT-<-1))
 (21 1 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-3))
 (16 9 (:REWRITE DEFAULT-+-2))
 (15 15 (:REWRITE DEFAULT-CDR))
 (12 4 (:REWRITE NFIX-WHEN-NATP))
 (10 10 (:REWRITE DEFAULT-CAR))
 (10 1 (:DEFINITION NAT-LISTP))
 (9 9 (:REWRITE DEFAULT-+-1))
 (6 2 (:DEFINITION NFIX))
 (6 1 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-2))
 (5 5 (:LINEAR POSITION-WHEN-MEMBER))
 (5 5 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (5 1 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-4))
 (4 4 (:TYPE-PRESCRIPTION ZP))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (2 2 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (2 2 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (2 1 (:DEFINITION MEMBER-EQUAL))
 (1 1 (:REWRITE SUBSETP-MEMBER . 2))
 (1 1 (:REWRITE SUBSETP-MEMBER . 1))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L4-REGULAR-FILE-ENTRY-P)
(L4-FS-P)
(L4-STAT)
(L4-RDCHS)
(L4-WRCHS
 (648 24 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (576 24 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (555 159 (:REWRITE DEFAULT-CDR))
 (389 135 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (276 3 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (216 24 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (201 6 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (175 30 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (154 49 (:REWRITE ZP-OPEN))
 (150 10 (:DEFINITION L3-FS-P))
 (133 16 (:REWRITE NFIX-WHEN-ZP))
 (131 131 (:REWRITE DEFAULT-CAR))
 (130 10 (:DEFINITION COUNT-FREE-BLOCKS))
 (125 76 (:REWRITE DEFAULT-<-2))
 (125 70 (:REWRITE DEFAULT-+-2))
 (120 3 (:DEFINITION NTH))
 (89 76 (:REWRITE DEFAULT-<-1))
 (81 70 (:REWRITE DEFAULT-+-1))
 (58 1 (:DEFINITION UNMAKE-BLOCKS))
 (44 11 (:REWRITE COMMUTATIVITY-OF-+))
 (35 15 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (32 2 (:REWRITE TAKE-OF-LEN-FREE))
 (30 30 (:LINEAR POSITION-WHEN-MEMBER))
 (30 30 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (30 6 (:DEFINITION ASSOC-EQUAL))
 (28 1 (:DEFINITION TAKE))
 (26 2 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (25 5 (:DEFINITION EQLABLE-ALISTP))
 (24 24 (:REWRITE DEFAULT-COERCE-2))
 (24 24 (:REWRITE DEFAULT-COERCE-1))
 (21 7 (:DEFINITION CHARACTER-LISTP))
 (16 2 (:DEFINITION MEMBER-EQUAL))
 (12 12 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (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))
 (3 1 (:DEFINITION BINARY-APPEND))
 (1 1 (:TYPE-PRESCRIPTION SET-INDICES))
 )
(L4-LIST-ALL-INDICES
 (199 92 (:REWRITE DEFAULT-+-2))
 (129 92 (:REWRITE DEFAULT-+-1))
 (85 9 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (72 18 (:DEFINITION INTEGER-ABS))
 (72 9 (:REWRITE LENGTH-WHEN-STRINGP))
 (45 9 (:DEFINITION LEN))
 (44 44 (:REWRITE DEFAULT-CAR))
 (33 15 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (31 23 (:REWRITE DEFAULT-<-2))
 (31 1 (:DEFINITION L4-LIST-ALL-INDICES))
 (27 23 (:REWRITE DEFAULT-<-1))
 (22 2 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (18 18 (:REWRITE DEFAULT-UNARY-MINUS))
 (16 2 (:DEFINITION STRING-LISTP))
 (15 1 (:DEFINITION TRUE-LISTP))
 (10 10 (:TYPE-PRESCRIPTION STRING-LISTP))
 (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))
 (7 1 (:DEFINITION BINARY-APPEND))
 )
(L4-LIST-ALL-INDICES-CORRECTNESS-1
 (89 89 (:REWRITE DEFAULT-CAR))
 (50 50 (:REWRITE DEFAULT-CDR))
 (41 15 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (22 4 (:DEFINITION BINARY-APPEND))
 (20 20 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (10 10 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE DEFAULT-<-1))
 )
(L4-STRICTER-FS-P)
(L4-WRCHS-RETURNS-FS
 (2496 832 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (2410 1173 (:REWRITE DEFAULT-CDR))
 (2256 24 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1656 48 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1498 24 (:DEFINITION UNMAKE-BLOCKS))
 (1483 1218 (:REWRITE DEFAULT-CAR))
 (1189 75 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (1132 241 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (960 24 (:DEFINITION NTH))
 (933 233 (:REWRITE ZP-OPEN))
 (912 48 (:REWRITE TAKE-OF-LEN-FREE))
 (715 59 (:REWRITE NFIX-WHEN-ZP))
 (702 74 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (697 521 (:REWRITE DEFAULT-<-2))
 (691 407 (:REWRITE DEFAULT-+-2))
 (680 136 (:DEFINITION ASSOC-EQUAL))
 (672 24 (:DEFINITION TAKE))
 (584 4 (:DEFINITION SET-INDICES))
 (556 521 (:REWRITE DEFAULT-<-1))
 (440 407 (:REWRITE DEFAULT-+-1))
 (364 28 (:DEFINITION COUNT-FREE-BLOCKS))
 (240 16 (:DEFINITION BLOCK-LISTP))
 (195 195 (:LINEAR POSITION-WHEN-MEMBER))
 (195 195 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (189 52 (:REWRITE COMMUTATIVITY-OF-+))
 (156 156 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (156 12 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (122 74 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (117 13 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (96 12 (:DEFINITION MEMBER-EQUAL))
 (80 16 (:DEFINITION BOOLEAN-LISTP))
 (78 26 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (74 74 (:REWRITE DEFAULT-COERCE-2))
 (74 74 (:REWRITE DEFAULT-COERCE-1))
 (72 24 (:DEFINITION NFIX))
 (72 24 (:DEFINITION BINARY-APPEND))
 (60 60 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (56 56 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (56 8 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (48 48 (:TYPE-PRESCRIPTION NATP))
 (48 48 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (48 16 (:DEFINITION CHARACTER-LISTP))
 (40 4 (:DEFINITION UPDATE-NTH))
 (34 34 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (26 26 (:TYPE-PRESCRIPTION NULL))
 (26 26 (:DEFINITION NULL))
 (24 24 (:REWRITE SUBSETP-MEMBER . 2))
 (24 24 (:REWRITE SUBSETP-MEMBER . 1))
 (20 20 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 )
(L4-WRCHS-RETURNS-ALV
 (1233 411 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1182 400 (:REWRITE DEFAULT-CDR))
 (846 9 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (629 429 (:REWRITE DEFAULT-CAR))
 (621 18 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (576 9 (:DEFINITION UNMAKE-BLOCKS))
 (500 44 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (468 4 (:DEFINITION SET-INDICES))
 (442 124 (:REWRITE ZP-OPEN))
 (360 9 (:DEFINITION NTH))
 (342 18 (:REWRITE TAKE-OF-LEN-FREE))
 (313 25 (:REWRITE NFIX-WHEN-ZP))
 (273 184 (:REWRITE DEFAULT-<-2))
 (252 9 (:DEFINITION TAKE))
 (251 145 (:REWRITE DEFAULT-+-2))
 (200 184 (:REWRITE DEFAULT-<-1))
 (195 39 (:DEFINITION ASSOC-EQUAL))
 (162 145 (:REWRITE DEFAULT-+-1))
 (150 10 (:DEFINITION BLOCK-LISTP))
 (132 44 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (117 13 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (117 9 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (104 104 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (104 8 (:DEFINITION COUNT-FREE-BLOCKS))
 (85 85 (:LINEAR POSITION-WHEN-MEMBER))
 (85 85 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (78 26 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (72 9 (:DEFINITION MEMBER-EQUAL))
 (68 17 (:REWRITE COMMUTATIVITY-OF-+))
 (66 28 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (64 8 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (54 9 (:DEFINITION NATP))
 (53 53 (:TYPE-PRESCRIPTION NATP))
 (52 52 (:TYPE-PRESCRIPTION NAT-LISTP))
 (45 45 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (44 44 (:REWRITE DEFAULT-COERCE-2))
 (44 44 (:REWRITE DEFAULT-COERCE-1))
 (40 4 (:DEFINITION UPDATE-NTH))
 (30 10 (:DEFINITION CHARACTER-LISTP))
 (27 27 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (27 9 (:DEFINITION NFIX))
 (27 9 (:DEFINITION BINARY-APPEND))
 (26 26 (:TYPE-PRESCRIPTION NULL))
 (26 26 (:DEFINITION NULL))
 (18 18 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (18 18 (:REWRITE SUBSETP-MEMBER . 2))
 (18 18 (:REWRITE SUBSETP-MEMBER . 1))
 (16 16 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (14 14 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (10 10 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (8 8 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 )
(L4-COLLECT-ALL-INDEX-LISTS
 (199 92 (:REWRITE DEFAULT-+-2))
 (153 13 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (129 92 (:REWRITE DEFAULT-+-1))
 (72 18 (:DEFINITION INTEGER-ABS))
 (72 9 (:REWRITE LENGTH-WHEN-STRINGP))
 (51 51 (:REWRITE DEFAULT-CAR))
 (45 9 (:DEFINITION LEN))
 (33 15 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (31 23 (:REWRITE DEFAULT-<-2))
 (29 1 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (27 23 (:REWRITE DEFAULT-<-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))
 (5 1 (:DEFINITION BINARY-APPEND))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 )
(L4-COLLECT-ALL-INDEX-LISTS-CORRECTNESS-1
 (162 18 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (108 18 (:DEFINITION STRING-LISTP))
 (99 9 (:DEFINITION TRUE-LISTP))
 (90 90 (:TYPE-PRESCRIPTION STRING-LISTP))
 (67 66 (:REWRITE DEFAULT-CDR))
 (65 64 (:REWRITE DEFAULT-CAR))
 (35 13 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (15 3 (:DEFINITION BINARY-APPEND))
 )
(L4-COLLECT-ALL-INDEX-LISTS-CORRECTNESS-2
 (57 9 (:DEFINITION BINARY-APPEND))
 (54 54 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (53 53 (:REWRITE DEFAULT-CAR))
 (45 45 (:REWRITE DEFAULT-CDR))
 (40 10 (:REWRITE FLATTEN-WHEN-NOT-CONSP))
 (35 13 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (24 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(L4-COLLECT-ALL-INDEX-LISTS-CORRECTNESS-3
 (124 4 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (72 4 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (68 4 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (56 4 (:DEFINITION L3-FS-P))
 (50 2 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (30 1 (:DEFINITION NO-DUPLICATES-LISTP))
 (27 27 (:REWRITE DEFAULT-CDR))
 (25 25 (:REWRITE DEFAULT-CAR))
 (24 4 (:DEFINITION BINARY-APPEND))
 (22 2 (:DEFINITION MEMBER-EQUAL))
 (16 16 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (16 4 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (8 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (4 4 (:REWRITE SUBSETP-MEMBER . 4))
 (4 4 (:REWRITE SUBSETP-MEMBER . 3))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (2 2 (:TYPE-PRESCRIPTION L4-LIST-ALL-INDICES))
 )
(INDICES-MARKED-LISTP)
(INDICES-MARKED-P-OF-FLATTEN
 (1819 62 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1080 31 (:DEFINITION NTH))
 (522 93 (:REWRITE ZP-OPEN))
 (522 62 (:REWRITE NFIX-WHEN-ZP))
 (372 372 (:TYPE-PRESCRIPTION LEN))
 (341 279 (:REWRITE DEFAULT-<-2))
 (310 62 (:DEFINITION LEN))
 (279 279 (:REWRITE DEFAULT-<-1))
 (199 62 (:REWRITE NFIX-WHEN-NATP))
 (169 169 (:REWRITE DEFAULT-CDR))
 (155 93 (:REWRITE DEFAULT-+-2))
 (154 17 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (106 31 (:DEFINITION NATP))
 (105 18 (:DEFINITION STRING-LISTP))
 (97 97 (:REWRITE DEFAULT-CAR))
 (93 93 (:REWRITE DEFAULT-+-1))
 (93 31 (:DEFINITION NFIX))
 (83 83 (:TYPE-PRESCRIPTION STRING-LISTP))
 (62 62 (:TYPE-PRESCRIPTION ZP))
 (62 62 (:TYPE-PRESCRIPTION NFIX))
 (62 62 (:LINEAR POSITION-WHEN-MEMBER))
 (62 62 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (31 31 (:TYPE-PRESCRIPTION NATP))
 (13 13 (:REWRITE FLATTEN-WHEN-NOT-CONSP))
 (3 1 (:DEFINITION BINARY-APPEND))
 )
(L4-INDICES-MARKED-P-OF-LIST-ALL-INDICES
 (148 2 (:DEFINITION INDICES-MARKED-P))
 (122 4 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (95 3 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (79 1 (:DEFINITION INDICES-MARKED-LISTP))
 (72 2 (:DEFINITION NTH))
 (54 3 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (51 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (42 3 (:DEFINITION L3-FS-P))
 (36 6 (:REWRITE ZP-OPEN))
 (36 4 (:REWRITE NFIX-WHEN-ZP))
 (24 24 (:TYPE-PRESCRIPTION LEN))
 (24 24 (:REWRITE DEFAULT-CDR))
 (22 18 (:REWRITE DEFAULT-<-2))
 (20 20 (:REWRITE DEFAULT-CAR))
 (20 4 (:DEFINITION LEN))
 (19 3 (:DEFINITION BINARY-APPEND))
 (18 18 (:REWRITE DEFAULT-<-1))
 (14 4 (:REWRITE NFIX-WHEN-NATP))
 (12 12 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (10 6 (:REWRITE DEFAULT-+-2))
 (8 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (8 2 (:DEFINITION NATP))
 (6 6 (:TYPE-PRESCRIPTION L4-LIST-ALL-INDICES))
 (6 6 (:REWRITE DEFAULT-+-1))
 (6 2 (:DEFINITION NFIX))
 (4 4 (:TYPE-PRESCRIPTION ZP))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:LINEAR POSITION-WHEN-MEMBER))
 (4 4 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 )
(INDICES-MARKED-LISTP-OF-BINARY-APPEND
 (1737 58 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1028 29 (:DEFINITION NTH))
 (506 87 (:REWRITE ZP-OPEN))
 (506 58 (:REWRITE NFIX-WHEN-ZP))
 (348 348 (:TYPE-PRESCRIPTION LEN))
 (319 261 (:REWRITE DEFAULT-<-2))
 (290 58 (:DEFINITION LEN))
 (261 261 (:REWRITE DEFAULT-<-1))
 (228 173 (:REWRITE DEFAULT-CDR))
 (195 58 (:REWRITE NFIX-WHEN-NATP))
 (184 92 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (177 119 (:REWRITE DEFAULT-CAR))
 (168 17 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (145 87 (:REWRITE DEFAULT-+-2))
 (121 20 (:DEFINITION STRING-LISTP))
 (108 29 (:DEFINITION NATP))
 (92 92 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (87 87 (:TYPE-PRESCRIPTION STRING-LISTP))
 (87 87 (:REWRITE DEFAULT-+-1))
 (87 29 (:DEFINITION NFIX))
 (58 58 (:TYPE-PRESCRIPTION ZP))
 (58 58 (:TYPE-PRESCRIPTION NFIX))
 (58 58 (:LINEAR POSITION-WHEN-MEMBER))
 (58 58 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (29 29 (:TYPE-PRESCRIPTION NATP))
 (21 21 (:REWRITE CONSP-OF-APPEND))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-1
 (1435 68 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (1204 77 (:DEFINITION L3-FS-P))
 (987 329 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (707 406 (:REWRITE DEFAULT-CDR))
 (616 616 (:TYPE-PRESCRIPTION L3-FS-P))
 (385 383 (:REWRITE DEFAULT-CAR))
 (165 33 (:DEFINITION BINARY-APPEND))
 (153 9 (:REWRITE L3-FS-P-ASSOC))
 (114 6 (:DEFINITION MEMBER-INTERSECTP-EQUAL))
 (60 60 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (60 60 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (60 60 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (60 60 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (60 60 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (60 60 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (60 60 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (48 12 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (18 18 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (12 12 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-2
 (6193 85 (:DEFINITION INDICES-MARKED-P))
 (5173 170 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (4950 1650 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (3054 85 (:DEFINITION NTH))
 (1524 255 (:REWRITE ZP-OPEN))
 (1524 170 (:REWRITE NFIX-WHEN-ZP))
 (1069 869 (:REWRITE DEFAULT-CDR))
 (935 765 (:REWRITE DEFAULT-<-2))
 (931 929 (:REWRITE DEFAULT-CAR))
 (850 170 (:DEFINITION LEN))
 (765 765 (:REWRITE DEFAULT-<-1))
 (592 170 (:REWRITE NFIX-WHEN-NATP))
 (425 255 (:REWRITE DEFAULT-+-2))
 (337 85 (:DEFINITION NATP))
 (260 52 (:DEFINITION BINARY-APPEND))
 (255 255 (:REWRITE DEFAULT-+-1))
 (255 85 (:DEFINITION NFIX))
 (170 170 (:TYPE-PRESCRIPTION NFIX))
 (170 170 (:LINEAR POSITION-WHEN-MEMBER))
 (170 170 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (143 49 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (115 37 (:REWRITE L3-FS-P-ASSOC))
 (85 85 (:TYPE-PRESCRIPTION NATP))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-3
 (4950 1650 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (2040 85 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (984 784 (:REWRITE DEFAULT-CDR))
 (935 85 (:DEFINITION MEMBER-EQUAL))
 (931 929 (:REWRITE DEFAULT-CAR))
 (680 170 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (260 52 (:DEFINITION BINARY-APPEND))
 (170 170 (:REWRITE SUBSETP-MEMBER . 4))
 (170 170 (:REWRITE SUBSETP-MEMBER . 3))
 (170 170 (:REWRITE SUBSETP-MEMBER . 2))
 (170 170 (:REWRITE SUBSETP-MEMBER . 1))
 (143 49 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (115 37 (:REWRITE L3-FS-P-ASSOC))
 (85 85 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-4
 (360 4 (:DEFINITION INTERSECTP-EQUAL))
 (230 11 (:DEFINITION SUBSETP-EQUAL))
 (222 21 (:DEFINITION MEMBER-EQUAL))
 (200 8 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (148 8 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (124 8 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (85 85 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (56 56 (:REWRITE DEFAULT-CDR))
 (55 55 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (54 54 (:REWRITE DEFAULT-CAR))
 (48 6 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (44 44 (:REWRITE SUBSETP-MEMBER . 2))
 (44 44 (:REWRITE SUBSETP-MEMBER . 1))
 (40 40 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (32 8 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (22 22 (:REWRITE SUBSETP-TRANS2))
 (22 22 (:REWRITE SUBSETP-TRANS))
 (20 4 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (8 8 (:REWRITE SUBSETP-MEMBER . 4))
 (8 8 (:REWRITE SUBSETP-MEMBER . 3))
 (8 8 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (8 8 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (8 8 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (8 8 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (8 8 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (8 8 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (8 8 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (4 4 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (2 2 (:REWRITE CDR-CONS))
 (2 2 (:REWRITE CAR-CONS))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-5
 (13939 220 (:DEFINITION SUBSETP-EQUAL))
 (12217 403 (:DEFINITION MEMBER-EQUAL))
 (11360 86 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (3869 43 (:DEFINITION INTERSECTP-EQUAL))
 (3082 3082 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (2532 8 (:REWRITE SUBSETP-APPEND1))
 (2392 2319 (:REWRITE DEFAULT-CAR))
 (2328 90 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (2237 2164 (:REWRITE DEFAULT-CDR))
 (1682 202 (:DEFINITION BINARY-APPEND))
 (1646 1646 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1554 84 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (1365 348 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (1302 84 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (1287 80 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (1124 1124 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (954 842 (:REWRITE SUBSETP-MEMBER . 2))
 (842 842 (:REWRITE SUBSETP-MEMBER . 1))
 (720 456 (:REWRITE SUBSETP-TRANS2))
 (456 456 (:REWRITE SUBSETP-TRANS))
 (420 420 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (387 135 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (314 80 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (276 12 (:REWRITE MEMBER-OF-BINARY-APPEND))
 (154 86 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (126 126 (:TYPE-PRESCRIPTION NULL))
 (126 126 (:DEFINITION NULL))
 (126 86 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (102 86 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (90 90 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (90 90 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (90 90 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (90 90 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (90 90 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (90 90 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (88 88 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (88 88 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (88 88 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (88 88 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (88 88 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (88 88 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (88 88 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (86 86 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (86 86 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (86 86 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (86 86 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (84 84 (:REWRITE SUBSETP-MEMBER . 4))
 (84 84 (:REWRITE SUBSETP-MEMBER . 3))
 (81 31 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-6
 (26165 388 (:DEFINITION SUBSETP-EQUAL))
 (21400 657 (:DEFINITION MEMBER-EQUAL))
 (20643 83 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (5069 83 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (3933 3789 (:REWRITE DEFAULT-CAR))
 (3728 3584 (:REWRITE DEFAULT-CDR))
 (3443 16 (:REWRITE SUBSETP-APPEND1))
 (3039 355 (:DEFINITION BINARY-APPEND))
 (2570 656 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (2070 80 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (1973 1973 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (1594 1354 (:REWRITE SUBSETP-MEMBER . 2))
 (1480 80 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (1356 808 (:REWRITE SUBSETP-TRANS2))
 (1354 1354 (:REWRITE SUBSETP-MEMBER . 1))
 (1240 80 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (808 808 (:REWRITE SUBSETP-TRANS))
 (659 231 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (642 24 (:REWRITE MEMBER-OF-BINARY-APPEND))
 (400 400 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (214 214 (:TYPE-PRESCRIPTION NULL))
 (214 214 (:DEFINITION NULL))
 (192 80 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (131 83 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (120 80 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (83 83 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (83 83 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (83 83 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (83 83 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (80 80 (:REWRITE SUBSETP-MEMBER . 4))
 (80 80 (:REWRITE SUBSETP-MEMBER . 3))
 (80 80 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (80 80 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (80 80 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (80 80 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (80 80 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (80 80 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (80 80 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (80 80 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (80 80 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (80 80 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (80 80 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (74 28 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-7
 (305 299 (:REWRITE DEFAULT-CDR))
 (293 290 (:REWRITE DEFAULT-CAR))
 (163 31 (:DEFINITION BINARY-APPEND))
 (74 28 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (59 21 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (41 41 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (41 41 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (41 41 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (41 41 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (41 41 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (41 41 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (41 41 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (38 2 (:DEFINITION MEMBER-INTERSECTP-EQUAL))
 (19 19 (:TYPE-PRESCRIPTION NULL))
 (19 19 (:DEFINITION NULL))
 (16 4 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (16 4 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (4 4 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-8
 (440 40 (:DEFINITION MEMBER-EQUAL))
 (364 361 (:REWRITE DEFAULT-CDR))
 (355 352 (:REWRITE DEFAULT-CAR))
 (320 80 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (144 28 (:DEFINITION BINARY-APPEND))
 (80 80 (:REWRITE SUBSETP-MEMBER . 4))
 (80 80 (:REWRITE SUBSETP-MEMBER . 3))
 (80 80 (:REWRITE SUBSETP-MEMBER . 2))
 (80 80 (:REWRITE SUBSETP-MEMBER . 1))
 (74 28 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (59 21 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (19 19 (:TYPE-PRESCRIPTION NULL))
 (19 19 (:DEFINITION NULL))
 (8 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-9
 (2420 80 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1430 40 (:DEFINITION NTH))
 (710 120 (:REWRITE ZP-OPEN))
 (710 80 (:REWRITE NFIX-WHEN-ZP))
 (480 480 (:TYPE-PRESCRIPTION LEN))
 (440 360 (:REWRITE DEFAULT-<-2))
 (426 423 (:REWRITE DEFAULT-CDR))
 (400 80 (:DEFINITION LEN))
 (377 374 (:REWRITE DEFAULT-CAR))
 (360 360 (:REWRITE DEFAULT-<-1))
 (275 80 (:REWRITE NFIX-WHEN-NATP))
 (200 120 (:REWRITE DEFAULT-+-2))
 (155 40 (:DEFINITION NATP))
 (144 28 (:DEFINITION BINARY-APPEND))
 (120 120 (:REWRITE DEFAULT-+-1))
 (120 40 (:DEFINITION NFIX))
 (80 80 (:TYPE-PRESCRIPTION ZP))
 (80 80 (:TYPE-PRESCRIPTION NFIX))
 (80 80 (:LINEAR POSITION-WHEN-MEMBER))
 (80 80 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (74 28 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (59 21 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (55 11 (:DEFINITION BOOLEAN-LISTP))
 (40 40 (:TYPE-PRESCRIPTION NATP))
 (19 19 (:TYPE-PRESCRIPTION NULL))
 (19 19 (:DEFINITION NULL))
 (8 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-10
 (3000 96 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (2895 965 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1764 48 (:DEFINITION NTH))
 (900 144 (:REWRITE ZP-OPEN))
 (900 96 (:REWRITE NFIX-WHEN-ZP))
 (845 435 (:REWRITE DEFAULT-CDR))
 (533 420 (:REWRITE DEFAULT-CAR))
 (528 432 (:REWRITE DEFAULT-<-2))
 (480 96 (:DEFINITION LEN))
 (432 432 (:REWRITE DEFAULT-<-1))
 (354 96 (:REWRITE NFIX-WHEN-NATP))
 (240 144 (:REWRITE DEFAULT-+-2))
 (210 48 (:DEFINITION NATP))
 (144 144 (:REWRITE DEFAULT-+-1))
 (144 48 (:DEFINITION NFIX))
 (96 96 (:TYPE-PRESCRIPTION NFIX))
 (96 96 (:LINEAR POSITION-WHEN-MEMBER))
 (96 96 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (71 25 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (65 13 (:DEFINITION BOOLEAN-LISTP))
 (57 11 (:REWRITE L3-FS-P-ASSOC))
 (48 48 (:TYPE-PRESCRIPTION NATP))
 (40 8 (:DEFINITION BINARY-APPEND))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-11
 (2103 701 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (771 361 (:REWRITE DEFAULT-CDR))
 (528 48 (:DEFINITION MEMBER-EQUAL))
 (507 394 (:REWRITE DEFAULT-CAR))
 (384 96 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (96 96 (:REWRITE SUBSETP-MEMBER . 4))
 (96 96 (:REWRITE SUBSETP-MEMBER . 3))
 (96 96 (:REWRITE SUBSETP-MEMBER . 2))
 (96 96 (:REWRITE SUBSETP-MEMBER . 1))
 (71 25 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (57 11 (:REWRITE L3-FS-P-ASSOC))
 (40 8 (:DEFINITION BINARY-APPEND))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-12
 (5837 190 (:DEFINITION SUBSETP-EQUAL))
 (3276 1092 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (2294 78 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (1722 57 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (1503 1029 (:REWRITE DEFAULT-CDR))
 (1443 78 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (1272 1095 (:REWRITE DEFAULT-CAR))
 (1209 78 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (1150 78 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (950 950 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (875 78 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (821 54 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (794 794 (:REWRITE SUBSETP-MEMBER . 2))
 (794 794 (:REWRITE SUBSETP-MEMBER . 1))
 (608 22 (:REWRITE MEMBER-OF-BINARY-APPEND))
 (390 390 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (380 380 (:REWRITE SUBSETP-TRANS2))
 (380 380 (:REWRITE SUBSETP-TRANS))
 (158 78 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (120 24 (:DEFINITION BINARY-APPEND))
 (78 78 (:REWRITE SUBSETP-MEMBER . 4))
 (78 78 (:REWRITE SUBSETP-MEMBER . 3))
 (78 78 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (78 78 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (78 78 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (78 78 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (78 78 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (78 78 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (78 78 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (78 78 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (78 78 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (78 78 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (71 25 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (57 57 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (57 11 (:REWRITE L3-FS-P-ASSOC))
 (56 32 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (54 54 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (54 54 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (54 54 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-13
 (2379 793 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1486 44 (:DEFINITION SUBSETP-EQUAL))
 (883 66 (:DEFINITION MEMBER-EQUAL))
 (823 57 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (766 330 (:REWRITE DEFAULT-CDR))
 (597 476 (:REWRITE DEFAULT-CAR))
 (532 51 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (410 410 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (291 56 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (224 56 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (220 220 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (167 51 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (159 51 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (151 151 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (115 115 (:REWRITE SUBSETP-MEMBER . 2))
 (115 115 (:REWRITE SUBSETP-MEMBER . 1))
 (115 51 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (112 8 (:REWRITE MEMBER-OF-BINARY-APPEND))
 (89 17 (:DEFINITION BINARY-APPEND))
 (88 88 (:REWRITE SUBSETP-TRANS2))
 (88 88 (:REWRITE SUBSETP-TRANS))
 (78 28 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (72 12 (:REWRITE L3-FS-P-ASSOC))
 (51 51 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (51 51 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (51 51 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (36 18 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (18 18 (:REWRITE CDR-CONS))
 (18 18 (:REWRITE CAR-CONS))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-14
 (8914 261 (:DEFINITION SUBSETP-EQUAL))
 (7745 489 (:DEFINITION MEMBER-EQUAL))
 (7466 90 (:DEFINITION INTERSECTP-EQUAL))
 (5522 36 (:DEFINITION MEMBER-INTERSECTP-EQUAL))
 (4601 25 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-6))
 (4337 166 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (3161 220 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (3100 158 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (2886 962 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (2754 2206 (:REWRITE DEFAULT-CDR))
 (2626 158 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (2380 2242 (:REWRITE DEFAULT-CAR))
 (1973 1973 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1716 2 (:REWRITE MEMBER-INTERSECTP-BINARY-APPEND . 1))
 (1455 83 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (1385 18 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-5))
 (1317 1317 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (1194 6 (:REWRITE SUBSETP-APPEND1))
 (1073 1 (:REWRITE MEMBER-INTERSECTP-OF-SET-DIFFERENCE$-LEMMA-1))
 (1066 220 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (1063 979 (:REWRITE SUBSETP-MEMBER . 2))
 (1005 133 (:DEFINITION BINARY-APPEND))
 (979 979 (:REWRITE SUBSETP-MEMBER . 1))
 (856 220 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (790 790 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (732 534 (:REWRITE SUBSETP-TRANS2))
 (680 170 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (534 534 (:REWRITE SUBSETP-TRANS))
 (462 81 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (454 220 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (292 1 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-4))
 (220 220 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (220 220 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (166 166 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (166 166 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (166 166 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (166 166 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (166 166 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (166 166 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (164 164 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (164 164 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (164 164 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (164 164 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (164 164 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (164 164 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (164 164 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (158 158 (:REWRITE SUBSETP-MEMBER . 4))
 (158 158 (:REWRITE SUBSETP-MEMBER . 3))
 (126 126 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (117 43 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (81 81 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (78 28 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (72 12 (:REWRITE L3-FS-P-ASSOC))
 (37 37 (:TYPE-PRESCRIPTION NULL))
 (37 37 (:DEFINITION NULL))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-15
 (613 22 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (374 11 (:DEFINITION NTH))
 (264 21 (:DEFINITION MEMBER-EQUAL))
 (235 14 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (195 14 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (176 33 (:REWRITE ZP-OPEN))
 (176 22 (:REWRITE NFIX-WHEN-ZP))
 (118 96 (:REWRITE DEFAULT-<-2))
 (110 22 (:DEFINITION LEN))
 (96 96 (:REWRITE DEFAULT-<-1))
 (92 92 (:REWRITE DEFAULT-CDR))
 (69 69 (:REWRITE DEFAULT-CAR))
 (62 62 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (59 6 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (58 22 (:REWRITE NFIX-WHEN-NATP))
 (55 33 (:REWRITE DEFAULT-+-2))
 (52 46 (:REWRITE SUBSETP-MEMBER . 1))
 (46 46 (:REWRITE SUBSETP-MEMBER . 2))
 (33 33 (:REWRITE DEFAULT-+-1))
 (30 10 (:DEFINITION NATP))
 (27 9 (:DEFINITION NFIX))
 (22 22 (:TYPE-PRESCRIPTION ZP))
 (22 22 (:LINEAR POSITION-WHEN-MEMBER))
 (22 22 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (17 17 (:REWRITE SUBSETP-TRANS2))
 (17 17 (:REWRITE SUBSETP-TRANS))
 (14 1 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
 (10 10 (:REWRITE SUBSETP-MEMBER . 4))
 (10 10 (:REWRITE SUBSETP-MEMBER . 3))
 (10 1 (:DEFINITION NAT-LISTP))
 (9 9 (:TYPE-PRESCRIPTION NATP))
 (7 7 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (6 6 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (6 6 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (6 6 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (6 6 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (6 6 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (6 6 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (6 6 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (6 6 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (6 6 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (6 6 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (6 6 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (2 2 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 )
(LIST-EQUIV-IMPLIES-EQUAL-INDICES-MARKED-P-1
 (456 16 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (272 8 (:DEFINITION NTH))
 (128 24 (:REWRITE ZP-OPEN))
 (128 16 (:REWRITE NFIX-WHEN-ZP))
 (96 96 (:TYPE-PRESCRIPTION LEN))
 (88 72 (:REWRITE DEFAULT-<-2))
 (80 16 (:DEFINITION LEN))
 (72 72 (:REWRITE DEFAULT-<-1))
 (48 16 (:REWRITE NFIX-WHEN-NATP))
 (40 24 (:REWRITE DEFAULT-+-2))
 (36 36 (:REWRITE DEFAULT-CDR))
 (24 24 (:REWRITE DEFAULT-+-1))
 (24 8 (:DEFINITION NFIX))
 (24 8 (:DEFINITION NATP))
 (20 20 (:REWRITE DEFAULT-CAR))
 (16 16 (:TYPE-PRESCRIPTION ZP))
 (16 16 (:TYPE-PRESCRIPTION NFIX))
 (16 16 (:LINEAR POSITION-WHEN-MEMBER))
 (16 16 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (8 8 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 )
(LIST-EQUIV-IMPLIES-EQUAL-FETCH-BLOCKS-BY-INDICES-2
 (570 20 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (340 10 (:DEFINITION NTH))
 (160 30 (:REWRITE ZP-OPEN))
 (160 20 (:REWRITE NFIX-WHEN-ZP))
 (150 30 (:DEFINITION LEN))
 (130 100 (:REWRITE DEFAULT-<-2))
 (110 100 (:REWRITE DEFAULT-<-1))
 (70 40 (:REWRITE DEFAULT-+-2))
 (60 20 (:REWRITE NFIX-WHEN-NATP))
 (56 56 (:REWRITE DEFAULT-CDR))
 (40 40 (:REWRITE DEFAULT-+-1))
 (34 34 (:REWRITE DEFAULT-CAR))
 (30 10 (:DEFINITION NFIX))
 (30 10 (:DEFINITION NATP))
 (20 20 (:TYPE-PRESCRIPTION ZP))
 (20 20 (:TYPE-PRESCRIPTION NFIX))
 (20 20 (:LINEAR POSITION-WHEN-MEMBER))
 (20 20 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (10 10 (:TYPE-PRESCRIPTION NATP))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 )
(LIST-EQUIV-IMPLIES-EQUAL-L4-LIST-ALL-INDICES-1
 (18 2 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (14 2 (:DEFINITION BINARY-APPEND))
 (14 1 (:DEFINITION L3-FS-P))
 (12 12 (:REWRITE DEFAULT-CDR))
 (12 12 (:REWRITE DEFAULT-CAR))
 (8 8 (:TYPE-PRESCRIPTION L3-FS-P))
 (3 3 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 )
(LIST-EQUIV-IMPLIES-EQUAL-L3-TO-L2-FS-1
 (820 10 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (720 10 (:REWRITE DEFAULT-COERCE-3))
 (680 10 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (620 20 (:DEFINITION BLOCK-LISTP))
 (580 10 (:DEFINITION UNMAKE-BLOCKS))
 (570 20 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (450 450 (:TYPE-PRESCRIPTION LEN))
 (350 70 (:DEFINITION LEN))
 (340 10 (:DEFINITION NTH))
 (330 10 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (320 20 (:REWRITE TAKE-OF-LEN-FREE))
 (250 10 (:DEFINITION TAKE))
 (230 230 (:REWRITE DEFAULT-CDR))
 (200 40 (:REWRITE ZP-OPEN))
 (190 110 (:REWRITE DEFAULT-+-2))
 (180 180 (:REWRITE DEFAULT-CAR))
 (160 20 (:REWRITE NFIX-WHEN-ZP))
 (140 110 (:REWRITE DEFAULT-<-2))
 (138 10 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (120 110 (:REWRITE DEFAULT-<-1))
 (120 110 (:REWRITE DEFAULT-+-1))
 (120 20 (:DEFINITION CHARACTER-LISTP))
 (112 8 (:DEFINITION L3-FS-P))
 (100 100 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (100 100 (:TYPE-PRESCRIPTION BLOCK-LISTP))
 (100 100 (:LINEAR POSITION-WHEN-MEMBER))
 (100 100 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (64 64 (:TYPE-PRESCRIPTION L3-FS-P))
 (60 20 (:REWRITE NFIX-WHEN-NATP))
 (40 40 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (40 10 (:REWRITE COMMUTATIVITY-OF-+))
 (30 30 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (30 30 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (30 10 (:DEFINITION NFIX))
 (30 10 (:DEFINITION NATP))
 (30 10 (:DEFINITION BINARY-APPEND))
 (20 20 (:TYPE-PRESCRIPTION ZP))
 (20 20 (:TYPE-PRESCRIPTION NFIX))
 (10 10 (:TYPE-PRESCRIPTION NATP))
 (10 10 (:REWRITE DEFAULT-COERCE-2))
 (3 3 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 )
(LIST-EQUIV-IMPLIES-EQUAL-INDICES-MARKED-P-2
 (570 20 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (160 20 (:REWRITE NFIX-WHEN-ZP))
 (111 91 (:REWRITE DEFAULT-<-2))
 (100 20 (:DEFINITION LEN))
 (91 91 (:REWRITE DEFAULT-<-1))
 (60 20 (:REWRITE NFIX-WHEN-NATP))
 (50 30 (:REWRITE DEFAULT-+-2))
 (35 35 (:REWRITE DEFAULT-CDR))
 (33 11 (:DEFINITION NATP))
 (30 30 (:REWRITE DEFAULT-+-1))
 (30 10 (:DEFINITION NFIX))
 (21 21 (:REWRITE DEFAULT-CAR))
 (20 20 (:TYPE-PRESCRIPTION ZP))
 (20 20 (:LINEAR POSITION-WHEN-MEMBER))
 (20 20 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (14 1 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
 (10 10 (:TYPE-PRESCRIPTION NATP))
 (10 1 (:DEFINITION NAT-LISTP))
 (5 5 (:TYPE-PRESCRIPTION NAT-LISTP))
 (5 5 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (5 5 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (2 2 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 )
(LIST-EQUIV-IMPLIES-LIST-EQUIV-SET-INDICES-IN-ALV-1
 (498 42 (:DEFINITION UPDATE-NTH))
 (326 10 (:REWRITE UPDATE-NTH-OF-UPDATE-NTH-1))
 (284 208 (:REWRITE DEFAULT-<-2))
 (271 175 (:REWRITE DEFAULT-CDR))
 (262 209 (:REWRITE DEFAULT-+-2))
 (209 209 (:REWRITE DEFAULT-+-1))
 (208 208 (:REWRITE DEFAULT-<-1))
 (154 94 (:REWRITE DEFAULT-CAR))
 (136 20 (:REWRITE NFIX-WHEN-ZP))
 (120 54 (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH))
 (118 58 (:TYPE-PRESCRIPTION SET-INDICES))
 (100 20 (:REWRITE NFIX-WHEN-NATP))
 (88 26 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (88 26 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (60 20 (:DEFINITION NFIX))
 (60 20 (:DEFINITION NATP))
 (54 54 (:TYPE-PRESCRIPTION UPDATE-NTH))
 (54 54 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (26 26 (:TYPE-PRESCRIPTION ZP))
 (20 20 (:TYPE-PRESCRIPTION NFIX))
 (20 20 (:TYPE-PRESCRIPTION NATP))
 (20 16 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-MAKE-LIST-AC))
 (16 16 (:TYPE-PRESCRIPTION MAKE-LIST-AC))
 (3 3 (:LINEAR POSITION-WHEN-MEMBER))
 (3 3 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-17
 (1303 40 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (320 40 (:REWRITE NFIX-WHEN-ZP))
 (306 33 (:DEFINITION MEMBER-EQUAL))
 (301 57 (:DEFINITION LEN))
 (282 234 (:REWRITE DEFAULT-<-2))
 (270 27 (:DEFINITION NAT-LISTP))
 (248 8 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-2))
 (234 234 (:REWRITE DEFAULT-<-1))
 (205 205 (:REWRITE DEFAULT-CDR))
 (195 28 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (187 187 (:REWRITE DEFAULT-CAR))
 (134 77 (:REWRITE DEFAULT-+-2))
 (127 14 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (104 8 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-3))
 (97 10 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (84 40 (:REWRITE NFIX-WHEN-NATP))
 (82 5 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
 (77 77 (:REWRITE DEFAULT-+-1))
 (69 69 (:REWRITE SUBSETP-MEMBER . 2))
 (69 69 (:REWRITE SUBSETP-MEMBER . 1))
 (53 53 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (48 48 (:LINEAR POSITION-WHEN-MEMBER))
 (48 48 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (45 9 (:DEFINITION BOOLEAN-LISTP))
 (44 44 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (40 40 (:TYPE-PRESCRIPTION ZP))
 (34 34 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (34 10 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (33 11 (:DEFINITION NFIX))
 (27 27 (:REWRITE SUBSETP-TRANS2))
 (27 27 (:REWRITE SUBSETP-TRANS))
 (19 19 (:TYPE-PRESCRIPTION NATP))
 (14 14 (:REWRITE SUBSETP-MEMBER . 4))
 (14 14 (:REWRITE SUBSETP-MEMBER . 3))
 (11 11 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (10 10 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (10 10 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (10 10 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (10 10 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (10 10 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (10 10 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (10 10 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (10 10 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (10 10 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (10 10 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (10 10 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-19
 (2937 30 (:DEFINITION INDICES-MARKED-P))
 (2181 60 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1096 30 (:DEFINITION NTH))
 (534 90 (:REWRITE ZP-OPEN))
 (534 60 (:REWRITE NFIX-WHEN-ZP))
 (449 449 (:TYPE-PRESCRIPTION LEN))
 (405 334 (:REWRITE DEFAULT-<-2))
 (382 72 (:DEFINITION LEN))
 (341 11 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-2))
 (334 334 (:REWRITE DEFAULT-<-1))
 (309 83 (:DEFINITION NATP))
 (305 31 (:DEFINITION NAT-LISTP))
 (298 295 (:REWRITE DEFAULT-CDR))
 (253 250 (:REWRITE DEFAULT-CAR))
 (242 11 (:DEFINITION BOUNDED-NAT-LISTP))
 (207 60 (:REWRITE NFIX-WHEN-NATP))
 (174 102 (:REWRITE DEFAULT-+-2))
 (143 11 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-3))
 (102 102 (:REWRITE DEFAULT-+-1))
 (90 30 (:DEFINITION NFIX))
 (88 11 (:DEFINITION MEMBER-EQUAL))
 (71 71 (:LINEAR POSITION-WHEN-MEMBER))
 (71 71 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (66 11 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-4))
 (62 62 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (60 60 (:TYPE-PRESCRIPTION ZP))
 (60 60 (:TYPE-PRESCRIPTION NFIX))
 (55 55 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (53 19 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (45 9 (:DEFINITION BOOLEAN-LISTP))
 (45 9 (:DEFINITION BINARY-APPEND))
 (44 44 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (41 41 (:TYPE-PRESCRIPTION NATP))
 (22 22 (:REWRITE SUBSETP-MEMBER . 2))
 (22 22 (:REWRITE SUBSETP-MEMBER . 1))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-20
 (15635 243 (:DEFINITION SUBSETP-EQUAL))
 (14117 188 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (12039 411 (:DEFINITION MEMBER-EQUAL))
 (6111 2037 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (4093 4093 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (3464 14 (:REWRITE SUBSETP-APPEND1))
 (2975 1959 (:REWRITE DEFAULT-CDR))
 (2886 166 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (2513 2388 (:REWRITE DEFAULT-CAR))
 (1552 200 (:DEFINITION BINARY-APPEND))
 (1468 1468 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1257 1257 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (1139 296 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (1002 806 (:REWRITE SUBSETP-MEMBER . 2))
 (976 514 (:REWRITE SUBSETP-TRANS2))
 (806 806 (:REWRITE SUBSETP-MEMBER . 1))
 (664 166 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (514 514 (:REWRITE SUBSETP-TRANS))
 (460 20 (:REWRITE MEMBER-OF-BINARY-APPEND))
 (143 49 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (139 139 (:REWRITE CDR-CONS))
 (139 139 (:REWRITE CAR-CONS))
 (115 37 (:REWRITE L3-FS-P-ASSOC))
 (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))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-21
 (1197 42 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1190 5 (:DEFINITION INTERSECTP-EQUAL))
 (1134 16 (:DEFINITION INDICES-MARKED-P))
 (714 21 (:DEFINITION NTH))
 (592 27 (:DEFINITION SUBSETP-EQUAL))
 (514 18 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (400 39 (:DEFINITION MEMBER-EQUAL))
 (336 63 (:REWRITE ZP-OPEN))
 (336 42 (:REWRITE NFIX-WHEN-ZP))
 (335 5 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-5))
 (252 252 (:TYPE-PRESCRIPTION LEN))
 (237 195 (:REWRITE DEFAULT-<-2))
 (210 42 (:DEFINITION LEN))
 (195 195 (:REWRITE DEFAULT-<-1))
 (185 10 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (183 183 (:REWRITE DEFAULT-CDR))
 (155 10 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (152 152 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (148 148 (:REWRITE DEFAULT-CAR))
 (132 132 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (126 42 (:REWRITE NFIX-WHEN-NATP))
 (107 107 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (105 63 (:REWRITE DEFAULT-+-2))
 (76 76 (:REWRITE SUBSETP-MEMBER . 2))
 (76 76 (:REWRITE SUBSETP-MEMBER . 1))
 (63 63 (:REWRITE DEFAULT-+-1))
 (63 21 (:DEFINITION NFIX))
 (60 7 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (58 18 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (54 54 (:REWRITE SUBSETP-TRANS2))
 (54 54 (:REWRITE SUBSETP-TRANS))
 (50 50 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (50 18 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (45 7 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (42 42 (:TYPE-PRESCRIPTION ZP))
 (42 42 (:TYPE-PRESCRIPTION NFIX))
 (42 42 (:LINEAR POSITION-WHEN-MEMBER))
 (42 42 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (38 18 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (34 18 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (30 6 (:DEFINITION BOOLEAN-LISTP))
 (28 7 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (21 21 (:TYPE-PRESCRIPTION NATP))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (18 18 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (10 10 (:REWRITE SUBSETP-MEMBER . 4))
 (10 10 (:REWRITE SUBSETP-MEMBER . 3))
 (7 7 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (7 7 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (7 7 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (7 7 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (1 1 (:REWRITE CDR-CONS))
 (1 1 (:REWRITE CAR-CONS))
 )
(LIST-EQUIV-IMPLIES-EQUAL-INDICES-MARKED-LISTP-2
 (570 20 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (340 10 (:DEFINITION NTH))
 (160 30 (:REWRITE ZP-OPEN))
 (160 20 (:REWRITE NFIX-WHEN-ZP))
 (120 120 (:TYPE-PRESCRIPTION LEN))
 (110 90 (:REWRITE DEFAULT-<-2))
 (100 20 (:DEFINITION LEN))
 (90 90 (:REWRITE DEFAULT-<-1))
 (60 20 (:REWRITE NFIX-WHEN-NATP))
 (50 30 (:REWRITE DEFAULT-+-2))
 (44 44 (:REWRITE DEFAULT-CDR))
 (30 30 (:REWRITE DEFAULT-CAR))
 (30 30 (:REWRITE DEFAULT-+-1))
 (30 10 (:DEFINITION NFIX))
 (30 10 (:DEFINITION NATP))
 (20 20 (:TYPE-PRESCRIPTION ZP))
 (20 20 (:TYPE-PRESCRIPTION NFIX))
 (20 20 (:LINEAR POSITION-WHEN-MEMBER))
 (20 20 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (10 10 (:TYPE-PRESCRIPTION NATP))
 (5 5 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (5 5 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-22
 (2661 28 (:DEFINITION INDICES-MARKED-P))
 (1893 56 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1620 18 (:DEFINITION INTERSECTP-EQUAL))
 (970 28 (:DEFINITION NTH))
 (948 87 (:DEFINITION MEMBER-EQUAL))
 (900 36 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (840 42 (:DEFINITION SUBSETP-EQUAL))
 (666 36 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (604 604 (:REWRITE DEFAULT-CDR))
 (576 110 (:DEFINITION LEN))
 (558 36 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (512 512 (:REWRITE DEFAULT-CAR))
 (502 391 (:REWRITE DEFAULT-<-2))
 (448 84 (:REWRITE ZP-OPEN))
 (448 56 (:REWRITE NFIX-WHEN-ZP))
 (403 117 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (403 13 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-2))
 (391 391 (:REWRITE DEFAULT-<-1))
 (288 32 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (248 138 (:REWRITE DEFAULT-+-2))
 (210 210 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (192 192 (:REWRITE SUBSETP-MEMBER . 2))
 (192 192 (:REWRITE SUBSETP-MEMBER . 1))
 (192 32 (:DEFINITION STRING-LISTP))
 (180 180 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (180 36 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (176 16 (:DEFINITION TRUE-LISTP))
 (168 56 (:REWRITE NFIX-WHEN-NATP))
 (160 160 (:TYPE-PRESCRIPTION STRING-LISTP))
 (138 138 (:REWRITE DEFAULT-+-1))
 (117 9 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-3))
 (84 84 (:REWRITE SUBSETP-TRANS2))
 (84 84 (:REWRITE SUBSETP-TRANS))
 (84 28 (:DEFINITION NFIX))
 (81 81 (:LINEAR POSITION-WHEN-MEMBER))
 (81 81 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (57 19 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (56 56 (:TYPE-PRESCRIPTION ZP))
 (56 56 (:TYPE-PRESCRIPTION NFIX))
 (45 9 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-4))
 (44 44 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (40 40 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (38 38 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (37 37 (:TYPE-PRESCRIPTION NATP))
 (36 36 (:REWRITE SUBSETP-MEMBER . 4))
 (36 36 (:REWRITE SUBSETP-MEMBER . 3))
 (36 36 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (36 36 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (36 36 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (36 36 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (36 36 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (36 36 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (36 36 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (36 36 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (36 36 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (36 36 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (36 36 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (36 36 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (21 21 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (21 21 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (21 21 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (21 21 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (21 21 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (21 21 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (21 21 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (21 7 (:DEFINITION BINARY-APPEND))
 (19 19 (:REWRITE FLATTEN-WHEN-NOT-CONSP))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-24
 (893 794 (:REWRITE DEFAULT-CAR))
 (886 643 (:REWRITE DEFAULT-CDR))
 (720 240 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (390 78 (:DEFINITION LEN))
 (385 161 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (224 28 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-3))
 (222 148 (:REWRITE DEFAULT-<-2))
 (174 174 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (156 78 (:REWRITE DEFAULT-+-2))
 (148 148 (:REWRITE DEFAULT-<-1))
 (90 26 (:DEFINITION BINARY-APPEND))
 (85 5 (:REWRITE L3-FS-P-ASSOC))
 (78 78 (:REWRITE DEFAULT-+-1))
 (56 56 (:TYPE-PRESCRIPTION L3-BOUNDED-FS-P))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-25
 (1570 22 (:DEFINITION INDICES-MARKED-P))
 (1306 44 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (774 22 (:DEFINITION NTH))
 (418 412 (:REWRITE DEFAULT-CDR))
 (378 66 (:REWRITE ZP-OPEN))
 (378 44 (:REWRITE NFIX-WHEN-ZP))
 (375 369 (:REWRITE DEFAULT-CAR))
 (269 216 (:REWRITE DEFAULT-<-2))
 (265 53 (:DEFINITION LEN))
 (216 216 (:REWRITE DEFAULT-<-1))
 (175 33 (:DEFINITION BINARY-APPEND))
 (156 70 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (145 44 (:REWRITE NFIX-WHEN-NATP))
 (128 75 (:REWRITE DEFAULT-+-2))
 (75 75 (:REWRITE DEFAULT-+-1))
 (66 22 (:DEFINITION NFIX))
 (44 44 (:TYPE-PRESCRIPTION ZP))
 (44 44 (:TYPE-PRESCRIPTION NFIX))
 (44 44 (:LINEAR POSITION-WHEN-MEMBER))
 (44 44 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (32 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (22 22 (:TYPE-PRESCRIPTION NATP))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-26
 (34546 711 (:DEFINITION SUBSETP-EQUAL))
 (27506 1199 (:DEFINITION MEMBER-EQUAL))
 (25082 192 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (8266 192 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (7732 85 (:DEFINITION INTERSECTP-EQUAL))
 (6972 2324 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (6176 4543 (:REWRITE DEFAULT-CDR))
 (5060 28 (:REWRITE SUBSETP-APPEND1))
 (4962 4733 (:REWRITE DEFAULT-CAR))
 (4931 4931 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (4414 170 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (3633 3633 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (3145 170 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (2865 2473 (:REWRITE SUBSETP-MEMBER . 2))
 (2655 327 (:DEFINITION BINARY-APPEND))
 (2635 170 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (2473 2473 (:REWRITE SUBSETP-MEMBER . 1))
 (2402 1478 (:REWRITE SUBSETP-TRANS2))
 (2110 550 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (1478 1478 (:REWRITE SUBSETP-TRANS))
 (1070 40 (:REWRITE MEMBER-OF-BINARY-APPEND))
 (850 850 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (400 192 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (218 170 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (192 192 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (192 192 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (192 192 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (192 192 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (170 170 (:REWRITE SUBSETP-MEMBER . 4))
 (170 170 (:REWRITE SUBSETP-MEMBER . 3))
 (170 170 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (170 170 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (170 170 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (170 170 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (170 170 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (170 170 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (170 170 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (170 170 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (170 170 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (170 170 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (170 170 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (170 170 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (143 49 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (115 37 (:REWRITE L3-FS-P-ASSOC))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-27
 (4700 156 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (3573 1623 (:REWRITE DEFAULT-CDR))
 (2844 78 (:DEFINITION NTH))
 (2302 25 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (2046 682 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (2032 1579 (:REWRITE DEFAULT-CAR))
 (1957 460 (:REWRITE ZP-OPEN))
 (1633 53 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (1620 165 (:REWRITE NFIX-WHEN-ZP))
 (1619 21 (:DEFINITION INDICES-MARKED-LISTP))
 (1576 25 (:DEFINITION UNMAKE-BLOCKS))
 (1434 107 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (1320 986 (:REWRITE DEFAULT-<-2))
 (1308 90 (:DEFINITION L3-FS-P))
 (1170 104 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1058 606 (:REWRITE DEFAULT-+-2))
 (1053 9 (:DEFINITION SET-INDICES))
 (1024 986 (:REWRITE DEFAULT-<-1))
 (954 53 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (926 50 (:REWRITE TAKE-OF-LEN-FREE))
 (807 14 (:DEFINITION SUBSETP-EQUAL))
 (784 39 (:DEFINITION MEMBER-EQUAL))
 (700 25 (:DEFINITION TAKE))
 (648 606 (:REWRITE DEFAULT-+-1))
 (600 120 (:DEFINITION ASSOC-EQUAL))
 (600 22 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (435 113 (:DEFINITION NATP))
 (376 78 (:DEFINITION BINARY-APPEND))
 (343 343 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (324 36 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (312 104 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (302 302 (:LINEAR POSITION-WHEN-MEMBER))
 (302 302 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (289 25 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (252 18 (:DEFINITION BOUNDED-NAT-LISTP))
 (234 78 (:DEFINITION NFIX))
 (221 17 (:DEFINITION COUNT-FREE-BLOCKS))
 (216 72 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (200 8 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (182 182 (:TYPE-PRESCRIPTION NATP))
 (170 17 (:DEFINITION NAT-LISTP))
 (168 42 (:REWRITE COMMUTATIVITY-OF-+))
 (156 156 (:TYPE-PRESCRIPTION NFIX))
 (144 18 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (115 22 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (104 104 (:REWRITE DEFAULT-COERCE-2))
 (104 104 (:REWRITE DEFAULT-COERCE-1))
 (90 9 (:DEFINITION UPDATE-NTH))
 (78 78 (:REWRITE SUBSETP-MEMBER . 2))
 (78 78 (:REWRITE SUBSETP-MEMBER . 1))
 (75 75 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (72 72 (:TYPE-PRESCRIPTION NULL))
 (72 72 (:DEFINITION NULL))
 (72 18 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (70 70 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (57 19 (:DEFINITION CHARACTER-LISTP))
 (50 50 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (34 34 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (34 34 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (34 34 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (28 28 (:REWRITE SUBSETP-TRANS2))
 (28 28 (:REWRITE SUBSETP-TRANS))
 (22 22 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (22 22 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (22 22 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (22 22 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (22 22 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (18 18 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (8 8 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (8 8 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (3 3 (:REWRITE CDR-CONS))
 (3 3 (:REWRITE CAR-CONS))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-28
 (10354 16 (:DEFINITION L4-WRCHS))
 (4195 142 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (3942 1606 (:REWRITE DEFAULT-CDR))
 (3744 128 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (3264 96 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (2544 71 (:DEFINITION NTH))
 (2194 1394 (:REWRITE DEFAULT-CAR))
 (1986 501 (:REWRITE ZP-OPEN))
 (1872 16 (:DEFINITION SET-INDICES))
 (1586 158 (:REWRITE NFIX-WHEN-ZP))
 (1568 128 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1472 16 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1418 1030 (:REWRITE DEFAULT-<-2))
 (1363 47 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (1315 96 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (1062 1030 (:REWRITE DEFAULT-<-1))
 (1009 572 (:REWRITE DEFAULT-+-2))
 (994 16 (:DEFINITION UNMAKE-BLOCKS))
 (846 47 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (752 16 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-2))
 (604 572 (:REWRITE DEFAULT-+-1))
 (578 32 (:REWRITE TAKE-OF-LEN-FREE))
 (576 64 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (523 158 (:REWRITE NFIX-WHEN-NATP))
 (448 16 (:DEFINITION TAKE))
 (404 348 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (396 44 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (384 128 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (384 128 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (384 128 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (368 368 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (366 366 (:TYPE-PRESCRIPTION ZP))
 (293 29 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (292 66 (:DEFINITION BINARY-APPEND))
 (288 144 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (264 44 (:DEFINITION STRING-LISTP))
 (263 112 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (260 260 (:LINEAR POSITION-WHEN-MEMBER))
 (260 260 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (256 32 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (242 22 (:DEFINITION TRUE-LISTP))
 (236 12 (:DEFINITION SUBSETP-EQUAL))
 (224 224 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (224 224 (:TYPE-PRESCRIPTION COUNT-FREE-BLOCKS))
 (220 220 (:TYPE-PRESCRIPTION STRING-LISTP))
 (219 28 (:DEFINITION MEMBER-EQUAL))
 (213 71 (:DEFINITION NFIX))
 (208 16 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (208 16 (:DEFINITION COUNT-FREE-BLOCKS))
 (199 199 (:TYPE-PRESCRIPTION NATP))
 (176 16 (:REWRITE L3-FS-P-ASSOC))
 (176 16 (:DEFINITION MIN))
 (160 160 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (160 32 (:DEFINITION ASSOC-EQUAL))
 (160 16 (:DEFINITION UPDATE-NTH))
 (148 37 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (142 142 (:TYPE-PRESCRIPTION NFIX))
 (128 128 (:TYPE-PRESCRIPTION NULL))
 (128 128 (:REWRITE DEFAULT-COERCE-2))
 (128 128 (:REWRITE DEFAULT-COERCE-1))
 (128 128 (:DEFINITION NULL))
 (128 32 (:REWRITE COMMUTATIVITY-OF-+))
 (119 51 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (100 10 (:DEFINITION NAT-LISTP))
 (64 64 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (60 60 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (57 37 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (55 55 (:REWRITE SUBSETP-MEMBER . 2))
 (55 55 (:REWRITE SUBSETP-MEMBER . 1))
 (51 17 (:DEFINITION CHARACTER-LISTP))
 (48 48 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (37 37 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (32 32 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (32 32 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (32 32 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (32 32 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (29 29 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (29 29 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (29 29 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (29 29 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (29 29 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (29 29 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (24 24 (:REWRITE SUBSETP-TRANS2))
 (24 24 (:REWRITE SUBSETP-TRANS))
 (22 22 (:REWRITE FLATTEN-WHEN-NOT-CONSP))
 (20 20 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-30
 (10703 106 (:DEFINITION SUBSETP-EQUAL))
 (9447 192 (:DEFINITION MEMBER-EQUAL))
 (8430 26 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-5))
 (8120 264 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (3944 219 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (3332 3176 (:REWRITE DEFAULT-CDR))
 (3204 1068 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (2940 392 (:DEFINITION BINARY-APPEND))
 (2809 228 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (1960 490 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (710 228 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (586 586 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (530 530 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (441 12 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-6))
 (436 228 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (356 356 (:REWRITE SUBSETP-MEMBER . 2))
 (356 356 (:REWRITE SUBSETP-MEMBER . 1))
 (315 109 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (258 94 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (228 228 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (228 228 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (228 228 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (219 219 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (212 212 (:REWRITE SUBSETP-TRANS2))
 (212 212 (:REWRITE SUBSETP-TRANS))
 (169 169 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (128 2 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-4))
 (122 16 (:REWRITE L3-FS-P-ASSOC))
 (106 10 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (103 103 (:TYPE-PRESCRIPTION NULL))
 (103 103 (:DEFINITION NULL))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-31
 (1200 5 (:DEFINITION L3-FS-P))
 (1091 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (644 7 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (643 57 (:DEFINITION LEN))
 (528 16 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (434 7 (:DEFINITION UNMAKE-BLOCKS))
 (420 216 (:REWRITE DEFAULT-CDR))
 (316 8 (:DEFINITION NTH))
 (315 105 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (280 14 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (266 14 (:REWRITE TAKE-OF-LEN-FREE))
 (236 53 (:REWRITE ZP-OPEN))
 (230 10 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (199 196 (:REWRITE DEFAULT-CAR))
 (196 7 (:DEFINITION TAKE))
 (191 17 (:REWRITE NFIX-WHEN-ZP))
 (166 125 (:REWRITE DEFAULT-<-2))
 (152 29 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (149 90 (:REWRITE DEFAULT-+-2))
 (134 125 (:REWRITE DEFAULT-<-1))
 (130 26 (:DEFINITION ASSOC-EQUAL))
 (122 12 (:DEFINITION NAT-LISTP))
 (105 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (104 1 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (92 90 (:REWRITE DEFAULT-+-1))
 (92 1 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (77 1 (:DEFINITION INDICES-MARKED-LISTP))
 (71 1 (:DEFINITION INDICES-MARKED-P))
 (70 14 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (46 46 (:LINEAR POSITION-WHEN-MEMBER))
 (46 46 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (44 44 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (29 9 (:REWRITE COMMUTATIVITY-OF-+))
 (26 8 (:DEFINITION BINARY-APPEND))
 (26 2 (:DEFINITION COUNT-FREE-BLOCKS))
 (24 24 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (24 8 (:DEFINITION NFIX))
 (16 16 (:TYPE-PRESCRIPTION NFIX))
 (15 15 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (15 1 (:DEFINITION BLOCK-LISTP))
 (14 14 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (14 14 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (14 14 (:REWRITE DEFAULT-COERCE-2))
 (14 14 (:REWRITE DEFAULT-COERCE-1))
 (11 11 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (8 8 (:TYPE-PRESCRIPTION NATP))
 (8 8 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (7 7 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 5 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (5 1 (:DEFINITION BOOLEAN-LISTP))
 (4 4 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (3 1 (:DEFINITION CHARACTER-LISTP))
 (1 1 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-32
 (426 4 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (368 4 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (327 10 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (259 128 (:REWRITE DEFAULT-CDR))
 (232 4 (:DEFINITION UNMAKE-BLOCKS))
 (196 5 (:DEFINITION NTH))
 (174 58 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (134 31 (:REWRITE ZP-OPEN))
 (130 129 (:REWRITE DEFAULT-CAR))
 (128 8 (:REWRITE TAKE-OF-LEN-FREE))
 (112 4 (:DEFINITION TAKE))
 (106 10 (:REWRITE NFIX-WHEN-ZP))
 (100 20 (:DEFINITION ASSOC-EQUAL))
 (94 56 (:REWRITE DEFAULT-+-2))
 (86 63 (:REWRITE DEFAULT-<-2))
 (72 8 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (71 1 (:DEFINITION INDICES-MARKED-P))
 (68 63 (:REWRITE DEFAULT-<-1))
 (65 56 (:REWRITE DEFAULT-+-1))
 (65 5 (:DEFINITION COUNT-FREE-BLOCKS))
 (43 10 (:REWRITE NFIX-WHEN-NATP))
 (36 9 (:REWRITE COMMUTATIVITY-OF-+))
 (29 1 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (28 5 (:DEFINITION NATP))
 (24 8 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (20 20 (:LINEAR POSITION-WHEN-MEMBER))
 (20 20 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (18 1 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (17 5 (:DEFINITION BINARY-APPEND))
 (16 16 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (15 5 (:DEFINITION NFIX))
 (13 13 (:TYPE-PRESCRIPTION NATP))
 (12 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (10 10 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (10 10 (:TYPE-PRESCRIPTION NFIX))
 (8 8 (:TYPE-PRESCRIPTION NAT-LISTP))
 (8 8 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (8 8 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (8 8 (:REWRITE DEFAULT-COERCE-2))
 (8 8 (:REWRITE DEFAULT-COERCE-1))
 (7 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (3 1 (:DEFINITION CHARACTER-LISTP))
 (2 2 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (1 1 (:REWRITE L3-FS-P-ASSOC))
 (1 1 (:REWRITE CDR-CONS))
 (1 1 (:REWRITE CAR-CONS))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-33
 (95027 650 (:DEFINITION MEMBER-EQUAL))
 (30524 12727 (:REWRITE DEFAULT-CDR))
 (26588 289 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (22394 684 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (18496 289 (:DEFINITION UNMAKE-BLOCKS))
 (18409 13852 (:REWRITE DEFAULT-CAR))
 (13420 342 (:DEFINITION NTH))
 (12131 3214 (:REWRITE ZP-OPEN))
 (11162 986 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (10982 578 (:REWRITE TAKE-OF-LEN-FREE))
 (10296 88 (:DEFINITION SET-INDICES))
 (10189 103 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (8949 2983 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (8624 752 (:REWRITE NFIX-WHEN-ZP))
 (8092 289 (:DEFINITION TAKE))
 (7377 5186 (:REWRITE DEFAULT-<-2))
 (6821 3991 (:REWRITE DEFAULT-+-2))
 (5571 5186 (:REWRITE DEFAULT-<-1))
 (4992 4 (:REWRITE SUBSETP-APPEND1))
 (4702 756 (:DEFINITION BINARY-APPEND))
 (4433 3991 (:REWRITE DEFAULT-+-1))
 (4230 470 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (3913 43 (:DEFINITION INTERSECTP-EQUAL))
 (3667 53 (:DEFINITION INDICES-MARKED-P))
 (3000 750 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (2958 986 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (2836 2836 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (2786 940 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (2436 94 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (2225 2225 (:LINEAR POSITION-WHEN-MEMBER))
 (2225 2225 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (2041 115 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1994 366 (:DEFINITION NATP))
 (1989 153 (:DEFINITION COUNT-FREE-BLOCKS))
 (1768 442 (:REWRITE COMMUTATIVITY-OF-+))
 (1591 86 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (1408 176 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (1407 1335 (:REWRITE SUBSETP-MEMBER . 2))
 (1335 1335 (:REWRITE SUBSETP-MEMBER . 1))
 (1333 86 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (1328 1328 (:TYPE-PRESCRIPTION NATP))
 (1026 342 (:DEFINITION NFIX))
 (986 986 (:REWRITE DEFAULT-COERCE-2))
 (986 986 (:REWRITE DEFAULT-COERCE-1))
 (923 923 (:TYPE-PRESCRIPTION NULL))
 (923 923 (:DEFINITION NULL))
 (880 88 (:DEFINITION UPDATE-NTH))
 (867 867 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (754 602 (:REWRITE SUBSETP-TRANS2))
 (684 684 (:TYPE-PRESCRIPTION NFIX))
 (602 602 (:REWRITE SUBSETP-TRANS))
 (578 578 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (430 430 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (360 24 (:DEFINITION BLOCK-LISTP))
 (309 309 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (306 306 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (296 296 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (168 24 (:DEFINITION NAT-LISTP))
 (135 103 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (120 24 (:DEFINITION BOOLEAN-LISTP))
 (103 103 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (103 103 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (103 103 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (103 103 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (94 94 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (94 94 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (86 86 (:REWRITE SUBSETP-MEMBER . 4))
 (86 86 (:REWRITE SUBSETP-MEMBER . 3))
 (72 24 (:DEFINITION CHARACTER-LISTP))
 (48 48 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (24 24 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-34
 (10967 17 (:DEFINITION L4-WRCHS))
 (9137 21 (:DEFINITION SUBSETP-EQUAL))
 (8890 45 (:DEFINITION MEMBER-EQUAL))
 (7426 32 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (3978 136 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (3803 1315 (:REWRITE DEFAULT-CDR))
 (3468 102 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (2165 70 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (2060 1204 (:REWRITE DEFAULT-CAR))
 (1989 17 (:DEFINITION SET-INDICES))
 (1763 55 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (1666 136 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1564 17 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1468 22 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (1447 98 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (1445 411 (:REWRITE ZP-OPEN))
 (1310 35 (:DEFINITION NTH))
 (1022 17 (:DEFINITION UNMAKE-BLOCKS))
 (1020 87 (:REWRITE NFIX-WHEN-ZP))
 (990 55 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (880 606 (:REWRITE DEFAULT-<-2))
 (799 17 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-2))
 (717 410 (:REWRITE DEFAULT-+-2))
 (640 606 (:REWRITE DEFAULT-<-1))
 (612 68 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (580 34 (:REWRITE TAKE-OF-LEN-FREE))
 (476 17 (:DEFINITION TAKE))
 (444 410 (:REWRITE DEFAULT-+-1))
 (419 75 (:DEFINITION BINARY-APPEND))
 (408 136 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (408 136 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (408 136 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (391 391 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (379 355 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (308 308 (:TYPE-PRESCRIPTION ZP))
 (306 153 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (304 87 (:REWRITE NFIX-WHEN-NATP))
 (294 38 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (272 34 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (245 19 (:DEFINITION TRUE-LISTP))
 (238 238 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (238 238 (:TYPE-PRESCRIPTION COUNT-FREE-BLOCKS))
 (238 32 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (221 17 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (221 17 (:DEFINITION COUNT-FREE-BLOCKS))
 (197 197 (:LINEAR POSITION-WHEN-MEMBER))
 (197 197 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (194 194 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (192 32 (:DEFINITION STRING-LISTP))
 (187 17 (:REWRITE L3-FS-P-ASSOC))
 (187 17 (:DEFINITION MIN))
 (183 3 (:REWRITE CDR-OF-LIST-FIX))
 (171 171 (:TYPE-PRESCRIPTION NATP))
 (170 170 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (170 34 (:DEFINITION ASSOC-EQUAL))
 (170 17 (:DEFINITION UPDATE-NTH))
 (168 42 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (166 22 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (160 160 (:TYPE-PRESCRIPTION STRING-LISTP))
 (136 136 (:TYPE-PRESCRIPTION NULL))
 (136 136 (:REWRITE DEFAULT-COERCE-2))
 (136 136 (:REWRITE DEFAULT-COERCE-1))
 (136 136 (:DEFINITION NULL))
 (136 34 (:REWRITE COMMUTATIVITY-OF-+))
 (128 32 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (111 6 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (105 105 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (105 35 (:DEFINITION NFIX))
 (88 88 (:REWRITE SUBSETP-MEMBER . 2))
 (88 88 (:REWRITE SUBSETP-MEMBER . 1))
 (84 6 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (70 70 (:TYPE-PRESCRIPTION NFIX))
 (68 68 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (63 27 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (53 22 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (51 51 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (42 42 (:REWRITE SUBSETP-TRANS2))
 (42 42 (:REWRITE SUBSETP-TRANS))
 (34 34 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (34 34 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (34 34 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (34 34 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (27 9 (:DEFINITION CHARACTER-LISTP))
 (22 22 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (22 22 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (22 22 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (20 20 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (20 20 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (8 8 (:REWRITE FLATTEN-WHEN-NOT-CONSP))
 (7 7 (:REWRITE CDR-CONS))
 (7 7 (:REWRITE CAR-CONS))
 (6 6 (:REWRITE NAT-LISTP-WHEN-SUBSETP))
 (6 6 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (6 3 (:REWRITE CAR-OF-LIST-FIX))
 (3 3 (:REWRITE CONSP-OF-LIST-FIX))
 )
(L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-35
 (6448 10 (:DEFINITION L4-WRCHS))
 (4456 21 (:DEFINITION SUBSETP-EQUAL))
 (4213 37 (:DEFINITION MEMBER-EQUAL))
 (2589 34 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (2491 1027 (:REWRITE DEFAULT-CDR))
 (2340 80 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (2040 60 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (1751 58 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1739 55 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (1614 22 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (1441 937 (:REWRITE DEFAULT-CAR))
 (1251 84 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (1170 10 (:DEFINITION SET-INDICES))
 (1064 29 (:DEFINITION NTH))
 (992 267 (:REWRITE ZP-OPEN))
 (990 55 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (980 80 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (920 10 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (742 68 (:REWRITE NFIX-WHEN-ZP))
 (621 443 (:REWRITE DEFAULT-<-2))
 (598 10 (:DEFINITION UNMAKE-BLOCKS))
 (491 280 (:REWRITE DEFAULT-+-2))
 (470 10 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-2))
 (463 443 (:REWRITE DEFAULT-<-1))
 (389 69 (:DEFINITION BINARY-APPEND))
 (360 40 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (338 20 (:REWRITE TAKE-OF-LEN-FREE))
 (300 280 (:REWRITE DEFAULT-+-1))
 (294 38 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (280 10 (:DEFINITION TAKE))
 (245 19 (:DEFINITION TRUE-LISTP))
 (241 217 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (240 80 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (240 80 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (240 80 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (240 34 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (233 68 (:REWRITE NFIX-WHEN-NATP))
 (230 230 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (198 198 (:TYPE-PRESCRIPTION ZP))
 (192 32 (:DEFINITION STRING-LISTP))
 (183 3 (:REWRITE CDR-OF-LIST-FIX))
 (180 90 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (160 160 (:TYPE-PRESCRIPTION STRING-LISTP))
 (160 20 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (158 22 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (144 36 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (142 142 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (140 140 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (140 140 (:TYPE-PRESCRIPTION COUNT-FREE-BLOCKS))
 (130 34 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (130 10 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (130 10 (:DEFINITION COUNT-FREE-BLOCKS))
 (129 129 (:LINEAR POSITION-WHEN-MEMBER))
 (129 129 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (111 6 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (110 10 (:REWRITE L3-FS-P-ASSOC))
 (110 10 (:DEFINITION MIN))
 (109 109 (:TYPE-PRESCRIPTION NATP))
 (105 105 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (100 100 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (100 20 (:DEFINITION ASSOC-EQUAL))
 (100 10 (:DEFINITION UPDATE-NTH))
 (87 29 (:DEFINITION NFIX))
 (84 6 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (80 80 (:TYPE-PRESCRIPTION NULL))
 (80 80 (:REWRITE DEFAULT-COERCE-2))
 (80 80 (:REWRITE DEFAULT-COERCE-1))
 (80 80 (:DEFINITION NULL))
 (80 20 (:REWRITE COMMUTATIVITY-OF-+))
 (73 22 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (69 69 (:REWRITE SUBSETP-MEMBER . 2))
 (69 69 (:REWRITE SUBSETP-MEMBER . 1))
 (63 27 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (58 58 (:TYPE-PRESCRIPTION NFIX))
 (42 42 (:REWRITE SUBSETP-TRANS2))
 (42 42 (:REWRITE SUBSETP-TRANS))
 (40 40 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (30 30 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (27 9 (:DEFINITION CHARACTER-LISTP))
 (26 26 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (22 22 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (22 22 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (22 22 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (20 20 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (20 20 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (20 20 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (20 20 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (19 19 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (10 10 (:REWRITE FLATTEN-WHEN-NOT-CONSP))
 (6 6 (:REWRITE NAT-LISTP-WHEN-SUBSETP))
 (6 6 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (6 6 (:REWRITE CDR-CONS))
 (6 6 (:REWRITE CAR-CONS))
 (6 3 (:REWRITE CAR-OF-LIST-FIX))
 (3 3 (:REWRITE CONSP-OF-LIST-FIX))
 )
(L4-WRCHS-RETURNS-STRICTER-FS
 (4707 4 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-5))
 (4011 14 (:DEFINITION MEMBER-INTERSECTP-EQUAL))
 (2923 2297 (:REWRITE DEFAULT-CDR))
 (2883 18 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-20))
 (2503 2370 (:REWRITE DEFAULT-CAR))
 (2494 43 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (2261 74 (:DEFINITION MEMBER-EQUAL))
 (2222 72 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (2163 24 (:DEFINITION SUBSETP-EQUAL))
 (1991 59 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (1947 649 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1483 259 (:DEFINITION BINARY-APPEND))
 (1336 36 (:DEFINITION NTH))
 (1332 10 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-34))
 (920 10 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (863 181 (:REWRITE ZP-OPEN))
 (763 77 (:REWRITE NFIX-WHEN-ZP))
 (640 10 (:DEFINITION UNMAKE-BLOCKS))
 (623 3 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-2))
 (578 436 (:REWRITE DEFAULT-<-2))
 (536 22 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (520 104 (:DEFINITION ASSOC-EQUAL))
 (487 277 (:REWRITE DEFAULT-+-2))
 (451 436 (:REWRITE DEFAULT-<-1))
 (416 104 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (386 59 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (380 20 (:REWRITE TAKE-OF-LEN-FREE))
 (358 34 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (342 9 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-26))
 (333 5 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-33))
 (322 14 (:DEFINITION BOUNDED-NAT-LISTP))
 (296 277 (:REWRITE DEFAULT-+-1))
 (288 32 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (280 10 (:DEFINITION TAKE))
 (250 250 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (234 2 (:DEFINITION SET-INDICES))
 (208 16 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (192 64 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (176 44 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (148 148 (:REWRITE SUBSETP-MEMBER . 2))
 (148 148 (:REWRITE SUBSETP-MEMBER . 1))
 (143 143 (:LINEAR POSITION-WHEN-MEMBER))
 (143 143 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (120 120 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (118 48 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (117 9 (:DEFINITION COUNT-FREE-BLOCKS))
 (108 36 (:DEFINITION NFIX))
 (102 34 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (76 19 (:REWRITE COMMUTATIVITY-OF-+))
 (70 70 (:TYPE-PRESCRIPTION NATP))
 (64 64 (:TYPE-PRESCRIPTION NULL))
 (64 64 (:DEFINITION NULL))
 (59 59 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (59 59 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (59 59 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (59 59 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (48 48 (:REWRITE SUBSETP-TRANS2))
 (48 48 (:REWRITE SUBSETP-TRANS))
 (47 47 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (45 45 (:TYPE-PRESCRIPTION L4-LIST-ALL-INDICES))
 (44 44 (:REWRITE SUBSETP-MEMBER . 4))
 (44 44 (:REWRITE SUBSETP-MEMBER . 3))
 (43 43 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (38 3 (:REWRITE FLATTEN-OF-APPEND))
 (36 12 (:DEFINITION CHARACTER-LISTP))
 (34 34 (:REWRITE DEFAULT-COERCE-2))
 (34 34 (:REWRITE DEFAULT-COERCE-1))
 (33 33 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (33 33 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (32 4 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (30 30 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (20 20 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-FLATTEN))
 (20 20 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (20 2 (:DEFINITION UPDATE-NTH))
 (18 18 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (13 13 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (5 5 (:REWRITE FLATTEN-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 )
(L4-TO-L2-FS)
(L4-TO-L2-FS-CORRECTNESS-1)
(L4-STAT-CORRECTNESS-1
 (976 4 (:DEFINITION L3-STAT))
 (458 5 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (333 10 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (314 5 (:DEFINITION UNMAKE-BLOCKS))
 (248 1 (:REWRITE L3-STAT-CORRECTNESS-2))
 (195 195 (:TYPE-PRESCRIPTION LEN))
 (194 5 (:DEFINITION NTH))
 (192 1 (:DEFINITION L3-TO-L2-FS))
 (184 10 (:REWRITE TAKE-OF-LEN-FREE))
 (155 31 (:DEFINITION LEN))
 (144 25 (:REWRITE ZP-OPEN))
 (137 5 (:DEFINITION TAKE))
 (133 10 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (125 5 (:REWRITE DEFAULT-COERCE-3))
 (112 112 (:REWRITE DEFAULT-CDR))
 (110 5 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (104 10 (:REWRITE NFIX-WHEN-ZP))
 (96 32 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (90 90 (:REWRITE DEFAULT-CAR))
 (87 51 (:REWRITE DEFAULT-+-2))
 (87 7 (:DEFINITION L3-FS-P))
 (75 60 (:REWRITE DEFAULT-<-2))
 (65 60 (:REWRITE DEFAULT-<-1))
 (56 51 (:REWRITE DEFAULT-+-1))
 (52 4 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (44 4 (:REWRITE L3-FS-P-ASSOC))
 (42 42 (:TYPE-PRESCRIPTION ZP))
 (42 10 (:REWRITE NFIX-WHEN-NATP))
 (40 8 (:DEFINITION ASSOC-EQUAL))
 (40 5 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (34 34 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (32 4 (:DEFINITION MEMBER-EQUAL))
 (30 30 (:LINEAR POSITION-WHEN-MEMBER))
 (30 30 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (27 5 (:DEFINITION NATP))
 (20 20 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (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))
 (15 1 (:DEFINITION BLOCK-LISTP))
 (10 10 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (10 10 (:TYPE-PRESCRIPTION NFIX))
 (10 10 (:TYPE-PRESCRIPTION NATP))
 (10 10 (:TYPE-PRESCRIPTION NAT-LISTP))
 (10 10 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (7 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (5 5 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (5 5 (:REWRITE DEFAULT-COERCE-2))
 (3 1 (:DEFINITION SYMBOL-LISTP))
 (3 1 (:DEFINITION CHARACTER-LISTP))
 (1 1 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (1 1 (:REWRITE L3-READ-AFTER-WRITE-1-LEMMA-2))
 )
(L4-STAT-CORRECTNESS-2
 (976 4 (:DEFINITION L3-STAT))
 (622 7 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (576 3 (:DEFINITION L3-TO-L2-FS))
 (447 14 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (430 7 (:DEFINITION UNMAKE-BLOCKS))
 (262 7 (:DEFINITION NTH))
 (259 259 (:TYPE-PRESCRIPTION LEN))
 (248 14 (:REWRITE TAKE-OF-LEN-FREE))
 (245 1 (:REWRITE L3-READ-AFTER-WRITE-1-LEMMA-2))
 (215 43 (:DEFINITION LEN))
 (192 35 (:REWRITE ZP-OPEN))
 (187 7 (:DEFINITION TAKE))
 (175 7 (:REWRITE DEFAULT-COERCE-3))
 (171 13 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (154 7 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (150 150 (:REWRITE DEFAULT-CDR))
 (136 14 (:REWRITE NFIX-WHEN-ZP))
 (130 9 (:DEFINITION L3-FS-P))
 (121 71 (:REWRITE DEFAULT-+-2))
 (116 116 (:REWRITE DEFAULT-CAR))
 (105 84 (:REWRITE DEFAULT-<-2))
 (96 32 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (91 84 (:REWRITE DEFAULT-<-1))
 (78 71 (:REWRITE DEFAULT-+-1))
 (56 7 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (54 14 (:REWRITE NFIX-WHEN-NATP))
 (52 4 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (48 48 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (46 46 (:TYPE-PRESCRIPTION ZP))
 (44 4 (:REWRITE L3-FS-P-ASSOC))
 (42 42 (:LINEAR POSITION-WHEN-MEMBER))
 (42 42 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (40 8 (:DEFINITION ASSOC-EQUAL))
 (33 7 (:DEFINITION NATP))
 (32 4 (:DEFINITION MEMBER-EQUAL))
 (28 28 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (28 7 (:REWRITE COMMUTATIVITY-OF-+))
 (21 21 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (21 7 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (21 7 (:DEFINITION NFIX))
 (21 7 (:DEFINITION BINARY-APPEND))
 (20 20 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (15 1 (:DEFINITION BLOCK-LISTP))
 (14 14 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (14 14 (:TYPE-PRESCRIPTION NFIX))
 (14 14 (:TYPE-PRESCRIPTION NATP))
 (14 14 (:TYPE-PRESCRIPTION NAT-LISTP))
 (14 14 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (14 6 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (7 7 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (7 7 (:REWRITE DEFAULT-COERCE-2))
 (3 1 (:DEFINITION SYMBOL-LISTP))
 (3 1 (:DEFINITION CHARACTER-LISTP))
 (1 1 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 )
(L4-RDCHS-CORRECTNESS-1
 (5314 22 (:DEFINITION L3-STAT))
 (2478 27 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1983 62 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1638 27 (:DEFINITION UNMAKE-BLOCKS))
 (1486 5 (:REWRITE L3-STAT-CORRECTNESS-2))
 (1290 62 (:REWRITE TAKE-OF-LEN-FREE))
 (1201 31 (:DEFINITION TAKE))
 (1174 31 (:DEFINITION NTH))
 (1100 200 (:DEFINITION LEN))
 (954 5 (:DEFINITION L3-TO-L2-FS))
 (903 175 (:REWRITE ZP-OPEN))
 (853 691 (:REWRITE DEFAULT-CDR))
 (741 87 (:REWRITE NFIX-WHEN-ZP))
 (719 54 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (700 31 (:REWRITE DEFAULT-COERCE-3))
 (662 210 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (617 551 (:REWRITE DEFAULT-CAR))
 (594 27 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (584 354 (:REWRITE DEFAULT-+-2))
 (502 392 (:REWRITE DEFAULT-<-2))
 (474 37 (:DEFINITION L3-FS-P))
 (441 1 (:DEFINITION L2-STAT))
 (429 392 (:REWRITE DEFAULT-<-1))
 (401 62 (:DEFINITION ASSOC-EQUAL))
 (384 354 (:REWRITE DEFAULT-+-1))
 (300 300 (:TYPE-PRESCRIPTION ZP))
 (299 23 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (297 87 (:REWRITE NFIX-WHEN-NATP))
 (277 4 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (277 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (253 23 (:REWRITE L3-FS-P-ASSOC))
 (251 12 (:REWRITE DEFAULT-COERCE-1))
 (243 5 (:REWRITE L3-READ-AFTER-WRITE-1-LEMMA-2))
 (216 27 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (208 4 (:REWRITE CAR-OF-NTHCDR))
 (194 194 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (184 23 (:DEFINITION MEMBER-EQUAL))
 (182 182 (:LINEAR POSITION-WHEN-MEMBER))
 (182 182 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (162 8 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (159 3 (:REWRITE LEN-OF-NTHCDR))
 (132 4 (:DEFINITION NTHCDR))
 (115 115 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (111 109 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (105 105 (:TYPE-PRESCRIPTION L3-TO-L2-FS))
 (95 29 (:DEFINITION NFIX))
 (81 81 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (81 27 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (81 27 (:DEFINITION BINARY-APPEND))
 (81 1 (:REWRITE L2-FS-P-ASSOC))
 (76 8 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (75 1 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (70 1 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (69 69 (:TYPE-PRESCRIPTION NFIX))
 (60 4 (:REWRITE CONSP-OF-NTHCDR))
 (60 4 (:DEFINITION BLOCK-LISTP))
 (57 57 (:TYPE-PRESCRIPTION NATP))
 (54 54 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (54 54 (:TYPE-PRESCRIPTION NAT-LISTP))
 (54 54 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (48 1 (:DEFINITION L2-FS-P))
 (46 46 (:REWRITE SUBSETP-MEMBER . 2))
 (46 46 (:REWRITE SUBSETP-MEMBER . 1))
 (46 5 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-2))
 (43 43 (: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))
 (27 27 (: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 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-8))
 (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-+))
 )
(LIST-EQUIV-IMPLIES-EQUAL-FETCH-BLOCKS-BY-INDICES-1
 (342 12 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (204 6 (:DEFINITION NTH))
 (110 22 (:DEFINITION LEN))
 (96 18 (:REWRITE ZP-OPEN))
 (96 12 (:REWRITE NFIX-WHEN-ZP))
 (86 64 (:REWRITE DEFAULT-<-2))
 (74 64 (:REWRITE DEFAULT-<-1))
 (50 28 (:REWRITE DEFAULT-+-2))
 (36 12 (:REWRITE NFIX-WHEN-NATP))
 (32 32 (:REWRITE DEFAULT-CDR))
 (28 28 (:REWRITE DEFAULT-+-1))
 (22 22 (:REWRITE DEFAULT-CAR))
 (18 6 (:DEFINITION NFIX))
 (18 6 (:DEFINITION NATP))
 (14 14 (:LINEAR POSITION-WHEN-MEMBER))
 (14 14 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (12 12 (:TYPE-PRESCRIPTION ZP))
 (12 12 (:TYPE-PRESCRIPTION NFIX))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 6 (:TYPE-PRESCRIPTION NATP))
 (5 5 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (5 5 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-1
 (240 48 (:DEFINITION LEN))
 (204 6 (:DEFINITION NTH))
 (157 30 (:REWRITE NFIX-WHEN-ZP))
 (135 9 (:DEFINITION BLOCK-LISTP))
 (127 112 (:REWRITE DEFAULT-<-2))
 (125 34 (:REWRITE ZP-OPEN))
 (122 112 (:REWRITE DEFAULT-<-1))
 (115 67 (:REWRITE DEFAULT-+-2))
 (104 98 (:REWRITE DEFAULT-CDR))
 (87 81 (:REWRITE DEFAULT-CAR))
 (67 67 (:REWRITE DEFAULT-+-1))
 (57 13 (:REWRITE SUBSETP-MEMBER . 1))
 (40 2 (:DEFINITION SUBSETP-EQUAL))
 (35 5 (:DEFINITION UPDATE-NTH))
 (31 31 (:TYPE-PRESCRIPTION ZP))
 (27 9 (:DEFINITION CHARACTER-LISTP))
 (24 8 (:DEFINITION NFIX))
 (23 9 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (15 15 (:LINEAR POSITION-WHEN-MEMBER))
 (15 15 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (13 13 (:REWRITE SUBSETP-MEMBER . 2))
 (11 11 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (9 9 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (9 9 (:REWRITE SUBSETP-MEMBER . 4))
 (9 9 (:REWRITE SUBSETP-MEMBER . 3))
 (7 7 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (7 7 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (6 6 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-2
 (248 13 (:DEFINITION MEMBER-EQUAL))
 (170 9 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (148 8 (:DEFINITION SUBSETP-EQUAL))
 (143 9 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (123 7 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (102 7 (:DEFINITION L3-FS-P))
 (99 9 (:REWRITE SUBSETP-MEMBER . 3))
 (70 70 (:REWRITE DEFAULT-CDR))
 (63 63 (:REWRITE DEFAULT-CAR))
 (56 56 (:TYPE-PRESCRIPTION L3-FS-P))
 (45 45 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (40 40 (:TYPE-PRESCRIPTION L4-LIST-ALL-INDICES))
 (35 35 (:REWRITE SUBSETP-MEMBER . 2))
 (28 10 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (27 5 (:DEFINITION BINARY-APPEND))
 (17 17 (:REWRITE SUBSETP-TRANS2))
 (17 17 (:REWRITE SUBSETP-TRANS))
 (9 9 (:REWRITE SUBSETP-MEMBER . 4))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-3
 (69 4 (:DEFINITION MEMBER-EQUAL))
 (59 3 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (51 3 (:REWRITE SUBSETP-MEMBER . 3))
 (50 3 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (40 2 (:DEFINITION SUBSETP-EQUAL))
 (30 2 (:DEFINITION L3-FS-P))
 (21 2 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (20 20 (:REWRITE DEFAULT-CDR))
 (16 16 (:REWRITE DEFAULT-CAR))
 (15 15 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (11 11 (:REWRITE SUBSETP-MEMBER . 2))
 (8 1 (:DEFINITION BINARY-APPEND))
 (7 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (5 5 (:REWRITE SUBSETP-TRANS2))
 (5 5 (:REWRITE SUBSETP-TRANS))
 (3 3 (:REWRITE SUBSETP-MEMBER . 4))
 (2 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-4
 (140 7 (:DEFINITION MEMBER-EQUAL))
 (96 5 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (84 4 (:DEFINITION SUBSETP-EQUAL))
 (81 5 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (65 18 (:REWRITE SUBSETP-MEMBER . 1))
 (39 39 (:REWRITE DEFAULT-CDR))
 (39 15 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (36 36 (:REWRITE DEFAULT-CAR))
 (30 30 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (25 25 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (18 18 (:REWRITE SUBSETP-MEMBER . 2))
 (10 5 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (9 9 (:REWRITE SUBSETP-TRANS2))
 (9 9 (:REWRITE SUBSETP-TRANS))
 (5 5 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (5 5 (:REWRITE SUBSETP-MEMBER . 4))
 (5 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (4 4 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-3))
 (4 1 (:DEFINITION BINARY-APPEND))
 )
(LIST-EQUIV-IMPLIES-EQUAL-L3-TO-L2-FS-2
 (492 6 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (432 6 (:REWRITE DEFAULT-COERCE-3))
 (408 6 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (372 12 (:DEFINITION BLOCK-LISTP))
 (348 6 (:DEFINITION UNMAKE-BLOCKS))
 (342 12 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (270 270 (:TYPE-PRESCRIPTION LEN))
 (210 42 (:DEFINITION LEN))
 (204 6 (:DEFINITION NTH))
 (198 6 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (192 12 (:REWRITE TAKE-OF-LEN-FREE))
 (150 6 (:DEFINITION TAKE))
 (136 136 (:REWRITE DEFAULT-CDR))
 (120 24 (:REWRITE ZP-OPEN))
 (114 66 (:REWRITE DEFAULT-+-2))
 (108 108 (:REWRITE DEFAULT-CAR))
 (102 6 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (96 12 (:REWRITE NFIX-WHEN-ZP))
 (84 66 (:REWRITE DEFAULT-<-2))
 (84 6 (:DEFINITION L3-FS-P))
 (72 66 (:REWRITE DEFAULT-<-1))
 (72 66 (:REWRITE DEFAULT-+-1))
 (72 12 (:DEFINITION CHARACTER-LISTP))
 (60 60 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (60 60 (:TYPE-PRESCRIPTION BLOCK-LISTP))
 (60 60 (:LINEAR POSITION-WHEN-MEMBER))
 (60 60 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (48 48 (:TYPE-PRESCRIPTION L3-FS-P))
 (36 12 (:REWRITE NFIX-WHEN-NATP))
 (24 24 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (24 6 (:REWRITE COMMUTATIVITY-OF-+))
 (18 18 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (18 18 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (18 6 (:DEFINITION NFIX))
 (18 6 (:DEFINITION NATP))
 (18 6 (:DEFINITION BINARY-APPEND))
 (12 12 (:TYPE-PRESCRIPTION ZP))
 (12 12 (:TYPE-PRESCRIPTION NFIX))
 (6 6 (:TYPE-PRESCRIPTION NATP))
 (6 6 (:REWRITE DEFAULT-COERCE-2))
 (4 4 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (4 4 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-5
 (720 10 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (598 22 (:DEFINITION SUBSETP-EQUAL))
 (580 10 (:DEFINITION UNMAKE-BLOCKS))
 (510 20 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (450 25 (:REWRITE SUBSETP-MEMBER . 3))
 (430 86 (:DEFINITION LEN))
 (340 10 (:DEFINITION NTH))
 (339 339 (:REWRITE DEFAULT-CDR))
 (325 81 (:REWRITE SUBSETP-MEMBER . 1))
 (320 20 (:REWRITE TAKE-OF-LEN-FREE))
 (298 298 (:REWRITE DEFAULT-CAR))
 (250 10 (:REWRITE DEFAULT-COERCE-3))
 (250 10 (:DEFINITION TAKE))
 (247 57 (:REWRITE ZP-OPEN))
 (229 133 (:REWRITE DEFAULT-+-2))
 (220 10 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (195 13 (:DEFINITION BLOCK-LISTP))
 (169 146 (:REWRITE DEFAULT-<-2))
 (160 20 (:REWRITE NFIX-WHEN-ZP))
 (156 146 (:REWRITE DEFAULT-<-1))
 (143 133 (:REWRITE DEFAULT-+-1))
 (110 110 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (81 81 (:REWRITE SUBSETP-MEMBER . 2))
 (80 10 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (62 62 (:LINEAR POSITION-WHEN-MEMBER))
 (62 62 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (60 20 (:REWRITE NFIX-WHEN-NATP))
 (51 25 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (49 7 (:DEFINITION UPDATE-NTH))
 (44 44 (:REWRITE SUBSETP-TRANS2))
 (44 44 (:REWRITE SUBSETP-TRANS))
 (44 16 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (40 10 (:REWRITE COMMUTATIVITY-OF-+))
 (39 13 (:DEFINITION CHARACTER-LISTP))
 (30 30 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (30 10 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (30 10 (:DEFINITION NFIX))
 (30 10 (:DEFINITION NATP))
 (30 10 (:DEFINITION BINARY-APPEND))
 (25 25 (:REWRITE SUBSETP-MEMBER . 4))
 (20 20 (:TYPE-PRESCRIPTION ZP))
 (20 20 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (20 20 (:TYPE-PRESCRIPTION NFIX))
 (20 20 (:TYPE-PRESCRIPTION NATP))
 (20 20 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (13 13 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (13 13 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (13 13 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (10 10 (:REWRITE DEFAULT-COERCE-2))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-6
 (5511 210 (:DEFINITION SUBSETP-EQUAL))
 (2807 141 (:REWRITE SUBSETP-MEMBER . 3))
 (2171 141 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (1916 714 (:REWRITE SUBSETP-MEMBER . 1))
 (1796 117 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (1486 38 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (1122 1122 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (1008 995 (:REWRITE DEFAULT-CDR))
 (999 984 (:REWRITE DEFAULT-CAR))
 (971 8 (:REWRITE SUBSETP-APPEND1))
 (888 714 (:REWRITE SUBSETP-MEMBER . 2))
 (845 9 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-2))
 (835 43 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (794 450 (:REWRITE SUBSETP-TRANS2))
 (585 585 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (450 450 (:REWRITE SUBSETP-TRANS))
 (396 42 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (368 50 (:DEFINITION BINARY-APPEND))
 (308 126 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-4))
 (290 80 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (141 141 (:REWRITE SUBSETP-MEMBER . 4))
 (126 126 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-3))
 (122 50 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (70 42 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (43 43 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (43 43 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (43 43 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (42 42 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (38 38 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (34 34 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (31 31 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (15 15 (:REWRITE DEFAULT-<-2))
 (15 15 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE SUBSETP-APPEND2))
 (1 1 (:REWRITE SUBSETP-APPEND3))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-7
 (607 7 (:DEFINITION INTERSECTP-EQUAL))
 (436 14 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (429 38 (:DEFINITION MEMBER-EQUAL))
 (277 9 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (259 14 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (217 14 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (174 12 (:DEFINITION L3-FS-P))
 (170 170 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (165 12 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (162 9 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (148 148 (:REWRITE DEFAULT-CDR))
 (146 146 (:REWRITE DEFAULT-CAR))
 (90 9 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-6))
 (81 81 (:REWRITE SUBSETP-MEMBER . 2))
 (81 81 (:REWRITE SUBSETP-MEMBER . 1))
 (70 70 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (54 54 (:TYPE-PRESCRIPTION L3-REGULAR-FILE-ENTRY-P))
 (53 9 (:DEFINITION BINARY-APPEND))
 (37 37 (:REWRITE SUBSETP-TRANS2))
 (37 37 (:REWRITE SUBSETP-TRANS))
 (21 9 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (16 16 (:TYPE-PRESCRIPTION L4-LIST-ALL-INDICES))
 (16 16 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (16 16 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (16 16 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (16 16 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (16 4 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (15 15 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (14 14 (:REWRITE SUBSETP-MEMBER . 4))
 (14 14 (:REWRITE SUBSETP-MEMBER . 3))
 (14 14 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (14 14 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (13 13 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (7 4 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-4))
 (6 6 (:REWRITE CAR-CONS))
 (4 4 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-3))
 (4 4 (:REWRITE CDR-CONS))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-8
 (55 43 (:REWRITE DEFAULT-CAR))
 (52 46 (:REWRITE DEFAULT-CDR))
 (47 25 (:REWRITE DEFAULT-+-2))
 (25 25 (:REWRITE DEFAULT-+-1))
 (16 10 (:REWRITE DEFAULT-<-2))
 (15 15 (:LINEAR POSITION-WHEN-MEMBER))
 (15 15 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (10 10 (:REWRITE DEFAULT-<-1))
 (5 5 (:REWRITE ZP-OPEN))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-9
 (1872 18 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1218 39 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1020 18 (:DEFINITION UNMAKE-BLOCKS))
 (983 18 (:REWRITE DEFAULT-COERCE-3))
 (921 18 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (753 55 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (744 682 (:REWRITE DEFAULT-CDR))
 (691 18 (:DEFINITION NTH))
 (672 617 (:REWRITE DEFAULT-CAR))
 (667 23 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (552 36 (:REWRITE TAKE-OF-LEN-FREE))
 (520 105 (:REWRITE ZP-OPEN))
 (483 279 (:REWRITE DEFAULT-+-2))
 (450 18 (:DEFINITION TAKE))
 (447 18 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (414 23 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (408 58 (:REWRITE NFIX-WHEN-ZP))
 (374 324 (:REWRITE DEFAULT-<-2))
 (342 324 (:REWRITE DEFAULT-<-1))
 (297 279 (:REWRITE DEFAULT-+-1))
 (251 89 (:TYPE-PRESCRIPTION SET-INDICES))
 (220 17 (:DEFINITION MEMBER-EQUAL))
 (218 42 (:DEFINITION CHARACTER-LISTP))
 (204 3 (:REWRITE NTH-UPDATE-NTH))
 (169 41 (:DEFINITION BINARY-APPEND))
 (167 3 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-1))
 (164 164 (:LINEAR POSITION-WHEN-MEMBER))
 (164 164 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (148 14 (:REWRITE SET-INDICES-CORRECTNESS-3))
 (100 100 (:TYPE-PRESCRIPTION UPDATE-NTH))
 (100 100 (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH))
 (98 42 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (96 9 (:DEFINITION UPDATE-NTH))
 (84 10 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (79 35 (:REWRITE SUBSETP-MEMBER . 1))
 (75 25 (:DEFINITION NFIX))
 (72 18 (:REWRITE COMMUTATIVITY-OF-+))
 (59 3 (:DEFINITION SUBSETP-EQUAL))
 (55 3 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-2))
 (54 54 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (52 52 (:TYPE-PRESCRIPTION L4-LIST-ALL-INDICES))
 (52 52 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (50 50 (:TYPE-PRESCRIPTION ZP))
 (46 46 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (45 21 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (44 44 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (43 43 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (41 41 (:TYPE-PRESCRIPTION NFIX))
 (35 35 (:REWRITE SUBSETP-MEMBER . 2))
 (35 7 (:REWRITE SET-INDICES-CORRECTNESS-1))
 (32 32 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (28 1 (:REWRITE UPDATE-NTH-OF-UPDATE-NTH-1))
 (28 1 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-5))
 (24 12 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-4))
 (21 21 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (21 21 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (21 21 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (21 21 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (21 21 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (20 14 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (18 18 (:REWRITE DEFAULT-COERCE-2))
 (15 15 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (14 14 (:REWRITE SUBSETP-MEMBER . 4))
 (14 14 (:REWRITE SUBSETP-MEMBER . 3))
 (14 12 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-3))
 (10 10 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (6 6 (:REWRITE SUBSETP-TRANS2))
 (6 6 (:REWRITE SUBSETP-TRANS))
 (3 3 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (3 3 (:DEFINITION NO-DUPLICATESP-EQUAL))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-11
 (73 1 (:DEFINITION INDICES-MARKED-LISTP))
 (69 1 (:DEFINITION INDICES-MARKED-P))
 (57 2 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (34 1 (:DEFINITION NTH))
 (16 3 (:REWRITE ZP-OPEN))
 (16 2 (:REWRITE NFIX-WHEN-ZP))
 (12 12 (:TYPE-PRESCRIPTION LEN))
 (12 10 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE DEFAULT-<-1))
 (10 2 (:DEFINITION LEN))
 (7 7 (:REWRITE DEFAULT-CDR))
 (6 2 (:REWRITE NFIX-WHEN-NATP))
 (5 5 (:REWRITE DEFAULT-CAR))
 (5 3 (:REWRITE DEFAULT-+-2))
 (5 1 (:DEFINITION BOOLEAN-LISTP))
 (3 3 (:REWRITE DEFAULT-+-1))
 (3 1 (:DEFINITION NFIX))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:LINEAR POSITION-WHEN-MEMBER))
 (2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-12
 (9561 48 (:DEFINITION L3-TO-L2-FS))
 (8832 292 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (8366 97 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (7766 3999 (:REWRITE DEFAULT-CDR))
 (5920 97 (:DEFINITION UNMAKE-BLOCKS))
 (5356 146 (:DEFINITION NTH))
 (5178 170 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (4791 3541 (:REWRITE DEFAULT-CAR))
 (4579 314 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (4279 999 (:REWRITE ZP-OPEN))
 (4152 289 (:DEFINITION L3-FS-P))
 (3920 248 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (3773 49 (:DEFINITION INDICES-MARKED-LISTP))
 (3479 49 (:DEFINITION INDICES-MARKED-P))
 (3453 1151 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (3398 194 (:REWRITE TAKE-OF-LEN-FREE))
 (3210 317 (:REWRITE NFIX-WHEN-ZP))
 (3060 170 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (2925 25 (:DEFINITION SET-INDICES))
 (2617 1947 (:REWRITE DEFAULT-<-2))
 (2609 1516 (:REWRITE DEFAULT-+-2))
 (2572 97 (:DEFINITION TAKE))
 (2096 1947 (:REWRITE DEFAULT-<-1))
 (1671 1516 (:REWRITE DEFAULT-+-1))
 (1623 48 (:REWRITE DEFAULT-COERCE-3))
 (1253 267 (:DEFINITION BINARY-APPEND))
 (1014 248 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (930 186 (:DEFINITION ASSOC-EQUAL))
 (873 39 (:DEFINITION BLOCK-LISTP))
 (785 785 (:LINEAR POSITION-WHEN-MEMBER))
 (785 785 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (780 26 (:DEFINITION NO-DUPLICATES-LISTP))
 (712 89 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (712 58 (:DEFINITION COUNT-FREE-BLOCKS))
 (671 60 (:DEFINITION MEMBER-EQUAL))
 (634 146 (:DEFINITION NATP))
 (624 26 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (620 155 (:REWRITE COMMUTATIVITY-OF-+))
 (468 52 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (438 146 (:DEFINITION NFIX))
 (421 37 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (385 385 (:TYPE-PRESCRIPTION NATP))
 (312 104 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (292 292 (:TYPE-PRESCRIPTION NFIX))
 (291 291 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (250 25 (:DEFINITION UPDATE-NTH))
 (248 248 (:REWRITE DEFAULT-COERCE-2))
 (224 56 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (212 212 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (208 52 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (200 200 (:REWRITE DEFAULT-COERCE-1))
 (200 50 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (198 52 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (188 188 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (182 182 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (171 39 (:DEFINITION CHARACTER-LISTP))
 (142 1 (:DEFINITION SUBSETP-EQUAL))
 (119 119 (:REWRITE SUBSETP-MEMBER . 2))
 (119 119 (:REWRITE SUBSETP-MEMBER . 1))
 (115 23 (:DEFINITION BOOLEAN-LISTP))
 (104 104 (:TYPE-PRESCRIPTION NULL))
 (104 104 (:DEFINITION NULL))
 (74 74 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (62 62 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (52 52 (:REWRITE SUBSETP-MEMBER . 4))
 (52 52 (:REWRITE SUBSETP-MEMBER . 3))
 (50 50 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (50 50 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (49 49 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (30 3 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-26))
 (25 25 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (25 25 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (25 25 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (25 25 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (25 25 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (25 25 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (24 24 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (24 24 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-7))
 (24 24 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-6))
 (12 12 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (5 5 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (2 2 (:REWRITE SUBSETP-TRANS2))
 (2 2 (:REWRITE SUBSETP-TRANS))
 (1 1 (:REWRITE CDR-CONS))
 (1 1 (:REWRITE CAR-CONS))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-13
 (617 15 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (581 415 (:REWRITE DEFAULT-CDR))
 (460 387 (:REWRITE DEFAULT-<-2))
 (443 73 (:REWRITE NFIX-WHEN-ZP))
 (431 84 (:REWRITE ZP-OPEN))
 (410 387 (:REWRITE DEFAULT-<-1))
 (408 359 (:REWRITE DEFAULT-CAR))
 (401 233 (:REWRITE DEFAULT-+-2))
 (339 11 (:REWRITE UPDATE-NTH-OF-UPDATE-NTH-1))
 (336 24 (:DEFINITION UPDATE-NTH))
 (288 6 (:DEFINITION NTH))
 (252 66 (:TYPE-PRESCRIPTION SET-INDICES))
 (233 233 (:REWRITE DEFAULT-+-1))
 (224 22 (:DEFINITION MEMBER-EQUAL))
 (190 95 (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH))
 (152 44 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (96 96 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (95 95 (:TYPE-PRESCRIPTION UPDATE-NTH))
 (86 43 (:TYPE-PRESCRIPTION MAX))
 (85 85 (:LINEAR POSITION-WHEN-MEMBER))
 (85 85 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (66 22 (:DEFINITION CHARACTER-LISTP))
 (56 56 (:TYPE-PRESCRIPTION ZP))
 (44 44 (:REWRITE SUBSETP-MEMBER . 4))
 (44 44 (:REWRITE SUBSETP-MEMBER . 3))
 (44 44 (:REWRITE SUBSETP-MEMBER . 2))
 (44 44 (:REWRITE SUBSETP-MEMBER . 1))
 (37 37 (:TYPE-PRESCRIPTION NFIX))
 (35 35 (:TYPE-PRESCRIPTION NATP))
 (16 16 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-14
 (378 6 (:DEFINITION NTH))
 (322 12 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (257 16 (:REWRITE COUNT-FREE-BLOCKS-ALT-CORRECTNESS-2))
 (234 12 (:REWRITE NTH-UNDER-IFF-1))
 (215 43 (:DEFINITION LEN))
 (136 81 (:REWRITE DEFAULT-+-2))
 (112 8 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-2))
 (101 23 (:REWRITE ZP-OPEN))
 (96 12 (:REWRITE NFIX-WHEN-ZP))
 (81 81 (:REWRITE DEFAULT-+-1))
 (71 61 (:REWRITE DEFAULT-<-2))
 (69 69 (:REWRITE DEFAULT-CDR))
 (65 61 (:REWRITE DEFAULT-<-1))
 (39 27 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (36 12 (:REWRITE NFIX-WHEN-NATP))
 (27 27 (:REWRITE SUBSETP-MEMBER . 4))
 (27 27 (:REWRITE SUBSETP-MEMBER . 3))
 (27 27 (:REWRITE SUBSETP-MEMBER . 2))
 (27 27 (:REWRITE SUBSETP-MEMBER . 1))
 (26 26 (:REWRITE DEFAULT-CAR))
 (20 4 (:DEFINITION BOOLEAN-LISTP))
 (18 6 (:REWRITE FOLD-CONSTS-IN-+))
 (18 6 (:DEFINITION NFIX))
 (18 6 (:DEFINITION NATP))
 (12 12 (:TYPE-PRESCRIPTION NFIX))
 (11 11 (:LINEAR POSITION-WHEN-MEMBER))
 (11 11 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (9 9 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (8 8 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV-CORRECTNESS-1))
 (8 8 (:TYPE-PRESCRIPTION BOUNDED-NAT-LISTP))
 (8 8 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (8 8 (:DEFINITION BOUNDED-NAT-LISTP))
 (6 6 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:DEFINITION NO-DUPLICATESP-EQUAL))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-15
 (115 6 (:REWRITE NTH-UNDER-IFF-1))
 (109 6 (:DEFINITION SUBSETP-EQUAL))
 (92 6 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (90 20 (:REWRITE SUBSETP-MEMBER . 3))
 (86 32 (:REWRITE SUBSETP-MEMBER . 1))
 (50 50 (:REWRITE DEFAULT-CDR))
 (42 42 (:REWRITE DEFAULT-CAR))
 (32 32 (:REWRITE SUBSETP-MEMBER . 2))
 (30 6 (:DEFINITION LEN))
 (29 20 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (28 4 (:REWRITE NFIX-WHEN-ZP))
 (27 27 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (25 20 (:REWRITE DEFAULT-<-2))
 (22 7 (:REWRITE ZP-OPEN))
 (20 20 (:REWRITE SUBSETP-MEMBER . 4))
 (20 20 (:REWRITE DEFAULT-<-1))
 (15 9 (:REWRITE DEFAULT-+-2))
 (14 14 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (12 12 (:REWRITE SUBSETP-TRANS2))
 (12 12 (:REWRITE SUBSETP-TRANS))
 (10 2 (:DEFINITION BOOLEAN-LISTP))
 (9 9 (:REWRITE DEFAULT-+-1))
 (5 5 (:TYPE-PRESCRIPTION ZP))
 (5 5 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (5 5 (:LINEAR POSITION-WHEN-MEMBER))
 (5 5 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (4 4 (:REWRITE NFIX-WHEN-NATP))
 (4 4 (:DEFINITION NO-DUPLICATESP-EQUAL))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-16
 (4726 160 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (3065 107 (:REWRITE COUNT-FREE-BLOCKS-ALT-CORRECTNESS-2))
 (2504 474 (:DEFINITION LEN))
 (2433 152 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-2))
 (2007 92 (:REWRITE NTH-UNDER-IFF-1))
 (1475 924 (:REWRITE DEFAULT-+-2))
 (1262 160 (:REWRITE NFIX-WHEN-ZP))
 (1121 1121 (:REWRITE DEFAULT-CDR))
 (1089 986 (:REWRITE DEFAULT-<-2))
 (1004 986 (:REWRITE DEFAULT-<-1))
 (924 924 (:REWRITE DEFAULT-+-1))
 (812 80 (:DEFINITION BOUNDED-NAT-LISTP))
 (741 741 (:REWRITE DEFAULT-CAR))
 (519 303 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (472 160 (:REWRITE NFIX-WHEN-NATP))
 (439 408 (:REWRITE SUBSETP-MEMBER . 1))
 (408 408 (:REWRITE SUBSETP-MEMBER . 2))
 (348 303 (:REWRITE SUBSETP-MEMBER . 3))
 (303 303 (:REWRITE SUBSETP-MEMBER . 4))
 (228 228 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (225 75 (:DEFINITION NFIX))
 (222 222 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (208 208 (:LINEAR POSITION-WHEN-MEMBER))
 (208 208 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (180 180 (:TYPE-PRESCRIPTION BOUNDED-NAT-LISTP))
 (140 10 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
 (123 123 (:TYPE-PRESCRIPTION NATP))
 (107 107 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV-CORRECTNESS-1))
 (61 5 (:DEFINITION SUBSETP-EQUAL))
 (13 13 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (7 7 (:REWRITE SUBSETP-TRANS2))
 (7 7 (:REWRITE SUBSETP-TRANS))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-17
 (1325 7 (:DEFINITION COUNT-FREE-BLOCKS-ALT))
 (886 32 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (392 21 (:REWRITE COUNT-FREE-BLOCKS-ALT-CORRECTNESS-2))
 (368 72 (:DEFINITION LEN))
 (288 14 (:REWRITE NTH-UNDER-IFF-1))
 (256 32 (:REWRITE NFIX-WHEN-ZP))
 (230 137 (:REWRITE DEFAULT-+-2))
 (216 12 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-2))
 (203 167 (:REWRITE DEFAULT-<-2))
 (173 167 (:REWRITE DEFAULT-<-1))
 (172 172 (:REWRITE DEFAULT-CDR))
 (140 137 (:REWRITE DEFAULT-+-1))
 (100 100 (:REWRITE DEFAULT-CAR))
 (83 44 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (77 44 (:REWRITE SUBSETP-MEMBER . 3))
 (76 4 (:DEFINITION BOUNDED-NAT-LISTP))
 (72 32 (:REWRITE NFIX-WHEN-NATP))
 (56 3 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-4))
 (50 50 (:REWRITE SUBSETP-MEMBER . 2))
 (50 50 (:REWRITE SUBSETP-MEMBER . 1))
 (44 44 (:REWRITE SUBSETP-MEMBER . 4))
 (40 3 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-3))
 (32 32 (:TYPE-PRESCRIPTION ZP))
 (32 32 (:TYPE-PRESCRIPTION NFIX))
 (32 3 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-15))
 (30 10 (:DEFINITION NFIX))
 (29 29 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (28 28 (:TYPE-PRESCRIPTION BOUNDED-NAT-LISTP))
 (25 25 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (25 25 (:LINEAR POSITION-WHEN-MEMBER))
 (25 25 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (25 2 (:DEFINITION SUBSETP-EQUAL))
 (21 7 (:REWRITE FOLD-CONSTS-IN-+))
 (16 16 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (10 10 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION NATP))
 (9 9 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV-CORRECTNESS-1))
 (4 4 (:REWRITE SUBSETP-TRANS2))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-18
 (680 16 (:DEFINITION NTH))
 (386 202 (:REWRITE DEFAULT-+-2))
 (348 28 (:DEFINITION MEMBER-EQUAL))
 (339 40 (:REWRITE NFIX-WHEN-ZP))
 (311 311 (:REWRITE DEFAULT-CDR))
 (268 199 (:REWRITE DEFAULT-<-2))
 (243 47 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (233 12 (:REWRITE NTH-UNDER-IFF-1))
 (226 199 (:REWRITE DEFAULT-<-1))
 (207 202 (:REWRITE DEFAULT-+-1))
 (163 163 (:REWRITE DEFAULT-CAR))
 (80 8 (:DEFINITION NAT-LISTP))
 (63 6 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-4))
 (59 59 (:REWRITE SUBSETP-MEMBER . 2))
 (59 59 (:REWRITE SUBSETP-MEMBER . 1))
 (48 47 (:REWRITE SUBSETP-MEMBER . 3))
 (47 47 (:REWRITE SUBSETP-MEMBER . 4))
 (46 46 (:LINEAR POSITION-WHEN-MEMBER))
 (46 46 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (42 14 (:DEFINITION NFIX))
 (37 6 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-3))
 (35 35 (:TYPE-PRESCRIPTION ZP))
 (28 2 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
 (18 18 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (14 14 (:TYPE-PRESCRIPTION NATP))
 (10 6 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-19
 (2788 34 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (2342 34 (:DEFINITION UNMAKE-BLOCKS))
 (2280 80 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1415 611 (:REWRITE DEFAULT-CDR))
 (1360 40 (:DEFINITION NTH))
 (1088 68 (:REWRITE TAKE-OF-LEN-FREE))
 (952 241 (:REWRITE ZP-OPEN))
 (850 34 (:DEFINITION TAKE))
 (784 93 (:REWRITE NFIX-WHEN-ZP))
 (766 443 (:REWRITE DEFAULT-+-2))
 (753 57 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (733 529 (:REWRITE DEFAULT-<-2))
 (585 529 (:REWRITE DEFAULT-<-1))
 (495 443 (:REWRITE DEFAULT-+-1))
 (414 6 (:DEFINITION INDICES-MARKED-P))
 (398 398 (:REWRITE DEFAULT-CAR))
 (390 16 (:DEFINITION BLOCK-LISTP))
 (370 10 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (287 34 (:DEFINITION BINARY-APPEND))
 (275 275 (:LINEAR POSITION-WHEN-MEMBER))
 (275 275 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (184 46 (:REWRITE COMMUTATIVITY-OF-+))
 (144 6 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (132 12 (:DEFINITION COUNT-FREE-BLOCKS))
 (123 123 (:TYPE-PRESCRIPTION ZP))
 (120 40 (:DEFINITION NFIX))
 (120 40 (:DEFINITION NATP))
 (102 102 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (102 6 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (84 6 (:DEFINITION L3-FS-P))
 (78 16 (:DEFINITION CHARACTER-LISTP))
 (68 68 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (66 6 (:DEFINITION MEMBER-EQUAL))
 (57 57 (:REWRITE DEFAULT-COERCE-2))
 (57 57 (:REWRITE DEFAULT-COERCE-1))
 (48 48 (:TYPE-PRESCRIPTION L3-FS-P))
 (48 12 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (30 6 (:DEFINITION BOOLEAN-LISTP))
 (12 12 (:REWRITE SUBSETP-MEMBER . 4))
 (12 12 (:REWRITE SUBSETP-MEMBER . 3))
 (12 12 (:REWRITE SUBSETP-MEMBER . 2))
 (12 12 (:REWRITE SUBSETP-MEMBER . 1))
 (6 6 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 )
(L4-WRCHS-CORRECTNESS-1-LEMMA-20
 (1379 5 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (1365 7 (:DEFINITION L3-FS-P))
 (793 54 (:DEFINITION LEN))
 (752 8 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (613 18 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (535 186 (:REWRITE DEFAULT-CDR))
 (512 8 (:DEFINITION UNMAKE-BLOCKS))
 (424 18 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (368 14 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (356 9 (:DEFINITION NTH))
 (336 112 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (304 16 (:REWRITE TAKE-OF-LEN-FREE))
 (253 62 (:REWRITE ZP-OPEN))
 (224 8 (:DEFINITION TAKE))
 (194 18 (:REWRITE NFIX-WHEN-ZP))
 (170 167 (:REWRITE DEFAULT-CAR))
 (166 119 (:REWRITE DEFAULT-<-2))
 (152 89 (:REWRITE DEFAULT-+-2))
 (144 16 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (128 119 (:REWRITE DEFAULT-<-1))
 (105 21 (:DEFINITION ASSOC-EQUAL))
 (98 89 (:REWRITE DEFAULT-+-1))
 (79 18 (:REWRITE NFIX-WHEN-NATP))
 (79 1 (:DEFINITION INDICES-MARKED-LISTP))
 (73 1 (:DEFINITION INDICES-MARKED-P))
 (64 64 (:LINEAR POSITION-WHEN-MEMBER))
 (64 64 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (58 2 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (52 9 (:DEFINITION NATP))
 (50 50 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (48 16 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (38 20 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (36 9 (:REWRITE COMMUTATIVITY-OF-+))
 (36 2 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (34 10 (:DEFINITION BINARY-APPEND))
 (32 32 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (30 1 (:DEFINITION NO-DUPLICATES-LISTP))
 (28 1 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-31))
 (27 9 (:DEFINITION NFIX))
 (25 25 (:TYPE-PRESCRIPTION NATP))
 (24 24 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (24 1 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (21 21 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (18 18 (:TYPE-PRESCRIPTION NFIX))
 (18 18 (:REWRITE DEFAULT-COERCE-2))
 (18 18 (:REWRITE DEFAULT-COERCE-1))
 (16 16 (:TYPE-PRESCRIPTION NAT-LISTP))
 (16 16 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (15 1 (:REWRITE L3-FS-P-ASSOC))
 (15 1 (:DEFINITION BLOCK-LISTP))
 (12 12 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (11 1 (:DEFINITION MEMBER-EQUAL))
 (11 1 (:DEFINITION COUNT-FREE-BLOCKS))
 (8 8 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (8 2 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (7 7 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (7 3 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (5 1 (:DEFINITION BOOLEAN-LISTP))
 (3 1 (:DEFINITION CHARACTER-LISTP))
 (2 2 (:REWRITE SUBSETP-MEMBER . 4))
 (2 2 (:REWRITE SUBSETP-MEMBER . 3))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (1 1 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 )
(L4-WRCHS-CORRECTNESS-1
 (35406 408 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (32269 1042 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (25614 13438 (:REWRITE DEFAULT-CDR))
 (25032 408 (:DEFINITION UNMAKE-BLOCKS))
 (19396 521 (:DEFINITION NTH))
 (17549 681 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (16874 12678 (:REWRITE DEFAULT-CAR))
 (14838 490 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (14424 816 (:REWRITE TAKE-OF-LEN-FREE))
 (14404 3466 (:REWRITE ZP-OPEN))
 (12498 779 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (10884 408 (:DEFINITION TAKE))
 (10098 1048 (:REWRITE NFIX-WHEN-ZP))
 (9919 113 (:DEFINITION INDICES-MARKED-P))
 (9836 266 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (9185 6881 (:REWRITE DEFAULT-<-2))
 (9147 5292 (:REWRITE DEFAULT-+-2))
 (8280 322 (:REWRITE DEFAULT-COERCE-3))
 (7340 6881 (:REWRITE DEFAULT-<-1))
 (5751 5292 (:REWRITE DEFAULT-+-1))
 (5733 49 (:DEFINITION SET-INDICES))
 (5273 107 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (4696 266 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (3959 1048 (:REWRITE NFIX-WHEN-NATP))
 (2897 2897 (:LINEAR POSITION-WHEN-MEMBER))
 (2897 2897 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (2595 675 (:DEFINITION BINARY-APPEND))
 (2484 246 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (2445 5 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-21))
 (2183 193 (:DEFINITION MEMBER-EQUAL))
 (1846 36 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (1836 459 (:REWRITE COMMUTATIVITY-OF-+))
 (1770 40 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-17))
 (1644 118 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1605 75 (:DEFINITION BLOCK-LISTP))
 (1590 53 (:DEFINITION NO-DUPLICATES-LISTP))
 (1563 521 (:DEFINITION NFIX))
 (1477 26 (:REWRITE L2-FS-P-ASSOC))
 (1412 492 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (1364 792 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (1305 1305 (:TYPE-PRESCRIPTION NATP))
 (1272 53 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (1243 26 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (1224 1224 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1143 1143 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (1042 1042 (:TYPE-PRESCRIPTION NFIX))
 (1029 1029 (:REWRITE DEFAULT-COERCE-2))
 (987 177 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (987 32 (:DEFINITION L2-FS-P))
 (846 846 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (798 6 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-2))
 (784 784 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (747 747 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (707 707 (:REWRITE DEFAULT-COERCE-1))
 (593 1 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-5))
 (573 51 (:DEFINITION COUNT-FREE-BLOCKS))
 (516 6 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (509 2 (:DEFINITION MEMBER-INTERSECTP-EQUAL))
 (490 49 (:DEFINITION UPDATE-NTH))
 (486 2 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-20))
 (473 473 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (460 460 (:TYPE-PRESCRIPTION NULL))
 (460 460 (:DEFINITION NULL))
 (424 106 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (420 20 (:DEFINITION BOUNDED-NAT-LISTP))
 (406 5 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (386 386 (:REWRITE SUBSETP-MEMBER . 2))
 (386 386 (:REWRITE SUBSETP-MEMBER . 1))
 (360 20 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-3))
 (356 4 (:DEFINITION SUBSETP-EQUAL))
 (329 10 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (315 75 (:DEFINITION CHARACTER-LISTP))
 (300 5 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-2))
 (235 47 (:DEFINITION BOOLEAN-LISTP))
 (205 22 (:REWRITE L3-WRCHS-CORRECTNESS-1))
 (196 196 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (175 1 (:REWRITE INDICES-MARKED-LISTP-OF-BINARY-APPEND))
 (160 20 (:REWRITE SET-INDICES-IN-ALV-CORRECTNESS-4))
 (123 52 (:REWRITE L3-TO-L2-FS-CORRECTNESS-1))
 (106 106 (:REWRITE SUBSETP-MEMBER . 4))
 (106 106 (:REWRITE SUBSETP-MEMBER . 3))
 (72 18 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (70 70 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (66 66 (:TYPE-PRESCRIPTION L3-BOUNDED-FS-P))
 (66 6 (:DEFINITION MIN))
 (63 10 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (60 5 (:DEFINITION TRUE-LIST-LISTP))
 (52 52 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (45 5 (:REWRITE FLATTEN-OF-CONS))
 (38 1 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-26))
 (36 12 (:REWRITE L3-BOUNDED-FS-P-ASSOC))
 (25 10 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (20 20 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (10 10 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (10 10 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (10 10 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (8 8 (:REWRITE SUBSETP-TRANS2))
 (8 8 (:REWRITE SUBSETP-TRANS))
 (6 6 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (5 5 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (2 2 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 )
(L4-WRCHS-RETURNS-DISK-LEMMA-1
 (212 184 (:REWRITE DEFAULT-CAR))
 (194 100 (:REWRITE DEFAULT-+-2))
 (176 162 (:REWRITE DEFAULT-CDR))
 (100 100 (:REWRITE DEFAULT-+-1))
 (54 42 (:REWRITE DEFAULT-<-2))
 (43 42 (:REWRITE DEFAULT-<-1))
 (40 4 (:DEFINITION UPDATE-NTH))
 (38 38 (:LINEAR POSITION-WHEN-MEMBER))
 (38 38 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (27 27 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (22 5 (:REWRITE ZP-OPEN))
 (9 9 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 4 (:TYPE-PRESCRIPTION MAX))
 (8 1 (:REWRITE NFIX-WHEN-ZP))
 (5 1 (:REWRITE NFIX-WHEN-NATP))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 )
(L4-WRCHS-RETURNS-DISK-LEMMA-2
 (2530 164 (:DEFINITION L3-FS-P))
 (1707 81 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (1319 57 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-25))
 (1312 1312 (:TYPE-PRESCRIPTION L3-FS-P))
 (1222 793 (:REWRITE DEFAULT-CDR))
 (987 873 (:REWRITE DEFAULT-CAR))
 (777 259 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (446 30 (:REWRITE L3-FS-P-ASSOC))
 (396 60 (:DEFINITION BINARY-APPEND))
 (300 60 (:DEFINITION LEN))
 (198 132 (:REWRITE DEFAULT-<-2))
 (149 149 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (144 18 (:REWRITE CONSP-OF-APPEND))
 (144 6 (:DEFINITION TRUE-LISTP))
 (132 132 (:REWRITE DEFAULT-<-1))
 (132 12 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (120 60 (:REWRITE DEFAULT-+-2))
 (96 12 (:DEFINITION STRING-LISTP))
 (60 60 (:TYPE-PRESCRIPTION STRING-LISTP))
 (60 60 (:REWRITE DEFAULT-+-1))
 (24 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (24 3 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-3))
 (6 6 (:TYPE-PRESCRIPTION L3-BOUNDED-FS-P))
 )
(L4-WRCHS-RETURNS-DISK
 (3459 110 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (3216 42 (:DEFINITION INDICES-MARKED-P))
 (2783 1081 (:REWRITE DEFAULT-CDR))
 (2618 14 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (2438 29 (:DEFINITION INDICES-MARKED-LISTP))
 (2084 55 (:DEFINITION NTH))
 (1871 16 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-25))
 (1579 369 (:REWRITE ZP-OPEN))
 (1510 13 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-10))
 (1452 484 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1347 947 (:REWRITE DEFAULT-CAR))
 (1325 123 (:REWRITE NFIX-WHEN-ZP))
 (1198 13 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1055 755 (:REWRITE DEFAULT-<-2))
 (936 8 (:DEFINITION SET-INDICES))
 (928 80 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (841 29 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (832 13 (:DEFINITION UNMAKE-BLOCKS))
 (796 454 (:REWRITE DEFAULT-+-2))
 (790 755 (:REWRITE DEFAULT-<-1))
 (720 9 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-19))
 (522 29 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (494 26 (:REWRITE TAKE-OF-LEN-FREE))
 (490 454 (:REWRITE DEFAULT-+-1))
 (364 13 (:DEFINITION TAKE))
 (321 71 (:DEFINITION NATP))
 (281 23 (:DEFINITION COUNT-FREE-BLOCKS))
 (270 30 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (240 80 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (240 48 (:DEFINITION ASSOC-EQUAL))
 (232 232 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (220 220 (:LINEAR POSITION-WHEN-MEMBER))
 (220 220 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (210 210 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (192 192 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (184 42 (:DEFINITION BINARY-APPEND))
 (180 60 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (165 55 (:DEFINITION NFIX))
 (156 12 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (145 145 (:TYPE-PRESCRIPTION INDICES-MARKED-LISTP))
 (144 36 (:REWRITE COMMUTATIVITY-OF-+))
 (135 135 (:TYPE-PRESCRIPTION NATP))
 (128 16 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (116 1 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-2))
 (101 43 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (98 98 (:REWRITE DEFAULT-COERCE-2))
 (98 98 (:REWRITE DEFAULT-COERCE-1))
 (96 12 (:DEFINITION MEMBER-EQUAL))
 (90 30 (:DEFINITION CHARACTER-LISTP))
 (80 8 (:DEFINITION UPDATE-NTH))
 (60 60 (:TYPE-PRESCRIPTION NULL))
 (60 60 (:DEFINITION NULL))
 (39 39 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (35 35 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (33 33 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (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))
 (16 16 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 )
(L4-STAT-AFTER-WRITE-LEMMA-1
 (19342 24 (:DEFINITION L4-WRCHS))
 (15824 13 (:DEFINITION L2-WRCHS))
 (13654 156 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (11817 61 (:DEFINITION L3-TO-L2-FS))
 (11794 48 (:DEFINITION L3-STAT))
 (10916 5199 (:REWRITE DEFAULT-CDR))
 (10832 348 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (10007 7 (:REWRITE L2-STAT-AFTER-WRITE))
 (9492 156 (:DEFINITION UNMAKE-BLOCKS))
 (7881 39 (:REWRITE L3-UNLINK-CORRECTNESS-1-LEMMA-1))
 (7810 5222 (:REWRITE DEFAULT-CAR))
 (7637 291 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (6530 174 (:DEFINITION NTH))
 (6446 204 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (6106 711 (:DEFINITION ASSOC-EQUAL))
 (5849 116 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (5623 347 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (5509 24 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-19))
 (5436 312 (:REWRITE TAKE-OF-LEN-FREE))
 (5229 1327 (:REWRITE ZP-OPEN))
 (4863 16 (:DEFINITION L2-STAT))
 (4449 1309 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (4185 156 (:DEFINITION TAKE))
 (4071 9 (:REWRITE L3-STAT-CORRECTNESS-2))
 (3821 299 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (3509 122 (:REWRITE DEFAULT-COERCE-3))
 (3418 349 (:REWRITE NFIX-WHEN-ZP))
 (3310 1914 (:REWRITE DEFAULT-+-2))
 (3228 2409 (:REWRITE DEFAULT-<-2))
 (2808 24 (:DEFINITION SET-INDICES))
 (2573 2409 (:REWRITE DEFAULT-<-1))
 (2078 1914 (:REWRITE DEFAULT-+-1))
 (1972 9 (:REWRITE L3-STAT-CORRECTNESS-1))
 (1971 8 (:REWRITE L3-READ-AFTER-WRITE-1-LEMMA-2))
 (1834 1834 (:TYPE-PRESCRIPTION ZP))
 (1724 127 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-4))
 (1628 29 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (1588 29 (:REWRITE L2-FS-P-ASSOC))
 (1477 29 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (1428 157 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (1360 112 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (1353 349 (:REWRITE NFIX-WHEN-NATP))
 (1342 120 (:REWRITE L3-FS-P-ASSOC))
 (1328 347 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (1327 101 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1324 18 (:DEFINITION INDICES-MARKED-P))
 (1301 149 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-2))
 (1095 1037 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (1069 29 (:DEFINITION L2-FS-P))
 (1044 36 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (1008 112 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (978 978 (:LINEAR POSITION-WHEN-MEMBER))
 (978 978 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (921 110 (:DEFINITION MEMBER-EQUAL))
 (908 908 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (742 7 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-12))
 (672 224 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (669 623 (:REWRITE L3-STAT-CORRECTNESS-2-LEMMA-1))
 (656 164 (:REWRITE COMMUTATIVITY-OF-+))
 (648 192 (:DEFINITION BINARY-APPEND))
 (648 36 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (603 341 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (567 110 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (537 537 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (522 174 (:DEFINITION NFIX))
 (521 521 (:TYPE-PRESCRIPTION NATP))
 (514 514 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (511 127 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-8))
 (506 506 (:TYPE-PRESCRIPTION NAT-LISTP))
 (468 468 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (426 426 (:REWRITE DEFAULT-COERCE-2))
 (348 348 (:TYPE-PRESCRIPTION NFIX))
 (330 330 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (312 312 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (304 304 (:REWRITE DEFAULT-COERCE-1))
 (240 24 (:DEFINITION UPDATE-NTH))
 (224 224 (:TYPE-PRESCRIPTION NULL))
 (224 224 (:DEFINITION NULL))
 (220 220 (:REWRITE SUBSETP-MEMBER . 2))
 (220 220 (:REWRITE SUBSETP-MEMBER . 1))
 (216 9 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (140 25 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-10))
 (133 1 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-2))
 (104 13 (:REWRITE L3-WRCHS-CORRECTNESS-1))
 (90 8 (:DEFINITION COUNT-FREE-BLOCKS))
 (86 1 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (78 78 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (72 18 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (70 30 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (48 48 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (42 14 (:REWRITE L2-WRCHS-RETURNS-FS))
 (38 2 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (34 2 (:REWRITE L4-LIST-ALL-INDICES-CORRECTNESS-1))
 (32 32 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (26 26 (:TYPE-PRESCRIPTION L3-BOUNDED-FS-P))
 (23 23 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-11))
 (21 7 (:DEFINITION CHARACTER-LISTP))
 (18 18 (:REWRITE SUBSETP-MEMBER . 4))
 (18 18 (:REWRITE SUBSETP-MEMBER . 3))
 (11 1 (:DEFINITION MIN))
 (2 2 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (2 2 (:TYPE-PRESCRIPTION L4-FS-P))
 )
(L4-STAT-AFTER-WRITE
 (76170 84 (:DEFINITION L4-WRCHS))
 (33873 1082 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (29419 13598 (:REWRITE DEFAULT-CDR))
 (23698 272 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (22410 811 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (20866 269 (:DEFINITION INDICES-MARKED-P))
 (20448 13308 (:REWRITE DEFAULT-CAR))
 (20414 541 (:DEFINITION NTH))
 (19232 16 (:DEFINITION L2-WRCHS))
 (18958 580 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (17361 84 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-19))
 (15852 3697 (:REWRITE ZP-OPEN))
 (15218 272 (:DEFINITION UNMAKE-BLOCKS))
 (13449 56 (:DEFINITION L3-STAT))
 (12906 243 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (12676 875 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (12056 1151 (:REWRITE NFIX-WHEN-ZP))
 (11916 926 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (11480 1334 (:DEFINITION ASSOC-EQUAL))
 (9828 84 (:DEFINITION SET-INDICES))
 (9456 48 (:REWRITE L3-UNLINK-CORRECTNESS-1-LEMMA-1))
 (9455 7014 (:REWRITE DEFAULT-<-2))
 (9177 69 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-2))
 (8961 309 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (8146 544 (:REWRITE TAKE-OF-LEN-FREE))
 (8088 153 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-10))
 (7827 4544 (:REWRITE DEFAULT-+-2))
 (7378 7014 (:REWRITE DEFAULT-<-1))
 (7265 272 (:DEFINITION TAKE))
 (5934 69 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (5562 309 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (5476 204 (:REWRITE DEFAULT-COERCE-3))
 (4908 4544 (:REWRITE DEFAULT-+-1))
 (4394 1151 (:REWRITE NFIX-WHEN-NATP))
 (3570 60 (:REWRITE L2-FS-P-ASSOC))
 (3556 60 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (3321 369 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (3177 60 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (2865 875 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (2860 238 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-4))
 (2664 333 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (2664 203 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (2598 2466 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (2591 66 (:DEFINITION L2-FS-P))
 (2452 276 (:DEFINITION MEMBER-EQUAL))
 (2416 218 (:REWRITE L3-FS-P-ASSOC))
 (2376 2376 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (2361 581 (:DEFINITION BINARY-APPEND))
 (2214 738 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (1905 369 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (1810 1810 (:LINEAR POSITION-WHEN-MEMBER))
 (1810 1810 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1752 73 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (1623 541 (:DEFINITION NFIX))
 (1456 364 (:REWRITE COMMUTATIVITY-OF-+))
 (1408 1408 (:TYPE-PRESCRIPTION NATP))
 (1401 1401 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (1392 12 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-25))
 (1362 242 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (1150 92 (:DEFINITION COUNT-FREE-BLOCKS))
 (1088 1088 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1082 1082 (:TYPE-PRESCRIPTION NFIX))
 (1046 1046 (:REWRITE DEFAULT-COERCE-2))
 (1027 439 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (954 954 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (943 238 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-8))
 (842 842 (:REWRITE DEFAULT-COERCE-1))
 (840 84 (:DEFINITION UPDATE-NTH))
 (816 816 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (759 69 (:DEFINITION MIN))
 (738 738 (:TYPE-PRESCRIPTION NULL))
 (738 738 (:DEFINITION NULL))
 (584 146 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (560 560 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (559 14 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-12))
 (552 552 (:REWRITE SUBSETP-MEMBER . 2))
 (552 552 (:REWRITE SUBSETP-MEMBER . 1))
 (303 85 (:DEFINITION CHARACTER-LISTP))
 (206 206 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (168 168 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (146 146 (:REWRITE SUBSETP-MEMBER . 4))
 (146 146 (:REWRITE SUBSETP-MEMBER . 3))
 (138 138 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (128 16 (:REWRITE L3-WRCHS-CORRECTNESS-1))
 (88 88 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (66 22 (:REWRITE L2-WRCHS-RETURNS-FS))
 (32 32 (:TYPE-PRESCRIPTION L3-BOUNDED-FS-P))
 (15 15 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-11))
 )
(L4-READ-AFTER-WRITE-1
 (26900 9577 (:REWRITE DEFAULT-CDR))
 (23454 253 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (20304 622 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (16424 253 (:DEFINITION UNMAKE-BLOCKS))
 (12327 957 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (12296 8744 (:REWRITE DEFAULT-CAR))
 (12147 311 (:DEFINITION NTH))
 (11272 532 (:REWRITE TAKE-OF-LEN-FREE))
 (10802 3129 (:REWRITE ZP-OPEN))
 (10359 3453 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (9094 266 (:DEFINITION TAKE))
 (8263 71 (:DEFINITION SET-INDICES))
 (7928 4532 (:REWRITE DEFAULT-+-2))
 (7291 742 (:REWRITE NFIX-WHEN-ZP))
 (7066 4886 (:REWRITE DEFAULT-<-2))
 (6322 218 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (5243 4886 (:REWRITE DEFAULT-<-1))
 (5122 4532 (:REWRITE DEFAULT-+-1))
 (3924 218 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (3689 957 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (3339 43 (:DEFINITION INDICES-MARKED-LISTP))
 (2995 68 (:REWRITE DEFAULT-COERCE-3))
 (2292 2292 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (2112 2112 (:LINEAR POSITION-WHEN-MEMBER))
 (2112 2112 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1951 177 (:DEFINITION COUNT-FREE-BLOCKS))
 (1907 191 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (1849 471 (:DEFINITION BINARY-APPEND))
 (1846 130 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1809 201 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (1654 34 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (1640 170 (:DEFINITION MEMBER-EQUAL))
 (1438 11 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (1268 1268 (:TYPE-PRESCRIPTION NATP))
 (1212 40 (:DEFINITION NO-DUPLICATES-LISTP))
 (1206 402 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (1157 1157 (:REWRITE DEFAULT-COERCE-2))
 (1148 1148 (:TYPE-PRESCRIPTION NAT-LISTP))
 (1089 1089 (:REWRITE DEFAULT-COERCE-1))
 (968 40 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (958 12 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 1))
 (943 305 (:DEFINITION NFIX))
 (823 50 (:REWRITE L4-WRCHS-RETURNS-DISK))
 (775 775 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (755 755 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (710 71 (:DEFINITION UPDATE-NTH))
 (694 694 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (677 13 (:REWRITE CAR-OF-NTHCDR))
 (664 13 (:REWRITE LEN-OF-NTHCDR))
 (605 17 (:DEFINITION NTHCDR))
 (510 510 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (402 402 (:TYPE-PRESCRIPTION NULL))
 (402 402 (:DEFINITION NULL))
 (393 30 (:REWRITE L4-WRCHS-RETURNS-DISK-LEMMA-2))
 (340 340 (:REWRITE SUBSETP-MEMBER . 2))
 (340 340 (:REWRITE SUBSETP-MEMBER . 1))
 (320 80 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (284 284 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (284 13 (:REWRITE CONSP-OF-TAKE))
 (275 117 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (272 2 (:REWRITE L4-WRCHS-RETURNS-DISK-LEMMA-1))
 (268 268 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (247 26 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (196 13 (:REWRITE CONSP-OF-NTHCDR))
 (144 4 (:REWRITE SET-INDICES-CORRECTNESS-3))
 (141 43 (:DEFINITION CHARACTER-LISTP))
 (80 80 (:REWRITE SUBSETP-MEMBER . 4))
 (80 80 (:REWRITE SUBSETP-MEMBER . 3))
 (65 65 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (48 12 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (41 41 (:REWRITE FOLD-CONSTS-IN-+))
 (34 2 (:REWRITE L4-LIST-ALL-INDICES-CORRECTNESS-1))
 (30 30 (:REWRITE DEFAULT-UNARY-MINUS))
 (12 2 (:REWRITE SET-INDICES-CORRECTNESS-1))
 (8 8 (:TYPE-PRESCRIPTION SET-INDICES))
 (4 4 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (2 2 (:TYPE-PRESCRIPTION L4-FS-P))
 )
(L4-READ-AFTER-WRITE-2
 (3440 4 (:DEFINITION L4-WRCHS))
 (2036 64 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1651 801 (:REWRITE DEFAULT-CDR))
 (1388 15 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1218 32 (:DEFINITION NTH))
 (1192 44 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (1121 15 (:DEFINITION INDICES-MARKED-P))
 (1100 36 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (1004 45 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1002 73 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (986 34 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (944 218 (:REWRITE ZP-OPEN))
 (870 15 (:DEFINITION UNMAKE-BLOCKS))
 (857 657 (:REWRITE DEFAULT-CAR))
 (854 4 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-19))
 (758 80 (:REWRITE NFIX-WHEN-ZP))
 (710 34 (:REWRITE TAKE-OF-LEN-FREE))
 (700 17 (:DEFINITION TAKE))
 (621 11 (:REWRITE DEFAULT-COERCE-3))
 (612 34 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (592 439 (:REWRITE DEFAULT-<-2))
 (522 307 (:REWRITE DEFAULT-+-2))
 (468 4 (:DEFINITION SET-INDICES))
 (466 439 (:REWRITE DEFAULT-<-1))
 (439 45 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (396 132 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (370 8 (:REWRITE L4-WRCHS-RETURNS-DISK))
 (338 307 (:REWRITE DEFAULT-+-1))
 (318 80 (:REWRITE NFIX-WHEN-NATP))
 (266 2 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-2))
 (240 10 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (238 238 (:TYPE-PRESCRIPTION ZP))
 (238 8 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-25))
 (236 6 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-10))
 (215 49 (:DEFINITION BINARY-APPEND))
 (214 23 (:DEFINITION MEMBER-EQUAL))
 (210 17 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (172 2 (:REWRITE L4-WRCHS-CORRECTNESS-1-LEMMA-18))
 (169 13 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (151 13 (:REWRITE L3-FS-P-ASSOC))
 (140 44 (:DEFINITION NFIX))
 (130 26 (:DEFINITION ASSOC-EQUAL))
 (126 14 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (124 124 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (122 122 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (121 121 (:LINEAR POSITION-WHEN-MEMBER))
 (121 121 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (120 2 (:REWRITE CAR-OF-NTHCDR))
 (110 2 (:REWRITE LEN-OF-NTHCDR))
 (106 4 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (91 39 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (84 28 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (83 83 (:TYPE-PRESCRIPTION NATP))
 (80 20 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (78 78 (:TYPE-PRESCRIPTION NFIX))
 (76 4 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (75 75 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (73 73 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (70 6 (:DEFINITION COUNT-FREE-BLOCKS))
 (68 4 (:REWRITE L4-LIST-ALL-INDICES-CORRECTNESS-1))
 (67 67 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (66 66 (:TYPE-PRESCRIPTION NAT-LISTP))
 (66 2 (:DEFINITION NTHCDR))
 (61 61 (:REWRITE DEFAULT-COERCE-2))
 (58 58 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (58 4 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (50 50 (:REWRITE DEFAULT-COERCE-1))
 (46 46 (:REWRITE SUBSETP-MEMBER . 2))
 (46 46 (:REWRITE SUBSETP-MEMBER . 1))
 (40 4 (:DEFINITION UPDATE-NTH))
 (38 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (38 2 (:REWRITE CONSP-OF-NTHCDR))
 (30 30 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (28 28 (:TYPE-PRESCRIPTION NULL))
 (28 28 (:DEFINITION NULL))
 (22 2 (:DEFINITION MIN))
 (20 20 (:REWRITE SUBSETP-MEMBER . 4))
 (20 20 (:REWRITE SUBSETP-MEMBER . 3))
 (14 14 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (14 14 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (12 4 (:DEFINITION CHARACTER-LISTP))
 (12 2 (:REWRITE CONSP-OF-TAKE))
 (10 10 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (8 8 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (8 8 (:TYPE-PRESCRIPTION BOUNDED-NAT-LISTP))
 (6 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 4 (:TYPE-PRESCRIPTION TRUE-LISTP-TAKE))
 (4 4 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (4 4 (:TYPE-PRESCRIPTION L4-FS-P))
 (4 4 (:REWRITE L4-WRCHS-RETURNS-FS))
 (4 4 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 (4 2 (:REWRITE FIX-WHEN-ACL2-NUMBERP))
 (2 2 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-11))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(L4-CREATE
 (605 207 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (260 20 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (178 154 (:REWRITE DEFAULT-CDR))
 (160 20 (:DEFINITION MEMBER-EQUAL))
 (154 10 (:DEFINITION L3-FS-P))
 (129 129 (:REWRITE DEFAULT-CAR))
 (120 21 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (100 100 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (88 47 (:REWRITE DEFAULT-+-2))
 (66 6 (:DEFINITION COUNT-FREE-BLOCKS))
 (53 47 (:REWRITE DEFAULT-+-1))
 (49 21 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (40 40 (:REWRITE SUBSETP-MEMBER . 2))
 (40 40 (:REWRITE SUBSETP-MEMBER . 1))
 (27 9 (:DEFINITION CHARACTER-LISTP))
 (25 6 (:REWRITE NFIX-WHEN-ZP))
 (24 6 (:REWRITE COMMUTATIVITY-OF-+))
 (20 4 (:DEFINITION ASSOC-EQUAL))
 (16 16 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (16 8 (:REWRITE DEFAULT-<-2))
 (16 1 (:REWRITE ZP-OPEN))
 (15 15 (:LINEAR POSITION-WHEN-MEMBER))
 (15 15 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (15 3 (:DEFINITION EQLABLE-ALISTP))
 (14 8 (:REWRITE DEFAULT-<-1))
 (8 8 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (1 1 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 (1 1 (:TYPE-PRESCRIPTION SET-INDICES))
 (1 1 (:REWRITE DEFAULT-COERCE-2))
 (1 1 (:REWRITE DEFAULT-COERCE-1))
 )
(L4-CREATE-RETURNS-FS
 (1977 659 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1380 88 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (625 527 (:REWRITE DEFAULT-CDR))
 (541 516 (:REWRITE DEFAULT-CAR))
 (451 49 (:DEFINITION NAT-LISTP))
 (394 132 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (374 34 (:DEFINITION COUNT-FREE-BLOCKS))
 (272 89 (:DEFINITION NATP))
 (270 154 (:REWRITE DEFAULT-+-2))
 (208 16 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (195 39 (:DEFINITION ASSOC-EQUAL))
 (188 154 (:REWRITE DEFAULT-+-1))
 (187 11 (:REWRITE NFIX-WHEN-ZP))
 (162 14 (:REWRITE ZP-OPEN))
 (158 126 (:REWRITE DEFAULT-<-2))
 (139 126 (:REWRITE DEFAULT-<-1))
 (136 34 (:REWRITE COMMUTATIVITY-OF-+))
 (128 16 (:DEFINITION MEMBER-EQUAL))
 (96 96 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (92 4 (:DEFINITION SET-INDICES))
 (90 18 (:DEFINITION BOOLEAN-LISTP))
 (80 80 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (54 6 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (40 4 (:DEFINITION UPDATE-NTH))
 (36 12 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (34 34 (:REWRITE DEFAULT-COERCE-2))
 (34 34 (:REWRITE DEFAULT-COERCE-1))
 (32 32 (:REWRITE SUBSETP-MEMBER . 2))
 (32 32 (:REWRITE SUBSETP-MEMBER . 1))
 (25 25 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (14 14 (:LINEAR POSITION-WHEN-MEMBER))
 (14 14 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (12 12 (:TYPE-PRESCRIPTION NULL))
 (12 12 (:DEFINITION NULL))
 )
(L4-CREATE-CORRECTNESS-1-LEMMA-1
 (1772 22 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1753 62 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1276 22 (:DEFINITION UNMAKE-BLOCKS))
 (1072 31 (:DEFINITION NTH))
 (879 293 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (832 22 (:REWRITE DEFAULT-COERCE-3))
 (824 764 (:REWRITE DEFAULT-CDR))
 (820 56 (:DEFINITION L3-FS-P))
 (800 143 (:REWRITE ZP-OPEN))
 (760 22 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (704 44 (:REWRITE TAKE-OF-LEN-FREE))
 (693 9 (:DEFINITION INDICES-MARKED-LISTP))
 (665 71 (:REWRITE NFIX-WHEN-ZP))
 (639 9 (:DEFINITION INDICES-MARKED-P))
 (630 618 (:REWRITE DEFAULT-CAR))
 (571 330 (:REWRITE DEFAULT-+-2))
 (550 22 (:DEFINITION TAKE))
 (507 21 (:DEFINITION BLOCK-LISTP))
 (476 368 (:REWRITE DEFAULT-<-2))
 (399 368 (:REWRITE DEFAULT-<-1))
 (362 330 (:REWRITE DEFAULT-+-1))
 (319 11 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (246 22 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (198 11 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (172 172 (:LINEAR POSITION-WHEN-MEMBER))
 (172 172 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (128 32 (:REWRITE COMMUTATIVITY-OF-+))
 (128 16 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (126 54 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (121 33 (:DEFINITION BINARY-APPEND))
 (110 22 (:DEFINITION ASSOC-EQUAL))
 (110 10 (:DEFINITION COUNT-FREE-BLOCKS))
 (104 8 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (102 31 (:DEFINITION NATP))
 (99 21 (:DEFINITION CHARACTER-LISTP))
 (93 31 (:DEFINITION NFIX))
 (92 4 (:DEFINITION SET-INDICES))
 (76 76 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (66 66 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (64 64 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (64 8 (:DEFINITION MEMBER-EQUAL))
 (56 56 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (54 6 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (50 50 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (47 47 (:TYPE-PRESCRIPTION NATP))
 (45 9 (:DEFINITION BOOLEAN-LISTP))
 (40 40 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (40 4 (:DEFINITION UPDATE-NTH))
 (36 12 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (35 35 (:REWRITE DEFAULT-COERCE-2))
 (32 32 (:TYPE-PRESCRIPTION NAT-LISTP))
 (16 16 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (16 16 (:REWRITE SUBSETP-MEMBER . 2))
 (16 16 (:REWRITE SUBSETP-MEMBER . 1))
 (16 16 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (13 13 (:REWRITE DEFAULT-COERCE-1))
 (12 12 (:TYPE-PRESCRIPTION NULL))
 (12 12 (:DEFINITION NULL))
 (9 9 (:TYPE-PRESCRIPTION INDICES-MARKED-P))
 (8 8 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (4 4 (:REWRITE LENGTH-WHEN-STRINGP))
 (2 2 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 )
(L4-CREATE-CORRECTNESS-1
 (6366 76 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (6236 212 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (4158 76 (:DEFINITION UNMAKE-BLOCKS))
 (3802 106 (:DEFINITION NTH))
 (3357 2856 (:REWRITE DEFAULT-CDR))
 (3211 2667 (:REWRITE DEFAULT-CAR))
 (3090 172 (:DEFINITION L3-FS-P))
 (2602 473 (:REWRITE ZP-OPEN))
 (2498 64 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (2441 28 (:DEFINITION INDICES-MARKED-LISTP))
 (2298 238 (:DEFINITION ASSOC-EQUAL))
 (2186 152 (:REWRITE TAKE-OF-LEN-FREE))
 (2134 77 (:REWRITE DEFAULT-COERCE-3))
 (2046 220 (:REWRITE NFIX-WHEN-ZP))
 (1969 76 (:DEFINITION TAKE))
 (1904 74 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (1734 1007 (:REWRITE DEFAULT-+-2))
 (1654 64 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (1585 1263 (:REWRITE DEFAULT-<-2))
 (1357 1263 (:REWRITE DEFAULT-<-1))
 (1116 18 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (1099 1007 (:REWRITE DEFAULT-+-1))
 (958 5 (:REWRITE INDICES-MARKED-LISTP-OF-BINARY-APPEND))
 (597 156 (:DEFINITION NATP))
 (588 144 (:DEFINITION BINARY-APPEND))
 (572 342 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (548 69 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (438 6 (:REWRITE L2-FS-P-ASSOC))
 (432 6 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (405 45 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (374 94 (:REWRITE COMMUTATIVITY-OF-+))
 (372 12 (:DEFINITION NO-DUPLICATES-LISTP))
 (368 74 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (358 358 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (334 334 (:LINEAR POSITION-WHEN-MEMBER))
 (334 334 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (318 106 (:DEFINITION NFIX))
 (296 12 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (270 90 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (266 26 (:DEFINITION MEMBER-EQUAL))
 (245 245 (:TYPE-PRESCRIPTION NAT-LISTP))
 (224 224 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (220 24 (:DEFINITION NAT-LISTP))
 (218 22 (:REWRITE L3-CREATE-CORRECTNESS-1))
 (200 14 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (198 18 (:DEFINITION COUNT-FREE-BLOCKS))
 (192 6 (:DEFINITION L2-FS-P))
 (173 173 (:TYPE-PRESCRIPTION NATP))
 (170 1 (:REWRITE L4-WRCHS-RETURNS-STRICTER-FS-LEMMA-21))
 (168 30 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (162 162 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (115 115 (:REWRITE DEFAULT-COERCE-2))
 (110 110 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (96 24 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (90 90 (:TYPE-PRESCRIPTION NULL))
 (90 90 (:DEFINITION NULL))
 (90 20 (:DEFINITION CHARACTER-LISTP))
 (86 86 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (86 86 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (78 18 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (72 72 (:TYPE-PRESCRIPTION L3-BOUNDED-FS-P))
 (57 57 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (56 56 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (52 52 (:REWRITE SUBSETP-MEMBER . 2))
 (52 52 (:REWRITE SUBSETP-MEMBER . 1))
 (48 48 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
 (46 2 (:DEFINITION SET-INDICES))
 (42 14 (:REWRITE L3-BOUNDED-FS-P-ASSOC))
 (40 10 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (38 38 (:REWRITE DEFAULT-COERCE-1))
 (36 6 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (26 26 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (24 24 (:REWRITE SUBSETP-MEMBER . 4))
 (24 24 (:REWRITE SUBSETP-MEMBER . 3))
 (20 2 (:DEFINITION UPDATE-NTH))
 (18 6 (:REWRITE L3-TO-L2-FS-CORRECTNESS-1))
 (4 1 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (2 2 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 (1 1 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (1 1 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (1 1 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (1 1 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (1 1 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 )
(L4-CREATE-RETURNS-DISK
 (651 217 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (289 229 (:REWRITE DEFAULT-CDR))
 (228 216 (:REWRITE DEFAULT-CAR))
 (204 6 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (168 12 (:DEFINITION L3-FS-P))
 (158 86 (:REWRITE DEFAULT-+-2))
 (151 9 (:REWRITE NFIX-WHEN-ZP))
 (134 12 (:REWRITE ZP-OPEN))
 (110 10 (:DEFINITION COUNT-FREE-BLOCKS))
 (102 6 (:REWRITE L3-FS-P-ASSOC))
 (96 96 (:TYPE-PRESCRIPTION L3-FS-P))
 (96 86 (:REWRITE DEFAULT-+-1))
 (92 4 (:DEFINITION SET-INDICES))
 (91 7 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (75 15 (:DEFINITION ASSOC-EQUAL))
 (56 7 (:DEFINITION MEMBER-EQUAL))
 (54 18 (:DEFINITION CHARACTER-LISTP))
 (54 6 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (53 29 (:REWRITE DEFAULT-<-2))
 (45 9 (:DEFINITION BOOLEAN-LISTP))
 (40 10 (:REWRITE COMMUTATIVITY-OF-+))
 (40 4 (:DEFINITION UPDATE-NTH))
 (38 29 (:REWRITE DEFAULT-<-1))
 (36 12 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (35 35 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (21 21 (:LINEAR POSITION-WHEN-MEMBER))
 (21 21 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (16 16 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (14 14 (:REWRITE SUBSETP-MEMBER . 2))
 (14 14 (:REWRITE SUBSETP-MEMBER . 1))
 (13 13 (:REWRITE DEFAULT-COERCE-2))
 (13 13 (:REWRITE DEFAULT-COERCE-1))
 (12 12 (:TYPE-PRESCRIPTION NULL))
 (12 12 (:DEFINITION NULL))
 (8 8 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (4 4 (:REWRITE LENGTH-WHEN-STRINGP))
 (2 2 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 )
(L4-READ-AFTER-CREATE-1
 (37827 1259 (:DEFINITION BLOCK-LISTP))
 (35288 396 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (34946 1116 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (32887 458 (:REWRITE DEFAULT-COERCE-3))
 (30050 396 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (28908 25088 (:REWRITE DEFAULT-CDR))
 (28848 36 (:DEFINITION L2-CREATE))
 (27453 116 (:DEFINITION L3-TO-L2-FS))
 (24832 22638 (:REWRITE DEFAULT-CAR))
 (22470 396 (:DEFINITION UNMAKE-BLOCKS))
 (20892 558 (:DEFINITION NTH))
 (18110 592 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (17654 2634 (:REWRITE ZP-OPEN))
 (17200 778 (:DEFINITION MEMBER-EQUAL))
 (16356 564 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (16190 396 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (15294 1350 (:REWRITE NFIX-WHEN-ZP))
 (14363 8222 (:REWRITE DEFAULT-+-2))
 (12529 450 (:DEFINITION TAKE))
 (12312 4062 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (10152 564 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (9864 7272 (:REWRITE DEFAULT-<-2))
 (9025 8222 (:REWRITE DEFAULT-+-1))
 (8123 7272 (:REWRITE DEFAULT-<-1))
 (7407 1259 (:DEFINITION CHARACTER-LISTP))
 (6497 233 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (5967 471 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (5464 19 (:DEFINITION L2-STAT))
 (5336 232 (:DEFINITION SET-INDICES))
 (4913 4913 (:LINEAR POSITION-WHEN-MEMBER))
 (4913 4913 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (4883 179 (:REWRITE L4-CREATE-RETURNS-DISK))
 (4472 186 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (4015 365 (:DEFINITION COUNT-FREE-BLOCKS))
 (4008 960 (:DEFINITION BINARY-APPEND))
 (3861 111 (:DEFINITION L2-FS-P))
 (3564 108 (:REWRITE L3-UNLINK-CORRECTNESS-1-LEMMA-1))
 (3224 669 (:DEFINITION NATP))
 (3150 3150 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (2860 2860 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (2826 942 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (2697 176 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-4))
 (2420 55 (:REWRITE L2-FS-P-ASSOC))
 (2320 232 (:DEFINITION UPDATE-NTH))
 (2309 176 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-8))
 (1933 142 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (1752 1752 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (1674 558 (:DEFINITION NFIX))
 (1584 1584 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (1556 1556 (:REWRITE SUBSETP-MEMBER . 2))
 (1556 1556 (:REWRITE SUBSETP-MEMBER . 1))
 (1527 1527 (:REWRITE DEFAULT-COERCE-2))
 (1488 372 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (1456 624 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (1412 43 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-2))
 (1339 1069 (:REWRITE DEFAULT-COERCE-1))
 (1225 55 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (1188 1188 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1146 45 (:REWRITE THEN-SUBSEQ-SAME-2))
 (1146 45 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (1083 54 (:REWRITE CONSP-OF-TAKE))
 (1042 33 (:REWRITE L3-TO-L2-FS-CORRECTNESS-1))
 (1031 1006 (:REWRITE L3-STAT-CORRECTNESS-2-LEMMA-1))
 (942 942 (:TYPE-PRESCRIPTION NULL))
 (942 942 (:DEFINITION NULL))
 (708 45 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (685 55 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (650 25 (:REWRITE L4-CREATE-CORRECTNESS-1-LEMMA-1))
 (644 644 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (558 558 (:TYPE-PRESCRIPTION NATP))
 (536 536 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (372 372 (:REWRITE SUBSETP-MEMBER . 4))
 (372 372 (:REWRITE SUBSETP-MEMBER . 3))
 (333 111 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (330 11 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-1))
 (246 36 (:REWRITE L3-CREATE-CORRECTNESS-1))
 (207 7 (:REWRITE L3-STAT-CORRECTNESS-2))
 (207 7 (:REWRITE L3-STAT-CORRECTNESS-1))
 (72 24 (:REWRITE L2-CREATE-RETURNS-FS))
 (60 60 (:TYPE-PRESCRIPTION L3-BOUNDED-FS-P))
 (38 38 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (9 1 (:REWRITE L3-RDCHS-CORRECTNESS-1-LEMMA-1))
 (7 7 (:REWRITE INDICES-MARKED-P-CORRECTNESS-1))
 )
(L4-READ-AFTER-CREATE-2
 (65520 360 (:DEFINITION L4-CREATE))
 (53862 614 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (53204 1810 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (46766 33120 (:REWRITE DEFAULT-CDR))
 (40623 31725 (:REWRITE DEFAULT-CAR))
 (35677 783 (:DEFINITION TAKE))
 (35329 1566 (:REWRITE TAKE-OF-LEN-FREE))
 (34766 614 (:DEFINITION UNMAKE-BLOCKS))
 (34328 717 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (32601 905 (:DEFINITION NTH))
 (31450 6009 (:REWRITE ZP-OPEN))
 (31251 2409 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (30405 3897 (:DEFINITION ASSOC-EQUAL))
 (29145 28 (:DEFINITION L2-CREATE))
 (28929 3350 (:REWRITE NFIX-WHEN-ZP))
 (21030 13155 (:REWRITE DEFAULT-+-2))
 (17803 783 (:REWRITE DEFAULT-COERCE-3))
 (17168 12957 (:REWRITE DEFAULT-<-2))
 (16836 84 (:REWRITE L3-UNLINK-CORRECTNESS-1-LEMMA-1))
 (14616 614 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (14335 12957 (:REWRITE DEFAULT-<-1))
 (14261 13155 (:REWRITE DEFAULT-+-1))
 (13680 360 (:REWRITE FIND-N-FREE-BLOCKS-CORRECTNESS-2))
 (11604 887 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (10647 263 (:DEFINITION L2-FS-P))
 (9762 3350 (:REWRITE NFIX-WHEN-NATP))
 (9611 871 (:REWRITE L3-FS-P-ASSOC))
 (9512 328 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (9509 173 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (9305 173 (:REWRITE L2-FS-P-ASSOC))
 (8946 163 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (8836 122 (:DEFINITION INDICES-MARKED-P))
 (8677 169 (:REWRITE CAR-OF-NTHCDR))
 (8281 168 (:REWRITE LEN-OF-NTHCDR))
 (8280 360 (:DEFINITION SET-INDICES))
 (8159 977 (:DEFINITION MEMBER-EQUAL))
 (7640 173 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (7470 338 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (7409 1292 (:REWRITE DEFAULT-COERCE-1))
 (7236 804 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (6813 63 (:REWRITE L4-CREATE-CORRECTNESS-1-LEMMA-1))
 (5997 511 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-4))
 (5904 328 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (5577 169 (:DEFINITION NTHCDR))
 (5466 614 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (4824 1608 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (4548 4548 (:LINEAR POSITION-WHEN-MEMBER))
 (4548 4548 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (4525 4525 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (4301 391 (:DEFINITION COUNT-FREE-BLOCKS))
 (3791 603 (:REWRITE L3-STAT-CORRECTNESS-1-LEMMA-3))
 (3693 3693 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
 (3600 360 (:DEFINITION UPDATE-NTH))
 (3492 804 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (3482 942 (:DEFINITION BINARY-APPEND))
 (3245 2719 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (3211 338 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (3081 899 (:DEFINITION NFIX))
 (2491 169 (:REWRITE CONSP-OF-NTHCDR))
 (2396 614 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (2222 2222 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
 (2160 90 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (2147 2147 (:TYPE-PRESCRIPTION NFIX))
 (2075 2075 (:REWRITE DEFAULT-COERCE-2))
 (1954 1954 (:REWRITE SUBSETP-MEMBER . 2))
 (1954 1954 (:REWRITE SUBSETP-MEMBER . 1))
 (1942 511 (:REWRITE L3-WRCHS-CORRECTNESS-1-LEMMA-8))
 (1842 1842 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1800 360 (:DEFINITION MIN))
 (1690 724 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (1608 1608 (:TYPE-PRESCRIPTION NULL))
 (1608 1608 (:DEFINITION NULL))
 (1518 1518 (:TYPE-PRESCRIPTION NATP))
 (1228 1228 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (1228 1228 (:TYPE-PRESCRIPTION NAT-LISTP))
 (1228 1228 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (845 845 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (840 168 (:REWRITE CONSP-OF-TAKE))
 (751 751 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
 (720 720 (:TYPE-PRESCRIPTION FIND-N-FREE-BLOCKS))
 (720 180 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (614 614 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (331 331 (:REWRITE DEFAULT-UNARY-MINUS))
 (290 290 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (264 88 (:DEFINITION CHARACTER-LISTP))
 (217 28 (:REWRITE L3-CREATE-CORRECTNESS-1))
 (180 180 (:REWRITE SUBSETP-MEMBER . 4))
 (180 180 (:REWRITE SUBSETP-MEMBER . 3))
 (163 163 (:REWRITE FOLD-CONSTS-IN-+))
 (111 68 (:REWRITE L2-CREATE-RETURNS-FS))
 (54 54 (:TYPE-PRESCRIPTION L3-BOUNDED-FS-P))
 (1 1 (:REWRITE L3-READ-AFTER-WRITE-1-LEMMA-2))
 )
(L4-UNLINK
 (312 124 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (94 6 (:DEFINITION L3-FS-P))
 (52 11 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 2))
 (50 50 (:REWRITE DEFAULT-CAR))
 (44 44 (:REWRITE DEFAULT-CDR))
 (35 15 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (26 2 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (16 2 (:DEFINITION MEMBER-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (10 2 (:DEFINITION ASSOC-EQUAL))
 (5 1 (:DEFINITION EQLABLE-ALISTP))
 (4 4 (:REWRITE SUBSETP-MEMBER . 2))
 (4 4 (:REWRITE SUBSETP-MEMBER . 1))
 (1 1 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV))
 )
(L4-UNLINK-RETURNS-FS
 (588 196 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (237 237 (:REWRITE DEFAULT-CAR))
 (160 32 (:DEFINITION ASSOC-EQUAL))
 (155 155 (:REWRITE DEFAULT-CDR))
 (130 10 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (108 12 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (107 45 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (80 10 (:DEFINITION MEMBER-EQUAL))
 (72 24 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (50 50 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (24 24 (:TYPE-PRESCRIPTION NULL))
 (24 24 (:DEFINITION NULL))
 (20 20 (:REWRITE SUBSETP-MEMBER . 2))
 (20 20 (:REWRITE SUBSETP-MEMBER . 1))
 )
(L4-UNLINK-CORRECTNESS-1
 (1746 60 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1722 21 (:DEFINITION FETCH-BLOCKS-BY-INDICES))
 (1218 21 (:DEFINITION UNMAKE-BLOCKS))
 (1143 381 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1038 30 (:DEFINITION NTH))
 (923 923 (:REWRITE DEFAULT-CDR))
 (918 918 (:REWRITE DEFAULT-CAR))
 (870 30 (:DEFINITION L4-COLLECT-ALL-INDEX-LISTS))
 (765 153 (:DEFINITION LEN))
 (672 42 (:REWRITE TAKE-OF-LEN-FREE))
 (666 132 (:REWRITE ZP-OPEN))
 (657 9 (:DEFINITION INDICES-MARKED-P))
 (540 30 (:DEFINITION L4-REGULAR-FILE-ENTRY-P))
 (525 21 (:REWRITE DEFAULT-COERCE-3))
 (525 21 (:DEFINITION TAKE))
 (498 60 (:REWRITE NFIX-WHEN-ZP))
 (462 21 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
 (420 246 (:REWRITE DEFAULT-+-2))
 (414 333 (:REWRITE DEFAULT-<-2))
 (354 333 (:REWRITE DEFAULT-<-1))
 (295 59 (:DEFINITION ASSOC-EQUAL))
 (270 9 (:DEFINITION NO-DUPLICATES-LISTP))
 (267 246 (:REWRITE DEFAULT-+-1))
 (243 27 (:DEFINITION MEMBER-EQUAL))
 (234 26 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (234 18 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (216 9 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (213 51 (:DEFINITION BINARY-APPEND))
 (189 60 (:REWRITE NFIX-WHEN-NATP))
 (168 21 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-2))
 (156 52 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (144 144 (:LINEAR POSITION-WHEN-MEMBER))
 (144 144 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (135 9 (:DEFINITION BLOCK-LISTP))
 (132 132 (:TYPE-PRESCRIPTION L4-COLLECT-ALL-INDEX-LISTS))
 (99 99 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (99 30 (:DEFINITION NATP))
 (90 30 (:DEFINITION NFIX))
 (84 84 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-1))
 (84 21 (:REWRITE COMMUTATIVITY-OF-+))
 (72 18 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (66 28 (:REWRITE L3-REGULAR-FILE-ENTRY-P-CORRECTNESS-3 . 1))
 (63 63 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (63 21 (:REWRITE FETCH-BLOCKS-BY-INDICES-CORRECTNESS-1))
 (60 60 (:TYPE-PRESCRIPTION NFIX))
 (54 54 (:REWRITE SUBSETP-MEMBER . 2))
 (54 54 (:REWRITE SUBSETP-MEMBER . 1))
 (52 52 (:TYPE-PRESCRIPTION NULL))
 (52 52 (:DEFINITION NULL))
 (51 51 (:TYPE-PRESCRIPTION NATP))
 (50 10 (:DEFINITION BOOLEAN-LISTP))
 (42 42 (:TYPE-PRESCRIPTION UNMAKE-BLOCKS))
 (42 42 (:TYPE-PRESCRIPTION NAT-LISTP))
 (42 42 (:TYPE-PRESCRIPTION FETCH-BLOCKS-BY-INDICES))
 (27 9 (:DEFINITION CHARACTER-LISTP))
 (21 21 (:TYPE-PRESCRIPTION FEASIBLE-FILE-LENGTH-P))
 (21 21 (:REWRITE DEFAULT-COERCE-2))
 (18 18 (:REWRITE SUBSETP-MEMBER . 4))
 (18 18 (:REWRITE SUBSETP-MEMBER . 3))
 (9 9 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 )