(ADE::ROMP)
(ADE::ROM-GUTS
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::RAM)
(ADE::RAMP)
(ADE::RAM-GUTS
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::STUBP)
(ADE::STUB-GUTS
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::ROMP-IS-NOT-RAMP-NOR-STUBP
 (18 6 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 12 (:TYPE-PRESCRIPTION ADE::BVP))
 (12 12 (:REWRITE DEFAULT-CDR))
 (10 5 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CAR))
 (5 5 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION ADE::4V-LISTP))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::4V-LISTP-ROM-GUTS-OF-ROMP
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (11 11 (:REWRITE DEFAULT-CDR))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::4V-LISTP=>TRUE-LISTP
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (10 2 (:DEFINITION TRUE-LISTP))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-CAR))
 )
(ADE::TRUE-LISTP-ROM-GUTS-OF-ROMP
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (10 10 (:REWRITE DEFAULT-CDR))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION ADE::4V-LISTP))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::ROM-GUTS-OF-ROMP
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (11 11 (:REWRITE DEFAULT-CDR))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION ADE::4V-LISTP))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::RAMP-RAM
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 2 (:REWRITE ADE::BVP-V-FOURFIX))
 (2 2 (:TYPE-PRESCRIPTION ADE::BVP))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::RAM-GUTS-RAM
 (5 3 (:REWRITE ADE::BVP-V-FOURFIX))
 (3 3 (:REWRITE DEFAULT-CDR))
 (2 2 (:TYPE-PRESCRIPTION ADE::BVP))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:TYPE-PRESCRIPTION LEN))
 (1 1 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::RAMP-IS-NOT-ROMP-NOR-STUBP
 (18 6 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 12 (:TYPE-PRESCRIPTION ADE::BVP))
 (12 12 (:REWRITE DEFAULT-CDR))
 (10 5 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CAR))
 (5 5 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION ADE::4V-LISTP))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::4V-LISTP-RAM-GUTS-OF-RAMP
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (11 11 (:REWRITE DEFAULT-CDR))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::TRUE-LISTP-RAM-GUTS-OF-RAMP
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (10 10 (:REWRITE DEFAULT-CDR))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION ADE::4V-LISTP))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::RAM-GUTS-OF-RAMP
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (11 11 (:REWRITE DEFAULT-CDR))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION ADE::4V-LISTP))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::STUBP-IS-NOT-ROMP-NOR-RAMP
 (18 6 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 12 (:TYPE-PRESCRIPTION ADE::BVP))
 (12 12 (:REWRITE DEFAULT-CDR))
 (10 5 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CAR))
 (5 5 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION ADE::4V-LISTP))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::4V-LISTP-STUB-GUTS-OF-STUBP
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (11 11 (:REWRITE DEFAULT-CDR))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::TRUE-LISTP-STUB-GUTS-OF-STUBP
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (10 10 (:REWRITE DEFAULT-CDR))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION ADE::4V-LISTP))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::STUB-GUTS-OF-STUBP
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (11 11 (:REWRITE DEFAULT-CDR))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 1 (:DEFINITION ADE::4V-LISTP))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::MEMP)
(ADE::MEMP=>CONSP
 (9 3 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (6 6 (:TYPE-PRESCRIPTION ADE::BVP))
 )
(ADE::MEMORY-PROPERP)
(ADE::MEMORY-OKP)
(ADE::READ-MEM1)
(ADE::READ-MEM)
(ADE::WRITE-MEM1)
(ADE::TRUE-LISTP-WRITE-MEM1
 (204 68 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (142 142 (:TYPE-PRESCRIPTION ADE::BVP))
 (122 122 (:REWRITE DEFAULT-CDR))
 (106 53 (:REWRITE DEFAULT-+-2))
 (102 102 (:REWRITE DEFAULT-CAR))
 (53 53 (:REWRITE DEFAULT-+-1))
 (9 3 (:REWRITE ADE::BVP-V-FOURFIX))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::TRUE-LISTP-WRITE-MEM1=>TRUE-LISTP-MEM
 (48 6 (:DEFINITION TRUE-LISTP))
 (36 12 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (24 24 (:TYPE-PRESCRIPTION ADE::BVP))
 (17 17 (:REWRITE DEFAULT-CDR))
 (14 14 (:REWRITE DEFAULT-CAR))
 )
(ADE::LEN-WRITE-MEM1
 (237 79 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (236 118 (:REWRITE DEFAULT-+-2))
 (170 170 (:TYPE-PRESCRIPTION ADE::BVP))
 (139 128 (:REWRITE DEFAULT-CDR))
 (118 118 (:REWRITE DEFAULT-+-1))
 (96 96 (:LINEAR LEN-WHEN-PREFIXP))
 (52 28 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-MEM1))
 (18 6 (:REWRITE ADE::BVP-V-FOURFIX))
 )
(ADE::4V-LISTP-OF-WRITE-MEM1
 (1573 1562 (:REWRITE DEFAULT-CDR))
 (1337 1326 (:REWRITE DEFAULT-CAR))
 (768 384 (:REWRITE DEFAULT-+-2))
 (384 384 (:REWRITE DEFAULT-+-1))
 (189 63 (:REWRITE ADE::BVP-V-FOURFIX))
 (126 126 (:TYPE-PRESCRIPTION ADE::BVP))
 (92 92 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::4V-LISTP-OF-CAR-WRITE-MEM1
 (276 92 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (228 228 (:REWRITE DEFAULT-CDR))
 (194 194 (:TYPE-PRESCRIPTION ADE::BVP))
 (116 58 (:REWRITE DEFAULT-+-2))
 (58 58 (:REWRITE DEFAULT-+-1))
 (16 16 (:REWRITE CDR-CONS))
 (15 5 (:REWRITE ADE::BVP-V-FOURFIX))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::ROMP-WRITE-MEM1
 (2958 986 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (1990 1990 (:TYPE-PRESCRIPTION ADE::BVP))
 (1402 701 (:REWRITE DEFAULT-+-2))
 (701 701 (:REWRITE DEFAULT-+-1))
 (176 176 (:LINEAR LEN-WHEN-PREFIXP))
 (27 9 (:REWRITE ADE::BVP-V-FOURFIX))
 )
(ADE::ROMP-CONS-WRITE-MEM1-1
 (186 3 (:DEFINITION ADE::WRITE-MEM1))
 (69 3 (:DEFINITION ADE::STUBP))
 (69 3 (:DEFINITION ADE::RAMP))
 (62 53 (:REWRITE DEFAULT-CDR))
 (60 20 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (46 46 (:TYPE-PRESCRIPTION ADE::BVP))
 (44 35 (:REWRITE DEFAULT-CAR))
 (32 8 (:DEFINITION ADE::4V-LISTP))
 (24 12 (:REWRITE DEFAULT-+-2))
 (18 18 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (12 12 (:REWRITE DEFAULT-+-1))
 (12 3 (:DEFINITION ADE::RAM))
 (9 3 (:REWRITE ADE::BVP-V-FOURFIX))
 (8 8 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::ROMP-CONS-WRITE-MEM1-2
 (1254 418 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (864 864 (:TYPE-PRESCRIPTION ADE::BVP))
 (829 829 (:REWRITE DEFAULT-CDR))
 (570 285 (:REWRITE DEFAULT-+-2))
 (469 469 (:REWRITE DEFAULT-CAR))
 (285 285 (:REWRITE DEFAULT-+-1))
 (78 78 (:LINEAR LEN-WHEN-PREFIXP))
 (42 14 (:REWRITE ADE::BVP-V-FOURFIX))
 )
(ADE::RAMP-WRITE-MEM1
 (2958 986 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (2016 2016 (:TYPE-PRESCRIPTION ADE::BVP))
 (1402 701 (:REWRITE DEFAULT-+-2))
 (701 701 (:REWRITE DEFAULT-+-1))
 (176 176 (:LINEAR LEN-WHEN-PREFIXP))
 (66 22 (:REWRITE ADE::BVP-V-FOURFIX))
 )
(ADE::RAMP-CONS-WRITE-MEM1-1
 (138 3 (:DEFINITION ADE::WRITE-MEM1))
 (69 3 (:DEFINITION ADE::STUBP))
 (54 45 (:REWRITE DEFAULT-CDR))
 (48 16 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (38 38 (:TYPE-PRESCRIPTION ADE::BVP))
 (38 29 (:REWRITE DEFAULT-CAR))
 (24 6 (:DEFINITION ADE::4V-LISTP))
 (20 10 (:REWRITE DEFAULT-+-2))
 (18 18 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (12 3 (:DEFINITION ADE::RAM))
 (10 10 (:REWRITE DEFAULT-+-1))
 (9 3 (:REWRITE ADE::BVP-V-FOURFIX))
 (6 6 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::RAMP-CONS-WRITE-MEM1-2
 (1254 418 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (864 864 (:TYPE-PRESCRIPTION ADE::BVP))
 (829 829 (:REWRITE DEFAULT-CDR))
 (570 285 (:REWRITE DEFAULT-+-2))
 (469 469 (:REWRITE DEFAULT-CAR))
 (285 285 (:REWRITE DEFAULT-+-1))
 (78 78 (:LINEAR LEN-WHEN-PREFIXP))
 (42 14 (:REWRITE ADE::BVP-V-FOURFIX))
 )
(ADE::STUBP-WRITE-MEM1
 (2790 930 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (1874 1874 (:TYPE-PRESCRIPTION ADE::BVP))
 (1306 653 (:REWRITE DEFAULT-+-2))
 (653 653 (:REWRITE DEFAULT-+-1))
 (116 116 (:LINEAR LEN-WHEN-PREFIXP))
 (21 7 (:REWRITE ADE::BVP-V-FOURFIX))
 )
(ADE::STUBP-CONS-WRITE-MEM1-1
 (138 3 (:DEFINITION ADE::WRITE-MEM1))
 (69 3 (:DEFINITION ADE::RAMP))
 (54 45 (:REWRITE DEFAULT-CDR))
 (48 16 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (38 38 (:TYPE-PRESCRIPTION ADE::BVP))
 (38 29 (:REWRITE DEFAULT-CAR))
 (24 6 (:DEFINITION ADE::4V-LISTP))
 (20 10 (:REWRITE DEFAULT-+-2))
 (18 18 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (12 3 (:DEFINITION ADE::RAM))
 (10 10 (:REWRITE DEFAULT-+-1))
 (9 3 (:REWRITE ADE::BVP-V-FOURFIX))
 (6 6 (:TYPE-PRESCRIPTION ADE::4VP))
 )
(ADE::STUBP-CONS-WRITE-MEM1-2
 (1254 418 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (864 864 (:TYPE-PRESCRIPTION ADE::BVP))
 (829 829 (:REWRITE DEFAULT-CDR))
 (570 285 (:REWRITE DEFAULT-+-2))
 (469 469 (:REWRITE DEFAULT-CAR))
 (285 285 (:REWRITE DEFAULT-+-1))
 (78 78 (:LINEAR LEN-WHEN-PREFIXP))
 (42 14 (:REWRITE ADE::BVP-V-FOURFIX))
 )
(ADE::WRITE-MEM)
(ADE::TRUE-LISTP-WRITE-MEM)
(ADE::TRUE-LISTP-WRITE-MEM=>TRUE-LISTP-MEM
 (4 3 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-MEM))
 )
(ADE::LEN-WRITE-MEM)
(ADE::ROMP-WRITE-MEM)
(ADE::ROMP-CONS-WRITE-MEM-1)
(ADE::ROMP-CONS-WRITE-MEM-2)
(ADE::RAMP-WRITE-MEM)
(ADE::RAMP-CONS-WRITE-MEM-1)
(ADE::RAMP-CONS-WRITE-MEM-2)
(ADE::STUBP-WRITE-MEM)
(ADE::STUBP-CONS-WRITE-MEM-1)
(ADE::STUBP-CONS-WRITE-MEM-2)
(ADE::RAMP-MEM1)
(ADE::RAMP-MEM)
(ADE::ALL-RAMP-MEM)
(ADE::CONSTANT-RAM)
(ADE::TRUE-LISTP-CONSTANT-RAM
 (123 41 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (88 88 (:TYPE-PRESCRIPTION ADE::BVP))
 (61 61 (:REWRITE DEFAULT-CDR))
 (60 30 (:REWRITE DEFAULT-+-2))
 (30 30 (:REWRITE DEFAULT-+-1))
 (28 28 (:REWRITE DEFAULT-CAR))
 (9 3 (:REWRITE ADE::BVP-V-FOURFIX))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::TRUE-LISTP-CONSTANT-RAM=>TRUE-LISTP-MEM
 (47 7 (:DEFINITION TRUE-LISTP))
 (42 14 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (28 28 (:TYPE-PRESCRIPTION ADE::BVP))
 (9 9 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(ADE::LEN-CONSTANT-RAM
 (84 28 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (64 64 (:TYPE-PRESCRIPTION ADE::BVP))
 (60 53 (:REWRITE DEFAULT-CDR))
 (58 29 (:REWRITE DEFAULT-+-2))
 (52 28 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-CONSTANT-RAM))
 (38 38 (:LINEAR LEN-WHEN-PREFIXP))
 (29 29 (:REWRITE DEFAULT-+-1))
 (21 21 (:REWRITE DEFAULT-CAR))
 (12 4 (:REWRITE ADE::BVP-V-FOURFIX))
 )
(ADE::CONSTANT-RAM-OF-4VP
 (1065 355 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (724 724 (:TYPE-PRESCRIPTION ADE::BVP))
 (565 565 (:REWRITE DEFAULT-CDR))
 (188 94 (:REWRITE DEFAULT-+-2))
 (94 94 (:REWRITE DEFAULT-+-1))
 (61 61 (:REWRITE DEFAULT-CAR))
 (21 7 (:REWRITE ADE::BVP-V-FOURFIX))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::4V-LISTP-OF-CONSTANT-RAM
 (340 177 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-CONSTANT-RAM))
 (186 62 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (159 145 (:REWRITE DEFAULT-CDR))
 (130 130 (:TYPE-PRESCRIPTION ADE::BVP))
 (112 91 (:REWRITE DEFAULT-CAR))
 (84 42 (:REWRITE DEFAULT-+-2))
 (42 42 (:REWRITE DEFAULT-+-1))
 (9 3 (:REWRITE ADE::BVP-V-FOURFIX))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::4V-LISTP-OF-CAR-CONSTANT-RAM
 (64 12 (:DEFINITION ADE::4V-LISTP))
 (45 15 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (42 42 (:TYPE-PRESCRIPTION ADE::BVP))
 (36 36 (:REWRITE DEFAULT-CDR))
 (26 13 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-CONSTANT-RAM))
 (18 9 (:REWRITE DEFAULT-+-2))
 (18 6 (:REWRITE ADE::BVP-V-FOURFIX))
 (13 13 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (12 12 (:TYPE-PRESCRIPTION ADE::4VP))
 (9 9 (:REWRITE DEFAULT-+-1))
 )
(ADE::ROMP-CONSTANT-RAM
 (8329 4169 (:REWRITE DEFAULT-+-2))
 (4169 4169 (:REWRITE DEFAULT-+-1))
 (1023 341 (:REWRITE ADE::BVP-V-FOURFIX))
 (682 682 (:TYPE-PRESCRIPTION ADE::BVP))
 (576 576 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::RAMP-CONSTANT-RAM
 (7357 3683 (:REWRITE DEFAULT-+-2))
 (3683 3683 (:REWRITE DEFAULT-+-1))
 (639 213 (:REWRITE ADE::BVP-V-FOURFIX))
 (426 426 (:TYPE-PRESCRIPTION ADE::BVP))
 (422 422 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::STUBP-CONSTANT-RAM
 (8329 4169 (:REWRITE DEFAULT-+-2))
 (4169 4169 (:REWRITE DEFAULT-+-1))
 (1023 341 (:REWRITE ADE::BVP-V-FOURFIX))
 (682 682 (:TYPE-PRESCRIPTION ADE::BVP))
 (576 576 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::MEMORY-PROPERP-IF)
(ADE::MEMORY-OKP-IF)
(ADE::MEMORY-PROPERP-CONSTANT-RAM
 (1995 1026 (:REWRITE DEFAULT-+-2))
 (1950 1657 (:REWRITE DEFAULT-CDR))
 (1749 583 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (1206 1206 (:TYPE-PRESCRIPTION ADE::BVP))
 (1149 762 (:REWRITE DEFAULT-CAR))
 (1026 1026 (:REWRITE DEFAULT-+-1))
 (344 344 (:LINEAR LEN-WHEN-PREFIXP))
 (60 20 (:REWRITE ADE::BVP-V-FOURFIX))
 (57 57 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (21 21 (:REWRITE DEFAULT-<-2))
 (21 21 (:REWRITE DEFAULT-<-1))
 )
(ADE::MEMORY-PROPERP-AFTER-WRITE-MEM1
 (2217 739 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (2043 1799 (:REWRITE DEFAULT-CDR))
 (1810 945 (:REWRITE DEFAULT-+-2))
 (1492 1492 (:TYPE-PRESCRIPTION ADE::BVP))
 (1211 979 (:REWRITE DEFAULT-CAR))
 (945 945 (:REWRITE DEFAULT-+-1))
 (488 26 (:REWRITE ADE::ROMP-WRITE-MEM1))
 (488 26 (:REWRITE ADE::RAMP-WRITE-MEM1))
 (460 356 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-MEM1))
 (320 40 (:REWRITE ZP-OPEN))
 (244 13 (:REWRITE ADE::STUBP-WRITE-MEM1))
 (80 40 (:REWRITE DEFAULT-<-2))
 (40 40 (:REWRITE DEFAULT-<-1))
 (21 7 (:REWRITE ADE::BVP-V-FOURFIX))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::MEMORY-PROPERP-AFTER-WRITE-MEM
 (396 327 (:REWRITE DEFAULT-CDR))
 (288 96 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (284 147 (:REWRITE DEFAULT-+-2))
 (261 192 (:REWRITE DEFAULT-CAR))
 (249 48 (:DEFINITION TRUE-LISTP))
 (214 214 (:TYPE-PRESCRIPTION ADE::BVP))
 (147 147 (:REWRITE DEFAULT-+-1))
 (134 52 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-MEM1))
 (96 4 (:REWRITE ADE::ROMP-WRITE-MEM1))
 (96 4 (:REWRITE ADE::RAMP-WRITE-MEM1))
 (52 52 (:TYPE-PRESCRIPTION ADE::WRITE-MEM1))
 (49 10 (:REWRITE REVERSE-REMOVAL))
 (48 2 (:REWRITE ADE::STUBP-WRITE-MEM1))
 (44 12 (:REWRITE REV-WHEN-NOT-CONSP))
 (36 6 (:REWRITE ADE::LEN-WRITE-MEM1))
 (33 11 (:REWRITE ADE::BVP-V-FOURFIX))
 (16 16 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (16 8 (:REWRITE STR::CONSP-OF-EXPLODE))
 (10 5 (:REWRITE DEFAULT-<-2))
 (8 8 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (6 6 (:REWRITE CONSP-OF-REV))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (5 5 (:REWRITE DEFAULT-<-1))
 )
(ADE::MEMORY-OKP-AFTER-WRITE-MEM1
 (7527 716 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (3513 3089 (:REWRITE DEFAULT-CDR))
 (2580 2150 (:REWRITE DEFAULT-CAR))
 (2232 1157 (:REWRITE DEFAULT-+-2))
 (1157 1157 (:REWRITE DEFAULT-+-1))
 (772 632 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-MEM1))
 (768 26 (:REWRITE ADE::ROMP-WRITE-MEM1))
 (768 26 (:REWRITE ADE::RAMP-WRITE-MEM1))
 (384 13 (:REWRITE ADE::STUBP-WRITE-MEM1))
 (320 40 (:REWRITE ZP-OPEN))
 (142 142 (:LINEAR LEN-WHEN-PREFIXP))
 (81 41 (:REWRITE DEFAULT-<-2))
 (41 41 (:REWRITE DEFAULT-<-1))
 )
(ADE::MEMORY-OKP-AFTER-WRITE-MEM
 (628 469 (:REWRITE DEFAULT-CDR))
 (435 267 (:REWRITE DEFAULT-CAR))
 (422 216 (:REWRITE DEFAULT-+-2))
 (288 96 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (224 88 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-MEM1))
 (216 216 (:REWRITE DEFAULT-+-1))
 (96 4 (:REWRITE ADE::ROMP-WRITE-MEM1))
 (96 4 (:REWRITE ADE::RAMP-WRITE-MEM1))
 (88 88 (:TYPE-PRESCRIPTION ADE::WRITE-MEM1))
 (72 12 (:REWRITE ADE::LEN-WRITE-MEM1))
 (54 14 (:REWRITE REV-WHEN-NOT-CONSP))
 (49 10 (:REWRITE REVERSE-REMOVAL))
 (48 2 (:REWRITE ADE::STUBP-WRITE-MEM1))
 (47 1 (:REWRITE ADE::MEMORY-OKP-IF))
 (24 24 (:LINEAR LEN-WHEN-PREFIXP))
 (20 20 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (20 10 (:REWRITE STR::CONSP-OF-EXPLODE))
 (10 10 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (10 5 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE CONSP-OF-REV))
 (5 5 (:REWRITE DEFAULT-<-1))
 )
(ADE::V-IFF-V-ADDR1-V-ADDR2-READ-MEM1-WRITE-MEM1
 (1190 46 (:REWRITE ADE::V-IFF=EQUAL))
 (1098 46 (:DEFINITION ADE::BV2P))
 (954 318 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (890 890 (:TYPE-PRESCRIPTION ADE::BVP))
 (712 356 (:REWRITE DEFAULT-+-2))
 (651 593 (:REWRITE DEFAULT-CDR))
 (558 522 (:REWRITE DEFAULT-CAR))
 (356 356 (:REWRITE DEFAULT-+-1))
 (148 148 (:LINEAR LEN-WHEN-PREFIXP))
 (99 33 (:REWRITE ADE::BVP-V-FOURFIX))
 (72 56 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-MEM1))
 (48 2 (:REWRITE ADE::STUBP-WRITE-MEM1))
 (48 2 (:REWRITE ADE::ROMP-WRITE-MEM1))
 (48 2 (:REWRITE ADE::RAMP-WRITE-MEM1))
 (46 46 (:TYPE-PRESCRIPTION ADE::BV2P))
 (46 2 (:DEFINITION ADE::ROMP))
 (42 2 (:DEFINITION ADE::STUB-GUTS))
 (42 2 (:DEFINITION ADE::ROM-GUTS))
 (36 6 (:REWRITE ADE::LEN-WRITE-MEM1))
 )
(ADE::V-IFF-V-ADDR1-V-ADDR2-READ-MEM1-WRITE-MEM1-NOT-RAM
 (3621 1207 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (2508 2508 (:TYPE-PRESCRIPTION ADE::BVP))
 (2383 2325 (:REWRITE DEFAULT-CDR))
 (1962 981 (:REWRITE DEFAULT-+-2))
 (1507 1427 (:REWRITE DEFAULT-CAR))
 (981 981 (:REWRITE DEFAULT-+-1))
 (324 18 (:REWRITE ADE::V-IFF-V-ADDR1-V-ADDR2-READ-MEM1-WRITE-MEM1))
 (270 18 (:REWRITE ADE::V-IFF=EQUAL))
 (234 18 (:DEFINITION ADE::BV2P))
 (170 18 (:DEFINITION ADE::RAM-GUTS))
 (158 158 (:LINEAR LEN-WHEN-PREFIXP))
 (48 2 (:REWRITE ADE::STUBP-WRITE-MEM1))
 (48 2 (:REWRITE ADE::ROMP-WRITE-MEM1))
 (48 2 (:REWRITE ADE::RAMP-WRITE-MEM1))
 (36 36 (:TYPE-PRESCRIPTION ADE::V-IFF))
 (36 9 (:DEFINITION ADE::RAM))
 (36 6 (:REWRITE ADE::LEN-WRITE-MEM1))
 (27 9 (:REWRITE ADE::BVP-V-FOURFIX))
 (18 18 (:TYPE-PRESCRIPTION ADE::BV2P))
 )
(ADE::NOT-V-IFF-V-ADDR1-V-ADDR2-READ-MEM1-WRITE-MEM1
 (4349 4039 (:REWRITE DEFAULT-CDR))
 (3495 1165 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (2853 2499 (:REWRITE DEFAULT-CAR))
 (2716 2716 (:TYPE-PRESCRIPTION ADE::BVP))
 (2624 78 (:REWRITE ADE::V-IFF=EQUAL))
 (2468 78 (:DEFINITION ADE::BV2P))
 (2284 1142 (:REWRITE DEFAULT-+-2))
 (2198 108 (:DEFINITION ADE::ROMP))
 (1520 18 (:REWRITE ADE::V-IFF-V-ADDR1-V-ADDR2-READ-MEM1-WRITE-MEM1-NOT-RAM))
 (1466 18 (:DEFINITION ADE::RAMP-MEM1))
 (1142 1142 (:REWRITE DEFAULT-+-1))
 (968 95 (:DEFINITION ADE::ROM-GUTS))
 (968 95 (:DEFINITION ADE::RAM-GUTS))
 (642 34 (:REWRITE ADE::V-IFF-V-ADDR1-V-ADDR2-READ-MEM1-WRITE-MEM1))
 (496 496 (:LINEAR LEN-WHEN-PREFIXP))
 (454 380 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-MEM1))
 (388 18 (:REWRITE ADE::STUBP-WRITE-MEM1))
 (388 18 (:REWRITE ADE::ROMP-WRITE-MEM1))
 (388 18 (:REWRITE ADE::RAMP-WRITE-MEM1))
 (288 48 (:REWRITE ADE::LEN-WRITE-MEM1))
 (148 37 (:DEFINITION ADE::RAM))
 (126 126 (:TYPE-PRESCRIPTION ADE::RAMP-MEM1))
 (111 37 (:REWRITE ADE::BVP-V-FOURFIX))
 (78 78 (:TYPE-PRESCRIPTION ADE::BV2P))
 )
(ADE::READ-MEM-WRITE-MEM
 (20991 1031 (:REWRITE ADE::V-IFF=EQUAL))
 (19108 850 (:DEFINITION ADE::BV2P))
 (13979 11459 (:REWRITE DEFAULT-CDR))
 (11336 11336 (:TYPE-PRESCRIPTION ADE::BVP))
 (8166 4083 (:REWRITE DEFAULT-+-2))
 (7934 5402 (:REWRITE DEFAULT-CAR))
 (6840 2280 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (4083 4083 (:REWRITE DEFAULT-+-1))
 (2364 1182 (:TYPE-PRESCRIPTION ADE::BVP-REV))
 (2019 2019 (:REWRITE CONSP-OF-REV))
 (1387 591 (:REWRITE ADE::BVP-REV))
 (854 854 (:TYPE-PRESCRIPTION ADE::BV2P))
 (827 60 (:REWRITE REVERSE-REMOVAL))
 (667 267 (:REWRITE ADE::BVP-V-FOURFIX))
 (528 528 (:LINEAR LEN-WHEN-PREFIXP))
 (322 322 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (322 161 (:REWRITE STR::CONSP-OF-EXPLODE))
 (197 197 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 )
(ADE::TRUE-LISTP-READ-MEM1-OF-MEMORY-PROPERP)
(ADE::LEN-READ-MEM1-OF-MEMORY-PROPERP
 (1506 502 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (1288 1288 (:REWRITE DEFAULT-CDR))
 (1218 635 (:REWRITE DEFAULT-+-2))
 (1004 1004 (:TYPE-PRESCRIPTION ADE::BVP))
 (720 720 (:REWRITE DEFAULT-CAR))
 (635 635 (:REWRITE DEFAULT-+-1))
 (112 112 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-READ-MEM1-OF-MEMORY-PROPERP))
 (58 58 (:LINEAR LEN-WHEN-PREFIXP))
 (56 28 (:REWRITE DEFAULT-<-2))
 (44 44 (:TYPE-PRESCRIPTION ADE::READ-MEM1))
 (28 28 (:REWRITE DEFAULT-<-1))
 )
(ADE::TRUE-LISTP-READ-MEM-OF-MEMORY-PROPERP)
(ADE::TRUE-LISTP-READ-MEM-OF-MEMORY-PROPERP-32)
(ADE::LEN-READ-MEM-OF-MEMORY-PROPERP
 (252 246 (:REWRITE DEFAULT-CDR))
 (204 105 (:REWRITE DEFAULT-+-2))
 (198 66 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (174 33 (:DEFINITION TRUE-LISTP))
 (159 153 (:REWRITE DEFAULT-CAR))
 (132 132 (:TYPE-PRESCRIPTION ADE::BVP))
 (105 105 (:REWRITE DEFAULT-+-1))
 (49 10 (:REWRITE REVERSE-REMOVAL))
 (44 12 (:REWRITE REV-WHEN-NOT-CONSP))
 (24 3 (:REWRITE ZP-OPEN))
 (16 16 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (16 8 (:REWRITE STR::CONSP-OF-EXPLODE))
 (15 15 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (6 6 (:REWRITE CONSP-OF-REV))
 (6 3 (:REWRITE DEFAULT-<-2))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (3 3 (:REWRITE ADE::LEN-READ-MEM1-OF-MEMORY-PROPERP))
 (3 3 (:REWRITE DEFAULT-<-1))
 )
(ADE::LEN-READ-MEM-OF-MEMORY-PROPERP-32
 (186 1 (:DEFINITION ADE::MEMORY-PROPERP))
 (60 12 (:DEFINITION LEN))
 (46 2 (:DEFINITION ADE::ROMP))
 (46 2 (:DEFINITION ADE::RAMP))
 (31 31 (:REWRITE DEFAULT-CDR))
 (30 10 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (26 14 (:REWRITE DEFAULT-+-2))
 (25 5 (:DEFINITION TRUE-LISTP))
 (23 1 (:DEFINITION ADE::STUBP))
 (20 20 (:TYPE-PRESCRIPTION ADE::BVP))
 (20 5 (:DEFINITION ADE::4V-LISTP))
 (19 19 (:REWRITE DEFAULT-CAR))
 (14 14 (:REWRITE DEFAULT-+-1))
 (8 1 (:REWRITE ZP-OPEN))
 (8 1 (:DEFINITION ADE::STUB-GUTS))
 (8 1 (:DEFINITION ADE::ROM-GUTS))
 (8 1 (:DEFINITION ADE::RAM-GUTS))
 (5 5 (:TYPE-PRESCRIPTION ADE::4VP))
 (5 5 (:TYPE-PRESCRIPTION ADE::4V-LISTP))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 )
(ADE::BVP-READ-MEM1-OF-MEMORY-OKP
 (1506 502 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (1361 1361 (:REWRITE DEFAULT-CDR))
 (1240 646 (:REWRITE DEFAULT-+-2))
 (784 784 (:REWRITE DEFAULT-CAR))
 (646 646 (:REWRITE DEFAULT-+-1))
 (208 26 (:REWRITE ZP-OPEN))
 (52 26 (:REWRITE DEFAULT-<-2))
 (26 26 (:REWRITE DEFAULT-<-1))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::LEN-READ-MEM1-OF-MEMORY-OKP
 (1506 502 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (1432 1432 (:REWRITE DEFAULT-CDR))
 (1362 707 (:REWRITE DEFAULT-+-2))
 (792 792 (:REWRITE DEFAULT-CAR))
 (707 707 (:REWRITE DEFAULT-+-1))
 (112 112 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-READ-MEM1-OF-MEMORY-PROPERP))
 (112 112 (:TYPE-PRESCRIPTION ADE::READ-MEM1))
 (58 58 (:LINEAR LEN-WHEN-PREFIXP))
 (56 56 (:REWRITE ADE::LEN-READ-MEM1-OF-MEMORY-PROPERP))
 (56 28 (:REWRITE DEFAULT-<-2))
 (28 28 (:REWRITE DEFAULT-<-1))
 )
(ADE::BVP-READ-MEM-OF-MEMORY-OKP
 (273 267 (:REWRITE DEFAULT-CDR))
 (216 111 (:REWRITE DEFAULT-+-2))
 (198 66 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (174 168 (:REWRITE DEFAULT-CAR))
 (174 33 (:DEFINITION TRUE-LISTP))
 (111 111 (:REWRITE DEFAULT-+-1))
 (49 10 (:REWRITE REVERSE-REMOVAL))
 (44 12 (:REWRITE REV-WHEN-NOT-CONSP))
 (24 3 (:REWRITE ZP-OPEN))
 (16 16 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (16 8 (:REWRITE STR::CONSP-OF-EXPLODE))
 (15 15 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (6 6 (:REWRITE CONSP-OF-REV))
 (6 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE ADE::BVP-READ-MEM1-OF-MEMORY-OKP))
 )
(ADE::BVP-READ-MEM-OF-MEMORY-OKP-32)
(ADE::LEN-READ-MEM-OF-MEMORY-OKP
 (282 276 (:REWRITE DEFAULT-CDR))
 (234 120 (:REWRITE DEFAULT-+-2))
 (198 66 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (174 168 (:REWRITE DEFAULT-CAR))
 (174 33 (:DEFINITION TRUE-LISTP))
 (120 120 (:REWRITE DEFAULT-+-1))
 (49 10 (:REWRITE REVERSE-REMOVAL))
 (44 12 (:REWRITE REV-WHEN-NOT-CONSP))
 (24 3 (:REWRITE ZP-OPEN))
 (16 16 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (16 8 (:REWRITE STR::CONSP-OF-EXPLODE))
 (15 15 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (6 6 (:REWRITE CONSP-OF-REV))
 (6 3 (:REWRITE DEFAULT-<-2))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (3 3 (:REWRITE ADE::LEN-READ-MEM1-OF-MEMORY-PROPERP))
 (3 3 (:REWRITE ADE::LEN-READ-MEM1-OF-MEMORY-OKP))
 (3 3 (:REWRITE DEFAULT-<-1))
 )
(ADE::ALL-RAMP-MEM->RAMP-MEM1
 (570 190 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (422 237 (:REWRITE DEFAULT-+-2))
 (407 407 (:REWRITE DEFAULT-CDR))
 (380 380 (:TYPE-PRESCRIPTION ADE::BVP))
 (291 291 (:REWRITE DEFAULT-CAR))
 (237 237 (:REWRITE DEFAULT-+-1))
 (208 26 (:REWRITE ZP-OPEN))
 (52 26 (:REWRITE DEFAULT-<-2))
 (26 26 (:REWRITE DEFAULT-<-1))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::ALL-RAMP-MEM->RAMP-MEM
 (190 29 (:DEFINITION TRUE-LISTP))
 (174 58 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (142 139 (:REWRITE DEFAULT-CDR))
 (116 116 (:TYPE-PRESCRIPTION ADE::BVP))
 (102 99 (:REWRITE DEFAULT-CAR))
 (96 57 (:REWRITE DEFAULT-+-2))
 (57 57 (:REWRITE DEFAULT-+-1))
 (45 6 (:REWRITE REVERSE-REMOVAL))
 (36 36 (:LINEAR LEN-WHEN-PREFIXP))
 (24 8 (:REWRITE REV-WHEN-NOT-CONSP))
 (18 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE DEFAULT-<-1))
 (8 8 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (8 4 (:REWRITE STR::CONSP-OF-EXPLODE))
 (4 4 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (3 3 (:REWRITE CONSP-OF-REV))
 )
(ADE::ALL-RAMP-MEM-AFTER-WRITE-MEM1
 (837 279 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (640 358 (:REWRITE DEFAULT-+-2))
 (619 608 (:REWRITE DEFAULT-CDR))
 (570 570 (:TYPE-PRESCRIPTION ADE::BVP))
 (430 419 (:REWRITE DEFAULT-CAR))
 (358 358 (:REWRITE DEFAULT-+-1))
 (304 38 (:REWRITE ZP-OPEN))
 (242 11 (:REWRITE ADE::STUBP-WRITE-MEM1))
 (242 11 (:REWRITE ADE::RAMP-WRITE-MEM1))
 (76 38 (:REWRITE DEFAULT-<-2))
 (63 34 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-MEM1))
 (38 38 (:REWRITE DEFAULT-<-1))
 (18 6 (:REWRITE ADE::BVP-V-FOURFIX))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 )
(ADE::ALL-RAMP-MEM-AFTER-WRITE-MEM
 (138 46 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (134 128 (:REWRITE DEFAULT-CDR))
 (124 23 (:DEFINITION TRUE-LISTP))
 (110 110 (:TYPE-PRESCRIPTION ADE::BVP))
 (94 88 (:REWRITE DEFAULT-CAR))
 (86 48 (:REWRITE DEFAULT-+-2))
 (48 48 (:REWRITE DEFAULT-+-1))
 (48 2 (:REWRITE ADE::STUBP-WRITE-MEM1))
 (48 2 (:REWRITE ADE::RAMP-WRITE-MEM1))
 (45 6 (:REWRITE REVERSE-REMOVAL))
 (27 9 (:REWRITE ADE::BVP-V-FOURFIX))
 (24 8 (:REWRITE REV-WHEN-NOT-CONSP))
 (19 19 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (14 4 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-MEM1))
 (10 5 (:REWRITE DEFAULT-<-2))
 (8 8 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (8 4 (:REWRITE STR::CONSP-OF-EXPLODE))
 (6 6 (:REWRITE CONSP-OF-REV))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (5 5 (:REWRITE DEFAULT-<-1))
 (4 4 (:TYPE-PRESCRIPTION ADE::WRITE-MEM1))
 (4 4 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 )
(ADE::ALL-RAMP-MEM-CONSTANT-RAM
 (1920 640 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (1469 1306 (:REWRITE DEFAULT-CDR))
 (1424 1424 (:TYPE-PRESCRIPTION ADE::BVP))
 (1022 859 (:REWRITE DEFAULT-CAR))
 (989 606 (:REWRITE DEFAULT-+-2))
 (606 606 (:REWRITE DEFAULT-+-1))
 (410 18 (:REWRITE ADE::STUBP-CONSTANT-RAM))
 (410 18 (:REWRITE ADE::RAMP-CONSTANT-RAM))
 (218 74 (:REWRITE ADE::BVP-V-FOURFIX))
 (66 66 (:LINEAR LEN-WHEN-PREFIXP))
 (42 42 (:REWRITE DEFAULT-<-2))
 (42 42 (:REWRITE DEFAULT-<-1))
 )
(ADE::MEMORY-OKP==>MEMORY-PROPERP
 (2544 848 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (1913 1913 (:REWRITE DEFAULT-CDR))
 (1674 926 (:REWRITE DEFAULT-+-2))
 (926 926 (:REWRITE DEFAULT-+-1))
 (916 916 (:REWRITE DEFAULT-CAR))
 (180 60 (:REWRITE FOLD-CONSTS-IN-+))
 (147 57 (:REWRITE ZP-OPEN))
 (30 30 (:REWRITE DEFAULT-<-2))
 (30 30 (:REWRITE DEFAULT-<-1))
 (16 16 (:LINEAR LEN-WHEN-PREFIXP))
 )