(FARRAY::SB60P-NTH-MEM
 (64 50 (:REWRITE DEFAULT-<-1))
 (59 50 (:REWRITE DEFAULT-<-2))
 (25 16 (:REWRITE DEFAULT-+-2))
 (16 16 (:REWRITE DEFAULT-CAR))
 (16 16 (:REWRITE DEFAULT-+-1))
 (15 15 (:REWRITE DEFAULT-CDR))
 (14 14 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (7 7 (:REWRITE ZP-OPEN))
 )
(FARRAY::MEMP-UPDATE-NTH
 (57 50 (:REWRITE DEFAULT-<-2))
 (55 50 (:REWRITE DEFAULT-<-1))
 (35 20 (:REWRITE DEFAULT-CDR))
 (34 19 (:REWRITE DEFAULT-CAR))
 (18 11 (:REWRITE DEFAULT-+-2))
 (11 11 (:REWRITE DEFAULT-+-1))
 (7 7 (:REWRITE ZP-OPEN))
 (5 5 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FARRAY::UPDATE-NTH-UPDATE-NTH-SAME
 (73 22 (:REWRITE DEFAULT-CDR))
 (60 15 (:REWRITE DEFAULT-CAR))
 (8 8 (:REWRITE ZP-OPEN))
 (7 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-+-1))
 )
(FARRAY::UPDATE-NTH-REDUNDANT
 (21 14 (:REWRITE DEFAULT-<-2))
 (21 14 (:REWRITE DEFAULT-+-2))
 (14 14 (:REWRITE DEFAULT-CDR))
 (14 14 (:REWRITE DEFAULT-<-1))
 (14 14 (:REWRITE DEFAULT-+-1))
 (8 8 (:REWRITE ZP-OPEN))
 (8 8 (:REWRITE DEFAULT-CAR))
 )
(FARRAY::UPDATE-NTH-UPDATE-NTH-DIFFERENT
 (1453 90 (:REWRITE FARRAY::UPDATE-NTH-REDUNDANT))
 (670 71 (:DEFINITION LEN))
 (550 550 (:TYPE-PRESCRIPTION LEN))
 (421 199 (:REWRITE DEFAULT-CDR))
 (348 16 (:REWRITE LEN-UPDATE-NTH))
 (295 198 (:REWRITE DEFAULT-+-2))
 (222 66 (:REWRITE DEFAULT-CAR))
 (221 144 (:REWRITE DEFAULT-<-2))
 (198 198 (:REWRITE DEFAULT-+-1))
 (160 144 (:REWRITE DEFAULT-<-1))
 (129 35 (:REWRITE FOLD-CONSTS-IN-+))
 (112 16 (:DEFINITION MAX))
 (106 37 (:REWRITE ZP-OPEN))
 (48 16 (:DEFINITION NFIX))
 (24 12 (:REWRITE UNICITY-OF-0))
 (12 12 (:DEFINITION FIX))
 (4 4 (:REWRITE NTH-0-CONS))
 )
(FARRAY::MEMP-RESIZE-LIST
 (526 526 (:REWRITE DEFAULT-<-2))
 (526 526 (:REWRITE DEFAULT-<-1))
 (377 323 (:REWRITE DEFAULT-+-2))
 (323 323 (:REWRITE DEFAULT-+-1))
 (304 277 (:REWRITE DEFAULT-CDR))
 (303 276 (:REWRITE DEFAULT-CAR))
 (234 78 (:REWRITE FOLD-CONSTS-IN-+))
 )
(FARRAY::LEN-RESIZE-LIST
 (25 22 (:REWRITE DEFAULT-+-2))
 (22 22 (:REWRITE DEFAULT-+-1))
 (13 13 (:REWRITE DEFAULT-<-2))
 (13 13 (:REWRITE DEFAULT-<-1))
 (12 10 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE DEFAULT-CAR))
 )
(FARRAY::NTH-*MEMI*
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(FARRAY::UPDATE-NTH-*MEMI*
 (22 11 (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH))
 (22 1 (:REWRITE FARRAY::UPDATE-NTH-REDUNDANT))
 (14 2 (:DEFINITION LEN))
 (11 11 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:TYPE-PRESCRIPTION LEN))
 (6 3 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(FARRAY::SB60P-MEMI
 (10 2 (:DEFINITION LEN))
 (9 1 (:DEFINITION FARRAY::MEMP))
 (6 4 (:REWRITE DEFAULT-<-1))
 (6 1 (:DEFINITION SIGNED-BYTE-P))
 (5 4 (:REWRITE DEFAULT-<-2))
 (5 1 (:DEFINITION INTEGER-RANGE-P))
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 1 (:DEFINITION TRUE-LISTP))
 )
(FARRAY::STP-!MEMI
 (16 8 (:REWRITE DEFAULT-+-2))
 (14 14 (:REWRITE DEFAULT-CDR))
 (9 1 (:DEFINITION FARRAY::MEMP))
 (8 8 (:REWRITE DEFAULT-+-1))
 (8 7 (:REWRITE DEFAULT-<-2))
 (8 7 (:REWRITE DEFAULT-<-1))
 (5 5 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE FARRAY::UPDATE-NTH-REDUNDANT))
 (1 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FARRAY::MEMI-!MEMI
 (13 1 (:REWRITE FARRAY::UPDATE-NTH-REDUNDANT))
 (6 6 (:TYPE-PRESCRIPTION LEN))
 (6 5 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-<-1))
 (5 1 (:DEFINITION LEN))
 (3 3 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(FARRAY::STP-RESIZE-MEM
 (19 19 (:REWRITE DEFAULT-CDR))
 (18 9 (:REWRITE DEFAULT-+-2))
 (10 10 (:REWRITE DEFAULT-CAR))
 (10 10 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE DEFAULT-<-1))
 (9 9 (:REWRITE DEFAULT-+-1))
 (2 2 (:TYPE-PRESCRIPTION RESIZE-LIST))
 )
(FARRAY::MEM-LEN-RESIZE-MEM
 (2 2 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(FARRAY::MEM-LEN-!MEMI
 (45 9 (:DEFINITION LEN))
 (20 11 (:REWRITE DEFAULT-+-2))
 (17 10 (:REWRITE DEFAULT-<-1))
 (13 10 (:REWRITE DEFAULT-<-2))
 (11 11 (:REWRITE DEFAULT-+-1))
 (10 10 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1 1 (:REWRITE FARRAY::UPDATE-NTH-REDUNDANT))
 )
(FARRAY::!MEMI-!MEMI-SAME
 (4 4 (:REWRITE FARRAY::UPDATE-NTH-REDUNDANT))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE FARRAY::UPDATE-NTH-UPDATE-NTH-DIFFERENT))
 )
(FARRAY::!MEMI-REDUNDANT
 (10 2 (:DEFINITION LEN))
 (9 1 (:DEFINITION FARRAY::MEMP))
 (6 1 (:DEFINITION SIGNED-BYTE-P))
 (5 5 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE DEFAULT-CAR))
 (5 4 (:REWRITE DEFAULT-<-2))
 (5 1 (:DEFINITION INTEGER-RANGE-P))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 )
(FARRAY::!MEMI-!MEMI-DIFFERENT
 (107 5 (:REWRITE FARRAY::UPDATE-NTH-REDUNDANT))
 (54 54 (:TYPE-PRESCRIPTION LEN))
 (36 2 (:REWRITE LEN-UPDATE-NTH))
 (25 5 (:DEFINITION LEN))
 (20 11 (:REWRITE DEFAULT-<-2))
 (14 2 (:DEFINITION MAX))
 (13 11 (:REWRITE DEFAULT-<-1))
 (12 7 (:REWRITE DEFAULT-+-2))
 (9 9 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 2 (:DEFINITION NFIX))
 (4 4 (:REWRITE DEFAULT-CAR))
 )
(FARRAY::SB60P-TYPES)
(FARRAY::INTEGERP-TYPES)
(FARRAY::INTEGERP-+)
(FARRAY::<=-0-+)
(FARRAY::FIELD-TABLEP
 (91 13 (:DEFINITION SIGNED-BYTE-P))
 (80 51 (:REWRITE DEFAULT-<-2))
 (78 13 (:DEFINITION INTEGER-RANGE-P))
 (64 51 (:REWRITE DEFAULT-<-1))
 (24 9 (:REWRITE DEFAULT-+-1))
 (22 3 (:REWRITE FARRAY::<=-0-+))
 (18 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (12 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (9 9 (:REWRITE DEFAULT-+-2))
 (3 2 (:REWRITE FARRAY::INTEGERP-+))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI
 (481 110 (:REWRITE FARRAY::SB60P-TYPES))
 (337 198 (:REWRITE DEFAULT-<-2))
 (326 46 (:DEFINITION SIGNED-BYTE-P))
 (280 46 (:DEFINITION INTEGER-RANGE-P))
 (198 198 (:REWRITE DEFAULT-<-1))
 (123 18 (:REWRITE FARRAY::INTEGERP-TYPES))
 (92 92 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (45 15 (:REWRITE FARRAY::SB60P-MEMI))
 (30 30 (:TYPE-PRESCRIPTION FARRAY::STP))
 (27 9 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (8 8 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-+-1))
 )
(FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI
 (468 108 (:REWRITE FARRAY::SB60P-TYPES))
 (366 192 (:REWRITE DEFAULT-<-2))
 (321 44 (:DEFINITION SIGNED-BYTE-P))
 (277 44 (:DEFINITION INTEGER-RANGE-P))
 (204 192 (:REWRITE DEFAULT-<-1))
 (170 29 (:REWRITE FARRAY::INTEGERP-TYPES))
 (88 88 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (39 13 (:REWRITE FARRAY::SB60P-MEMI))
 (30 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (26 26 (:TYPE-PRESCRIPTION FARRAY::STP))
 (8 8 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-+-1))
 )
(FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN
 (450 102 (:REWRITE FARRAY::SB60P-TYPES))
 (357 177 (:REWRITE DEFAULT-<-2))
 (312 41 (:DEFINITION SIGNED-BYTE-P))
 (271 41 (:DEFINITION INTEGER-RANGE-P))
 (185 177 (:REWRITE DEFAULT-<-1))
 (170 27 (:REWRITE FARRAY::INTEGERP-TYPES))
 (82 82 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (36 12 (:REWRITE FARRAY::SB60P-MEMI))
 (30 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (24 24 (:TYPE-PRESCRIPTION FARRAY::STP))
 (8 8 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-+-1))
 )
(FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI
 (452 104 (:REWRITE FARRAY::SB60P-TYPES))
 (357 171 (:REWRITE DEFAULT-<-2))
 (315 40 (:DEFINITION SIGNED-BYTE-P))
 (275 40 (:DEFINITION INTEGER-RANGE-P))
 (197 171 (:REWRITE DEFAULT-<-1))
 (194 29 (:REWRITE FARRAY::INTEGERP-TYPES))
 (80 80 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (36 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (33 11 (:REWRITE FARRAY::SB60P-MEMI))
 (22 22 (:TYPE-PRESCRIPTION FARRAY::STP))
 (8 8 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-+-1))
 )
(FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+
 (576 142 (:REWRITE FARRAY::SB60P-TYPES))
 (563 202 (:REWRITE DEFAULT-<-2))
 (398 48 (:DEFINITION SIGNED-BYTE-P))
 (350 48 (:DEFINITION INTEGER-RANGE-P))
 (348 50 (:REWRITE FARRAY::INTEGERP-TYPES))
 (210 202 (:REWRITE DEFAULT-<-1))
 (96 96 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (69 23 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (36 12 (:REWRITE FARRAY::SB60P-MEMI))
 (24 24 (:TYPE-PRESCRIPTION FARRAY::STP))
 (10 10 (:REWRITE DEFAULT-+-2))
 (10 10 (:REWRITE DEFAULT-+-1))
 )
(FARRAY::FIELD-TABLEP-!MEMI
 (1518 284 (:REWRITE FARRAY::SB60P-TYPES))
 (1451 696 (:REWRITE DEFAULT-<-2))
 (1126 105 (:DEFINITION SIGNED-BYTE-P))
 (1006 105 (:DEFINITION INTEGER-RANGE-P))
 (730 74 (:REWRITE FARRAY::INTEGERP-TYPES))
 (722 696 (:REWRITE DEFAULT-<-1))
 (347 104 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (223 85 (:REWRITE FARRAY::!MEMI-REDUNDANT))
 (210 210 (:TYPE-PRESCRIPTION FARRAY::STP))
 (210 210 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (111 37 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (108 36 (:REWRITE FARRAY::SB60P-MEMI))
 (95 83 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (95 83 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (74 72 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (46 38 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (39 39 (:REWRITE DEFAULT-+-2))
 (39 39 (:REWRITE DEFAULT-+-1))
 (30 30 (:TYPE-PRESCRIPTION INTEGER-RANGE-P))
 (21 19 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 )
(FARRAY::FARRAYP
 (20 10 (:REWRITE DEFAULT-+-2))
 (20 10 (:REWRITE DEFAULT-+-1))
 (10 5 (:REWRITE DEFAULT-<-1))
 (7 7 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (5 5 (:REWRITE DEFAULT-<-2))
 (5 1 (:DEFINITION INTEGER-RANGE-P))
 (4 4 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (1 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (1 1 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (1 1 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 )
(FARRAY::NUM-FIELDS)
(FARRAY::SB60P-NUM-FIELDS
 (30 24 (:REWRITE DEFAULT-<-1))
 (24 24 (:REWRITE DEFAULT-<-2))
 (21 3 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (17 17 (:REWRITE DEFAULT-+-2))
 (17 17 (:REWRITE DEFAULT-+-1))
 (12 4 (:REWRITE FARRAY::SB60P-TYPES))
 (7 1 (:REWRITE FARRAY::INTEGERP-TYPES))
 (6 6 (:REWRITE FOLD-CONSTS-IN-+))
 (6 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (6 2 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (6 2 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (3 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (3 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 )
(FARRAY::FIELDP)
(FARRAY::FIELDP-FORWARD-CHAINING)
(FARRAY::FLENGTH
 (149 104 (:REWRITE DEFAULT-<-1))
 (105 104 (:REWRITE DEFAULT-<-2))
 (54 54 (:REWRITE DEFAULT-+-2))
 (54 54 (:REWRITE DEFAULT-+-1))
 (33 3 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (21 21 (:REWRITE FOLD-CONSTS-IN-+))
 (9 3 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (3 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FARRAY::<-0-FLENGTH
 (120 46 (:REWRITE DEFAULT-+-1))
 (95 6 (:REWRITE FARRAY::INTEGERP-TYPES))
 (49 46 (:REWRITE DEFAULT-+-2))
 (49 30 (:REWRITE DEFAULT-<-1))
 (43 6 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (30 30 (:REWRITE DEFAULT-<-2))
 (23 8 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (17 5 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (17 5 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (15 15 (:REWRITE FOLD-CONSTS-IN-+))
 (14 4 (:REWRITE FARRAY::INTEGERP-+))
 (9 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (8 2 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (7 7 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (4 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 1 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 )
(FARRAY::INTEGERP-FLENGTH
 (134 22 (:REWRITE FARRAY::SB60P-TYPES))
 (129 63 (:REWRITE DEFAULT-<-1))
 (92 92 (:REWRITE DEFAULT-+-2))
 (92 92 (:REWRITE DEFAULT-+-1))
 (74 4 (:REWRITE FARRAY::INTEGERP-TYPES))
 (63 63 (:REWRITE DEFAULT-<-2))
 (40 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (34 34 (:REWRITE FOLD-CONSTS-IN-+))
 (22 10 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (19 7 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (16 4 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (6 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (6 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (1 1 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(FARRAY::FLENGTH-<-MEM-LEN
 (213 145 (:REWRITE DEFAULT-<-1))
 (213 127 (:REWRITE DEFAULT-+-1))
 (190 18 (:REWRITE FARRAY::INTEGERP-TYPES))
 (146 145 (:REWRITE DEFAULT-<-2))
 (146 127 (:REWRITE DEFAULT-+-2))
 (116 36 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (48 48 (:REWRITE FOLD-CONSTS-IN-+))
 (37 5 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (16 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (12 4 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (8 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 )
(FARRAY::SB60P-FLENGTH
 (503 295 (:REWRITE DEFAULT-<-1))
 (405 334 (:REWRITE DEFAULT-+-1))
 (352 334 (:REWRITE DEFAULT-+-2))
 (335 36 (:REWRITE FARRAY::INTEGERP-TYPES))
 (295 295 (:REWRITE DEFAULT-<-2))
 (229 65 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (174 42 (:REWRITE FARRAY::INTEGERP-+))
 (146 22 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (120 120 (:REWRITE FOLD-CONSTS-IN-+))
 (66 22 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (38 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (18 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (17 7 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (16 4 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (12 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FARRAY::FIELD-OFFSETP
 (133 101 (:REWRITE DEFAULT-<-1))
 (102 101 (:REWRITE DEFAULT-<-2))
 (97 47 (:REWRITE DEFAULT-+-1))
 (57 47 (:REWRITE DEFAULT-+-2))
 (22 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (21 21 (:REWRITE FOLD-CONSTS-IN-+))
 (6 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (6 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FARRAY::FLENGTH-+-INDEX-<-MEM-LEN
 (270 120 (:REWRITE DEFAULT-+-1))
 (188 103 (:REWRITE DEFAULT-<-1))
 (130 120 (:REWRITE DEFAULT-+-2))
 (121 42 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (104 103 (:REWRITE DEFAULT-<-2))
 (45 45 (:REWRITE FOLD-CONSTS-IN-+))
 (44 6 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (35 35 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (14 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (8 4 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (6 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 )
(FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN
 (170 106 (:REWRITE DEFAULT-<-1))
 (165 128 (:REWRITE DEFAULT-+-1))
 (157 128 (:REWRITE DEFAULT-+-2))
 (150 24 (:REWRITE FARRAY::INTEGERP-TYPES))
 (106 106 (:REWRITE DEFAULT-<-2))
 (102 36 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (64 16 (:REWRITE FARRAY::INTEGERP-+))
 (47 5 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (37 37 (:REWRITE FOLD-CONSTS-IN-+))
 (15 5 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (15 5 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(FARRAY::FIELD-OFFSETP-FORWARD-CHAINING)
(FARRAY::FIELD-OFFSETP-0
 (78 47 (:REWRITE DEFAULT-<-1))
 (47 47 (:REWRITE DEFAULT-<-2))
 (45 13 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (38 4 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (35 35 (:REWRITE DEFAULT-+-2))
 (35 35 (:REWRITE DEFAULT-+-1))
 (35 3 (:REWRITE FARRAY::INTEGERP-TYPES))
 (20 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (17 3 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (17 3 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (13 13 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 )
(FARRAY::FIELD-OFFSETP-1--NOT-0
 (150 40 (:REWRITE FARRAY::SB60P-TYPES))
 (146 22 (:REWRITE FARRAY::INTEGERP-TYPES))
 (133 21 (:REWRITE DEFAULT-+-1))
 (102 9 (:DEFINITION SIGNED-BYTE-P))
 (93 9 (:DEFINITION INTEGER-RANGE-P))
 (54 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (39 21 (:REWRITE DEFAULT-+-2))
 (30 14 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (21 21 (:REWRITE DEFAULT-<-2))
 (21 21 (:REWRITE DEFAULT-<-1))
 (18 18 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (8 8 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (8 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (8 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (8 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (8 4 (:REWRITE FARRAY::SB60P-MEMI))
 (4 4 (:TYPE-PRESCRIPTION FARRAY::STP))
 (4 4 (:REWRITE FOLD-CONSTS-IN-+))
 (4 4 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (1 1 (:REWRITE FARRAY::<=-0-+))
 )
(FARRAY::<-1+)
(FARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH
 (86 54 (:REWRITE DEFAULT-<-1))
 (55 54 (:REWRITE DEFAULT-<-2))
 (52 16 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (43 4 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (38 38 (:REWRITE DEFAULT-+-2))
 (38 38 (:REWRITE DEFAULT-+-1))
 (38 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (35 3 (:REWRITE FARRAY::INTEGERP-TYPES))
 (18 3 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (18 3 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (14 14 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 )
(FARRAY::FIELD-OFFSETP-1--SQUEEZE
 (229 61 (:REWRITE FARRAY::SB60P-TYPES))
 (219 33 (:REWRITE FARRAY::INTEGERP-TYPES))
 (203 35 (:REWRITE DEFAULT-+-1))
 (156 14 (:DEFINITION SIGNED-BYTE-P))
 (142 14 (:DEFINITION INTEGER-RANGE-P))
 (81 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (62 35 (:REWRITE DEFAULT-+-2))
 (45 21 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (32 32 (:REWRITE DEFAULT-<-2))
 (32 32 (:REWRITE DEFAULT-<-1))
 (28 28 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (13 13 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (13 13 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (13 13 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (12 12 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (12 6 (:REWRITE FARRAY::SB60P-MEMI))
 (7 7 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (6 6 (:TYPE-PRESCRIPTION FARRAY::STP))
 (6 6 (:REWRITE FOLD-CONSTS-IN-+))
 )
(FARRAY::SB60P-FIELD-OFFSETP
 (182 132 (:REWRITE DEFAULT-+-1))
 (176 111 (:REWRITE DEFAULT-<-1))
 (161 21 (:REWRITE FARRAY::INTEGERP-TYPES))
 (157 132 (:REWRITE DEFAULT-+-2))
 (144 45 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (141 33 (:REWRITE FARRAY::INTEGERP-+))
 (119 5 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (111 111 (:REWRITE DEFAULT-<-2))
 (47 47 (:REWRITE FOLD-CONSTS-IN-+))
 (31 3 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (15 5 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (15 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (6 2 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 )
(FARRAY::SB60P-1+-FIELD-OFFSETP
 (183 133 (:REWRITE DEFAULT-+-1))
 (181 116 (:REWRITE DEFAULT-<-1))
 (161 21 (:REWRITE FARRAY::INTEGERP-TYPES))
 (158 133 (:REWRITE DEFAULT-+-2))
 (144 45 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (141 33 (:REWRITE FARRAY::INTEGERP-+))
 (119 5 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (116 116 (:REWRITE DEFAULT-<-2))
 (47 47 (:REWRITE FOLD-CONSTS-IN-+))
 (31 3 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (15 5 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (15 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (6 2 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 )
(FARRAY::SB60P-1--FIELD-OFFSETP
 (183 133 (:REWRITE DEFAULT-+-1))
 (180 115 (:REWRITE DEFAULT-<-1))
 (161 21 (:REWRITE FARRAY::INTEGERP-TYPES))
 (158 133 (:REWRITE DEFAULT-+-2))
 (144 45 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (141 33 (:REWRITE FARRAY::INTEGERP-+))
 (119 5 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (115 115 (:REWRITE DEFAULT-<-2))
 (47 47 (:REWRITE FOLD-CONSTS-IN-+))
 (31 3 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (15 5 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (15 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (6 2 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 )
(FARRAY::FREAD
 (8085 1663 (:REWRITE DEFAULT-+-1))
 (5467 2804 (:REWRITE DEFAULT-<-1))
 (2861 2804 (:REWRITE DEFAULT-<-2))
 (1808 814 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1378 3 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (433 433 (:REWRITE FOLD-CONSTS-IN-+))
 (161 37 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (65 46 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (1 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 )
(FARRAY::FWRITE
 (8095 1663 (:REWRITE DEFAULT-+-1))
 (5724 3061 (:REWRITE DEFAULT-<-1))
 (3118 3061 (:REWRITE DEFAULT-<-2))
 (1808 814 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1386 3 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (433 433 (:REWRITE FOLD-CONSTS-IN-+))
 (161 37 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (65 46 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (1 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 )
(FARRAY::SB60P-FREAD
 (448 164 (:REWRITE DEFAULT-+-1))
 (414 25 (:REWRITE FARRAY::INTEGERP-TYPES))
 (282 68 (:REWRITE FARRAY::INTEGERP-+))
 (249 165 (:REWRITE DEFAULT-<-1))
 (216 67 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (184 164 (:REWRITE DEFAULT-+-2))
 (165 165 (:REWRITE DEFAULT-<-2))
 (147 6 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (100 10 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (75 9 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (71 71 (:REWRITE FOLD-CONSTS-IN-+))
 (71 1 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (20 5 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (18 6 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (12 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FARRAY::FARRAYP-FWRITE
 (880 3 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (728 488 (:REWRITE DEFAULT-<-1))
 (702 54 (:REWRITE FARRAY::INTEGERP-TYPES))
 (599 275 (:REWRITE DEFAULT-+-1))
 (490 488 (:REWRITE DEFAULT-<-2))
 (351 275 (:REWRITE DEFAULT-+-2))
 (251 10 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (111 111 (:REWRITE FOLD-CONSTS-IN-+))
 (37 2 (:REWRITE FARRAY::!MEMI-REDUNDANT))
 (30 10 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (24 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (22 4 (:REWRITE FARRAY::<=-0-+))
 (11 5 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FARRAY::FLENGTH-FWRITE
 (596 1 (:REWRITE FARRAY::!MEMI-REDUNDANT))
 (586 1 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (544 24 (:REWRITE FARRAY::INTEGERP-TYPES))
 (528 109 (:REWRITE DEFAULT-+-1))
 (453 38 (:REWRITE FARRAY::<-1+))
 (268 204 (:REWRITE DEFAULT-<-1))
 (204 204 (:REWRITE DEFAULT-<-2))
 (202 32 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (128 109 (:REWRITE DEFAULT-+-2))
 (67 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (53 53 (:REWRITE FOLD-CONSTS-IN-+))
 (47 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (27 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (19 9 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (11 2 (:REWRITE FARRAY::<=-0-+))
 (6 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 )
(FARRAY::FIELD-TABLEP-ORDERING-ARBITRARY-K
 (640 152 (:REWRITE FARRAY::SB60P-TYPES))
 (462 59 (:DEFINITION SIGNED-BYTE-P))
 (403 59 (:DEFINITION INTEGER-RANGE-P))
 (350 184 (:REWRITE DEFAULT-<-2))
 (321 184 (:REWRITE DEFAULT-<-1))
 (269 40 (:REWRITE FARRAY::INTEGERP-TYPES))
 (116 116 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (57 19 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (24 8 (:REWRITE FARRAY::SB60P-MEMI))
 (16 16 (:TYPE-PRESCRIPTION FARRAY::STP))
 (9 9 (:REWRITE DEFAULT-+-2))
 (9 9 (:REWRITE DEFAULT-+-1))
 )
(FARRAY::FIELD-TABLEP-ORDERING-ARBITRARY-J-K
 (290 62 (:REWRITE FARRAY::SB60P-TYPES))
 (201 128 (:REWRITE DEFAULT-<-2))
 (201 27 (:DEFINITION SIGNED-BYTE-P))
 (174 27 (:DEFINITION INTEGER-RANGE-P))
 (148 128 (:REWRITE DEFAULT-<-1))
 (84 13 (:REWRITE FARRAY::INTEGERP-TYPES))
 (54 54 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (27 9 (:REWRITE FARRAY::SB60P-MEMI))
 (21 21 (:REWRITE DEFAULT-+-2))
 (21 21 (:REWRITE DEFAULT-+-1))
 (18 18 (:TYPE-PRESCRIPTION FARRAY::STP))
 (12 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (4 2 (:REWRITE FARRAY::<-1+))
 (1 1 (:REWRITE FARRAY::<=-0-+))
 )
(FARRAY::FIELD-TABLEP-ORDERING-ARBITRARY-FIELD-BASED
 (54 41 (:REWRITE DEFAULT-<-1))
 (41 41 (:REWRITE DEFAULT-<-2))
 (34 8 (:REWRITE FARRAY::INTEGERP-+))
 (29 3 (:REWRITE FARRAY::<-1+))
 (28 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (23 7 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (22 22 (:REWRITE DEFAULT-+-2))
 (22 22 (:REWRITE DEFAULT-+-1))
 (14 1 (:REWRITE FARRAY::INTEGERP-TYPES))
 (7 7 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 )
(FARRAY::FIELD-TABLEP-ORDERING-ARBITRARY-FIELD-BASED-OFFSET-ONE
 (170 97 (:REWRITE DEFAULT-<-1))
 (142 134 (:REWRITE DEFAULT-+-2))
 (138 134 (:REWRITE DEFAULT-+-1))
 (105 97 (:REWRITE DEFAULT-<-2))
 (103 45 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (95 18 (:REWRITE FARRAY::INTEGERP-TYPES))
 (47 6 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (41 41 (:REWRITE FOLD-CONSTS-IN-+))
 (30 30 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 (12 6 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (6 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (1 1 (:REWRITE EQUAL-CONSTANT-+))
 (1 1 (:META CANCEL_TIMES-EQUAL-CORRECT))
 (1 1 (:META CANCEL_PLUS-EQUAL-CORRECT))
 )
(FARRAY::FIELD-TABLEP-ORDERING-ARBITRARY-FIELD-BASED-OFFSET-BOTH
 (292 155 (:REWRITE DEFAULT-+-1))
 (244 23 (:REWRITE FARRAY::INTEGERP-TYPES))
 (231 159 (:REWRITE DEFAULT-<-1))
 (226 54 (:REWRITE FARRAY::INTEGERP-+))
 (170 155 (:REWRITE DEFAULT-+-2))
 (167 59 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (161 159 (:REWRITE DEFAULT-<-2))
 (147 6 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (56 56 (:REWRITE FOLD-CONSTS-IN-+))
 (18 6 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (12 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 2 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (4 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1 1 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 )
(FARRAY::FIELD-TABLEP-ORDERING-ARBITRARY-FIELD-BASED-OFFSET-BOTH-NE
 (3282 920 (:REWRITE DEFAULT-+-1))
 (2954 136 (:REWRITE FARRAY::INTEGERP-TYPES))
 (1264 371 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-INTEGERP-MEMI))
 (1212 909 (:REWRITE DEFAULT-<-1))
 (1044 920 (:REWRITE DEFAULT-+-2))
 (909 909 (:REWRITE DEFAULT-<-2))
 (588 27 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (413 413 (:REWRITE FOLD-CONSTS-IN-+))
 (81 27 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (78 26 (:REWRITE DEFAULT-UNARY-MINUS))
 (68 34 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FARRAY::FREAD-FWRITE
 (2856 6 (:REWRITE FARRAY::!MEMI-REDUNDANT))
 (2812 6 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (2396 140 (:REWRITE FARRAY::INTEGERP-TYPES))
 (2029 657 (:REWRITE DEFAULT-+-1))
 (1764 1201 (:REWRITE DEFAULT-<-1))
 (1205 1201 (:REWRITE DEFAULT-<-2))
 (921 657 (:REWRITE DEFAULT-+-2))
 (576 19 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (359 1 (:REWRITE FARRAY::FIELD-TABLEP-ORDERING-ARBITRARY-FIELD-BASED-OFFSET-BOTH-NE))
 (285 285 (:REWRITE FOLD-CONSTS-IN-+))
 (77 14 (:REWRITE FARRAY::<=-0-+))
 (66 22 (:REWRITE DEFAULT-UNARY-MINUS))
 (57 19 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (44 22 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FARRAY::FWRITE-FWRITE-SAME
 (1788 3 (:REWRITE FARRAY::!MEMI-REDUNDANT))
 (1758 3 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (835 37 (:REWRITE FARRAY::INTEGERP-TYPES))
 (825 65 (:REWRITE FARRAY::<-1+))
 (729 163 (:REWRITE DEFAULT-+-1))
 (593 1 (:REWRITE FARRAY::STP-!MEMI))
 (546 374 (:REWRITE DEFAULT-<-1))
 (424 72 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (374 374 (:REWRITE DEFAULT-<-2))
 (197 163 (:REWRITE DEFAULT-+-2))
 (145 4 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (101 14 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (81 81 (:REWRITE FOLD-CONSTS-IN-+))
 (33 6 (:REWRITE FARRAY::<=-0-+))
 (20 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (19 1 (:REWRITE FARRAY::!MEMI-!MEMI-DIFFERENT))
 (12 4 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (12 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 2 (:REWRITE DEFAULT-CDR))
 (4 2 (:REWRITE DEFAULT-CAR))
 )
(FARRAY::FWRITE-REDUNDANT
 (454 168 (:REWRITE DEFAULT-+-1))
 (418 27 (:REWRITE FARRAY::INTEGERP-TYPES))
 (249 165 (:REWRITE DEFAULT-<-1))
 (190 168 (:REWRITE DEFAULT-+-2))
 (165 165 (:REWRITE DEFAULT-<-2))
 (147 6 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (100 10 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (75 9 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (71 71 (:REWRITE FOLD-CONSTS-IN-+))
 (71 1 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (20 5 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (18 6 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (12 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(FARRAY::FWRITE-FWRITE-DIFFERENT-FIELD
 (4738 18 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (4262 968 (:REWRITE DEFAULT-+-1))
 (4106 169 (:REWRITE FARRAY::INTEGERP-TYPES))
 (3518 4 (:REWRITE FARRAY::FWRITE-REDUNDANT))
 (2568 8 (:REWRITE FARRAY::!MEMI-REDUNDANT))
 (1864 8 (:REWRITE FARRAY::MEM-LEN-!MEMI))
 (1673 1234 (:REWRITE DEFAULT-<-1))
 (1666 6 (:REWRITE FARRAY::STP-!MEMI))
 (1407 185 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (1236 1234 (:REWRITE DEFAULT-<-2))
 (1116 968 (:REWRITE DEFAULT-+-2))
 (520 19 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (493 493 (:REWRITE FOLD-CONSTS-IN-+))
 (362 72 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (110 54 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (90 30 (:REWRITE DEFAULT-UNARY-MINUS))
 (51 17 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (32 2 (:REWRITE FARRAY::!MEMI-!MEMI-DIFFERENT))
 (30 2 (:DEFINITION FARRAY::FREAD))
 (8 4 (:REWRITE DEFAULT-CDR))
 (8 4 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE FARRAY::FIELD-TABLEP-!MEMI))
 )
(FARRAY::FWRITE-FWRITE-DIFFERENT-OFFSET
 (9332 32 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (7036 8 (:REWRITE FARRAY::FWRITE-REDUNDANT))
 (6067 1184 (:REWRITE DEFAULT-+-1))
 (6061 231 (:REWRITE FARRAY::INTEGERP-TYPES))
 (5812 495 (:REWRITE FARRAY::<-1+))
 (4952 12 (:REWRITE FARRAY::!MEMI-REDUNDANT))
 (3728 16 (:REWRITE FARRAY::MEM-LEN-!MEMI))
 (3316 10 (:REWRITE FARRAY::STP-!MEMI))
 (2497 1844 (:REWRITE DEFAULT-<-1))
 (1848 1844 (:REWRITE DEFAULT-<-2))
 (1377 1184 (:REWRITE DEFAULT-+-2))
 (663 663 (:REWRITE FOLD-CONSTS-IN-+))
 (491 15 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (363 2 (:REWRITE FARRAY::FIELD-TABLEP-ORDERING-ARBITRARY-FIELD-BASED-OFFSET-BOTH-NE))
 (172 84 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (114 38 (:REWRITE DEFAULT-UNARY-MINUS))
 (60 4 (:DEFINITION FARRAY::FREAD))
 (46 3 (:REWRITE FARRAY::!MEMI-!MEMI-DIFFERENT))
 (33 11 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (12 6 (:REWRITE DEFAULT-CDR))
 (12 6 (:REWRITE DEFAULT-CAR))
 (12 4 (:REWRITE FARRAY::FIELD-TABLEP-!MEMI))
 )
(FARRAY::NUM-FIELDS-FWRITE
 (596 1 (:REWRITE FARRAY::!MEMI-REDUNDANT))
 (586 1 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (552 46 (:REWRITE FARRAY::<-1+))
 (551 23 (:REWRITE FARRAY::INTEGERP-TYPES))
 (528 124 (:REWRITE DEFAULT-+-1))
 (458 1 (:REWRITE FARRAY::FWRITE-REDUNDANT))
 (309 215 (:REWRITE DEFAULT-<-1))
 (284 37 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (241 35 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (215 215 (:REWRITE DEFAULT-<-2))
 (142 124 (:REWRITE DEFAULT-+-2))
 (88 3 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (62 10 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (61 61 (:REWRITE FOLD-CONSTS-IN-+))
 (15 1 (:DEFINITION FARRAY::FREAD))
 (12 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (11 2 (:REWRITE FARRAY::<=-0-+))
 (9 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 )
(FARRAY::FIELDP-FWRITE
 (596 1 (:REWRITE FARRAY::!MEMI-REDUNDANT))
 (586 1 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (565 25 (:REWRITE FARRAY::INTEGERP-TYPES))
 (552 46 (:REWRITE FARRAY::<-1+))
 (528 124 (:REWRITE DEFAULT-+-1))
 (458 1 (:REWRITE FARRAY::FWRITE-REDUNDANT))
 (349 240 (:REWRITE DEFAULT-<-1))
 (311 37 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (242 34 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (240 240 (:REWRITE DEFAULT-<-2))
 (142 124 (:REWRITE DEFAULT-+-2))
 (88 3 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (62 10 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (61 61 (:REWRITE FOLD-CONSTS-IN-+))
 (15 7 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (15 1 (:DEFINITION FARRAY::FREAD))
 (11 2 (:REWRITE FARRAY::<=-0-+))
 (9 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 )
(FARRAY::FIELD-OFFSETP-FWRITE
 (713 31 (:REWRITE FARRAY::INTEGERP-TYPES))
 (706 154 (:REWRITE DEFAULT-+-1))
 (652 55 (:REWRITE FARRAY::<-1+))
 (596 1 (:REWRITE FARRAY::!MEMI-REDUNDANT))
 (586 1 (:REWRITE FARRAY::FIELD-OFFSETP-IMPLIES-OFFSET-+-INDEX-<-MEM-LEN))
 (458 1 (:REWRITE FARRAY::FWRITE-REDUNDANT))
 (345 257 (:REWRITE DEFAULT-<-1))
 (273 37 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (257 257 (:REWRITE DEFAULT-<-2))
 (178 154 (:REWRITE DEFAULT-+-2))
 (88 3 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (75 75 (:REWRITE FOLD-CONSTS-IN-+))
 (70 12 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEMI-1+))
 (30 5 (:REWRITE DEFAULT-UNARY-MINUS))
 (23 11 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (15 1 (:DEFINITION FARRAY::FREAD))
 (11 2 (:REWRITE FARRAY::<=-0-+))
 (6 2 (:REWRITE FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 )
(FARRAY::PRINT-ST1
 (62 17 (:REWRITE FARRAY::SB60P-TYPES))
 (45 6 (:DEFINITION SIGNED-BYTE-P))
 (39 6 (:DEFINITION INTEGER-RANGE-P))
 (25 5 (:REWRITE FARRAY::INTEGERP-TYPES))
 (24 9 (:REWRITE DEFAULT-+-1))
 (21 21 (:REWRITE DEFAULT-<-2))
 (21 21 (:REWRITE DEFAULT-<-1))
 (18 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (12 12 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (12 9 (:REWRITE DEFAULT-+-2))
 (12 2 (:REWRITE FARRAY::INTEGERP-+))
 (7 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (7 3 (:REWRITE FARRAY::<=-0-+))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 )
(FARRAY::PRINT-ST)
(FARRAY::SB60-LISTP)
(FARRAY::WRITE-LIST1
 (95 22 (:REWRITE FARRAY::SB60P-TYPES))
 (46 37 (:REWRITE DEFAULT-<-1))
 (39 37 (:REWRITE DEFAULT-<-2))
 (18 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (16 12 (:REWRITE DEFAULT-+-2))
 (16 12 (:REWRITE DEFAULT-+-1))
 (12 2 (:REWRITE FARRAY::INTEGERP-TYPES))
 (12 2 (:REWRITE FARRAY::INTEGERP-+))
 (11 11 (:REWRITE DEFAULT-CAR))
 (9 9 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (6 6 (:REWRITE DEFAULT-CDR))
 (6 2 (:REWRITE FARRAY::!MEMI-REDUNDANT))
 (3 1 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE FARRAY::<-1+))
 )
(FARRAY::WRITE-LIST)
(FARRAY::FIELD-MEMBERP
 (131 35 (:REWRITE FARRAY::SB60P-TYPES))
 (94 11 (:DEFINITION SIGNED-BYTE-P))
 (83 11 (:DEFINITION INTEGER-RANGE-P))
 (59 11 (:REWRITE FARRAY::INTEGERP-TYPES))
 (52 24 (:REWRITE DEFAULT-+-1))
 (47 34 (:REWRITE DEFAULT-<-1))
 (40 10 (:REWRITE FARRAY::INTEGERP-+))
 (34 34 (:REWRITE DEFAULT-<-2))
 (30 24 (:REWRITE DEFAULT-+-2))
 (18 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (15 5 (:REWRITE FARRAY::<=-0-+))
 (15 5 (:REWRITE FARRAY::<-1+))
 (14 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 5 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (5 5 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (5 5 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (2 2 (:REWRITE FARRAY::SB60P-1+-FIELD-OFFSETP))
 )
(FARRAY::FIELD-MEMBERP-FWRITE-DIFF-FIELD
 (531 176 (:REWRITE FARRAY::SB60P-TYPES))
 (436 74 (:REWRITE FARRAY::INTEGERP-TYPES))
 (381 51 (:REWRITE DEFAULT-+-2))
 (310 119 (:REWRITE DEFAULT-<-1))
 (119 119 (:REWRITE DEFAULT-<-2))
 (111 37 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (51 51 (:REWRITE DEFAULT-+-1))
 (15 3 (:REWRITE FARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (10 10 (:REWRITE FARRAY::FWRITE-REDUNDANT))
 (10 10 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (10 10 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (10 10 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (3 3 (:REWRITE FARRAY::FIELD-OFFSETP-1--NOT-0))
 )
(FARRAY::FIELD-MEMBERP-FREAD-FWRITE-WEIRD
 (6 6 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE DEFAULT-<-1))
 (5 1 (:REWRITE FARRAY::SB60P-TYPES))
 (2 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE FARRAY::FWRITE-REDUNDANT))
 (1 1 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-DIFF-FIELD))
 (1 1 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (1 1 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (1 1 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 )
(FARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-LOW
 (581 204 (:REWRITE FARRAY::SB60P-TYPES))
 (486 88 (:REWRITE FARRAY::INTEGERP-TYPES))
 (387 63 (:REWRITE DEFAULT-+-2))
 (308 129 (:REWRITE DEFAULT-<-1))
 (207 129 (:REWRITE DEFAULT-<-2))
 (132 44 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (63 63 (:REWRITE DEFAULT-+-1))
 (10 10 (:REWRITE FARRAY::FWRITE-REDUNDANT))
 (10 10 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-DIFF-FIELD))
 (9 9 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (9 9 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (9 9 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 )
(FARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-HIGH
 (705 236 (:REWRITE FARRAY::SB60P-TYPES))
 (610 104 (:REWRITE FARRAY::INTEGERP-TYPES))
 (453 172 (:REWRITE DEFAULT-<-1))
 (417 61 (:REWRITE DEFAULT-+-2))
 (250 172 (:REWRITE DEFAULT-<-2))
 (156 52 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (121 11 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-LOW))
 (61 61 (:REWRITE DEFAULT-+-1))
 (27 3 (:REWRITE FARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (10 10 (:REWRITE FARRAY::FWRITE-REDUNDANT))
 (10 10 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-DIFF-FIELD))
 (8 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (8 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (8 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (3 3 (:REWRITE FARRAY::FIELD-OFFSETP-1--NOT-0))
 )
(FARRAY::FIELD-MEMBERP-FWRITE-SAME-VALUE
 (142 2 (:DEFINITION FARRAY::FIELD-MEMBERP))
 (100 17 (:REWRITE FARRAY::INTEGERP-TYPES))
 (96 6 (:REWRITE DEFAULT-+-2))
 (50 20 (:REWRITE DEFAULT-<-1))
 (24 8 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (20 20 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE DEFAULT-+-1))
 (1 1 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (1 1 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (1 1 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 )
(FARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-IS-ELEM
 (65 19 (:REWRITE FARRAY::SB60P-TYPES))
 (49 49 (:REWRITE DEFAULT-<-2))
 (49 49 (:REWRITE DEFAULT-<-1))
 (42 42 (:REWRITE DEFAULT-+-2))
 (42 42 (:REWRITE DEFAULT-+-1))
 (31 31 (:REWRITE FARRAY::FWRITE-REDUNDANT))
 (15 15 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (15 15 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (15 15 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (7 7 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-SAME-VALUE))
 (7 7 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-LOW))
 (7 7 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-HIGH))
 (7 7 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-DIFF-FIELD))
 (1 1 (:REWRITE FARRAY::FIELD-OFFSETP-1--NOT-0))
 )
(FARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-NOT-ELEM
 (675 224 (:REWRITE FARRAY::SB60P-TYPES))
 (580 98 (:REWRITE FARRAY::INTEGERP-TYPES))
 (431 75 (:REWRITE DEFAULT-+-2))
 (420 175 (:REWRITE DEFAULT-<-1))
 (253 175 (:REWRITE DEFAULT-<-2))
 (150 12 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-HIGH))
 (147 49 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (124 12 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-LOW))
 (75 75 (:REWRITE DEFAULT-+-1))
 (40 4 (:REWRITE FARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (19 19 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-IS-ELEM))
 (12 12 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-SAME-VALUE))
 (12 12 (:REWRITE FARRAY::FIELD-MEMBERP-FWRITE-DIFF-FIELD))
 (11 3 (:REWRITE FARRAY::FIELD-MEMBERP-FREAD-FWRITE-WEIRD))
 (10 10 (:REWRITE FARRAY::FWRITE-REDUNDANT))
 (8 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<=-0-MEMI))
 (8 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-MEMI-MEM-LEN))
 (8 8 (:LINEAR FARRAY::FIELD-TABLEP-IMPLIES-<-END-MEMI))
 (4 4 (:REWRITE FARRAY::FIELD-OFFSETP-1--NOT-0))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 )