(L2-FS-P
 (846 388 (:REWRITE DEFAULT-+-2))
 (539 388 (:REWRITE DEFAULT-+-1))
 (280 70 (:DEFINITION INTEGER-ABS))
 (256 32 (:REWRITE LENGTH-WHEN-STRINGP))
 (160 32 (:DEFINITION LEN))
 (119 92 (:REWRITE DEFAULT-<-2))
 (116 92 (:REWRITE DEFAULT-<-1))
 (70 70 (:REWRITE DEFAULT-UNARY-MINUS))
 (36 36 (:REWRITE DEFAULT-REALPART))
 (36 36 (:REWRITE DEFAULT-NUMERATOR))
 (36 36 (:REWRITE DEFAULT-IMAGPART))
 (36 36 (:REWRITE DEFAULT-DENOMINATOR))
 (32 32 (:TYPE-PRESCRIPTION LEN))
 (32 32 (:REWRITE DEFAULT-COERCE-2))
 (32 32 (:REWRITE DEFAULT-COERCE-1))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L2-TO-L1-FS
 (199 92 (:REWRITE DEFAULT-+-2))
 (129 92 (:REWRITE DEFAULT-+-1))
 (72 18 (:DEFINITION INTEGER-ABS))
 (72 9 (:REWRITE LENGTH-WHEN-STRINGP))
 (45 9 (:DEFINITION LEN))
 (35 35 (:REWRITE DEFAULT-CAR))
 (34 26 (:REWRITE DEFAULT-<-2))
 (30 26 (: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))
 )
(L2-TO-L1-FS-CORRECTNESS-1
 (320 320 (:REWRITE DEFAULT-CAR))
 (197 197 (:REWRITE DEFAULT-CDR))
 (9 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE DEFAULT-<-1))
 )
(ALISTP-L2-FS-P
 (150 150 (:REWRITE DEFAULT-CAR))
 (112 6 (:REWRITE ALISTP-L1-FS-P))
 (105 105 (:REWRITE DEFAULT-CDR))
 (96 9 (:DEFINITION L1-FS-P))
 (59 59 (:TYPE-PRESCRIPTION L1-FS-P))
 (6 6 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE DEFAULT-<-1))
 )
(L2-FS-P-ASSOC
 (1243 1243 (:REWRITE DEFAULT-CAR))
 (101 101 (:REWRITE DEFAULT-<-2))
 (101 101 (:REWRITE DEFAULT-<-1))
 )
