(X86ISA::POPCOUNT-HYPS)
(CODEWALKER-WRAPPER
 (180 4 (:DEFINITION MEMBER-EQUAL))
 (129 9 (:REWRITE SUBSETP-MEMBER . 3))
 (79 17 (:REWRITE NATP-WHEN-INTEGERP))
 (68 12 (:REWRITE NFIX-WHEN-NOT-NATP))
 (58 58 (:TYPE-PRESCRIPTION NFIX))
 (46 42 (:REWRITE DEFAULT-<-2))
 (46 42 (:REWRITE DEFAULT-<-1))
 (42 9 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (39 9 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (38 4 (:REWRITE O<=-O-FINP-DEF))
 (36 18 (:TYPE-PRESCRIPTION X86ISA::RIP-IS-INTEGERP))
 (36 3 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (24 24 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (24 24 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (24 24 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (24 24 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (24 24 (:REWRITE CONSP-BY-LEN))
 (22 2 (:REWRITE |a < b  <=>  c+a < c+b :l1|))
 (18 18 (:TYPE-PRESCRIPTION X86ISA::X86P))
 (18 18 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (14 14 (:REWRITE DEFAULT-+-1))
 (12 2 (:REWRITE O-FIRST-EXPT-<))
 (10 10 (:REWRITE DEFAULT-UNARY-MINUS))
 (9 9 (:REWRITE SUBSETP-TRANS2))
 (9 9 (:REWRITE SUBSETP-TRANS))
 (9 9 (:REWRITE SUBSETP-MEMBER . 4))
 (9 9 (:REWRITE SUBSETP-MEMBER . 2))
 (9 9 (:REWRITE SUBSETP-MEMBER . 1))
 (9 9 (:REWRITE INTERSECTP-MEMBER . 3))
 (9 9 (:REWRITE INTERSECTP-MEMBER . 2))
 (8 4 (:REWRITE O-FIRST-EXPT-DEF-O-FINP))
 (8 4 (:REWRITE AC-<))
 (7 7 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (6 4 (:REWRITE O-INFP-O-FINP-O<=))
 (4 4 (:REWRITE |a < b & b < c  =>  a < c|))
 (4 4 (:REWRITE INEQUALITY-WITH-NFIX-HYP-2))
 (4 4 (:REWRITE INEQUALITY-WITH-NFIX-HYP-1))
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 2 (:REWRITE O-FIRST-COEFF-<))
 )
(CODEWALKER-WRAPPER-RULE-1
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 )
(CODEWALKER-WRAPPER-RULE-2
 (331 8 (:DEFINITION BINARY-APPEND))
 (153 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (122 3 (:DEFINITION MEMBER-EQUAL))
 (94 29 (:REWRITE CONSP-OF-REV))
 (75 11 (:REWRITE DEFAULT-CDR))
 (75 11 (:REWRITE DEFAULT-CAR))
 (74 74 (:TYPE-PRESCRIPTION REV))
 (74 74 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (74 74 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (74 74 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (74 74 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (74 74 (:REWRITE CONSP-BY-LEN))
 (64 8 (:REWRITE SUBSETP-MEMBER . 3))
 (56 28 (:TYPE-PRESCRIPTION X86ISA::RIP-IS-INTEGERP))
 (39 6 (:REWRITE MEMBER-WHEN-ATOM))
 (32 6 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (32 6 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (30 5 (:REWRITE REV-WHEN-NOT-CONSP))
 (28 28 (:TYPE-PRESCRIPTION X86ISA::X86P))
 (13 13 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (12 1 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (8 8 (:REWRITE SUBSETP-TRANS2))
 (8 8 (:REWRITE SUBSETP-TRANS))
 (8 8 (:REWRITE SUBSETP-MEMBER . 4))
 (8 8 (:REWRITE SUBSETP-MEMBER . 2))
 (8 8 (:REWRITE INTERSECTP-MEMBER . 3))
 (8 8 (:REWRITE INTERSECTP-MEMBER . 2))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (3 1 (:REWRITE NATP-WHEN-GTE-0))
 (2 2 (:REWRITE CODEWALKER-WRAPPER-RULE-1))
 (1 1 (:REWRITE NATP-WHEN-INTEGERP))
 )
(CODEWALKER-WRAPPER-IGNORES-SPLITTERS
 (1162 28 (:DEFINITION BINARY-APPEND))
 (718 20 (:DEFINITION MEMBER-EQUAL))
 (490 56 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (308 98 (:REWRITE CONSP-OF-REV))
 (282 282 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (282 282 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (282 282 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (282 282 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (282 282 (:REWRITE CONSP-BY-LEN))
 (272 48 (:REWRITE DEFAULT-CDR))
 (272 48 (:REWRITE DEFAULT-CAR))
 (252 252 (:TYPE-PRESCRIPTION REV))
 (152 76 (:TYPE-PRESCRIPTION X86ISA::RIP-IS-INTEGERP))
 (134 28 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (130 28 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (96 40 (:REWRITE CODEWALKER-WRAPPER-RULE-2))
 (92 40 (:REWRITE CODEWALKER-WRAPPER-RULE-1))
 (84 14 (:REWRITE REV-WHEN-NOT-CONSP))
 (76 76 (:TYPE-PRESCRIPTION X86ISA::X86P))
 (74 74 (:REWRITE DEFAULT-<-2))
 (74 74 (:REWRITE DEFAULT-<-1))
 (72 6 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (68 68 (:REWRITE SUBSETP-MEMBER . 4))
 (68 68 (:REWRITE INTERSECTP-MEMBER . 3))
 (68 68 (:REWRITE INTERSECTP-MEMBER . 2))
 (66 24 (:REWRITE X86ISA::X86-FETCH-DECODE-EXECUTE-OPENER))
 (60 60 (:REWRITE DEFAULT-+-1))
 (56 56 (:REWRITE SUBSETP-MEMBER . 2))
 (56 56 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (42 21 (:DEFINITION X86ISA::MS))
 (40 40 (:REWRITE SUBSETP-TRANS2))
 (40 40 (:REWRITE SUBSETP-TRANS))
 (28 28 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (21 21 (:DEFINITION X86ISA::MS$A))
 (11 11 (:REWRITE NATP-WHEN-INTEGERP))
 (10 10 (:TYPE-PRESCRIPTION NATP))
 )
(CODEWALKER-WRAPPER-RULE-3
 (1467 39 (:DEFINITION MEMBER-EQUAL))
 (1228 614 (:TYPE-PRESCRIPTION X86ISA::RIP-IS-INTEGERP))
 (1084 26 (:DEFINITION BINARY-APPEND))
 (832 18 (:REWRITE ASSOCIATIVITY-OF-APPEND))
 (614 614 (:TYPE-PRESCRIPTION X86ISA::X86P))
 (390 52 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (378 378 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (378 378 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (378 378 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (378 378 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (378 378 (:REWRITE CONSP-BY-LEN))
 (374 75 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (373 79 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (272 64 (:REWRITE DEFAULT-CDR))
 (272 64 (:REWRITE DEFAULT-CAR))
 (256 86 (:REWRITE CONSP-OF-REV))
 (228 19 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (224 224 (:TYPE-PRESCRIPTION REV))
 (159 57 (:REWRITE X86ISA::X86-FETCH-DECODE-EXECUTE-OPENER))
 (137 137 (:REWRITE SUBSETP-MEMBER . 4))
 (137 137 (:REWRITE INTERSECTP-MEMBER . 3))
 (137 137 (:REWRITE INTERSECTP-MEMBER . 2))
 (121 121 (:REWRITE SUBSETP-TRANS2))
 (121 121 (:REWRITE SUBSETP-TRANS))
 (113 113 (:REWRITE DEFAULT-<-2))
 (113 113 (:REWRITE DEFAULT-<-1))
 (110 48 (:REWRITE CODEWALKER-WRAPPER-RULE-2))
 (104 104 (:REWRITE SUBSETP-MEMBER . 2))
 (102 51 (:DEFINITION X86ISA::MS))
 (97 97 (:REWRITE DEFAULT-+-1))
 (81 81 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (51 51 (:DEFINITION X86ISA::MS$A))
 (48 8 (:REWRITE REV-WHEN-NOT-CONSP))
 (48 3 (:REWRITE SUBSETP-OF-CONS))
 (36 36 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (30 10 (:REWRITE NATP-WHEN-GTE-0))
 (24 4 (:DEFINITION ATOM))
 (10 10 (:REWRITE NATP-WHEN-INTEGERP))
 )
(X86ISA::CLK-X400610)
(X86ISA::SEM-X400610)
(X86ISA::SEM-X400610-CORRECT
 (100785 1299 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (80657 87 (:REWRITE X86ISA::ZF-SPEC-THM))
 (67620 2559 (:REWRITE BFIX-WHEN-NOT-1))
 (58737 468 (:LINEAR LOGHEAD-UPPER-BOUND))
 (56584 62 (:LINEAR X86ISA::N01P-ZF-SPEC))
 (38567 1221 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (33225 307 (:REWRITE BITOPS::BASIC-UNSIGNED-BYTE-P-OF-+-WITH-CIN . 2))
 (26429 89 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 2))
 (13010 610 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (13010 610 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (10929 45 (:REWRITE BITOPS::CANCEL-LOGEXT-UNDER-LOGHEAD))
 (10191 1706 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (9793 307 (:REWRITE BITOPS::BASIC-UNSIGNED-BYTE-P-OF-+-WITH-CIN . 1))
 (8550 14 (:REWRITE X86ISA::GREATER-LOGBITP-OF-UNSIGNED-BYTE-P . 2))
 (7852 604 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-5BITS-P))
 (7350 444 (:REWRITE DIFFERENCE-UNSIGNED-BYTE-P))
 (6940 755 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-11BITS-P))
 (6044 622 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR8BITS-P))
 (6044 622 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-4BITS-P))
 (5710 901 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (5443 2559 (:REWRITE BFIX-WHEN-NOT-BITP))
 (5118 5118 (:TYPE-PRESCRIPTION BIT->BOOL$INLINE))
 (5118 2559 (:REWRITE BFIX-WHEN-NOT-BIT->BOOL))
 (5118 2559 (:REWRITE BFIX-WHEN-BIT->BOOL))
 (4116 768 (:REWRITE LOGTAIL-IDENTITY))
 (3977 89 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-2))
 (3805 7 (:REWRITE EQUAL-1-OF-BOOL->BIT))
 (3463 461 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (3322 302 (:REWRITE X86ISA::5BITS-P-WHEN-UNSIGNED-BYTE-P))
 (3307 3307 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (2985 715 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (2807 2807 (:TYPE-PRESCRIPTION BITP))
 (2448 72 (:REWRITE BITOPS::BASIC-SIGNED-BYTE-P-OF-+-WITH-CIN . 2))
 (2294 2294 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (2286 271 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (2286 271 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (2120 306 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-13BITS-P))
 (2087 868 (:REWRITE DEFAULT-+-1))
 (1992 49 (:REWRITE X86ISA::GET-PREFIXES-OPENER-LEMMA-NO-LEGACY-PREFIX-BUT-REX-PREFIX))
 (1714 14 (:REWRITE BITOPS::LOGBITP-NONZERO-OF-BIT))
 (1706 1706 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (1623 1299 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (1623 1299 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (1510 1510 (:TYPE-PRESCRIPTION X86ISA::11BITS-P))
 (1510 755 (:REWRITE X86ISA::11BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1458 4 (:REWRITE BITOPS::UNSIGNED-BYTE-P-OF-0-X))
 (1412 2 (:DEFINITION X86ISA::RME08$INLINE))
 (1392 2 (:DEFINITION X86ISA::EA-TO-LA$INLINE))
 (1299 1299 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (1299 1299 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (1299 1299 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (1245 415 (:REWRITE DEFAULT-UNARY-MINUS))
 (1244 1244 (:TYPE-PRESCRIPTION X86ISA::CR8BITS-P$INLINE))
 (1244 1244 (:TYPE-PRESCRIPTION X86ISA::4BITS-P))
 (1244 622 (:REWRITE X86ISA::CR8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1244 622 (:REWRITE X86ISA::4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1220 1220 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (1220 1220 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (1220 610 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1220 610 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (985 985 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (906 906 (:TYPE-PRESCRIPTION X86ISA::5BITS-P))
 (858 224 (:REWRITE X86ISA::13BITS-P-WHEN-UNSIGNED-BYTE-P))
 (785 90 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-31BITS-P))
 (676 676 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (652 652 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (652 326 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (648 54 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-BASE-IS-N64P))
 (616 56 (:TYPE-PRESCRIPTION X86ISA::READ-*IP-WHEN-NOT-64-BIT-MODEP))
 (567 90 (:REWRITE O-INFP->NEQ-0))
 (544 544 (:TYPE-PRESCRIPTION X86ISA::NATP-CREATE-UNDEF))
 (530 530 (:TYPE-PRESCRIPTION X86ISA::13BITS-P))
 (450 450 (:TYPE-PRESCRIPTION NATP))
 (437 40 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-2BITS-P))
 (402 402 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (370 370 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (370 370 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (370 185 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (370 185 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (370 185 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (359 37 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-3BITS-P))
 (313 313 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (302 302 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (295 295 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (233 59 (:REWRITE DEFAULT-*-2))
 (188 188 (:REWRITE X86ISA::RME08-WHEN-64-BIT-MODEP-AND-FS/GS))
 (186 62 (:LINEAR X86ISA::N01P-SF-SPEC32))
 (186 62 (:LINEAR X86ISA::N01P-PF-SPEC32))
 (182 82 (:REWRITE NFIX-WHEN-NOT-NATP))
 (180 180 (:TYPE-PRESCRIPTION X86ISA::31BITS-P))
 (180 90 (:REWRITE X86ISA::31BITS-P-WHEN-UNSIGNED-BYTE-P))
 (178 89 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->VM-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->VIP-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->VIF-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->TF-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->RF-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->RES5-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->RES4-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->RES3-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->RES2-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->RES1-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->NT-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->IOPL-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->INTF-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->ID-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->DF-OF-WRITE-WITH-MASK))
 (157 157 (:REWRITE X86ISA::RFLAGSBITS->AC-OF-WRITE-WITH-MASK))
 (147 62 (:REWRITE DEFAULT-<-1))
 (126 26 (:REWRITE BITOPS::BASIC-SIGNED-BYTE-P-OF-MIXED-*))
 (122 122 (:REWRITE X86ISA::RFLAGSBITS->ZF-OF-WRITE-WITH-MASK))
 (122 122 (:REWRITE X86ISA::RFLAGSBITS->SF-OF-WRITE-WITH-MASK))
 (122 122 (:REWRITE X86ISA::RFLAGSBITS->PF-OF-WRITE-WITH-MASK))
 (122 122 (:REWRITE X86ISA::RFLAGSBITS->OF-OF-WRITE-WITH-MASK))
 (122 122 (:REWRITE X86ISA::RFLAGSBITS->CF-OF-WRITE-WITH-MASK))
 (122 122 (:REWRITE X86ISA::RFLAGSBITS->AF-OF-WRITE-WITH-MASK))
 (94 62 (:REWRITE DEFAULT-<-2))
 (85 85 (:REWRITE-QUOTED-CONSTANT X86ISA::RFLAGSBITS-FIX-UNDER-RFLAGSBITS-EQUIV))
 (83 77 (:REWRITE X86ISA::RB-XW-RFLAGS-NOT-AC-VALUES-IN-SYS-VIEW))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::2BITS-P))
 (80 40 (:REWRITE X86ISA::2BITS-P-WHEN-UNSIGNED-BYTE-P))
 (74 74 (:TYPE-PRESCRIPTION X86ISA::3BITS-P))
 (74 37 (:REWRITE X86ISA::3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (74 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (73 73 (:REWRITE X86ISA::SIGNED-BYTE-P-LIMITS-THM))
 (72 72 (:REWRITE BITOPS::BASIC-SIGNED-BYTE-P-OF-+-WITH-CIN . 1))
 (70 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX-PREFIXES-P))
 (70 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-24BITS-P))
 (66 66 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
 (63 57 (:REWRITE X86ISA::RB-RETURNS-X86-IN-NON-MARKING-VIEW-IF-NO-ERROR))
 (62 59 (:REWRITE DEFAULT-*-1))
 (57 51 (:REWRITE X86ISA::RB-XW-RFLAGS-NOT-AC-STATE-IN-SYS-VIEW))
 (51 26 (:REWRITE BITOPS::BASIC-SIGNED-BYTE-P-OF-*))
 (48 24 (:REWRITE NATP-WHEN-GTE-0))
 (48 16 (:LINEAR X86ISA::N01P-OF-SPEC32))
 (42 14 (:REWRITE BITOPS::LOGBITP-WHEN-BITMASKP))
 (41 41 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 (40 2 (:REWRITE X86ISA::LOGEXT-LOGHEAD-IDENTITY))
 (30 10 (:LINEAR X86ISA::N01P-ADD-AF-SPEC32))
 (28 2 (:REWRITE ZP-WHEN-INTEGERP))
 (26 2 (:REWRITE UNICITY-OF-0))
 (24 24 (:REWRITE NATP-WHEN-INTEGERP))
 (24 2 (:DEFINITION FIX))
 (18 9 (:REWRITE X86ISA::RME-SIZE-NON-CANONICAL-WHEN-64-BIT-MODEP-AND-NOT-FS/GS))
 (18 6 (:LINEAR X86ISA::N01P-SUB-AF-SPEC32))
 (14 14 (:TYPE-PRESCRIPTION RATIONALP-EXPT-TYPE-PRESCRIPTION))
 (14 14 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE))
 (14 14 (:REWRITE BITOPS::NORMALIZE-LOGBITP-WHEN-MODS-EQUAL))
 (14 14 (:REWRITE X86ISA::GREATER-LOGBITP-OF-UNSIGNED-BYTE-P . 1))
 (12 4 (:LINEAR X86ISA::N01P-CF-SPEC32))
 (10 10 (:TYPE-PRESCRIPTION X86ISA::VEX-PREFIXES-P$INLINE))
 (10 10 (:TYPE-PRESCRIPTION X86ISA::24BITS-P))
 (10 5 (:REWRITE X86ISA::VEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (10 5 (:REWRITE X86ISA::24BITS-P-WHEN-UNSIGNED-BYTE-P))
 (10 2 (:REWRITE BITOPS::BASIC-SIGNED-BYTE-P-OF-BINARY-MINUS))
 (9 9 (:REWRITE X86ISA::RME-SIZE-WHEN-64-BIT-MODEP-FS/GS))
 (9 9 (:REWRITE X86ISA::RME-SIZE-UNALIGNED-WHEN-64-BIT-MODEP-AND-NOT-FS/GS))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-UPPER-BOUND-IS-N32P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-LOWER-BOUND-IS-N33P))
 (6 6 (:TYPE-PRESCRIPTION LOGBITP))
 (6 3 (:DEFINITION X86ISA::MARKING-VIEW))
 (6 2 (:REWRITE X86ISA::EA-TO-LA-WHEN-64-BIT-MODEP-AND-NOT-FS/GS))
 (5 1 (:REWRITE X86ISA::X86-RUN-ALT-HALTED))
 (4 2 (:REWRITE ZP-WHEN-GT-0))
 (3 3 (:DEFINITION X86ISA::MARKING-VIEW$A))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::N32P-XR-RFLAGS))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-OF-LOGEXT))
 (2 2 (:REWRITE SIGNED-BYTE-P-LOGEXT))
 (2 2 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (2 2 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (1 1 (:REWRITE X86ISA::GET-PREFIXES-OPENER-LEMMA-ZERO-CNT))
 )
(X86ISA::POPCOUNT-RESULT-FN)
(X86ISA::POPCOUNT-RESULT-FN)
(X86ISA::POPCOUNT-RESULT-FN-CORRECT
 (2992 54 (:REWRITE LOGHEAD-IDENTITY))
 (2747 61 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (1564 782 (:TYPE-PRESCRIPTION BITOPS::LOGAND-NATP-TYPE-2))
 (1417 11 (:LINEAR LOGHEAD-UPPER-BOUND))
 (1374 1 (:REWRITE X86ISA::GREATER-LOGBITP-OF-UNSIGNED-BYTE-P . 2))
 (1217 21 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (1061 41 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (984 4 (:REWRITE BITOPS::CANCEL-LOGEXT-UNDER-LOGHEAD))
 (882 40 (:REWRITE BITOPS::BASIC-UNSIGNED-BYTE-P-OF-+))
 (880 8 (:REWRITE BITOPS::BASIC-UNSIGNED-BYTE-P-OF-+-WITH-CIN . 2))
 (748 748 (:TYPE-PRESCRIPTION LOGHEAD-TYPE))
 (679 256 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (542 1 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (540 1 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (514 30 (:REWRITE UNSIGNED-BYTE-P-OF-LOGAND-2))
 (404 36 (:REWRITE LOGEXT-IDENTITY))
 (376 62 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (357 51 (:REWRITE LOGTAIL-IDENTITY))
 (356 356 (:TYPE-PRESCRIPTION LOGEXT-TYPE))
 (344 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (344 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (250 4 (:LINEAR LOGEXT-BOUNDS))
 (230 4 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (224 8 (:REWRITE BITOPS::BASIC-UNSIGNED-BYTE-P-OF-+-WITH-CIN . 1))
 (210 14 (:REWRITE DIFFERENCE-UNSIGNED-BYTE-P))
 (208 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-5BITS-P))
 (204 6 (:REWRITE BITOPS::BASIC-SIGNED-BYTE-P-OF-+-WITH-CIN . 2))
 (195 31 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (186 186 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (186 18 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR8BITS-P))
 (186 18 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-4BITS-P))
 (184 20 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-11BITS-P))
 (147 147 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (137 1 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-2))
 (133 1 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 2))
 (127 127 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (113 1 (:REWRITE X86ISA::ZF-SPEC-THM))
 (112 48 (:REWRITE DEFAULT-+-1))
 (102 6 (:REWRITE BITOPS::BASIC-SIGNED-BYTE-P-OF-+))
 (100 14 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (100 14 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (100 14 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (100 14 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (95 95 (:TYPE-PRESCRIPTION BITP))
 (90 90 (:TYPE-PRESCRIPTION BITOPS::LOGAND-NATP-TYPE-1))
 (88 8 (:REWRITE X86ISA::5BITS-P-WHEN-UNSIGNED-BYTE-P))
 (82 22 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (82 22 (:REWRITE IFIX-WHEN-INTEGERP))
 (80 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-13BITS-P))
 (78 26 (:REWRITE DEFAULT-UNARY-MINUS))
 (69 61 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (69 61 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (62 62 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (61 61 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (61 61 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (61 61 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (60 30 (:REWRITE UNSIGNED-BYTE-P-OF-LOGHEAD))
 (60 30 (:REWRITE UNSIGNED-BYTE-P-OF-LOGAND-1))
 (60 6 (:REWRITE SIGNED-BYTE-P-LOGOPS))
 (46 46 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-2BITS-P))
 (40 40 (:TYPE-PRESCRIPTION X86ISA::11BITS-P))
 (40 20 (:REWRITE X86ISA::11BITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-3BITS-P))
 (36 36 (:TYPE-PRESCRIPTION X86ISA::CR8BITS-P$INLINE))
 (36 36 (:TYPE-PRESCRIPTION X86ISA::4BITS-P))
 (36 18 (:REWRITE X86ISA::CR8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (36 18 (:REWRITE X86ISA::4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (36 8 (:REWRITE X86ISA::13BITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (32 16 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 30 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (28 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX-PREFIXES-P))
 (28 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-24BITS-P))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::5BITS-P))
 (24 6 (:REWRITE DEFAULT-*-2))
 (23 1 (:REWRITE BITOPS::LOGBITP-NONZERO-OF-BIT))
 (22 20 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (21 21 (:TYPE-PRESCRIPTION NATP))
 (20 20 (:TYPE-PRESCRIPTION X86ISA::13BITS-P))
 (20 20 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (20 20 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (20 20 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (18 18 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (17 17 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (16 8 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (16 8 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (16 8 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (16 8 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-31BITS-P))
 (15 9 (:REWRITE BITOPS::BASIC-UNSIGNED-BYTE-P-OF-*))
 (12 4 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (9 4 (:REWRITE DEFAULT-<-1))
 (9 3 (:REWRITE NFIX-WHEN-NATP))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::NATP-CREATE-UNDEF))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::3BITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::2BITS-P))
 (8 4 (:REWRITE X86ISA::3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::2BITS-P-WHEN-UNSIGNED-BYTE-P))
 (7 3 (:REWRITE NFIX-WHEN-NOT-NATP))
 (6 6 (:REWRITE X86ISA::SIGNED-BYTE-P-LIMITS-THM))
 (6 6 (:REWRITE FOLD-CONSTS-IN-+))
 (6 6 (:REWRITE DEFAULT-*-1))
 (6 6 (:REWRITE BITOPS::BASIC-SIGNED-BYTE-P-OF-+-WITH-CIN . 1))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::VEX-PREFIXES-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::31BITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::24BITS-P))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 2 (:REWRITE X86ISA::VEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE NATP-WHEN-GTE-0))
 (4 2 (:REWRITE X86ISA::31BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::24BITS-P-WHEN-UNSIGNED-BYTE-P))
 (3 3 (:TYPE-PRESCRIPTION IFIX))
 (3 1 (:REWRITE BITOPS::LOGBITP-WHEN-BITMASKP))
 (2 2 (:REWRITE NATP-WHEN-INTEGERP))
 (2 1 (:REWRITE O-INFP->NEQ-0))
 (2 1 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (1 1 (:TYPE-PRESCRIPTION RATIONALP-EXPT-TYPE-PRESCRIPTION))
 (1 1 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE))
 (1 1 (:REWRITE X86ISA::XR-OF-XW-INTER-FIELD))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->VM-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->VIP-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->VIF-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->TF-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->RF-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->RES5-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->RES4-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->RES3-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->RES2-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->RES1-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->NT-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->IOPL-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->INTF-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->ID-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->DF-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE X86ISA::RFLAGSBITS->AC-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE BITOPS::NORMALIZE-LOGBITP-WHEN-MODS-EQUAL))
 (1 1 (:REWRITE X86ISA::GREATER-LOGBITP-OF-UNSIGNED-BYTE-P . 1))
 )
(X86ISA::X86-POPCOUNT-32-CORRECT
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )