File: assignment-st%40useless-runes.lsp

package info (click to toggle)
acl2 8.6%2Bdfsg-2
links: PTS
area: main
in suites: trixie
size: 1,111,420 kB
sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (2522 lines) | stat: -rw-r--r-- 141,106 bytes
parent folder | download | duplicates (3)
(PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP
 (40 10 (:REWRITE DEFAULT-+-2))
 (34 4 (:DEFINITION SIGNED-BYTE-P))
 (29 4 (:DEFINITION INTEGER-RANGE-P))
 (25 5 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (16 15 (:REWRITE DEFAULT-<-1))
 (15 15 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE DEFAULT-+-1))
 (7 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (2 2 (:TYPE-PRESCRIPTION INTEGER-RANGE-P))
 )
(PROOF-CHECKER-ARRAY::STACK-UNIQUEP
 (80 20 (:REWRITE DEFAULT-+-2))
 (50 6 (:DEFINITION SIGNED-BYTE-P))
 (49 9 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (47 2 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (43 6 (:DEFINITION INTEGER-RANGE-P))
 (22 21 (:REWRITE DEFAULT-<-1))
 (21 21 (:REWRITE DEFAULT-<-2))
 (20 20 (:REWRITE DEFAULT-+-1))
 (15 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (13 5 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (2 2 (:TYPE-PRESCRIPTION INTEGER-RANGE-P))
 )
(PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP
 (144 39 (:REWRITE DEFAULT-+-2))
 (85 15 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (74 9 (:DEFINITION SIGNED-BYTE-P))
 (64 9 (:DEFINITION INTEGER-RANGE-P))
 (51 2 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (39 39 (:REWRITE DEFAULT-+-1))
 (30 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (28 27 (:REWRITE DEFAULT-<-1))
 (27 27 (:REWRITE DEFAULT-<-2))
 (22 8 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (11 11 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (2 2 (:TYPE-PRESCRIPTION INTEGER-RANGE-P))
 )
(PROOF-CHECKER-ARRAY::INTEGERP-+-2)
(PROOF-CHECKER-ARRAY::INTEGERP--)
(PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP
 (266 51 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (213 21 (:DEFINITION SIGNED-BYTE-P))
 (192 21 (:DEFINITION INTEGER-RANGE-P))
 (81 53 (:REWRITE DEFAULT-<-2))
 (55 53 (:REWRITE DEFAULT-<-1))
 (48 3 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (47 38 (:REWRITE DEFAULT-+-2))
 (45 38 (:REWRITE DEFAULT-+-1))
 (43 10 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP--))
 (22 7 (:REWRITE DEFAULT-UNARY-MINUS))
 (20 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (13 7 (:REWRITE FOLD-CONSTS-IN-+))
 (9 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (2 2 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1--FIELD-OFFSETP))
 )
(PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*
 (189 61 (:REWRITE DEFAULT-<-2))
 (188 30 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (186 58 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (146 62 (:REWRITE DEFAULT-+-2))
 (108 14 (:DEFINITION SIGNED-BYTE-P))
 (94 14 (:DEFINITION INTEGER-RANGE-P))
 (62 62 (:REWRITE DEFAULT-+-1))
 (61 61 (:REWRITE DEFAULT-<-1))
 (56 12 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (42 14 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (18 6 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (16 12 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 )
(PROOF-CHECKER-ARRAY::STACK-IN-RANGEP
 (40 10 (:REWRITE DEFAULT-+-2))
 (35 4 (:DEFINITION SIGNED-BYTE-P))
 (30 4 (:DEFINITION INTEGER-RANGE-P))
 (25 5 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (16 15 (:REWRITE DEFAULT-<-1))
 (15 15 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE DEFAULT-+-1))
 (7 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 3 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-+-2))
 (5 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (2 2 (:TYPE-PRESCRIPTION INTEGER-RANGE-P))
 )
(PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P
 (103 28 (:REWRITE DEFAULT-+-2))
 (61 11 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (59 7 (:DEFINITION SIGNED-BYTE-P))
 (51 7 (:DEFINITION INTEGER-RANGE-P))
 (28 28 (:REWRITE DEFAULT-+-1))
 (22 21 (:REWRITE DEFAULT-<-1))
 (21 21 (:REWRITE DEFAULT-<-2))
 (20 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (16 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 3 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-+-2))
 (2 2 (:TYPE-PRESCRIPTION INTEGER-RANGE-P))
 )
(PROOF-CHECKER-ARRAY::NOT-EVENP-1+
 (36 12 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (26 6 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (24 3 (:DEFINITION SIGNED-BYTE-P))
 (21 3 (:DEFINITION INTEGER-RANGE-P))
 (20 5 (:REWRITE DEFAULT-*-1))
 (17 2 (:REWRITE DEFAULT-+-2))
 (11 5 (:REWRITE DEFAULT-*-2))
 (8 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 6 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (6 6 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::EVENP-+-2
 (36 12 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (26 6 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (24 3 (:DEFINITION SIGNED-BYTE-P))
 (21 3 (:DEFINITION INTEGER-RANGE-P))
 (20 5 (:REWRITE DEFAULT-*-1))
 (17 2 (:REWRITE DEFAULT-+-2))
 (11 5 (:REWRITE DEFAULT-*-2))
 (8 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 6 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (6 6 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::EVENP-<-1+
 (20 4 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (16 2 (:DEFINITION SIGNED-BYTE-P))
 (14 2 (:DEFINITION INTEGER-RANGE-P))
 (5 5 (:REWRITE DEFAULT-*-2))
 (5 5 (:REWRITE DEFAULT-*-1))
 (4 4 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2
 (20 4 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (16 2 (:DEFINITION SIGNED-BYTE-P))
 (14 2 (:DEFINITION INTEGER-RANGE-P))
 (5 5 (:REWRITE DEFAULT-*-2))
 (5 5 (:REWRITE DEFAULT-*-1))
 (4 4 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+
 (8 2 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (6 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (6 1 (:DEFINITION SIGNED-BYTE-P))
 (5 4 (:REWRITE DEFAULT-<-2))
 (5 1 (:DEFINITION INTEGER-RANGE-P))
 (4 4 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2
 (22 4 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (14 13 (:REWRITE DEFAULT-<-2))
 (13 13 (:REWRITE DEFAULT-<-1))
 (8 2 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (6 1 (:DEFINITION SIGNED-BYTE-P))
 (5 1 (:DEFINITION INTEGER-RANGE-P))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED
 (152 29 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (123 11 (:DEFINITION SIGNED-BYTE-P))
 (112 11 (:DEFINITION INTEGER-RANGE-P))
 (34 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (29 28 (:REWRITE DEFAULT-<-2))
 (29 28 (:REWRITE DEFAULT-<-1))
 (24 4 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (18 13 (:REWRITE DEFAULT-+-2))
 (17 13 (:REWRITE DEFAULT-+-1))
 (9 6 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP--))
 (6 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 )
(PROOF-CHECKER-ARRAY::EVENP-FLENGTH-*LOOKUP*
 (34 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (28 4 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (24 2 (:DEFINITION SIGNED-BYTE-P))
 (22 2 (:DEFINITION INTEGER-RANGE-P))
 (8 8 (:REWRITE DEFAULT-*-2))
 (8 8 (:REWRITE DEFAULT-*-1))
 (8 2 (:REWRITE <-*-/-LEFT-COMMUTED))
 (6 6 (:META CANCEL_PLUS-LESSP-CORRECT))
 (4 4 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::ASSIGNMENT-STP
 (1525 1243 (:REWRITE DEFAULT-+-2))
 (1251 417 (:REWRITE FOLD-CONSTS-IN-+))
 (1243 1243 (:REWRITE DEFAULT-+-1))
 (590 54 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (226 94 (:REWRITE DEFAULT-<-1))
 (139 27 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (132 14 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (105 15 (:REWRITE DEFAULT-*-2))
 (94 94 (:REWRITE DEFAULT-<-2))
 (90 14 (:DEFINITION SIGNED-BYTE-P))
 (76 14 (:DEFINITION INTEGER-RANGE-P))
 (72 27 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (58 58 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (58 58 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (54 54 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (50 50 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (15 15 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::LIT-IN-RANGEP)
(PROOF-CHECKER-ARRAY::ASSIGNEDP)
(PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*)
(PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1
 (372 124 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (372 62 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (342 27 (:REWRITE DEFAULT-+-2))
 (248 31 (:DEFINITION SIGNED-BYTE-P))
 (217 31 (:DEFINITION INTEGER-RANGE-P))
 (202 72 (:REWRITE DEFAULT-<-1))
 (93 31 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (72 72 (:REWRITE DEFAULT-<-2))
 (62 62 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (36 2 (:REWRITE FOLD-CONSTS-IN-+))
 (27 27 (:REWRITE DEFAULT-+-1))
 (25 7 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (17 7 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 )
(PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-ASSIGNEDP
 (1857 6 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (1249 821 (:REWRITE DEFAULT-+-2))
 (991 107 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (901 18 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (821 821 (:REWRITE DEFAULT-+-1))
 (806 11 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (709 32 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (550 24 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (478 11 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (457 37 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (318 66 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (223 49 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (198 103 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (162 27 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (137 21 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (104 68 (:REWRITE DEFAULT-<-1))
 (90 68 (:REWRITE DEFAULT-<-2))
 (81 27 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (77 11 (:REWRITE DEFAULT-*-2))
 (66 11 (:DEFINITION SIGNED-BYTE-P))
 (55 11 (:DEFINITION INTEGER-RANGE-P))
 (40 40 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (40 40 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (25 25 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (18 6 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (11 11 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::EQUAL-ASSIGNEDP-FIELD-MEMBERP-*STACK*
 (3966 2366 (:REWRITE DEFAULT-+-2))
 (2366 2366 (:REWRITE DEFAULT-+-1))
 (1939 129 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (1840 416 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (528 88 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (292 145 (:REWRITE DEFAULT-<-1))
 (245 35 (:REWRITE DEFAULT-*-2))
 (210 35 (:DEFINITION SIGNED-BYTE-P))
 (175 35 (:DEFINITION INTEGER-RANGE-P))
 (165 145 (:REWRITE DEFAULT-<-2))
 (97 97 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (82 82 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (35 35 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP
 (8 2 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (6 6 (:TYPE-PRESCRIPTION EVENP))
 (5 5 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 )
(PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*
 (568 115 (:REWRITE DEFAULT-+-2))
 (552 204 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (552 102 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (348 51 (:DEFINITION SIGNED-BYTE-P))
 (330 105 (:REWRITE DEFAULT-<-1))
 (297 51 (:DEFINITION INTEGER-RANGE-P))
 (153 51 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (115 115 (:REWRITE DEFAULT-+-1))
 (105 105 (:REWRITE DEFAULT-<-2))
 (44 26 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (29 29 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (26 26 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 )
(PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1
 (873 1 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (871 1 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (495 5 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (190 107 (:REWRITE DEFAULT-+-2))
 (179 27 (:REWRITE FOLD-CONSTS-IN-+))
 (137 137 (:TYPE-PRESCRIPTION EVENP))
 (115 7 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (107 107 (:REWRITE DEFAULT-+-1))
 (97 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (94 94 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (92 22 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (68 22 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (67 9 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (65 3 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (64 3 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (63 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (57 14 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (51 8 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (46 10 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (45 15 (:REWRITE UNICITY-OF-0))
 (41 2 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (41 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (30 15 (:DEFINITION FIX))
 (24 3 (:DEFINITION SIGNED-BYTE-P))
 (23 23 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::FIELDP))
 (23 10 (:REWRITE DEFAULT-<-2))
 (22 22 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (21 3 (:DEFINITION INTEGER-RANGE-P))
 (19 19 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (16 10 (:REWRITE DEFAULT-<-1))
 (15 5 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (11 11 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (11 7 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (10 10 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (8 8 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (8 8 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (8 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (7 1 (:REWRITE DEFAULT-*-2))
 (6 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5 5 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (5 5 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (5 5 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (4 4 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (2 2 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (2 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (1 1 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1
 (4090 38 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (4086 2 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (3338 10 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (950 42 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (679 405 (:REWRITE DEFAULT-+-2))
 (672 232 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (591 95 (:REWRITE FOLD-CONSTS-IN-+))
 (456 214 (:REWRITE DEFAULT-<-2))
 (432 72 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (428 428 (:TYPE-PRESCRIPTION EVENP))
 (408 132 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (405 405 (:REWRITE DEFAULT-+-1))
 (384 48 (:DEFINITION SIGNED-BYTE-P))
 (344 132 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (336 48 (:DEFINITION INTEGER-RANGE-P))
 (331 3 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (326 58 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (300 100 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (254 14 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (226 214 (:REWRITE DEFAULT-<-1))
 (188 188 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (171 8 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (138 46 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (128 6 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (126 2 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (104 104 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (95 95 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::FIELDP))
 (92 92 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (92 20 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (90 30 (:REWRITE UNICITY-OF-0))
 (82 2 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (77 77 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (70 54 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (60 30 (:DEFINITION FIX))
 (48 16 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (38 38 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (17 17 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (16 16 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (14 2 (:REWRITE DEFAULT-*-2))
 (11 11 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (8 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-<-NEGATE))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (3 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (2 2 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1
 (103 13 (:REWRITE DEFAULT-+-2))
 (83 22 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (75 10 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (46 6 (:DEFINITION SIGNED-BYTE-P))
 (40 6 (:DEFINITION INTEGER-RANGE-P))
 (34 1 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (15 5 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (15 5 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (14 14 (:REWRITE DEFAULT-<-2))
 (14 14 (:REWRITE DEFAULT-<-1))
 (13 13 (:REWRITE DEFAULT-+-1))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (9 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (8 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (3 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (2 2 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 )
(PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+
 (2568 22 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (2564 2 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (1853 8 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (936 22 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (574 144 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (554 26 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (540 110 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (368 284 (:REWRITE DEFAULT-+-2))
 (366 366 (:TYPE-PRESCRIPTION EVENP))
 (333 29 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (284 284 (:REWRITE DEFAULT-+-1))
 (244 40 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (218 66 (:REWRITE FOLD-CONSTS-IN-+))
 (199 22 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (194 2 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (130 6 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (128 6 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (126 2 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (114 114 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (109 109 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (87 16 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (82 2 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (72 24 (:REWRITE UNICITY-OF-0))
 (60 12 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (52 52 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (48 24 (:DEFINITION FIX))
 (48 8 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (46 34 (:REWRITE DEFAULT-<-1))
 (44 36 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (34 34 (:REWRITE DEFAULT-<-2))
 (34 4 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (24 8 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (22 22 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (22 22 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (16 16 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (16 16 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (16 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (16 2 (:DEFINITION SIGNED-BYTE-P))
 (14 2 (:REWRITE DEFAULT-*-2))
 (14 2 (:DEFINITION INTEGER-RANGE-P))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (8 8 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (8 2 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (4 4 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (4 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (2 2 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2
 (121463 517 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (121369 47 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (63499 202 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (61877 756 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (25224 606 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (24545 1010 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (23287 6284 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (19350 866 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (18870 4240 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (12618 12618 (:TYPE-PRESCRIPTION EVENP))
 (11678 971 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (10601 7102 (:REWRITE DEFAULT-+-2))
 (10534 10534 (:TYPE-PRESCRIPTION |x < y  =>  0 < -x+y|))
 (9254 6201 (:META CANCEL_PLUS-EQUAL-CORRECT))
 (9199 55 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (8065 1888 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (8030 1543 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (7102 7102 (:REWRITE DEFAULT-+-1))
 (6201 6201 (:META CANCEL_TIMES-EQUAL-CORRECT))
 (5903 157 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (5683 49 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (5436 145 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (5002 5002 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (4473 585 (:DEFINITION SIGNED-BYTE-P))
 (3915 47 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (3888 585 (:DEFINITION INTEGER-RANGE-P))
 (3665 2888 (:REWRITE DEFAULT-<-1))
 (3197 3197 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (3182 2888 (:REWRITE DEFAULT-<-2))
 (3126 1704 (:DEFINITION FIX))
 (2403 173 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (2393 867 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (2357 471 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (1818 606 (:REWRITE UNICITY-OF-0))
 (1534 1286 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (1456 266 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-+-2))
 (1071 357 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (573 573 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (541 257 (:REWRITE EQUAL-CONSTANT-+))
 (517 517 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (416 416 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (408 110 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (386 386 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (329 47 (:REWRITE DEFAULT-*-2))
 (275 275 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (245 245 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (235 235 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (204 204 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (171 57 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (138 138 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1+-FIELD-OFFSETP))
 (120 40 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-+-2))
 (112 8 (:REWRITE <-0-+-NEGATIVE-1))
 (102 102 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (102 102 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (47 47 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::<=-+-2-FLENGTH
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::<=-+-COUNT-ASSIGNED-COUNT-ASSIGNED-FLENGTH-*LOOKUP*-MINUS-I
 (7712 52 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (6896 52 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (6872 12 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (1816 896 (:REWRITE DEFAULT-+-2))
 (1564 64 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (911 896 (:REWRITE DEFAULT-+-1))
 (868 208 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (796 116 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (768 36 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (756 12 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (728 124 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (496 52 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (492 12 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (403 321 (:REWRITE DEFAULT-<-1))
 (368 46 (:DEFINITION SIGNED-BYTE-P))
 (335 321 (:REWRITE DEFAULT-<-2))
 (322 46 (:DEFINITION INTEGER-RANGE-P))
 (320 320 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (272 272 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (264 12 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (244 82 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (183 39 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (160 112 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (137 137 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (132 12 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (102 34 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (96 96 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (96 24 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (84 12 (:REWRITE DEFAULT-*-2))
 (60 60 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (60 60 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (60 60 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (52 52 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (24 24 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (12 12 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (12 12 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (12 12 (:REWRITE DEFAULT-*-1))
 (10 10 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(PROOF-CHECKER-ARRAY::<=-+-COUNT-ASSIGNED-COUNT-ASSIGNED-FLENGTH-*LOOKUP*-MINUS-I-2
 (36336 314 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (36248 44 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (7452 4100 (:REWRITE DEFAULT-+-2))
 (6243 1861 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (4131 4100 (:REWRITE DEFAULT-+-1))
 (3216 314 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (3201 565 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (2871 682 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (2688 126 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (2646 42 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (2621 384 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (1888 1601 (:REWRITE DEFAULT-<-1))
 (1722 42 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (1620 1601 (:REWRITE DEFAULT-<-2))
 (1535 1535 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (1192 149 (:DEFINITION SIGNED-BYTE-P))
 (1043 149 (:DEFINITION INTEGER-RANGE-P))
 (925 91 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (924 42 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (827 277 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (809 809 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (693 523 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (336 336 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (336 84 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (321 107 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (314 314 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (294 42 (:REWRITE DEFAULT-*-2))
 (210 210 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (210 210 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (210 210 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (84 84 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (42 42 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (42 42 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (42 42 (:REWRITE DEFAULT-*-1))
 (18 18 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 2 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-+-2))
 )
(PROOF-CHECKER-ARRAY::<=-+-COUNT-ASSIGNED-COUNT-ASSIGNED-FLENGTH-*LOOKUP*-MINUS-I-3
 (24592 126 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (24540 26 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (4826 736 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (4578 1004 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (4449 1609 (:META CANCEL_PLUS-EQUAL-CORRECT))
 (4138 1937 (:REWRITE DEFAULT-+-2))
 (2882 22 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (2816 66 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (2178 22 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (1960 126 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (1957 1937 (:REWRITE DEFAULT-+-1))
 (1946 729 (:REWRITE DEFAULT-<-1))
 (1866 624 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (1609 1609 (:META CANCEL_TIMES-EQUAL-CORRECT))
 (1232 22 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (1196 134 (:DEFINITION SIGNED-BYTE-P))
 (1090 1090 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (1062 134 (:DEFINITION INTEGER-RANGE-P))
 (745 729 (:REWRITE DEFAULT-<-2))
 (658 234 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (425 70 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (336 112 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (329 329 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (282 30 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (267 91 (:REWRITE EQUAL-CONSTANT-+))
 (176 176 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (176 44 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (154 22 (:REWRITE DEFAULT-*-2))
 (126 126 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (110 110 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (110 110 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (110 110 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (44 44 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (22 22 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (22 22 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (22 22 (:REWRITE DEFAULT-*-1))
 (10 10 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(PROOF-CHECKER-ARRAY::<=-+-COUNT-ASSIGNED-COUNT-ASSIGNED-FLENGTH-*LOOKUP*-MINUS-I-4
 (1334 6 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (1048 4 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (1040 4 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (458 188 (:REWRITE DEFAULT-+-2))
 (300 72 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (276 40 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (256 12 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (252 4 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (228 8 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (204 44 (:REWRITE FOLD-CONSTS-IN-+))
 (202 30 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (194 188 (:REWRITE DEFAULT-+-1))
 (164 4 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (128 16 (:DEFINITION SIGNED-BYTE-P))
 (112 16 (:DEFINITION INTEGER-RANGE-P))
 (90 60 (:REWRITE DEFAULT-<-1))
 (88 4 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (84 28 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (63 60 (:REWRITE DEFAULT-<-2))
 (44 4 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (42 26 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (40 40 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (36 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (32 32 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (32 32 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (32 8 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (28 4 (:REWRITE DEFAULT-*-2))
 (20 20 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (20 20 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (20 20 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (20 8 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (18 18 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (10 4 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (5 1 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (4 4 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (4 4 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (4 4 (:REWRITE DEFAULT-*-1))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (3 3 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-<=-FLENGTH-/-2
 (7081 31 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (7059 11 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (1987 282 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (1924 418 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (1512 514 (:META CANCEL_PLUS-EQUAL-CORRECT))
 (1415 582 (:REWRITE DEFAULT-+-2))
 (1179 9 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (1152 27 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (953 144 (:DEFINITION FIX))
 (932 84 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (891 9 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (692 66 (:DEFINITION SIGNED-BYTE-P))
 (641 215 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (626 66 (:DEFINITION INTEGER-RANGE-P))
 (623 263 (:META CANCEL_PLUS-LESSP-CORRECT))
 (601 229 (:REWRITE DEFAULT-<-1))
 (589 582 (:REWRITE DEFAULT-+-1))
 (574 131 (:REWRITE FOLD-CONSTS-IN-+))
 (514 514 (:META CANCEL_TIMES-EQUAL-CORRECT))
 (504 9 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (478 143 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (436 34 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (434 97 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (320 31 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (312 312 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (286 286 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (276 8 (:REWRITE <-*-/-LEFT-COMMUTED))
 (238 229 (:REWRITE DEFAULT-<-2))
 (207 75 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (177 18 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (148 57 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (141 47 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (112 15 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (112 4 (:REWRITE RATIONALP-*))
 (103 31 (:REWRITE EQUAL-CONSTANT-+))
 (99 33 (:REWRITE UNICITY-OF-0))
 (96 29 (:REWRITE DEFAULT-*-2))
 (89 89 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (72 72 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (72 18 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (50 1 (:LINEAR X*Y>1-POSITIVE))
 (45 45 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (45 45 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (45 45 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (45 18 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (37 29 (:REWRITE DEFAULT-*-1))
 (31 31 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (30 5 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (28 14 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-FLENGTH))
 (24 4 (:REWRITE <-*-LEFT-CANCEL))
 (24 4 (:REWRITE <-*-/-RIGHT-COMMUTED))
 (23 9 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FLENGTH))
 (21 2 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-+-2))
 (20 10 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (18 18 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (11 11 (:REWRITE DEFAULT-UNARY-MINUS))
 (9 9 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (9 9 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (4 4 (:REWRITE X*Y>1-POSITIVE-LEMMA))
 (4 4 (:REWRITE *-PRESERVES->=-FOR-NONNEGATIVES))
 (4 4 (:REWRITE *-PRESERVES->-FOR-NONNEGATIVES-1))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-<=-*NUM-VARS*
 (4287 16 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (3875 6 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (3677 15 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (3667 5 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (1188 20 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (885 133 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (857 193 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (801 266 (:META CANCEL_PLUS-EQUAL-CORRECT))
 (705 309 (:REWRITE DEFAULT-+-2))
 (655 5 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (640 15 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (511 78 (:DEFINITION FIX))
 (505 45 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (495 5 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (327 109 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (310 309 (:REWRITE DEFAULT-+-1))
 (304 71 (:REWRITE FOLD-CONSTS-IN-+))
 (296 116 (:META CANCEL_PLUS-LESSP-CORRECT))
 (280 5 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (266 266 (:META CANCEL_TIMES-EQUAL-CORRECT))
 (258 101 (:REWRITE DEFAULT-<-1))
 (252 30 (:DEFINITION SIGNED-BYTE-P))
 (247 70 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (223 18 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (222 30 (:DEFINITION INTEGER-RANGE-P))
 (214 49 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (164 15 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (159 159 (:TYPE-PRESCRIPTION EVENP))
 (151 151 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::FIELDP))
 (145 145 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (142 142 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (119 101 (:REWRITE DEFAULT-<-2))
 (110 40 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (103 12 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (100 100 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (72 24 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (70 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (63 10 (:REWRITE DEFAULT-*-2))
 (54 18 (:REWRITE UNICITY-OF-0))
 (53 27 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (53 13 (:REWRITE EQUAL-CONSTANT-+))
 (44 44 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (40 40 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (40 10 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (25 25 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (25 25 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (25 25 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (25 10 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (15 15 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (12 10 (:REWRITE DEFAULT-*-1))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (6 1 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (5 5 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (5 5 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (4 2 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (2 2 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****)
(PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2
 (6 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (3 2 (:REWRITE DEFAULT-<-2))
 (3 1 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-NEGATE-1+))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 )
(PROOF-CHECKER-ARRAY::<-1-NEGATE
 (39 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (37 1 (:DEFINITION SIGNED-BYTE-P))
 (36 1 (:DEFINITION INTEGER-RANGE-P))
 (9 2 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (5 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (5 4 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (5 4 (:REWRITE DEFAULT-LESS-THAN-2))
 (4 4 (:REWRITE THE-FLOOR-BELOW))
 (4 4 (:REWRITE THE-FLOOR-ABOVE))
 (4 4 (:REWRITE SIMPLIFY-SUMS-<))
 (4 4 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (4 4 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (4 4 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (4 4 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (4 4 (:REWRITE INTEGERP-<-CONSTANT))
 (4 4 (:REWRITE DEFAULT-LESS-THAN-1))
 (4 4 (:REWRITE CONSTANT-<-INTEGERP))
 (4 4 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (4 4 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (4 4 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (4 4 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (4 4 (:REWRITE |(< c (- x))|))
 (4 4 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (4 4 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (4 4 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (4 4 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (4 4 (:REWRITE |(< (/ x) (/ y))|))
 (4 4 (:REWRITE |(< (- x) c)|))
 (4 4 (:REWRITE |(< (- x) (- y))|))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (3 3 (:REWRITE REDUCE-INTEGERP-+))
 (3 3 (:REWRITE INTEGERP-MINUS-X))
 (3 3 (:META META-INTEGERP-CORRECT))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2 2 (:REWRITE NORMALIZE-ADDENDS))
 (2 2 (:REWRITE DEFAULT-PLUS-2))
 (2 2 (:REWRITE DEFAULT-PLUS-1))
 (2 2 (:REWRITE DEFAULT-LOGXOR-2))
 (2 2 (:REWRITE DEFAULT-LOGXOR-1))
 (1 1 (:REWRITE |(< x (if a b c))|))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-<=-*NUM-VARS*-2
 (1765 10 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (1748 7 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (1343 31 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (949 307 (:REWRITE DEFAULT-+-2))
 (907 11 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (764 29 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (740 185 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (665 93 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (461 57 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (363 46 (:DEFINITION SIGNED-BYTE-P))
 (333 7 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (317 46 (:DEFINITION INTEGER-RANGE-P))
 (307 307 (:REWRITE DEFAULT-+-1))
 (171 57 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (154 7 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (139 109 (:REWRITE DEFAULT-<-2))
 (115 109 (:REWRITE DEFAULT-<-1))
 (109 10 (:REWRITE DEFAULT-*-2))
 (108 36 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (106 10 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (97 53 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (88 22 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (76 76 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (55 55 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (55 22 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (43 43 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (35 35 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (35 35 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (33 10 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (28 10 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (27 9 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (16 8 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (13 4 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-<-NEGATE))
 (12 3 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (10 10 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (10 10 (:REWRITE DEFAULT-*-1))
 (7 7 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 )
(PROOF-CHECKER-ARRAY::FREAD-*STACK-END*-<-FREAD-*NUM-VARS*
 (37343 99 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (10235 8010 (:REWRITE DEFAULT-+-2))
 (8010 8010 (:REWRITE DEFAULT-+-1))
 (6576 105 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (5275 533 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (3476 404 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (2962 633 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (2946 1163 (:REWRITE DEFAULT-<-1))
 (2514 419 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (1889 3 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-ASSIGNEDP-FIELD-MEMBERP-*STACK*))
 (1883 164 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (1768 1163 (:REWRITE DEFAULT-<-2))
 (1263 421 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (1178 428 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (1142 384 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (840 210 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (645 106 (:DEFINITION SIGNED-BYTE-P))
 (539 106 (:DEFINITION INTEGER-RANGE-P))
 (525 210 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (460 106 (:REWRITE DEFAULT-*-2))
 (421 421 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (123 3 (:REWRITE PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-<=-*NUM-VARS*))
 (106 106 (:REWRITE DEFAULT-*-1))
 (106 24 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (89 41 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-<-NEGATE))
 (6 6 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNEDP))
 (6 3 (:REWRITE PROOF-CHECKER-ARRAY::LITERALP-NEGATE))
 )
(PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-FREAD-*STACK-END*-*STACK*
 (1510 166 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (783 124 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (762 86 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (753 563 (:REWRITE DEFAULT-<-1))
 (600 24 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (569 563 (:REWRITE DEFAULT-<-2))
 (560 72 (:DEFINITION SIGNED-BYTE-P))
 (527 19 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (488 72 (:DEFINITION INTEGER-RANGE-P))
 (450 23 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (450 23 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (338 255 (:REWRITE DEFAULT-+-2))
 (255 255 (:REWRITE DEFAULT-+-1))
 (182 38 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-<-NEGATE))
 (132 22 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (83 23 (:REWRITE PROOF-CHECKER-ARRAY::<=-0-NEGATE))
 (72 8 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (67 67 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (67 67 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (50 8 (:REWRITE DEFAULT-*-2))
 (45 45 (:TYPE-PRESCRIPTION EVENP))
 (44 44 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (40 10 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (31 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (28 4 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (28 1 (:REWRITE PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-<=-*NUM-VARS*))
 (25 10 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (8 8 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-FLENGTH))
 (8 8 (:REWRITE DEFAULT-*-1))
 (8 3 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (5 2 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 1 (:REWRITE PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-<=-*NUM-VARS*-2))
 )
(PROOF-CHECKER-ARRAY::ASSIGN-LIT
 (72860 957 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (45786 1958 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (37825 2334 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (36405 79 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (33913 14743 (:REWRITE DEFAULT-+-2))
 (14743 14743 (:REWRITE DEFAULT-+-1))
 (10213 2933 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (9974 1647 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (8815 1159 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (5023 2630 (:REWRITE DEFAULT-<-1))
 (4106 823 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (3149 2630 (:REWRITE DEFAULT-<-2))
 (2458 828 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (2447 817 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (2429 178 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (2183 2183 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (1865 999 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (1764 648 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (944 812 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (900 79 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (812 812 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (595 85 (:REWRITE DEFAULT-*-2))
 (592 148 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (370 148 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (110 18 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (88 22 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (85 85 (:REWRITE DEFAULT-*-1))
 (23 11 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-<-NEGATE))
 (16 6 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 )
(PROOF-CHECKER-ARRAY::FARRAYP-ASSIGN-LIT
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (37 4 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::NUM-FIELDS-ASSIGN-LIT
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (37 4 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::FLENGTH-ASSIGN-LIT
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (37 4 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::FIELDP-ASSIGN-LIT
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (37 4 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::FIELD-OFFSETP-ASSIGN-LIT
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (37 4 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::FREAD-*STACK-END*-ASSIGN-LIT
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (2 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(PROOF-CHECKER-ARRAY::FREAD-*NUM-VARS*-ASSIGN-LIT
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP-FWRITE-LITERAL
 (75 35 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (68 8 (:REWRITE DEFAULT-+-2))
 (48 16 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (48 8 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (37 37 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (37 37 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (32 5 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (32 4 (:DEFINITION SIGNED-BYTE-P))
 (28 4 (:DEFINITION INTEGER-RANGE-P))
 (16 5 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (12 12 (:REWRITE DEFAULT-<-2))
 (12 12 (:REWRITE DEFAULT-<-1))
 (12 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (10 10 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (8 8 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP-FWRITE-DIFF-FIELD
 (177 55 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (96 6 (:REWRITE DEFAULT-+-2))
 (78 36 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (72 12 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (44 44 (:REWRITE DEFAULT-<-2))
 (44 44 (:REWRITE DEFAULT-<-1))
 (29 29 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (29 29 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (18 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (16 5 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (16 5 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (10 10 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (6 6 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP-ASSIGN-LIT
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (9 9 (:REWRITE DEFAULT-+-2))
 (9 9 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (5 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP-0-ASSIGN-LIT
 (826 28 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (21 21 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (7 7 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(PROOF-CHECKER-ARRAY::STACK-UNIQUEP-FWRITE-DIFF-FIELD
 (1011 141 (:REWRITE DEFAULT-+-2))
 (791 260 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (696 116 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (240 63 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (174 58 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (172 172 (:REWRITE DEFAULT-<-2))
 (172 172 (:REWRITE DEFAULT-<-1))
 (151 32 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (141 141 (:REWRITE DEFAULT-+-1))
 (82 40 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (63 63 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (63 63 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (43 32 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 )
(PROOF-CHECKER-ARRAY::STACK-UNIQUEP-FWRITE-OUT-OF-BOUNDS-HIGH
 (1097 27 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (955 175 (:REWRITE DEFAULT-+-2))
 (727 255 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (727 137 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (472 59 (:DEFINITION SIGNED-BYTE-P))
 (447 29 (:REWRITE FOLD-CONSTS-IN-+))
 (413 59 (:DEFINITION INTEGER-RANGE-P))
 (328 180 (:REWRITE DEFAULT-<-1))
 (320 32 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (236 63 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (196 78 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (180 180 (:REWRITE DEFAULT-<-2))
 (175 175 (:REWRITE DEFAULT-+-1))
 (79 39 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (63 63 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (63 63 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (43 32 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (37 37 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (19 19 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-IS-ELEM))
 (14 14 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-SAME-VALUE))
 (14 14 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-NOT-ELEM))
 (12 12 (:REWRITE PROOF-CHECKER-ARRAY::STACK-UNIQUEP-FWRITE-DIFF-FIELD))
 (10 10 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (10 10 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (5 5 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-LOW))
 (5 5 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-FIELD))
 )
(PROOF-CHECKER-ARRAY::STACK-UNIQUEP-FWRITE-NOT-STACK-MEMBERP
 (31 31 (:REWRITE DEFAULT-+-2))
 (31 31 (:REWRITE DEFAULT-+-1))
 (30 9 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (25 5 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (16 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (9 9 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (9 9 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (5 5 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (2 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::STACK-UNIQUEP-FWRITE-DIFF-FIELD))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-SAME-VALUE))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-NOT-ELEM))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-IS-ELEM))
 )
(PROOF-CHECKER-ARRAY::STACK-UNIQUEP-ASSIGN-LIT
 (3570 22 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (3566 2 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (2814 8 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (1887 75 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (1210 312 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (961 55 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (946 186 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (760 68 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (475 475 (:TYPE-PRESCRIPTION EVENP))
 (365 293 (:REWRITE DEFAULT-+-2))
 (293 293 (:REWRITE DEFAULT-+-1))
 (254 42 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (214 22 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (210 2 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (146 7 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (129 3 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (128 6 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (126 2 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (114 114 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (112 112 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (86 12 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (72 24 (:REWRITE UNICITY-OF-0))
 (50 10 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (48 24 (:DEFINITION FIX))
 (46 38 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (46 34 (:REWRITE DEFAULT-<-1))
 (41 5 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (36 6 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (34 34 (:REWRITE DEFAULT-<-2))
 (22 22 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (22 22 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (22 2 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (18 18 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP))
 (18 6 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (16 16 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (16 4 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (16 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (16 2 (:DEFINITION SIGNED-BYTE-P))
 (14 2 (:REWRITE DEFAULT-*-2))
 (14 2 (:DEFINITION INTEGER-RANGE-P))
 (12 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (10 4 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (4 4 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (2 2 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::STACK-UNIQUEP-0-ASSIGN-LIT
 (118 4 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (34 3 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (4 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (3 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP-FWRITE-DIFF-FIELD
 (2297 287 (:REWRITE DEFAULT-+-2))
 (1703 564 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (1608 268 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (1149 48 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (580 48 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (409 50 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (402 134 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (357 2 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (332 332 (:REWRITE DEFAULT-<-2))
 (332 332 (:REWRITE DEFAULT-<-1))
 (287 287 (:REWRITE DEFAULT-+-1))
 (195 3 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (104 58 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (48 48 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (48 48 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (46 46 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (46 46 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (38 38 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 )
(PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP-FWRITE-OUT-OF-BOUNDS-HIGH
 (4326 45 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (3417 582 (:REWRITE DEFAULT-+-2))
 (3113 86 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (2404 828 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (2404 434 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (2250 145 (:REWRITE FOLD-CONSTS-IN-+))
 (1576 197 (:DEFINITION SIGNED-BYTE-P))
 (1379 197 (:DEFINITION INTEGER-RANGE-P))
 (766 542 (:REWRITE DEFAULT-<-1))
 (631 237 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (582 582 (:REWRITE DEFAULT-+-1))
 (542 542 (:REWRITE DEFAULT-<-2))
 (400 86 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (206 103 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (142 142 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (114 58 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (98 18 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-NOT-ELEM))
 (86 86 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (86 86 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (86 86 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (79 79 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (79 79 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (53 53 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP-FWRITE-DIFF-FIELD))
 (27 27 (:REWRITE PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP-FWRITE-DIFF-FIELD))
 (27 27 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-IS-ELEM))
 (18 18 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-SAME-VALUE))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-LOW))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-FIELD))
 )
(PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP-FWRITE-NOT-STACK-MEMBERP
 (187 10 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (88 12 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (72 72 (:REWRITE DEFAULT-+-2))
 (72 72 (:REWRITE DEFAULT-+-1))
 (43 10 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (15 11 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (11 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-NOT-ELEM))
 (10 10 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (10 10 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (10 10 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (9 9 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (9 9 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (5 5 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP-FWRITE-DIFF-FIELD))
 (2 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-SAME-VALUE))
 (2 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-IS-ELEM))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP-FWRITE-DIFF-FIELD))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERALP-IMPLIES-NOT-EQUAL-NEGATE))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 )
(PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP-ASSIGN-LIT
 (3822 13 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (3573 25 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (3566 2 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (2814 8 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (1889 77 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (1210 312 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (983 57 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (946 186 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (760 68 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (479 479 (:TYPE-PRESCRIPTION EVENP))
 (446 5 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (412 340 (:REWRITE DEFAULT-+-2))
 (340 340 (:REWRITE DEFAULT-+-1))
 (336 49 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (273 13 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (217 25 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (128 6 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (126 2 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (114 114 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (113 113 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (94 2 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (86 12 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (72 24 (:REWRITE UNICITY-OF-0))
 (58 44 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (50 10 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (48 36 (:REWRITE DEFAULT-<-1))
 (48 24 (:DEFINITION FIX))
 (48 5 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (36 36 (:REWRITE DEFAULT-<-2))
 (36 6 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (22 22 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (22 2 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (18 18 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP))
 (18 6 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (16 16 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (16 4 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (16 2 (:DEFINITION SIGNED-BYTE-P))
 (15 9 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (14 2 (:REWRITE DEFAULT-*-2))
 (14 2 (:DEFINITION INTEGER-RANGE-P))
 (13 13 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (10 10 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (10 4 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (9 9 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (3 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (2 2 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP-0-ASSIGN-LIT
 (118 4 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (40 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (34 3 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (21 7 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (4 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-DIFF-FIELD
 (177 55 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (101 49 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (96 6 (:REWRITE DEFAULT-+-2))
 (72 12 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (44 44 (:REWRITE DEFAULT-<-2))
 (44 44 (:REWRITE DEFAULT-<-1))
 (19 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (19 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (18 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (12 12 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (6 6 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-OUT-OF-BOUNDS-HIGH
 (146 42 (:REWRITE DEFAULT-<-1))
 (144 48 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (144 24 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (101 51 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (96 12 (:DEFINITION SIGNED-BYTE-P))
 (84 12 (:DEFINITION INTEGER-RANGE-P))
 (78 18 (:REWRITE DEFAULT-+-2))
 (52 7 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (42 42 (:REWRITE DEFAULT-<-2))
 (36 12 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (20 7 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (18 18 (:REWRITE DEFAULT-+-1))
 (14 14 (:REWRITE PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-DIFF-FIELD))
 (12 12 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-0))
 (11 11 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (11 11 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-ASSIGN-LIT
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (9 9 (:REWRITE DEFAULT-+-2))
 (9 9 (:REWRITE DEFAULT-+-1))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (5 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-0-ASSIGN-LIT
 (1062 36 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (27 27 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-DIFF-FIELD
 (897 117 (:REWRITE DEFAULT-+-2))
 (759 248 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (624 104 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (183 21 (:REWRITE FOLD-CONSTS-IN-+))
 (156 52 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (151 151 (:REWRITE DEFAULT-<-2))
 (151 151 (:REWRITE DEFAULT-<-1))
 (149 83 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (139 52 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (117 117 (:REWRITE DEFAULT-+-1))
 (48 48 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (41 41 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 )
(PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-OUT-OF-BOUNDS-HIGH
 (924 219 (:REWRITE DEFAULT-+-2))
 (676 228 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (676 116 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (448 56 (:DEFINITION SIGNED-BYTE-P))
 (392 56 (:DEFINITION INTEGER-RANGE-P))
 (306 177 (:REWRITE DEFAULT-<-1))
 (234 38 (:REWRITE FOLD-CONSTS-IN-+))
 (219 219 (:REWRITE DEFAULT-+-1))
 (177 177 (:REWRITE DEFAULT-<-2))
 (172 60 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (157 93 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (143 57 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (54 54 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (46 46 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (24 24 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-DIFF-FIELD))
 (21 21 (:REWRITE PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-DIFF-FIELD))
 (15 15 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (15 15 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 )
(PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-NOT-STACK-MEMBERP
 (617 92 (:REWRITE DEFAULT-+-2))
 (420 140 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (420 70 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (280 35 (:DEFINITION SIGNED-BYTE-P))
 (245 35 (:DEFINITION INTEGER-RANGE-P))
 (187 82 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (112 42 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (111 17 (:REWRITE FOLD-CONSTS-IN-+))
 (105 35 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (92 92 (:REWRITE DEFAULT-+-1))
 (87 87 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (70 70 (:REWRITE DEFAULT-<-2))
 (70 70 (:REWRITE DEFAULT-<-1))
 (39 39 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (22 22 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-DIFF-FIELD))
 )
(PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-ASSIGN-LIT
 (139 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (33 33 (:REWRITE DEFAULT-+-2))
 (33 33 (:REWRITE DEFAULT-+-1))
 (31 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (18 6 (:REWRITE FOLD-CONSTS-IN-+))
 (14 14 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (7 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (5 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-0-ASSIGN-LIT
 (1705 54 (:REWRITE PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-DIFF-FIELD))
 (1298 44 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (338 27 (:REWRITE PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-OUT-OF-BOUNDS-HIGH))
 (51 51 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (48 16 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-FWRITE-*LOOKUP*
 (249159 1263 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (248922 114 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (123699 515 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (72709 3868 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (48232 5694 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (42698 1830 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (31301 3536 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (30838 8411 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (29919 4165 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (29110 20196 (:REWRITE DEFAULT-+-2))
 (27174 27174 (:TYPE-PRESCRIPTION EVENP))
 (26213 8299 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (26177 6832 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (22743 306 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (22632 3036 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (20196 20196 (:REWRITE DEFAULT-+-1))
 (18597 5670 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (17739 5209 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (17196 715 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (15489 128 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (14895 1655 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-+-2))
 (12382 1985 (:DEFINITION SIGNED-BYTE-P))
 (10397 1985 (:DEFINITION INTEGER-RANGE-P))
 (9091 8392 (:REWRITE DEFAULT-<-1))
 (9030 2439 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (9027 8392 (:REWRITE DEFAULT-<-2))
 (8434 1263 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (8415 378 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (7967 7967 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (7468 482 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (6956 262 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (5856 1110 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (5793 114 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (4635 1545 (:REWRITE UNICITY-OF-0))
 (4042 2753 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (3090 1545 (:DEFINITION FIX))
 (2757 902 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (1926 1926 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (1771 1771 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (1655 1655 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1+-FIELD-OFFSETP))
 (1563 1563 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (1254 1254 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (1067 1067 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (980 249 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (932 214 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (813 114 (:REWRITE DEFAULT-*-2))
 (743 22 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-NOT-STACK-MEMBERP))
 (605 605 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (570 570 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (504 504 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (432 142 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (428 142 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (390 25 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP-FWRITE-DIFF-FIELD))
 (389 43 (:REWRITE PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-DIFF-FIELD))
 (321 107 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (252 252 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (252 252 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (114 114 (:REWRITE DEFAULT-*-1))
 (62 22 (:REWRITE PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP-FWRITE-DIFF-FIELD))
 (37 37 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-FLENGTH))
 (30 10 (:REWRITE PROOF-CHECKER-ARRAY::STACK-UNIQUEP-FWRITE-DIFF-FIELD))
 (22 22 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-DIFF-FIELD))
 (15 5 (:REWRITE PROOF-CHECKER-ARRAY::NUM-FIELDS-FWRITE))
 )
(PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-*STACK*-FWRITE-*STACK-END*
 (25 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (23 2 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-SAME-VALUE))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-IS-ELEM))
 (3 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-HIGH))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-LOW))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-NOT-ELEM))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-FIELD))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::INTEGERP-IMPLIES-EQUAL-+--1-1)
(PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-FWRITE-*STACK*-FWRITE-*STACK-END*
 (83060 41 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (62374 29 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-FREAD-*STACK-END*-*STACK*))
 (37041 151 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (27199 1136 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (21268 350 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (10954 999 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (10661 1338 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (10528 2801 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (9559 2824 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (8784 8784 (:TYPE-PRESCRIPTION EVENP))
 (7475 1951 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (7363 5658 (:REWRITE DEFAULT-+-2))
 (7315 2020 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (7081 456 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (6396 2012 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (5937 793 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (5658 5658 (:REWRITE DEFAULT-+-1))
 (5182 40 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (4916 781 (:DEFINITION SIGNED-BYTE-P))
 (4494 55 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (4135 781 (:DEFINITION INTEGER-RANGE-P))
 (3740 350 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (3733 150 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (3296 1427 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (3141 2618 (:REWRITE DEFAULT-<-2))
 (2864 2618 (:REWRITE DEFAULT-<-1))
 (2750 120 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (2728 168 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (2635 2635 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (2501 69 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-FLENGTH))
 (2068 40 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (1359 453 (:REWRITE UNICITY-OF-0))
 (1292 152 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (1015 707 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (939 260 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (906 453 (:DEFINITION FIX))
 (632 632 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (540 60 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-+-2))
 (476 476 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (414 6 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-OUT-OF-BOUNDS-HIGH))
 (400 80 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (379 379 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (366 122 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (320 320 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (320 80 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (302 302 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (280 40 (:REWRITE DEFAULT-*-2))
 (219 6 (:REWRITE PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-OUT-OF-BOUNDS-HIGH))
 (207 69 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (200 200 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (200 200 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (192 64 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (192 64 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (156 21 (:REWRITE PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-DIFF-FIELD))
 (126 15 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-DIFF-FIELD))
 (124 124 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1+-FIELD-OFFSETP))
 (91 91 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (91 91 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (68 17 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-IS-ELEM))
 (40 40 (:REWRITE DEFAULT-*-1))
 (36 9 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-SAME-VALUE))
 (12 9 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-VALUE-NOT-ELEM))
 (8 8 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-OUT-OF-BOUNDS-LOW))
 )
(PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-ASSIGN-LIT
 (1818 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-FREAD-*STACK-END*-*STACK*))
 (1816 1 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (1407 4 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (960 34 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (605 156 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (510 12 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (498 24 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (476 94 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (380 34 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (241 241 (:TYPE-PRESCRIPTION EVENP))
 (174 138 (:REWRITE DEFAULT-+-2))
 (138 138 (:REWRITE DEFAULT-+-1))
 (131 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (129 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (117 19 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (106 10 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (97 31 (:REWRITE FOLD-CONSTS-IN-+))
 (65 3 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (64 3 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (63 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (57 57 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (55 55 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (51 7 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (51 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (36 12 (:REWRITE UNICITY-OF-0))
 (25 5 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (24 12 (:DEFINITION FIX))
 (22 16 (:REWRITE DEFAULT-<-1))
 (21 17 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (20 10 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (18 3 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (17 17 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (16 16 (:REWRITE DEFAULT-<-2))
 (16 4 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (12 2 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (11 11 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (11 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (10 4 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (8 8 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (8 8 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (8 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (8 1 (:DEFINITION SIGNED-BYTE-P))
 (7 1 (:REWRITE DEFAULT-*-2))
 (7 1 (:DEFINITION INTEGER-RANGE-P))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (5 5 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (5 5 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (5 5 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-FWRITE-*LOOKUP*-LOW
 (400 88 (:REWRITE DEFAULT-+-2))
 (368 152 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (240 68 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (216 34 (:DEFINITION SIGNED-BYTE-P))
 (192 22 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (182 34 (:DEFINITION INTEGER-RANGE-P))
 (126 47 (:REWRITE DEFAULT-<-2))
 (102 34 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (88 88 (:REWRITE DEFAULT-+-1))
 (47 47 (:REWRITE DEFAULT-<-1))
 (34 34 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (14 7 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (9 9 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-FWRITE-*LOOKUP*-HIGH
 (1538 286 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (1392 959 (:REWRITE DEFAULT-+-2))
 (959 959 (:REWRITE DEFAULT-+-1))
 (218 218 (:REWRITE DEFAULT-<-2))
 (218 218 (:REWRITE DEFAULT-<-1))
 (190 190 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (122 122 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (55 31 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (22 22 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-FWRITE-*STACK*-FWRITE-*STACK-END*
 (432 96 (:REWRITE DEFAULT-+-2))
 (352 128 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (236 22 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (224 28 (:DEFINITION SIGNED-BYTE-P))
 (196 28 (:DEFINITION INTEGER-RANGE-P))
 (192 56 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (184 16 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (96 96 (:REWRITE DEFAULT-+-1))
 (84 28 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (56 56 (:REWRITE DEFAULT-<-2))
 (56 56 (:REWRITE DEFAULT-<-1))
 (36 36 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (18 18 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (12 12 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (8 8 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (8 8 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-ASSIGN-LIT
 (1760 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-FREAD-*STACK-END*-*STACK*))
 (1758 1 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (977 71 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (670 123 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (495 12 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (468 24 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (416 70 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (396 244 (:REWRITE DEFAULT-+-2))
 (244 244 (:REWRITE DEFAULT-+-1))
 (161 12 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (147 13 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (128 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (117 19 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (106 10 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (105 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (94 94 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (80 80 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (65 3 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (64 3 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (63 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (47 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (25 5 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (22 16 (:REWRITE DEFAULT-<-1))
 (21 17 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (20 10 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (18 3 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (16 16 (:REWRITE DEFAULT-<-2))
 (11 11 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (11 11 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (9 9 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (8 8 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (8 8 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (8 2 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (8 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (8 1 (:DEFINITION SIGNED-BYTE-P))
 (7 1 (:REWRITE DEFAULT-*-2))
 (7 1 (:DEFINITION INTEGER-RANGE-P))
 (5 5 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (5 5 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (5 5 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (5 2 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (2 2 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-ASSIGN-LIT-2
 (18105 38 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (16413 58 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (12221 110 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (8729 169 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (8625 375 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (8248 176 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (5707 579 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (5425 222 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (4279 3875 (:REWRITE DEFAULT-+-2))
 (3875 3875 (:REWRITE DEFAULT-+-1))
 (2615 114 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (2577 38 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (2057 405 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (2004 38 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (1789 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-FREAD-*STACK-END*-*STACK*))
 (1180 1180 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (950 190 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (693 469 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (684 114 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (667 58 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (664 664 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (646 646 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-IMPLIES-EQUAL-+--1-1))
 (622 394 (:REWRITE DEFAULT-<-1))
 (588 146 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (554 50 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (520 184 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (502 502 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (438 146 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (438 146 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (394 394 (:REWRITE DEFAULT-<-2))
 (370 370 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (342 114 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (312 78 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (304 304 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (304 38 (:DEFINITION SIGNED-BYTE-P))
 (266 38 (:REWRITE DEFAULT-*-2))
 (266 38 (:DEFINITION INTEGER-RANGE-P))
 (195 78 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (194 15 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (190 190 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (190 190 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (155 149 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (149 149 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (129 6 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (58 58 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (38 38 (:REWRITE DEFAULT-*-1))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 )
(PROOF-CHECKER-ARRAY::ASSIGNMENT-STP-ASSIGN-LIT
 (4266 183 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (3812 1816 (:REWRITE DEFAULT-+-2))
 (2050 40 (:REWRITE PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-ASSIGN-LIT-2))
 (1816 1816 (:REWRITE DEFAULT-+-1))
 (1592 40 (:REWRITE PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-ASSIGN-LIT))
 (1548 258 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (1180 94 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (1048 183 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (1041 412 (:REWRITE DEFAULT-<-1))
 (855 95 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (781 115 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (675 15 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (665 95 (:REWRITE DEFAULT-*-2))
 (592 148 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (570 95 (:DEFINITION SIGNED-BYTE-P))
 (475 95 (:DEFINITION INTEGER-RANGE-P))
 (427 412 (:REWRITE DEFAULT-<-2))
 (404 100 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (381 193 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (370 148 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (335 5 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-FREAD-*STACK-END*-*STACK*))
 (325 193 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (265 265 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (263 115 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (192 48 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (95 95 (:REWRITE DEFAULT-*-1))
 (48 48 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (40 15 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 )
(PROOF-CHECKER-ARRAY::UNASSIGN-ONE
 (38692 710 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (25530 47 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (25211 253 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (15620 5493 (:REWRITE DEFAULT-+-2))
 (15487 303 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (11625 654 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (10375 411 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (10323 1047 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (8980 2672 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (8760 1442 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (5493 5493 (:REWRITE DEFAULT-+-1))
 (5143 53 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (3940 57 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (2858 1867 (:REWRITE DEFAULT-<-1))
 (2016 1867 (:REWRITE DEFAULT-<-2))
 (1764 648 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (1758 1758 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (1266 794 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (1169 101 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (961 961 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (946 272 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (924 356 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (716 272 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (716 272 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (675 675 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (516 516 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (456 114 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (422 47 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (399 57 (:REWRITE DEFAULT-*-2))
 (285 114 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (268 268 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (268 268 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (57 57 (:REWRITE DEFAULT-*-1))
 (14 7 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (4 4 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1--FIELD-OFFSETP))
 )
(PROOF-CHECKER-ARRAY::FIELD-OFFSETP-FREAD-*STACK*-*LOOKUP*
 (66 24 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (66 12 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (52 13 (:REWRITE DEFAULT-<-1))
 (42 6 (:DEFINITION SIGNED-BYTE-P))
 (42 3 (:REWRITE DEFAULT-+-2))
 (36 6 (:DEFINITION INTEGER-RANGE-P))
 (18 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (13 13 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::FARRAYP-UNASSIGN-ONE
 (29 3 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (23 5 (:REWRITE DEFAULT-+-2))
 (18 3 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (15 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (14 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (6 1 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (5 5 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(PROOF-CHECKER-ARRAY::NUM-FIELDS-UNASSIGN-ONE
 (29 3 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (23 5 (:REWRITE DEFAULT-+-2))
 (18 3 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (15 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (14 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (6 1 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (5 5 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(PROOF-CHECKER-ARRAY::FLENGTH-UNASSIGN-ONE
 (29 3 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (23 5 (:REWRITE DEFAULT-+-2))
 (18 3 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (15 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (14 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (6 1 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (5 5 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(PROOF-CHECKER-ARRAY::FIELDP-UNASSIGN-ONE
 (29 3 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (23 5 (:REWRITE DEFAULT-+-2))
 (18 3 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (15 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (14 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (6 1 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (5 5 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(PROOF-CHECKER-ARRAY::FIELD-OFFSETP-UNASSIGN-ONE
 (29 3 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (23 5 (:REWRITE DEFAULT-+-2))
 (18 3 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (15 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (14 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (6 1 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (5 5 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(PROOF-CHECKER-ARRAY::FREAD-*STACK-END*-UNASSIGN-ONE
 (30 6 (:REWRITE DEFAULT-+-2))
 (29 3 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (24 4 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (20 4 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (14 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (12 4 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (6 6 (:REWRITE DEFAULT-+-1))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(PROOF-CHECKER-ARRAY::FREAD-*NUM-VARS*-UNASSIGN-ONE
 (29 3 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (23 5 (:REWRITE DEFAULT-+-2))
 (18 3 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (15 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (14 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (5 5 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 )
(PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP-UNASSIGN-ONE
 (128 33 (:REWRITE DEFAULT-+-2))
 (89 14 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (79 18 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (66 8 (:REWRITE PROOF-CHECKER-ARRAY::FARRAYP-FWRITE))
 (50 9 (:DEFINITION SIGNED-BYTE-P))
 (44 5 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (41 9 (:DEFINITION INTEGER-RANGE-P))
 (36 12 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (33 33 (:REWRITE DEFAULT-+-1))
 (20 3 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (13 13 (:REWRITE DEFAULT-<-2))
 (13 13 (:REWRITE DEFAULT-<-1))
 (13 7 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (12 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (12 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (11 7 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-FREAD-*STACK*-*LOOKUP*))
 (7 7 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1--FIELD-OFFSETP))
 (7 7 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (6 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 )
(PROOF-CHECKER-ARRAY::STACK-UNIQUEP-UNASSIGN-ONE
 (166 7 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (154 59 (:REWRITE DEFAULT-+-2))
 (103 16 (:REWRITE PROOF-CHECKER-ARRAY::FARRAYP-FWRITE))
 (89 14 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (80 15 (:DEFINITION SIGNED-BYTE-P))
 (79 18 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (68 14 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (65 15 (:DEFINITION INTEGER-RANGE-P))
 (62 9 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (59 59 (:REWRITE DEFAULT-+-1))
 (44 5 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (36 12 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (26 26 (:REWRITE DEFAULT-<-2))
 (26 26 (:REWRITE DEFAULT-<-1))
 (19 19 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (17 11 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-FREAD-*STACK*-*LOOKUP*))
 (14 14 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (14 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-FIELD))
 (13 13 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1--FIELD-OFFSETP))
 (12 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (12 4 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (6 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 )
(PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP-UNASSIGN-ONE
 (364 8 (:DEFINITION PROOF-CHECKER-ARRAY::FIELD-MEMBERP))
 (324 16 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (262 143 (:REWRITE DEFAULT-+-2))
 (159 13 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (146 7 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP-FWRITE-DIFF-FIELD))
 (143 143 (:REWRITE DEFAULT-+-1))
 (113 18 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (99 22 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (90 17 (:DEFINITION SIGNED-BYTE-P))
 (78 16 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (73 17 (:DEFINITION INTEGER-RANGE-P))
 (60 7 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (48 16 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (44 5 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (38 13 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (30 30 (:REWRITE DEFAULT-<-2))
 (30 30 (:REWRITE DEFAULT-<-1))
 (20 14 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (19 19 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (17 17 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (16 16 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (16 16 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (15 15 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1--FIELD-OFFSETP))
 (14 14 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (11 7 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-FREAD-*STACK*-*LOOKUP*))
 (6 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-FWRITE-DIFF-FIELD))
 (4 1 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3 3 (:TYPE-PRESCRIPTION EVENP))
 )
(PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-UNASSIGN-ONE
 (99 22 (:REWRITE DEFAULT-+-2))
 (77 10 (:REWRITE PROOF-CHECKER-ARRAY::FARRAYP-FWRITE))
 (71 11 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (65 12 (:DEFINITION SIGNED-BYTE-P))
 (64 15 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (53 12 (:DEFINITION INTEGER-RANGE-P))
 (44 5 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (27 9 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (22 22 (:REWRITE DEFAULT-+-1))
 (20 3 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (17 11 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-FREAD-*STACK*-*LOOKUP*))
 (16 16 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE DEFAULT-<-1))
 (10 10 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1--FIELD-OFFSETP))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (6 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 )
(PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-NOT-STACK-MEMBERP-2
 (685 229 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (685 115 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (675 87 (:REWRITE DEFAULT-+-2))
 (456 57 (:DEFINITION SIGNED-BYTE-P))
 (399 57 (:DEFINITION INTEGER-RANGE-P))
 (355 134 (:REWRITE DEFAULT-<-1))
 (214 93 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (213 75 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (172 58 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (152 150 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (147 134 (:REWRITE DEFAULT-<-2))
 (99 8 (:REWRITE FOLD-CONSTS-IN-+))
 (87 87 (:REWRITE DEFAULT-+-1))
 (51 51 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (44 14 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (36 36 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-DIFF-FIELD))
 )
(PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-UNASSIGN-ONE
 (695 271 (:REWRITE DEFAULT-+-2))
 (604 107 (:REWRITE PROOF-CHECKER-ARRAY::FARRAYP-FWRITE))
 (588 30 (:REWRITE PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-DIFF-FIELD))
 (549 10 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-NOT-STACK-MEMBERP-2))
 (475 87 (:DEFINITION SIGNED-BYTE-P))
 (388 87 (:DEFINITION INTEGER-RANGE-P))
 (370 55 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (351 91 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (322 73 (:REWRITE PROOF-CHECKER-ARRAY::FIELDP-FWRITE))
 (271 271 (:REWRITE DEFAULT-+-1))
 (202 41 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-FWRITE))
 (190 29 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (158 47 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (118 118 (:REWRITE DEFAULT-<-2))
 (118 118 (:REWRITE DEFAULT-<-1))
 (111 37 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (93 20 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (85 29 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (70 57 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (69 69 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1--FIELD-OFFSETP))
 (54 18 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (51 43 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-FREAD-*STACK*-*LOOKUP*))
 (47 47 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 )
(PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-FWRITE-*LOOKUP*-0
 (161781 891 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (161610 80 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (93505 345 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (61573 2758 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (43826 1668 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (36724 2498 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (23737 2584 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (20408 6025 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (19457 2922 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (18777 13573 (:REWRITE DEFAULT-+-2))
 (17661 5997 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (16987 16987 (:TYPE-PRESCRIPTION EVENP))
 (16535 4248 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (14584 2004 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (13818 184 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (13573 13573 (:REWRITE DEFAULT-+-1))
 (11513 94 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (10647 438 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (10164 3958 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (9711 1079 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-+-2))
 (8237 2474 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (7966 1289 (:DEFINITION SIGNED-BYTE-P))
 (6677 1289 (:DEFINITION INTEGER-RANGE-P))
 (6207 5712 (:REWRITE DEFAULT-<-1))
 (6205 276 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (5839 5712 (:REWRITE DEFAULT-<-2))
 (5785 891 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (5188 1313 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (5011 5011 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (4199 80 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (4132 22 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-NOT-STACK-MEMBERP-2))
 (3738 244 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (3282 570 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (3105 1035 (:REWRITE UNICITY-OF-0))
 (2544 1793 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (2070 1035 (:DEFINITION FIX))
 (1635 528 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (1259 1259 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (1214 1214 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (1079 1079 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1+-FIELD-OFFSETP))
 (920 920 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (880 880 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (795 795 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (708 181 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (634 146 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (608 242 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (575 80 (:REWRITE DEFAULT-*-2))
 (564 564 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-FREAD-*STACK*-*LOOKUP*))
 (435 435 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (400 400 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (395 43 (:REWRITE PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-DIFF-FIELD))
 (390 96 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (390 25 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP-FWRITE-DIFF-FIELD))
 (386 96 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (368 368 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (184 184 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (184 184 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (80 80 (:REWRITE DEFAULT-*-1))
 (63 21 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (62 22 (:REWRITE PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP-FWRITE-DIFF-FIELD))
 (30 10 (:REWRITE PROOF-CHECKER-ARRAY::STACK-UNIQUEP-FWRITE-DIFF-FIELD))
 (22 22 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-DIFF-FIELD))
 (15 5 (:REWRITE PROOF-CHECKER-ARRAY::NUM-FIELDS-FWRITE))
 (5 5 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-FLENGTH))
 )
(PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-FWRITE-*STACK-END*
 (80796 360 (:REWRITE PROOF-CHECKER-ARRAY::ASSIGNEDP-IMPLIES-FIELD-MEMBERP-*STACK*))
 (80730 33 (:DEFINITION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (41529 143 (:DEFINITION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (29295 1340 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (24164 927 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1-****))
 (19033 196 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (19017 14008 (:REWRITE DEFAULT-+-2))
 (14008 14008 (:REWRITE DEFAULT-+-1))
 (12001 356 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (11762 2392 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (11464 1074 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 (10909 76 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (9721 2564 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-+-2))
 (8061 2534 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (7182 7182 (:TYPE-PRESCRIPTION EVENP))
 (6235 1638 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (5809 148 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (5414 628 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (4380 1121 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (3819 1090 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (3758 620 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-<-1+))
 (3698 571 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (3114 462 (:DEFINITION SIGNED-BYTE-P))
 (2652 462 (:DEFINITION INTEGER-RANGE-P))
 (2380 578 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (2371 34 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (2194 115 (:REWRITE PROOF-CHECKER-ARRAY::STACK-IN-RANGEP-FWRITE-DIFF-FIELD))
 (2148 1894 (:REWRITE DEFAULT-<-1))
 (2124 2124 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::COUNT-ASSIGNED))
 (2021 1894 (:REWRITE DEFAULT-<-2))
 (1879 360 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-LOOKUP-1-IMPLIES-FIELD-MEMBERP-*STACK*))
 (1843 111 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (1377 1377 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (1318 54 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-DIFF-FIELD))
 (1287 429 (:REWRITE UNICITY-OF-0))
 (1135 60 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP-FWRITE-DIFF-FIELD))
 (1098 122 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-+-2))
 (1088 340 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (1064 22 (:REWRITE PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P-FWRITE-NOT-STACK-MEMBERP-2))
 (1051 1049 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-FREAD-*STACK*-*LOOKUP*))
 (1021 1021 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CORRESPONDS-WITH-LOOKUP-P))
 (881 155 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (858 429 (:DEFINITION FIX))
 (783 334 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (683 683 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP))
 (652 147 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-NOT-FIELD-MEMBERP-NEGATE-*STACK*))
 (630 210 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (563 563 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (530 530 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::NEGATE))
 (408 91 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE-2))
 (360 360 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::ASSIGNMENT-STP))
 (334 141 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-NEGATE-1))
 (282 282 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::LITERALP))
 (251 33 (:REWRITE DEFAULT-*-2))
 (174 55 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-FIELD-OFFSETP-NEGATE))
 (167 167 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::STACK-UNIQUEP))
 (155 155 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (122 122 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1+-FIELD-OFFSETP))
 (108 36 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-<-NEGATE))
 (102 22 (:REWRITE PROOF-CHECKER-ARRAY::STACK-NOT-CONFLICTINGP-FWRITE-DIFF-FIELD))
 (60 10 (:REWRITE PROOF-CHECKER-ARRAY::STACK-UNIQUEP-FWRITE-DIFF-FIELD))
 (33 33 (:REWRITE DEFAULT-*-1))
 (20 5 (:REWRITE PROOF-CHECKER-ARRAY::NUM-FIELDS-FWRITE))
 (5 5 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-FLENGTH))
 )
(PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-UNASSIGN-ONE
 (30 6 (:REWRITE DEFAULT-+-2))
 (24 4 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (20 4 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (20 3 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (15 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-IN-RANGEP))
 (12 4 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (10 1 (:REWRITE PROOF-CHECKER-ARRAY::FARRAYP-FWRITE))
 (8 2 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (6 6 (:REWRITE DEFAULT-+-1))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (6 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (5 5 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (5 2 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (5 1 (:DEFINITION SIGNED-BYTE-P))
 (4 1 (:DEFINITION INTEGER-RANGE-P))
 (3 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-1--FIELD-OFFSETP))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-FWRITE-*LOOKUP*-LOW-2
 (400 88 (:REWRITE DEFAULT-+-2))
 (368 152 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (240 68 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (216 34 (:DEFINITION SIGNED-BYTE-P))
 (192 22 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (182 34 (:DEFINITION INTEGER-RANGE-P))
 (126 47 (:REWRITE DEFAULT-<-2))
 (102 34 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (88 88 (:REWRITE DEFAULT-+-1))
 (47 47 (:REWRITE DEFAULT-<-1))
 (34 34 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (14 7 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (9 9 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (6 6 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-FWRITE-*LOOKUP*-HIGH-2
 (1856 292 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (1476 1021 (:REWRITE DEFAULT-+-2))
 (1021 1021 (:REWRITE DEFAULT-+-1))
 (230 230 (:REWRITE DEFAULT-<-2))
 (230 230 (:REWRITE DEFAULT-<-1))
 (198 198 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (128 128 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (63 35 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (22 22 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-FWRITE-*STACK*-FWRITE-*STACK-END*-2
 (432 96 (:REWRITE DEFAULT-+-2))
 (352 128 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (224 28 (:DEFINITION SIGNED-BYTE-P))
 (224 22 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (196 28 (:DEFINITION INTEGER-RANGE-P))
 (192 56 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (96 96 (:REWRITE DEFAULT-+-1))
 (84 28 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (56 56 (:REWRITE DEFAULT-<-2))
 (56 56 (:REWRITE DEFAULT-<-1))
 (27 27 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (24 8 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (18 18 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 (12 12 (:REWRITE PROOF-CHECKER-ARRAY::EQUAL-FREAD-*LOOKUP*-1-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1+-1))
 )
(PROOF-CHECKER-ARRAY::LITERALP-FREAD-*STACK*
 (66 24 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (66 12 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (52 13 (:REWRITE DEFAULT-<-1))
 (42 6 (:DEFINITION SIGNED-BYTE-P))
 (42 3 (:REWRITE DEFAULT-+-2))
 (36 6 (:DEFINITION INTEGER-RANGE-P))
 (18 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (13 13 (:REWRITE DEFAULT-<-2))
 (11 11 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (11 11 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (3 3 (:REWRITE DEFAULT-+-1))
 )
(PROOF-CHECKER-ARRAY::LITERALP-FREAD-*STACK*-2
 (54 4 (:REWRITE DEFAULT-+-2))
 (41 12 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (41 6 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (35 1 (:DEFINITION PROOF-CHECKER-ARRAY::STACK-CONTAINS-LITERALSP))
 (20 3 (:DEFINITION SIGNED-BYTE-P))
 (19 1 (:REWRITE FOLD-CONSTS-IN-+))
 (17 3 (:DEFINITION INTEGER-RANGE-P))
 (9 3 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (9 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 6 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (5 5 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:TYPE-PRESCRIPTION PROOF-CHECKER-ARRAY::FIELDP))
 (3 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (3 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (1 1 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 )
(PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-UNASSIGN-ONE
 (190 38 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (157 16 (:REWRITE PROOF-CHECKER-ARRAY::FWRITE-REDUNDANT))
 (149 146 (:REWRITE DEFAULT-+-2))
 (146 146 (:REWRITE DEFAULT-+-1))
 (28 6 (:REWRITE DEFAULT-<-1))
 (26 6 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-IMPLIES-FIELD-OFFSETP-1+))
 (26 2 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1+-NOT-FLENGTH))
 (22 2 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (20 2 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (16 2 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (13 13 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-MEMBERP-*STACK*-IMPLIES-EQUAL-FREAD-*LOOKUP*-1))
 (9 9 (:REWRITE PROOF-CHECKER-ARRAY::LITERAL-LISTP-IMPLIES-LITERALP-MEMBER))
 (9 9 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-IMPLIES-LITERALP))
 (6 6 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE PROOF-CHECKER-ARRAY::NOT-FIELD-MEMBERP-*STACK*-IMPLIES-NOT-EQUAL-FREAD-*LOOKUP*-1))
 )
(PROOF-CHECKER-ARRAY::ASSIGNMENT-STP-UNASSIGN-ONE
 (366 61 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (362 242 (:REWRITE DEFAULT-+-2))
 (242 242 (:REWRITE DEFAULT-+-1))
 (189 21 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (161 41 (:REWRITE DEFAULT-<-1))
 (152 38 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (147 21 (:REWRITE DEFAULT-*-2))
 (126 21 (:DEFINITION SIGNED-BYTE-P))
 (105 21 (:DEFINITION INTEGER-RANGE-P))
 (100 20 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (95 38 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (41 41 (:REWRITE DEFAULT-<-2))
 (21 21 (:REWRITE DEFAULT-*-1))
 (19 5 (:REWRITE PROOF-CHECKER-ARRAY::COUNT-ASSIGNED-UNASSIGN-ONE))
 )
(PROOF-CHECKER-ARRAY::UNASSIGN-ALL
 (120 26 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (93 58 (:REWRITE DEFAULT-+-2))
 (84 14 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (58 58 (:REWRITE DEFAULT-+-1))
 (45 5 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (42 14 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (40 10 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (39 15 (:REWRITE DEFAULT-<-1))
 (38 6 (:DEFINITION SIGNED-BYTE-P))
 (35 5 (:REWRITE DEFAULT-*-2))
 (32 6 (:DEFINITION INTEGER-RANGE-P))
 (31 3 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (25 10 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (15 15 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-*-1))
 )
(PROOF-CHECKER-ARRAY::ASSIGNMENT-STP-UNASSIGN-ALL
 (18927 14737 (:REWRITE DEFAULT-+-2))
 (14737 14737 (:REWRITE DEFAULT-+-1))
 (13464 561 (:REWRITE PROOF-CHECKER-ARRAY::FREAD-*STACK-END*-UNASSIGN-ONE))
 (12903 1683 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--SQUEEZE))
 (12437 2751 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-TYPES))
 (11220 561 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-UNASSIGN-ONE))
 (8562 1427 (:REWRITE PROOF-CHECKER-ARRAY::INTEGERP-TYPES))
 (5964 662 (:REWRITE PROOF-CHECKER-ARRAY::EVENP-SQUEEZE-EQUAL-+-2))
 (5264 1316 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-1+))
 (4634 662 (:REWRITE DEFAULT-*-2))
 (4281 1427 (:REWRITE PROOF-CHECKER-ARRAY::SB60P-FREAD))
 (3978 662 (:DEFINITION SIGNED-BYTE-P))
 (3316 662 (:DEFINITION INTEGER-RANGE-P))
 (3290 1316 (:REWRITE PROOF-CHECKER-ARRAY::LOOKUP-CORRESPONDS-WITH-STACKP-+-2))
 (1683 1683 (:REWRITE PROOF-CHECKER-ARRAY::FIELD-OFFSETP-1--NOT-0))
 (1683 561 (:REWRITE FOLD-CONSTS-IN-+))
 (1365 765 (:REWRITE DEFAULT-<-1))
 (765 765 (:REWRITE DEFAULT-<-2))
 (662 662 (:REWRITE DEFAULT-*-1))
 )