(L2-STAT
 (49501 16505 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (367 66 (:REWRITE L2-FS-P-ASSOC))
 (231 225 (:REWRITE DEFAULT-<-1))
 (225 225 (:REWRITE DEFAULT-<-2))
 (78 6 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (48 6 (:DEFINITION MEMBER-EQUAL))
 (30 30 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (12 12 (:REWRITE SUBSETP-MEMBER . 2))
 (12 12 (:REWRITE SUBSETP-MEMBER . 1))
 (6 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 1 (:DEFINITION EQLABLE-ALISTP))
 )
(L2-STAT-CORRECTNESS-1-LEMMA-1
 (740 740 (:REWRITE DEFAULT-CAR))
 (246 246 (:REWRITE DEFAULT-CDR))
 (9 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE DEFAULT-<-1))
 )
(L2-STAT-CORRECTNESS-1-LEMMA-3
 (3796 3796 (:REWRITE DEFAULT-CAR))
 (391 53 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-1))
 (316 28 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (192 24 (:DEFINITION MEMBER-EQUAL))
 (120 120 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (49 43 (:REWRITE DEFAULT-<-1))
 (48 48 (:REWRITE SUBSETP-MEMBER . 2))
 (48 48 (:REWRITE SUBSETP-MEMBER . 1))
 (43 43 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L2-STAT-CORRECTNESS-1-LEMMA-4
 (1748 512 (:REWRITE DEFAULT-CDR))
 (1703 974 (:REWRITE DEFAULT-CAR))
 (221 31 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-3))
 (167 31 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-1))
 (15 15 (:REWRITE DEFAULT-<-2))
 (15 15 (:REWRITE DEFAULT-<-1))
 )
(L2-STAT-CORRECTNESS-1-LEMMA-5
 (11982 3994 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1662 1068 (:REWRITE DEFAULT-CDR))
 (249 45 (:REWRITE L2-FS-P-ASSOC))
 (116 116 (:REWRITE DEFAULT-<-2))
 (116 116 (:REWRITE DEFAULT-<-1))
 )
(L2-STAT-CORRECTNESS-1
 (2487 829 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1017 201 (:DEFINITION ASSOC-EQUAL))
 (460 34 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (416 32 (:DEFINITION L2-FS-P))
 (290 34 (:DEFINITION MEMBER-EQUAL))
 (183 15 (:REWRITE L1-READ-AFTER-WRITE-2-LEMMA-2))
 (170 170 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (68 68 (:REWRITE SUBSETP-MEMBER . 2))
 (68 68 (:REWRITE SUBSETP-MEMBER . 1))
 (41 41 (:REWRITE DEFAULT-<-2))
 (41 41 (:REWRITE DEFAULT-<-1))
 (8 8 (:REWRITE L2-TO-L1-FS-CORRECTNESS-1))
 (8 1 (:REWRITE L2-FS-P-ASSOC))
 (4 4 (:REWRITE CAR-CONS))
 (2 2 (:REWRITE CDR-CONS))
 )
(L2-STAT-CORRECTNESS-2-LEMMA-2
 (22 22 (:REWRITE DEFAULT-CAR))
 (12 12 (:REWRITE DEFAULT-CDR))
 )
(L2-STAT-CORRECTNESS-2
 (2769 923 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1400 274 (:DEFINITION ASSOC-EQUAL))
 (743 53 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (478 53 (:DEFINITION MEMBER-EQUAL))
 (265 265 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (209 23 (:REWRITE L1-READ-AFTER-WRITE-2-LEMMA-2))
 (106 106 (:REWRITE SUBSETP-MEMBER . 2))
 (106 106 (:REWRITE SUBSETP-MEMBER . 1))
 (65 65 (:REWRITE DEFAULT-<-2))
 (65 65 (:REWRITE DEFAULT-<-1))
 (11 11 (:REWRITE CAR-CONS))
 (8 8 (:TYPE-PRESCRIPTION L1-FS-P))
 (8 8 (:REWRITE L2-TO-L1-FS-CORRECTNESS-1))
 (8 1 (:REWRITE L2-FS-P-ASSOC))
 (6 6 (:REWRITE CDR-CONS))
 )
(L2-STAT-OF-STAT
 (746 246 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (230 218 (:REWRITE DEFAULT-CAR))
 (180 13 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (163 31 (:DEFINITION ASSOC-EQUAL))
 (162 140 (:REWRITE DEFAULT-CDR))
 (115 13 (:DEFINITION MEMBER-EQUAL))
 (65 65 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (65 5 (:DEFINITION L2-FS-P))
 (26 26 (:REWRITE SUBSETP-MEMBER . 2))
 (26 26 (:REWRITE SUBSETP-MEMBER . 1))
 (15 5 (:DEFINITION NATP))
 (8 8 (:REWRITE CONSP-OF-APPEND))
 (5 5 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-<-1))
 (4 1 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (2 1 (:DEFINITION STRING-LISTP))
 (1 1 (:TYPE-PRESCRIPTION STRING-LISTP))
 )
(L2-RDCHS
 (31 1 (:DEFINITION L2-STAT))
 (25 15 (:REWRITE DEFAULT-<-1))
 (20 18 (:REWRITE DEFAULT-+-2))
 (18 18 (:REWRITE DEFAULT-+-1))
 (15 15 (:REWRITE DEFAULT-<-2))
 (13 1 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (13 1 (:DEFINITION L2-FS-P))
 (11 11 (:REWRITE DEFAULT-CDR))
 (11 11 (:REWRITE DEFAULT-CAR))
 (10 2 (:DEFINITION LEN))
 (8 1 (:DEFINITION MEMBER-EQUAL))
 (6 2 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (5 5 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (5 1 (:DEFINITION ASSOC-EQUAL))
 (3 1 (:DEFINITION SYMBOL-LISTP))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 (2 2 (:REWRITE SUBSETP-MEMBER . 2))
 (2 2 (:REWRITE SUBSETP-MEMBER . 1))
 (2 2 (:REWRITE DEFAULT-COERCE-2))
 (2 2 (:REWRITE DEFAULT-COERCE-1))
 )
(L2-RDCHS-CORRECTNESS-1-LEMMA-1
 (2043 681 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1035 1035 (:REWRITE DEFAULT-CAR))
 (835 167 (:DEFINITION ASSOC-EQUAL))
 (646 547 (:REWRITE DEFAULT-CDR))
 (351 27 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (216 27 (:DEFINITION MEMBER-EQUAL))
 (186 16 (:REWRITE L1-READ-AFTER-WRITE-2-LEMMA-2))
 (135 135 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (132 8 (:REWRITE L2-STAT-CORRECTNESS-1))
 (84 21 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-4))
 (54 54 (:REWRITE SUBSETP-MEMBER . 2))
 (54 54 (:REWRITE SUBSETP-MEMBER . 1))
 (22 22 (:REWRITE DEFAULT-<-2))
 (22 22 (:REWRITE DEFAULT-<-1))
 (8 1 (:REWRITE L2-FS-P-ASSOC))
 (5 5 (:TYPE-PRESCRIPTION L1-FS-P))
 (5 5 (:REWRITE L2-TO-L1-FS-CORRECTNESS-1))
 )
(L2-RDCHS-CORRECTNESS-1-LEMMA-2
 (14 14 (:REWRITE DEFAULT-CAR))
 (14 2 (:DEFINITION L2-TO-L1-FS))
 (10 10 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE L2-STAT-CORRECTNESS-2-LEMMA-2))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 )
(L2-RDCHS-CORRECTNESS-1
 (1650 550 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (983 983 (:REWRITE DEFAULT-CAR))
 (909 666 (:REWRITE DEFAULT-CDR))
 (775 155 (:DEFINITION ASSOC-EQUAL))
 (715 55 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (573 5 (:DEFINITION TAKE))
 (442 10 (:REWRITE TAKE-OF-LEN-FREE))
 (440 55 (:DEFINITION MEMBER-EQUAL))
 (390 53 (:DEFINITION LEN))
 (275 275 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (259 5 (:REWRITE CAR-OF-NTHCDR))
 (226 42 (:REWRITE NFIX-WHEN-ZP))
 (224 32 (:DEFINITION L2-TO-L1-FS))
 (224 10 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (206 10 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (200 4 (:REWRITE LEN-OF-NTHCDR))
 (183 146 (:REWRITE DEFAULT-<-2))
 (174 117 (:REWRITE DEFAULT-+-2))
 (168 146 (:REWRITE DEFAULT-<-1))
 (165 5 (:DEFINITION NTHCDR))
 (157 51 (:REWRITE ZP-OPEN))
 (155 5 (:DEFINITION NTH))
 (121 117 (:REWRITE DEFAULT-+-1))
 (110 110 (:REWRITE SUBSETP-MEMBER . 2))
 (110 110 (:REWRITE SUBSETP-MEMBER . 1))
 (95 10 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (84 42 (:REWRITE NFIX-WHEN-NATP))
 (79 16 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-4))
 (74 5 (:REWRITE CONSP-OF-NTHCDR))
 (73 73 (:LINEAR POSITION-WHEN-MEMBER))
 (73 73 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (66 24 (:REWRITE L1-READ-AFTER-WRITE-2-LEMMA-2))
 (38 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (33 5 (:REWRITE DEFAULT-COERCE-3))
 (30 30 (:REWRITE DEFAULT-COERCE-2))
 (30 25 (:REWRITE DEFAULT-COERCE-1))
 (25 25 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (20 4 (:REWRITE CONSP-OF-TAKE))
 (19 19 (:TYPE-PRESCRIPTION NFIX))
 (14 2 (:DEFINITION NFIX))
 (6 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:TYPE-PRESCRIPTION L1-FS-P))
 (2 2 (:REWRITE L2-TO-L1-FS-CORRECTNESS-1))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(L2-UNLINK
 (31693 10569 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (52 4 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (48 45 (:REWRITE DEFAULT-<-1))
 (45 45 (:REWRITE DEFAULT-<-2))
 (32 4 (:DEFINITION MEMBER-EQUAL))
 (20 20 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L2-WRCHS
 (613 209 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (143 11 (:DEFINITION L2-FS-P))
 (101 101 (:REWRITE DEFAULT-CAR))
 (83 83 (:REWRITE DEFAULT-CDR))
 (52 4 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (45 9 (:DEFINITION ASSOC-EQUAL))
 (32 4 (:DEFINITION MEMBER-EQUAL))
 (21 21 (:REWRITE DEFAULT-<-2))
 (21 21 (:REWRITE DEFAULT-<-1))
 (20 20 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (10 2 (:DEFINITION EQLABLE-ALISTP))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE SUBSETP-MEMBER . 1))
 (8 1 (:REWRITE L2-FS-P-ASSOC))
 (1 1 (:REWRITE DEFAULT-COERCE-2))
 (1 1 (:REWRITE DEFAULT-COERCE-1))
 )
(L2-WRCHS-RETURNS-FS-LEMMA-2
 (489 489 (:REWRITE DEFAULT-CAR))
 (380 380 (:REWRITE DEFAULT-CDR))
 (156 52 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (58 57 (:REWRITE DEFAULT-<-1))
 (57 57 (:REWRITE DEFAULT-<-2))
 (52 52 (:TYPE-PRESCRIPTION NULL))
 (52 52 (:DEFINITION NULL))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L2-WRCHS-RETURNS-FS-LEMMA-3
 (75 25 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (15 3 (:DEFINITION ASSOC-EQUAL))
 (13 13 (:REWRITE DEFAULT-CAR))
 (13 1 (:DEFINITION L2-FS-P))
 (8 8 (:REWRITE DEFAULT-CDR))
 (3 1 (:DEFINITION NATP))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(L2-WRCHS-RETURNS-FS-LEMMA-4
 (20535 6845 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1916 1160 (:REWRITE DEFAULT-CDR))
 (145 115 (:REWRITE DEFAULT-<-1))
 (115 115 (:REWRITE DEFAULT-<-2))
 (30 30 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L2-WRCHS-RETURNS-FS-LEMMA-5
 (1992 664 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (109 109 (:REWRITE DEFAULT-CDR))
 (9 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE DEFAULT-<-1))
 )
(L2-WRCHS-RETURNS-FS
 (849 283 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (464 461 (:REWRITE DEFAULT-CAR))
 (354 30 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (322 319 (:REWRITE DEFAULT-CDR))
 (270 54 (:DEFINITION ASSOC-EQUAL))
 (264 60 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (262 19 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (167 19 (:DEFINITION MEMBER-EQUAL))
 (95 95 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (72 9 (:DEFINITION LEN))
 (57 57 (:TYPE-PRESCRIPTION NULL))
 (57 57 (:DEFINITION NULL))
 (45 9 (:REWRITE DEFAULT-COERCE-3))
 (38 38 (:REWRITE SUBSETP-MEMBER . 2))
 (38 38 (:REWRITE SUBSETP-MEMBER . 1))
 (32 4 (:REWRITE L2-FS-P-ASSOC))
 (23 23 (:REWRITE DEFAULT-<-2))
 (23 23 (:REWRITE DEFAULT-<-1))
 (19 19 (:REWRITE DEFAULT-COERCE-2))
 (18 18 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (18 9 (:REWRITE DEFAULT-+-2))
 (15 15 (:TYPE-PRESCRIPTION L2-WRCHS))
 (11 4 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (10 10 (:REWRITE DEFAULT-COERCE-1))
 (9 9 (:REWRITE DEFAULT-+-1))
 )
(L2-UNLINK-RETURNS-FS
 (366 122 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (131 131 (:REWRITE DEFAULT-CAR))
 (96 96 (:REWRITE DEFAULT-CDR))
 (78 6 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (65 13 (:DEFINITION ASSOC-EQUAL))
 (54 6 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (48 6 (:DEFINITION MEMBER-EQUAL))
 (36 12 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (30 30 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (14 14 (:REWRITE DEFAULT-<-2))
 (14 14 (:REWRITE DEFAULT-<-1))
 (12 12 (:TYPE-PRESCRIPTION NULL))
 (12 12 (:REWRITE SUBSETP-MEMBER . 2))
 (12 12 (:REWRITE SUBSETP-MEMBER . 1))
 (12 12 (:DEFINITION NULL))
 )
(L2-WRCHS-CORRECTNESS-1-LEMMA-1
 (424 168 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (128 128 (:TYPE-PRESCRIPTION NULL))
 (128 128 (:DEFINITION NULL))
 (26 24 (:REWRITE DEFAULT-<-1))
 (24 24 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(L2-WRCHS-CORRECTNESS-1-LEMMA-2
 (299 299 (:REWRITE DEFAULT-CAR))
 (185 185 (:REWRITE DEFAULT-CDR))
 (11 11 (:REWRITE DEFAULT-<-2))
 (11 11 (:REWRITE DEFAULT-<-1))
 )
(L2-WRCHS-CORRECTNESS-1
 (1594 1561 (:REWRITE DEFAULT-CAR))
 (1371 457 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1106 211 (:DEFINITION ASSOC-EQUAL))
 (1094 921 (:REWRITE DEFAULT-CDR))
 (867 87 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (574 174 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (570 39 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (375 39 (:DEFINITION MEMBER-EQUAL))
 (195 195 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (155 155 (:TYPE-PRESCRIPTION NULL))
 (155 155 (:DEFINITION NULL))
 (144 18 (:DEFINITION LEN))
 (122 26 (:REWRITE DEFAULT-COERCE-3))
 (78 78 (:REWRITE SUBSETP-MEMBER . 2))
 (78 78 (:REWRITE SUBSETP-MEMBER . 1))
 (69 63 (:TYPE-PRESCRIPTION L2-WRCHS))
 (58 9 (:REWRITE L2-FS-P-ASSOC))
 (54 54 (:REWRITE DEFAULT-COERCE-2))
 (48 16 (:DEFINITION NATP))
 (42 42 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (36 18 (:REWRITE DEFAULT-+-2))
 (28 28 (:REWRITE DEFAULT-COERCE-1))
 (18 18 (:REWRITE DEFAULT-+-1))
 (16 16 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE DEFAULT-<-1))
 (16 9 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 )
(L2-CREATE
 (532 182 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (182 14 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (117 9 (:DEFINITION L2-FS-P))
 (112 14 (:DEFINITION MEMBER-EQUAL))
 (99 99 (:REWRITE DEFAULT-CAR))
 (84 84 (:REWRITE DEFAULT-CDR))
 (70 70 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (45 9 (:DEFINITION ASSOC-EQUAL))
 (28 28 (:REWRITE SUBSETP-MEMBER . 2))
 (28 28 (:REWRITE SUBSETP-MEMBER . 1))
 (27 9 (:DEFINITION NATP))
 (10 2 (:DEFINITION EQLABLE-ALISTP))
 (9 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE DEFAULT-<-1))
 (8 1 (:REWRITE L2-FS-P-ASSOC))
 (3 3 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 )
(L2-CREATE-RETURNS-FS
 (1173 391 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (464 458 (:REWRITE DEFAULT-CAR))
 (336 28 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (330 324 (:REWRITE DEFAULT-CDR))
 (288 21 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (252 56 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (229 49 (:DEFINITION ASSOC-EQUAL))
 (183 21 (:DEFINITION MEMBER-EQUAL))
 (105 105 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (55 11 (:DEFINITION LEN))
 (53 53 (:TYPE-PRESCRIPTION NULL))
 (53 53 (:DEFINITION NULL))
 (42 42 (:REWRITE SUBSETP-MEMBER . 2))
 (42 42 (:REWRITE SUBSETP-MEMBER . 1))
 (28 28 (:REWRITE DEFAULT-<-2))
 (28 28 (:REWRITE DEFAULT-<-1))
 (22 11 (:REWRITE DEFAULT-+-2))
 (16 2 (:REWRITE L2-FS-P-ASSOC))
 (11 11 (:REWRITE DEFAULT-COERCE-2))
 (11 11 (:REWRITE DEFAULT-COERCE-1))
 (11 11 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 )
(L2-CREATE-CORRECTNESS-1-LEMMA-1
 (20754 6918 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (23 23 (:REWRITE DEFAULT-<-2))
 (23 23 (:REWRITE DEFAULT-<-1))
 )
(L2-CREATE-CORRECTNESS-1-LEMMA-2
 (1 1 (:REWRITE DEFAULT-CAR))
 )
(L2-CREATE-CORRECTNESS-1
 (2901 967 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (2103 2077 (:REWRITE DEFAULT-CAR))
 (1507 1361 (:REWRITE DEFAULT-CDR))
 (826 70 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (637 44 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (572 140 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (425 112 (:DEFINITION NATP))
 (417 44 (:DEFINITION MEMBER-EQUAL))
 (290 45 (:REWRITE L2-FS-P-ASSOC))
 (220 220 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (126 126 (:TYPE-PRESCRIPTION NULL))
 (126 126 (:DEFINITION NULL))
 (113 89 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (112 112 (:REWRITE DEFAULT-<-2))
 (112 112 (:REWRITE DEFAULT-<-1))
 (103 51 (:REWRITE L2-WRCHS-CORRECTNESS-1-LEMMA-2))
 (100 20 (:DEFINITION LEN))
 (88 88 (:REWRITE SUBSETP-MEMBER . 2))
 (88 88 (:REWRITE SUBSETP-MEMBER . 1))
 (40 20 (:REWRITE DEFAULT-+-2))
 (20 20 (:REWRITE DEFAULT-COERCE-2))
 (20 20 (:REWRITE DEFAULT-COERCE-1))
 (20 20 (:REWRITE DEFAULT-+-1))
 )
(L2-READ-AFTER-WRITE-1-LEMMA-1
 (60 20 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (10 2 (:DEFINITION ASSOC-EQUAL))
 (6 6 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(L2-READ-AFTER-WRITE-2-LEMMA-1
 (9 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE DEFAULT-<-1))
 )
(L2-READ-AFTER-WRITE-2-LEMMA-2
 (484 37 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (406 138 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (301 13 (:DEFINITION L2-FS-P))
 (240 48 (:DEFINITION ASSOC-EQUAL))
 (160 160 (:REWRITE DEFAULT-CDR))
 (80 8 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (80 8 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (64 8 (:REWRITE L2-FS-P-ASSOC))
 (63 13 (:DEFINITION NATP))
 (39 3 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (24 3 (:DEFINITION MEMBER-EQUAL))
 (15 15 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (13 13 (:REWRITE DEFAULT-<-2))
 (13 13 (:REWRITE DEFAULT-<-1))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 )
(L2-READ-AFTER-WRITE-2-LEMMA-3
 (576 192 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (509 44 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (276 276 (:REWRITE DEFAULT-CAR))
 (245 49 (:DEFINITION ASSOC-EQUAL))
 (181 181 (:REWRITE DEFAULT-CDR))
 (130 10 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (80 10 (:DEFINITION MEMBER-EQUAL))
 (80 8 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (64 8 (:REWRITE L2-FS-P-ASSOC))
 (50 50 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (20 20 (:REWRITE SUBSETP-MEMBER . 2))
 (20 20 (:REWRITE SUBSETP-MEMBER . 1))
 (19 19 (:REWRITE DEFAULT-<-2))
 (19 19 (:REWRITE DEFAULT-<-1))
 )
(L2-READ-AFTER-WRITE-2-LEMMA-4
 (3435 246 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (2888 31 (:DEFINITION L2-STAT))
 (1661 11 (:DEFINITION L2-WRCHS))
 (1471 1471 (:REWRITE DEFAULT-CAR))
 (1256 240 (:DEFINITION ASSOC-EQUAL))
 (1194 1079 (:REWRITE DEFAULT-CDR))
 (693 51 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (631 9 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-3))
 (606 198 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (525 15 (:DEFINITION L2-TO-L1-FS))
 (518 51 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (469 51 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (452 51 (:REWRITE L2-FS-P-ASSOC))
 (438 51 (:DEFINITION MEMBER-EQUAL))
 (297 33 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (255 255 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (243 9 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-1))
 (209 209 (:TYPE-PRESCRIPTION LEN))
 (198 198 (:TYPE-PRESCRIPTION ZP))
 (198 66 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (165 165 (:TYPE-PRESCRIPTION L2-WRCHS))
 (102 102 (:REWRITE SUBSETP-MEMBER . 2))
 (102 102 (:REWRITE SUBSETP-MEMBER . 1))
 (88 11 (:DEFINITION LEN))
 (88 9 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-4))
 (87 87 (:REWRITE DEFAULT-<-2))
 (87 87 (:REWRITE DEFAULT-<-1))
 (66 66 (:TYPE-PRESCRIPTION NULL))
 (66 66 (:DEFINITION NULL))
 (62 62 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (55 55 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (55 11 (:REWRITE DEFAULT-COERCE-3))
 (33 33 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (22 22 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (22 22 (:REWRITE DEFAULT-COERCE-2))
 (22 11 (:REWRITE DEFAULT-+-2))
 (21 9 (:REWRITE L2-WRCHS-CORRECTNESS-1-LEMMA-2))
 (18 18 (:REWRITE L1-READ-AFTER-WRITE-2-LEMMA-2))
 (12 2 (:REWRITE L2-RDCHS-CORRECTNESS-1-LEMMA-1))
 (11 11 (:REWRITE DEFAULT-COERCE-1))
 (11 11 (:REWRITE DEFAULT-+-1))
 (6 1 (:DEFINITION SYMBOL-LISTP))
 (5 5 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 )
(L2-STAT-AFTER-WRITE
 (1620 115 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (1212 13 (:DEFINITION L2-STAT))
 (1000 5 (:DEFINITION L2-WRCHS))
 (828 6 (:REWRITE L2-STAT-CORRECTNESS-2))
 (715 715 (:REWRITE DEFAULT-CAR))
 (695 526 (:REWRITE DEFAULT-CDR))
 (628 120 (:DEFINITION ASSOC-EQUAL))
 (410 6 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-3))
 (384 4 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-3))
 (326 24 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (312 102 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (278 8 (:DEFINITION L2-TO-L1-FS))
 (267 16 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (244 24 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (215 11 (:DEFINITION LEN))
 (212 24 (:REWRITE L2-FS-P-ASSOC))
 (206 24 (:DEFINITION MEMBER-EQUAL))
 (204 204 (:TYPE-PRESCRIPTION LEN))
 (204 24 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (162 6 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-1))
 (150 6 (:REWRITE DEFAULT-COERCE-3))
 (135 15 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (120 120 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (113 113 (:TYPE-PRESCRIPTION ZP))
 (90 30 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (78 78 (:TYPE-PRESCRIPTION L2-WRCHS))
 (73 57 (:REWRITE DEFAULT-<-2))
 (57 57 (:REWRITE DEFAULT-<-1))
 (56 6 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-4))
 (48 48 (:REWRITE SUBSETP-MEMBER . 2))
 (48 48 (:REWRITE SUBSETP-MEMBER . 1))
 (30 30 (:TYPE-PRESCRIPTION NULL))
 (30 30 (:DEFINITION NULL))
 (28 28 (:REWRITE DEFAULT-COERCE-2))
 (27 27 (:REWRITE ZP-OPEN))
 (26 26 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (22 22 (:REWRITE DEFAULT-COERCE-1))
 (22 11 (:REWRITE DEFAULT-+-2))
 (15 15 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (12 12 (:REWRITE L1-READ-AFTER-WRITE-2-LEMMA-2))
 (12 6 (:REWRITE L2-WRCHS-CORRECTNESS-1-LEMMA-2))
 (11 11 (:REWRITE DEFAULT-+-1))
 (11 11 (:LINEAR POSITION-WHEN-MEMBER))
 (11 11 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(L2-READ-AFTER-WRITE-1
 (418 20 (:DEFINITION LEN))
 (311 23 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (269 80 (:REWRITE DEFAULT-CDR))
 (215 1 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (200 1 (:DEFINITION L2-WRCHS))
 (188 2 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (180 2 (:DEFINITION L2-STAT))
 (178 13 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (110 2 (:LINEAR INSERT-TEXT-CORRECTNESS-3 . 1))
 (98 4 (:DEFINITION L2-FS-P))
 (79 79 (:REWRITE DEFAULT-CAR))
 (65 34 (:REWRITE DEFAULT-+-2))
 (60 12 (:DEFINITION ASSOC-EQUAL))
 (57 32 (:REWRITE DEFAULT-<-2))
 (51 3 (:REWRITE DEFAULT-COERCE-3))
 (44 39 (:REWRITE ZP-OPEN))
 (39 3 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (39 1 (:DEFINITION NTHCDR))
 (38 38 (:REWRITE DEFAULT-COERCE-2))
 (38 35 (:REWRITE DEFAULT-COERCE-1))
 (35 34 (:REWRITE DEFAULT-+-1))
 (33 32 (:REWRITE DEFAULT-<-1))
 (30 3 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (30 3 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (28 28 (:TYPE-PRESCRIPTION ZP))
 (27 9 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (27 3 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (24 3 (:REWRITE L2-FS-P-ASSOC))
 (24 3 (:DEFINITION MEMBER-EQUAL))
 (20 4 (:REWRITE NFIX-WHEN-ZP))
 (18 6 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (15 15 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (15 15 (:LINEAR POSITION-WHEN-MEMBER))
 (15 15 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (6 6 (:TYPE-PRESCRIPTION NULL))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 (6 6 (:DEFINITION NULL))
 (4 4 (:REWRITE NFIX-WHEN-NATP))
 (4 4 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (3 3 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (3 1 (:DEFINITION SYMBOL-LISTP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(L2-READ-AFTER-WRITE-2
 (1537 17 (:DEFINITION L2-STAT))
 (1296 92 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (1000 5 (:DEFINITION L2-WRCHS))
 (675 464 (:REWRITE DEFAULT-CDR))
 (662 26 (:DEFINITION L2-FS-P))
 (546 546 (:REWRITE DEFAULT-CAR))
 (480 44 (:DEFINITION LEN))
 (460 4 (:DEFINITION TAKE))
 (440 88 (:DEFINITION ASSOC-EQUAL))
 (354 8 (:REWRITE TAKE-OF-LEN-FREE))
 (287 22 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (245 15 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (222 22 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (220 22 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (208 4 (:REWRITE CAR-OF-NTHCDR))
 (198 66 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (180 8 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (178 22 (:REWRITE L2-FS-P-ASSOC))
 (177 33 (:REWRITE NFIX-WHEN-ZP))
 (177 22 (:DEFINITION MEMBER-EQUAL))
 (162 8 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (159 3 (:REWRITE LEN-OF-NTHCDR))
 (156 112 (:REWRITE DEFAULT-<-2))
 (150 9 (:REWRITE DEFAULT-COERCE-3))
 (148 65 (:REWRITE ZP-OPEN))
 (137 90 (:REWRITE DEFAULT-+-2))
 (135 15 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (132 4 (:DEFINITION NTHCDR))
 (130 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (124 32 (:REWRITE DEFAULT-COERCE-1))
 (124 4 (:DEFINITION NTH))
 (122 112 (:REWRITE DEFAULT-<-1))
 (112 112 (:TYPE-PRESCRIPTION ZP))
 (110 110 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (93 90 (:REWRITE DEFAULT-+-1))
 (90 30 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (76 8 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (69 33 (:REWRITE NFIX-WHEN-NATP))
 (60 4 (:REWRITE CONSP-OF-NTHCDR))
 (50 50 (:LINEAR POSITION-WHEN-MEMBER))
 (50 50 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (44 44 (:REWRITE SUBSETP-MEMBER . 2))
 (44 44 (:REWRITE SUBSETP-MEMBER . 1))
 (41 41 (:REWRITE DEFAULT-COERCE-2))
 (34 34 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (30 30 (:TYPE-PRESCRIPTION NULL))
 (30 30 (:DEFINITION NULL))
 (25 25 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-INSERT-TEXT))
 (24 8 (:DEFINITION SYMBOL-LISTP))
 (20 20 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (15 15 (:TYPE-PRESCRIPTION NFIX))
 (15 15 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (15 3 (:REWRITE CONSP-OF-TAKE))
 (14 2 (:DEFINITION NFIX))
 (5 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:TYPE-PRESCRIPTION L2-WRCHS))
 (2 2 (:REWRITE L2-WRCHS-RETURNS-FS))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(L2-READ-AFTER-CREATE-1
 (3115 2921 (:REWRITE DEFAULT-CAR))
 (2128 2056 (:REWRITE DEFAULT-CDR))
 (1196 99 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1066 99 (:REWRITE L2-FS-P-ASSOC))
 (963 79 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (925 119 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (757 85 (:DEFINITION MEMBER-EQUAL))
 (726 158 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (660 136 (:DEFINITION NATP))
 (564 28 (:REWRITE TAKE-OF-LEN-FREE))
 (490 14 (:DEFINITION TAKE))
 (425 425 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (397 211 (:REWRITE DEFAULT-+-2))
 (350 14 (:REWRITE DEFAULT-COERCE-3))
 (308 14 (:REWRITE CONSP-OF-TAKE))
 (291 218 (:REWRITE DEFAULT-<-2))
 (286 11 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (236 218 (:REWRITE DEFAULT-<-1))
 (224 28 (:REWRITE ZP-OPEN))
 (222 211 (:REWRITE DEFAULT-+-1))
 (198 198 (:LINEAR POSITION-WHEN-MEMBER))
 (198 198 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (176 11 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (170 170 (:REWRITE SUBSETP-MEMBER . 2))
 (170 170 (:REWRITE SUBSETP-MEMBER . 1))
 (149 149 (:TYPE-PRESCRIPTION NULL))
 (149 149 (:DEFINITION NULL))
 (142 142 (:REWRITE DEFAULT-COERCE-2))
 (14 14 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-2))
 (11 11 (:TYPE-PRESCRIPTION NFIX))
 )
(L2-READ-AFTER-CREATE-2
 (7839 535 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (4050 30 (:DEFINITION L2-CREATE))
 (3120 3120 (:REWRITE DEFAULT-CAR))
 (2886 2490 (:REWRITE DEFAULT-CDR))
 (2232 438 (:DEFINITION ASSOC-EQUAL))
 (1637 47 (:DEFINITION L2-TO-L1-FS))
 (1532 114 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (1383 12 (:DEFINITION TAKE))
 (1245 24 (:REWRITE TAKE-OF-LEN-FREE))
 (1146 114 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (1080 357 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (1025 145 (:DEFINITION LEN))
 (1000 114 (:REWRITE L2-FS-P-ASSOC))
 (962 114 (:DEFINITION MEMBER-EQUAL))
 (928 114 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (810 90 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (639 12 (:REWRITE LEN-OF-NTHCDR))
 (624 12 (:REWRITE CAR-OF-NTHCDR))
 (585 108 (:REWRITE NFIX-WHEN-ZP))
 (579 3 (:DEFINITION L1-STAT))
 (570 570 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (540 180 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (540 24 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (540 24 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (505 351 (:REWRITE DEFAULT-+-2))
 (477 477 (:TYPE-PRESCRIPTION ZP))
 (469 388 (:REWRITE DEFAULT-<-2))
 (425 388 (:REWRITE DEFAULT-<-1))
 (411 132 (:REWRITE ZP-OPEN))
 (396 12 (:DEFINITION NTHCDR))
 (372 12 (:DEFINITION NTH))
 (360 351 (:REWRITE DEFAULT-+-1))
 (264 108 (:REWRITE NFIX-WHEN-NATP))
 (237 3 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-3))
 (234 234 (:TYPE-PRESCRIPTION L2-CREATE))
 (228 228 (:REWRITE SUBSETP-MEMBER . 2))
 (228 228 (:REWRITE SUBSETP-MEMBER . 1))
 (228 24 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (216 12 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (202 2 (:REWRITE L2-RDCHS-CORRECTNESS-1-LEMMA-1))
 (183 12 (:REWRITE CONSP-OF-NTHCDR))
 (180 180 (:TYPE-PRESCRIPTION NULL))
 (180 180 (:DEFINITION NULL))
 (162 162 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-2))
 (144 144 (:LINEAR POSITION-WHEN-MEMBER))
 (144 144 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (123 6 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-1))
 (96 12 (:REWRITE DEFAULT-COERCE-3))
 (90 90 (:REWRITE L2-READ-AFTER-WRITE-1-LEMMA-1))
 (85 85 (:REWRITE DEFAULT-COERCE-2))
 (81 3 (:REWRITE L2-READ-AFTER-WRITE-2-LEMMA-1))
 (73 73 (:REWRITE DEFAULT-COERCE-1))
 (72 12 (:DEFINITION NFIX))
 (60 60 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (60 12 (:REWRITE CONSP-OF-TAKE))
 (48 48 (:TYPE-PRESCRIPTION NFIX))
 (36 3 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-4))
 (24 24 (:REWRITE DEFAULT-UNARY-MINUS))
 (12 12 (:TYPE-PRESCRIPTION NATP))
 (12 12 (:REWRITE FOLD-CONSTS-IN-+))
 (12 3 (:REWRITE L2-WRCHS-CORRECTNESS-1-LEMMA-2))
 (6 6 (:TYPE-PRESCRIPTION L1-CREATE))
 (6 6 (:REWRITE L1-READ-AFTER-WRITE-2-LEMMA-2))
 )
(L2-FSCK
 (528 239 (:REWRITE DEFAULT-+-2))
 (335 239 (:REWRITE DEFAULT-+-1))
 (192 48 (:DEFINITION INTEGER-ABS))
 (176 22 (:REWRITE LENGTH-WHEN-STRINGP))
 (174 15 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (110 22 (:DEFINITION LEN))
 (88 68 (:REWRITE DEFAULT-<-2))
 (78 68 (:REWRITE DEFAULT-<-1))
 (48 48 (:REWRITE DEFAULT-UNARY-MINUS))
 (24 24 (:REWRITE DEFAULT-REALPART))
 (24 24 (:REWRITE DEFAULT-NUMERATOR))
 (24 24 (:REWRITE DEFAULT-IMAGPART))
 (24 24 (:REWRITE DEFAULT-DENOMINATOR))
 (22 22 (:TYPE-PRESCRIPTION LEN))
 (22 22 (:REWRITE DEFAULT-COERCE-2))
 (22 22 (:REWRITE DEFAULT-COERCE-1))
 )
(L2-FSCK-AFTER-L2-WRCHS-LEMMA-1
 (445 445 (:REWRITE DEFAULT-CAR))
 (389 389 (:REWRITE DEFAULT-CDR))
 (78 39 (:REWRITE DEFAULT-+-2))
 (69 23 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (39 39 (:REWRITE DEFAULT-COERCE-2))
 (39 39 (:REWRITE DEFAULT-COERCE-1))
 (39 39 (:REWRITE DEFAULT-<-2))
 (39 39 (:REWRITE DEFAULT-<-1))
 (39 39 (:REWRITE DEFAULT-+-1))
 (23 23 (:TYPE-PRESCRIPTION NULL))
 (23 23 (:DEFINITION NULL))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER))
 (1 1 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(L2-FSCK-AFTER-L2-WRCHS-LEMMA-2
 (682 55 (:REWRITE L2-CREATE-CORRECTNESS-1-LEMMA-2))
 (288 96 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (122 10 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (73 10 (:DEFINITION MEMBER-EQUAL))
 (58 29 (:REWRITE DEFAULT-+-2))
 (46 46 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (31 31 (:REWRITE DEFAULT-<-2))
 (31 31 (:REWRITE DEFAULT-<-1))
 (29 29 (:REWRITE DEFAULT-COERCE-2))
 (29 29 (:REWRITE DEFAULT-COERCE-1))
 (29 29 (:REWRITE DEFAULT-+-1))
 (19 19 (:REWRITE SUBSETP-MEMBER . 2))
 (19 19 (:REWRITE SUBSETP-MEMBER . 1))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER))
 (1 1 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(L2-FSCK-AFTER-L2-WRCHS-LEMMA-4
 (33225 11075 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (3009 2487 (:REWRITE DEFAULT-CAR))
 (2558 1514 (:REWRITE DEFAULT-CDR))
 (1816 88 (:REWRITE DEFAULT-COERCE-1))
 (710 80 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (254 80 (:REWRITE L2-FS-P-ASSOC))
 (176 88 (:REWRITE DEFAULT-+-2))
 (103 103 (:REWRITE DEFAULT-<-2))
 (103 103 (:REWRITE DEFAULT-<-1))
 (98 80 (:REWRITE L2-WRCHS-RETURNS-FS-LEMMA-3))
 (88 88 (:REWRITE DEFAULT-COERCE-2))
 (88 88 (:REWRITE DEFAULT-+-1))
 (42 42 (:LINEAR POSITION-WHEN-MEMBER))
 (42 42 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(L2-FSCK-AFTER-L2-WRCHS-LEMMA-5
 (3 1 (:DEFINITION CHARACTER-LISTP))
 (1 1 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-CAR))
 )
(L2-FSCK-AFTER-L2-WRCHS
 (1182 394 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (807 574 (:REWRITE DEFAULT-CDR))
 (740 736 (:REWRITE DEFAULT-CAR))
 (599 43 (:DEFINITION LEN))
 (544 34 (:REWRITE INSERT-TEXT-CORRECTNESS-4))
 (455 91 (:DEFINITION ASSOC-EQUAL))
 (354 30 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (275 20 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (264 60 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (250 10 (:REWRITE DEFAULT-COERCE-3))
 (175 20 (:DEFINITION MEMBER-EQUAL))
 (127 93 (:REWRITE DEFAULT-<-2))
 (124 17 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (124 17 (:REWRITE L2-FS-P-ASSOC))
 (100 100 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (93 93 (:REWRITE DEFAULT-<-1))
 (86 43 (:REWRITE DEFAULT-+-2))
 (79 79 (:REWRITE DEFAULT-COERCE-2))
 (69 69 (:REWRITE DEFAULT-COERCE-1))
 (57 57 (:TYPE-PRESCRIPTION NULL))
 (57 57 (:DEFINITION NULL))
 (56 56 (:REWRITE ZP-OPEN))
 (43 43 (:REWRITE DEFAULT-+-1))
 (40 40 (:REWRITE SUBSETP-MEMBER . 2))
 (40 40 (:REWRITE SUBSETP-MEMBER . 1))
 (22 22 (:LINEAR POSITION-WHEN-MEMBER))
 (22 22 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (18 18 (:TYPE-PRESCRIPTION L2-WRCHS))
 )
(L2-FSCK-AFTER-L2-UNLINK
 (486 162 (:TYPE-PRESCRIPTION ASSOC-WHEN-ZP-LEN))
 (274 274 (:REWRITE DEFAULT-CAR))
 (225 225 (:REWRITE DEFAULT-CDR))
 (155 31 (:DEFINITION ASSOC-EQUAL))
 (91 7 (:REWRITE ASSOC-OF-CAR-WHEN-MEMBER))
 (90 25 (:DEFINITION NATP))
 (65 13 (:DEFINITION LEN))
 (56 7 (:DEFINITION MEMBER-EQUAL))
 (54 6 (:DEFINITION REMOVE1-ASSOC-EQUAL))
 (50 5 (:REWRITE L2-STAT-CORRECTNESS-1-LEMMA-5))
 (40 5 (:REWRITE L2-FS-P-ASSOC))
 (36 12 (:REWRITE REMOVE1-ASSOC-WHEN-ABSENT . 1))
 (35 35 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (26 13 (:REWRITE DEFAULT-+-2))
 (25 25 (:REWRITE DEFAULT-<-2))
 (25 25 (:REWRITE DEFAULT-<-1))
 (14 14 (:REWRITE SUBSETP-MEMBER . 2))
 (14 14 (:REWRITE SUBSETP-MEMBER . 1))
 (13 13 (:REWRITE DEFAULT-COERCE-2))
 (13 13 (:REWRITE DEFAULT-COERCE-1))
 (13 13 (:REWRITE DEFAULT-+-1))
 (12 12 (:TYPE-PRESCRIPTION NULL))
 (12 12 (:DEFINITION NULL))
 )
(L2-WC-LEN)