(X86ISA::MEMBER-P-REMOVE-DUPLICATES-EQUAL-IFF-MEMBER-P)
(X86ISA::MEMBER-P-AND-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY
 (57 1 (:DEFINITION X86ISA::CREATE-QWORD-ADDRESS-LIST))
 (33 3 (:REWRITE ASH-0))
 (21 3 (:REWRITE ZIP-OPEN))
 (17 1 (:REWRITE X86ISA::NOT-MEMBER-P-CREATE-QWORD-ADDRESS-LIST))
 (16 1 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-0))
 (15 5 (:REWRITE DEFAULT-+-2))
 (12 4 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (12 4 (:REWRITE DEFAULT-<-2))
 (9 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (9 1 (:REWRITE LOGHEAD-IDENTITY))
 (9 1 (:REWRITE BITOPS::BASIC-UNSIGNED-BYTE-P-OF-+))
 (8 8 (:REWRITE X86ISA::MEMBER-P-AND-MULT-8-QWORD-PADDR-LISTP))
 (8 4 (:DEFINITION X86ISA::APP-VIEW))
 (8 1 (:REWRITE X86ISA::N52P-LEFT-SHIFTING-A-40-BIT-NATP-BY-12-+-7))
 (7 7 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 (6 3 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (6 1 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (5 5 (:REWRITE DEFAULT-+-1))
 (5 3 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (5 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-3BITS-P))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (4 4 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (4 4 (:DEFINITION X86ISA::APP-VIEW$A))
 (3 3 (:TYPE-PRESCRIPTION ZIP))
 (3 3 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (3 3 (:TYPE-PRESCRIPTION IFIX))
 (3 3 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (3 3 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->REFERENCE-ADDR-OF-WRITE-WITH-MASK))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::3BITS-P))
 (2 2 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (2 1 (:REWRITE X86ISA::3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1 1 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-3))
 (1 1 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-2))
 (1 1 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-1))
 )
(X86ISA::MEMBER-P-WHEN-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-THEN-MEMBER-P-ENTRIES-AUX
 (420 56 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (385 11 (:REWRITE X86ISA::MEMBER-P-AND-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY))
 (143 143 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS->REFERENCE-ADDR$INLINE))
 (121 11 (:REWRITE ASH-0))
 (120 12 (:DEFINITION BINARY-APPEND))
 (118 60 (:REWRITE X86ISA::MEMBER-P-CDR))
 (110 55 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
 (96 24 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (92 92 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (92 92 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (92 92 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (92 92 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (92 92 (:REWRITE CONSP-BY-LEN))
 (77 11 (:REWRITE ZIP-OPEN))
 (66 66 (:REWRITE DEFAULT-CAR))
 (60 60 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (60 60 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (60 60 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (54 54 (:REWRITE DEFAULT-CDR))
 (45 45 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (40 20 (:TYPE-PRESCRIPTION X86ISA::CONSP-APPEND))
 (33 11 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (33 11 (:REWRITE DEFAULT-<-2))
 (28 28 (:REWRITE X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-WITH-DIFFERENT-X86-ENTRIES))
 (22 11 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (22 11 (:REWRITE DEFAULT-<-1))
 (22 11 (:DEFINITION X86ISA::APP-VIEW))
 (20 20 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (11 11 (:TYPE-PRESCRIPTION ZIP))
 (11 11 (:TYPE-PRESCRIPTION IFIX))
 (11 11 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (11 11 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (11 11 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (11 11 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->REFERENCE-ADDR-OF-WRITE-WITH-MASK))
 (11 11 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (11 11 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (11 11 (:DEFINITION X86ISA::APP-VIEW$A))
 (2 2 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 )
(X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX-AND-ENTRIES)
(X86ISA::MEMBER-P-AFTER-REMOVE-DUPLICATES-EQUAL-OF-SUPERIOR-PADDRS-IN-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX-1
 (578 14 (:DEFINITION MEMBER-EQUAL))
 (474 28 (:REWRITE SUBSETP-CAR-MEMBER))
 (384 52 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (234 40 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (222 28 (:REWRITE MEMBER-WHEN-ATOM))
 (190 19 (:DEFINITION BINARY-APPEND))
 (188 188 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (188 188 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (188 188 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (188 188 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (188 188 (:REWRITE CONSP-BY-LEN))
 (174 12 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (152 38 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (140 4 (:REWRITE X86ISA::MEMBER-P-AND-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY))
 (121 121 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (119 117 (:REWRITE DEFAULT-CDR))
 (118 116 (:REWRITE DEFAULT-CAR))
 (114 57 (:REWRITE X86ISA::MEMBER-P-CDR))
 (80 80 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (57 57 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (57 57 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (57 57 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (52 52 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS->REFERENCE-ADDR$INLINE))
 (46 46 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (44 4 (:REWRITE ASH-0))
 (40 40 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (40 40 (:REWRITE SUBSETP-TRANS2))
 (40 40 (:REWRITE SUBSETP-TRANS))
 (40 20 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
 (29 29 (:REWRITE X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-WITH-DIFFERENT-X86-ENTRIES))
 (28 28 (:REWRITE SUBSETP-MEMBER . 4))
 (28 28 (:REWRITE SUBSETP-MEMBER . 3))
 (28 28 (:REWRITE SUBSETP-MEMBER . 2))
 (28 28 (:REWRITE SUBSETP-MEMBER . 1))
 (28 28 (:REWRITE INTERSECTP-MEMBER . 3))
 (28 28 (:REWRITE INTERSECTP-MEMBER . 2))
 (28 4 (:REWRITE ZIP-OPEN))
 (22 22 (:REWRITE X86ISA::MEMBER-P-WHEN-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-THEN-MEMBER-P-ENTRIES-AUX))
 (12 12 (:REWRITE CONSP-OF-CDDDR-BY-LEN))
 (12 4 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (12 4 (:REWRITE DEFAULT-<-2))
 (8 4 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (8 4 (:REWRITE DEFAULT-<-1))
 (8 4 (:DEFINITION X86ISA::APP-VIEW))
 (4 4 (:TYPE-PRESCRIPTION ZIP))
 (4 4 (:TYPE-PRESCRIPTION IFIX))
 (4 4 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (4 4 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (4 4 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->REFERENCE-ADDR-OF-WRITE-WITH-MASK))
 (4 4 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (4 4 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (4 4 (:DEFINITION X86ISA::APP-VIEW$A))
 )
(X86ISA::MEMBER-P-AFTER-REMOVE-DUPLICATES-EQUAL-OF-SUPERIOR-PADDRS-IN-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX-2
 (3461 79 (:REWRITE X86ISA::MEMBER-P-AFTER-REMOVE-DUPLICATES-EQUAL-OF-SUPERIOR-PADDRS-IN-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX-1))
 (1648 119 (:REWRITE SUBSETP-CAR-MEMBER))
 (950 95 (:DEFINITION BINARY-APPEND))
 (925 140 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (772 772 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (772 772 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (772 772 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (772 772 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (772 772 (:REWRITE CONSP-BY-LEN))
 (760 190 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (534 528 (:REWRITE DEFAULT-CDR))
 (526 16 (:REWRITE X86ISA::MEMBER-P-AND-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY))
 (510 504 (:REWRITE DEFAULT-CAR))
 (500 500 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (259 259 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (197 197 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (197 197 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (195 195 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS->REFERENCE-ADDR$INLINE))
 (192 24 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (178 19 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (165 15 (:REWRITE ASH-0))
 (153 153 (:REWRITE SUBSETP-TRANS2))
 (153 153 (:REWRITE SUBSETP-TRANS))
 (150 75 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
 (140 140 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (136 136 (:REWRITE SUBSETP-MEMBER . 4))
 (136 136 (:REWRITE INTERSECTP-MEMBER . 3))
 (136 136 (:REWRITE INTERSECTP-MEMBER . 2))
 (132 12 (:DEFINITION TRUE-LISTP))
 (130 130 (:REWRITE SUBSETP-MEMBER . 2))
 (123 123 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (112 112 (:REWRITE X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-WITH-DIFFERENT-X86-ENTRIES))
 (105 15 (:REWRITE ZIP-OPEN))
 (90 45 (:TYPE-PRESCRIPTION X86ISA::CONSP-APPEND))
 (48 48 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (48 24 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (48 24 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (45 45 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (45 15 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (45 15 (:REWRITE DEFAULT-<-2))
 (30 15 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (30 15 (:REWRITE DEFAULT-<-1))
 (30 15 (:DEFINITION X86ISA::APP-VIEW))
 (24 24 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (24 24 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (24 24 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (24 24 (:REWRITE SET::IN-SET))
 (15 15 (:TYPE-PRESCRIPTION ZIP))
 (15 15 (:TYPE-PRESCRIPTION IFIX))
 (15 15 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (15 15 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (15 15 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (15 15 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->REFERENCE-ADDR-OF-WRITE-WITH-MASK))
 (15 15 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (15 15 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (15 15 (:DEFINITION X86ISA::APP-VIEW$A))
 (6 6 (:REWRITE CONSP-OF-CDDDR-BY-LEN))
 )
(X86ISA::MEMBER-P-AFTER-REMOVE-DUPLICATES-EQUAL-OF-SUPERIOR-PADDRS-IN-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX
 (227 3 (:DEFINITION REMOVE-DUPLICATES-EQUAL))
 (111 3 (:DEFINITION MEMBER-EQUAL))
 (81 6 (:REWRITE SUBSETP-CAR-MEMBER))
 (45 6 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (45 6 (:REWRITE MEMBER-WHEN-ATOM))
 (20 20 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (20 20 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (20 20 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (20 20 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (20 20 (:REWRITE CONSP-BY-LEN))
 (18 2 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (15 15 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (12 12 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (12 12 (:REWRITE DEFAULT-CDR))
 (10 5 (:REWRITE X86ISA::MEMBER-P-CDR))
 (9 9 (:REWRITE DEFAULT-CAR))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX))
 (6 6 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (6 6 (:REWRITE SUBSETP-TRANS2))
 (6 6 (:REWRITE SUBSETP-TRANS))
 (6 6 (:REWRITE SUBSETP-MEMBER . 4))
 (6 6 (:REWRITE SUBSETP-MEMBER . 3))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 (6 6 (:REWRITE INTERSECTP-MEMBER . 3))
 (6 6 (:REWRITE INTERSECTP-MEMBER . 2))
 (6 6 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (5 5 (:REWRITE X86ISA::MEMBER-P-WHEN-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-THEN-MEMBER-P-ENTRIES-AUX))
 (5 5 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (3 3 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (2 2 (:TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQUAL))
 (2 2 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (2 2 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 )
(X86ISA::<=-LOGIOR
 (64 64 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 2))
 (64 64 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 1))
 (60 2 (:LINEAR LOGIOR-BOUNDS-NEG . 1))
 (3 3 (:REWRITE DEFAULT-LOGIOR-2))
 (3 3 (:REWRITE DEFAULT-LOGIOR-1))
 (2 2 (:REWRITE THE-FLOOR-BELOW))
 (2 2 (:REWRITE THE-FLOOR-ABOVE))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (2 2 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (2 2 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (2 2 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-<-CONSTANT))
 (2 2 (:REWRITE DEFAULT-LESS-THAN-2))
 (2 2 (:REWRITE DEFAULT-LESS-THAN-1))
 (2 2 (:REWRITE CONSTANT-<-INTEGERP))
 (2 2 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (2 2 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (2 2 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (2 2 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (2 2 (:REWRITE |(< c (- x))|))
 (2 2 (:REWRITE |(< 0 (/ x))|))
 (2 2 (:REWRITE |(< 0 (* x y))|))
 (2 2 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (2 2 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (2 2 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (2 2 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (2 2 (:REWRITE |(< (/ x) (/ y))|))
 (2 2 (:REWRITE |(< (- x) c)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:LINEAR LOGIOR-BOUNDS-NEG . 2))
 )
(X86ISA::PML4-TABLE-ENTRY-ADDR-IS-AT-THE-FIRST-LEVEL
 (533 1 (:REWRITE X86ISA::NOT-MEMBER-P-CREATE-QWORD-ADDRESS-LIST))
 (218 11 (:LINEAR LOGHEAD-UPPER-BOUND))
 (198 6 (:REWRITE BITOPS::ASH-<-0))
 (183 3 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-1))
 (174 15 (:REWRITE LOGHEAD-IDENTITY))
 (156 3 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-2))
 (145 14 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (77 22 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (72 34 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (69 3 (:LINEAR X86ISA::ASH-N-3-BOUND))
 (67 3 (:REWRITE ASH-0))
 (65 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (58 2 (:REWRITE ZIP-OPEN))
 (48 1 (:DEFINITION X86ISA::CREATE-QWORD-ADDRESS-LIST))
 (35 5 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (33 12 (:REWRITE DEFAULT-<-1))
 (30 15 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (29 29 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (25 3 (:REWRITE LOGTAIL-IDENTITY))
 (23 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR8BITS-P))
 (21 12 (:REWRITE DEFAULT-<-2))
 (17 17 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (17 17 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (17 1 (:REWRITE X86ISA::CR8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (15 15 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (12 4 (:REWRITE DEFAULT-+-2))
 (12 1 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-0))
 (12 1 (:REWRITE BITOPS::BASIC-UNSIGNED-BYTE-P-OF-+))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (10 10 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (9 9 (:TYPE-PRESCRIPTION NATP))
 (9 9 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (9 9 (:REWRITE X86ISA::MEMBER-P-AND-MULT-8-QWORD-PADDR-LISTP))
 (9 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-4BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (5 3 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (4 4 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (4 4 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 1 (:REWRITE X86ISA::N52P-LEFT-SHIFTING-A-40-BIT-NATP-BY-12-+-7))
 (3 3 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 (3 3 (:TYPE-PRESCRIPTION X86ISA::CR8BITS-P$INLINE))
 (3 3 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (3 3 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGIOR-FOR-NATURALS))
 (3 1 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (3 1 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (2 2 (:TYPE-PRESCRIPTION ZIP))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::4BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (2 2 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (2 2 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (2 2 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (2 2 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (2 1 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (1 1 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-3))
 (1 1 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-2))
 (1 1 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-1))
 )
(X86ISA::PML4-TABLE-ENTRY-ADDR-IS-A-MEMBER-OF-GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES
 (1595 1 (:DEFINITION REMOVE-DUPLICATES-EQUAL))
 (1008 3 (:REWRITE MEMBER-OF-APPEND))
 (697 53 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (647 11 (:REWRITE SUBSETP-CAR-MEMBER))
 (479 11 (:REWRITE SUBSETP-MEMBER . 3))
 (329 4 (:DEFINITION MEMBER-EQUAL))
 (313 6 (:REWRITE SUBSETP-OF-APPEND-WHEN-SUBSET-OF-EITHER))
 (257 257 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES))
 (257 14 (:REWRITE CONSP-OF-APPEND))
 (248 3 (:REWRITE X86ISA::CDR-APPEND-IS-APPEND-CDR))
 (237 4 (:REWRITE SUBSETP-APPEND1))
 (183 6 (:DEFINITION BINARY-APPEND))
 (173 53 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (171 38 (:TYPE-PRESCRIPTION X86ISA::CONSP-APPEND))
 (150 53 (:REWRITE SUBSETP-TRANS2))
 (128 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (112 112 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (111 12 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (109 109 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (109 109 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (109 109 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (109 109 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (109 109 (:REWRITE CONSP-BY-LEN))
 (106 106 (:TYPE-PRESCRIPTION X86ISA::GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (106 106 (:TYPE-PRESCRIPTION X86ISA::CONSP-GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (102 6 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (69 8 (:REWRITE MEMBER-WHEN-ATOM))
 (53 53 (:REWRITE SUBSETP-TRANS))
 (38 38 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (37 37 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (36 36 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (21 13 (:REWRITE DEFAULT-CDR))
 (18 12 (:REWRITE DEFAULT-CAR))
 (12 2 (:REWRITE X86ISA::CAR-OF-APPEND))
 (12 2 (:REWRITE ASH-0))
 (11 11 (:REWRITE SUBSETP-MEMBER . 4))
 (11 11 (:REWRITE SUBSETP-MEMBER . 2))
 (11 11 (:REWRITE SUBSETP-MEMBER . 1))
 (11 11 (:REWRITE INTERSECTP-MEMBER . 3))
 (11 11 (:REWRITE INTERSECTP-MEMBER . 2))
 (7 7 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (7 1 (:REWRITE ZIP-OPEN))
 (5 5 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (3 2 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (2 2 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (2 1 (:REWRITE X86ISA::MEMBER-P-CDR))
 (1 1 (:TYPE-PRESCRIPTION ZIP))
 (1 1 (:TYPE-PRESCRIPTION IFIX))
 (1 1 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (1 1 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (1 1 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (1 1 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 )
(X86ISA::PAGE-DIR-PTR-TABLE-ENTRY-ADDR-IS-AT-THE-SECOND-LEVEL
 (1822 4 (:DEFINITION REMOVE-DUPLICATES-EQUAL))
 (1034 3 (:REWRITE MEMBER-OF-APPEND))
 (821 59 (:REWRITE LOGHEAD-IDENTITY))
 (807 33 (:REWRITE ASH-0))
 (731 59 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (717 17 (:REWRITE SUBSETP-CAR-MEMBER))
 (715 47 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (708 22 (:REWRITE ZIP-OPEN))
 (554 22 (:LINEAR LOGHEAD-UPPER-BOUND))
 (501 17 (:REWRITE SUBSETP-MEMBER . 3))
 (469 3 (:REWRITE MEMBER-OF-REMOVE-DUPLICATES-EQUAL))
 (440 7 (:DEFINITION MEMBER-EQUAL))
 (416 64 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (355 33 (:REWRITE LOGTAIL-IDENTITY))
 (304 6 (:REWRITE SUBSETP-OF-APPEND-WHEN-SUBSET-OF-EITHER))
 (250 14 (:REWRITE CONSP-OF-APPEND))
 (238 74 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (238 12 (:DEFINITION BINARY-APPEND))
 (238 3 (:REWRITE X86ISA::CDR-APPEND-IS-APPEND-CDR))
 (237 4 (:REWRITE SUBSETP-APPEND1))
 (224 32 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (195 59 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (184 184 (:TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQUAL))
 (159 24 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (156 59 (:REWRITE SUBSETP-TRANS2))
 (153 153 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (153 153 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (153 153 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (153 153 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (153 153 (:REWRITE CONSP-BY-LEN))
 (134 6 (:DEFINITION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX))
 (132 38 (:TYPE-PRESCRIPTION X86ISA::CONSP-APPEND))
 (128 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (128 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (124 124 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (122 122 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (118 59 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (118 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (116 116 (:TYPE-PRESCRIPTION X86ISA::GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (116 116 (:TYPE-PRESCRIPTION X86ISA::CONSP-GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (114 14 (:REWRITE MEMBER-WHEN-ATOM))
 (110 110 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (102 6 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (99 55 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (96 96 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (92 8 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR8BITS-P))
 (75 75 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (72 10 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (68 4 (:REWRITE X86ISA::CR8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (64 64 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (62 62 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (59 59 (:REWRITE SUBSETP-TRANS))
 (58 42 (:REWRITE DEFAULT-CDR))
 (52 38 (:REWRITE DEFAULT-CAR))
 (49 33 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (44 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (38 38 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (37 37 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (36 8 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-4BITS-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))
 (26 12 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (22 22 (:TYPE-PRESCRIPTION ZIP))
 (22 11 (:REWRITE X86ISA::MEMBER-P-CDR))
 (17 17 (:TYPE-PRESCRIPTION NATP))
 (17 17 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (17 17 (:REWRITE SUBSETP-MEMBER . 4))
 (17 17 (:REWRITE SUBSETP-MEMBER . 2))
 (17 17 (:REWRITE SUBSETP-MEMBER . 1))
 (17 17 (:REWRITE INTERSECTP-MEMBER . 3))
 (17 17 (:REWRITE INTERSECTP-MEMBER . 2))
 (16 16 (:TYPE-PRESCRIPTION IFIX))
 (16 16 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (14 7 (:DEFINITION X86ISA::APP-VIEW))
 (13 13 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::CR8BITS-P$INLINE))
 (12 12 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (12 12 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (12 12 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (12 4 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (12 4 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (12 4 (:REWRITE DEFAULT-+-2))
 (12 2 (:REWRITE X86ISA::CAR-OF-APPEND))
 (11 11 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (11 11 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (11 11 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (11 11 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::4BITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (8 8 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (8 8 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (8 8 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (8 8 (:REWRITE X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-WITH-DIFFERENT-X86-ENTRIES))
 (8 4 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 (7 7 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (7 7 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (7 7 (:DEFINITION X86ISA::APP-VIEW$A))
 (6 6 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (4 4 (:REWRITE X86ISA::MEMBER-P-AND-MULT-8-QWORD-PADDR-LISTP))
 (4 4 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->REFERENCE-ADDR-OF-WRITE-WITH-MASK))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (2 2 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGIOR-FOR-NATURALS))
 (1 1 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 )
(X86ISA::PAGE-DIR-PTR-TABLE-ENTRY-ADDR-IS-A-MEMBER-OF-GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES
 (1595 1 (:DEFINITION REMOVE-DUPLICATES-EQUAL))
 (1008 3 (:REWRITE MEMBER-OF-APPEND))
 (697 53 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (647 11 (:REWRITE SUBSETP-CAR-MEMBER))
 (479 11 (:REWRITE SUBSETP-MEMBER . 3))
 (329 4 (:DEFINITION MEMBER-EQUAL))
 (313 6 (:REWRITE SUBSETP-OF-APPEND-WHEN-SUBSET-OF-EITHER))
 (257 257 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES))
 (257 14 (:REWRITE CONSP-OF-APPEND))
 (248 3 (:REWRITE X86ISA::CDR-APPEND-IS-APPEND-CDR))
 (237 4 (:REWRITE SUBSETP-APPEND1))
 (183 6 (:DEFINITION BINARY-APPEND))
 (173 53 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (171 38 (:TYPE-PRESCRIPTION X86ISA::CONSP-APPEND))
 (150 53 (:REWRITE SUBSETP-TRANS2))
 (128 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (124 6 (:REWRITE ASH-0))
 (112 112 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (111 12 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (109 109 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (109 109 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (109 109 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (109 109 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (109 109 (:REWRITE CONSP-BY-LEN))
 (107 107 (:TYPE-PRESCRIPTION X86ISA::GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (107 107 (:TYPE-PRESCRIPTION X86ISA::CONSP-GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (102 6 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (100 6 (:REWRITE ZIP-OPEN))
 (88 4 (:REWRITE LOGHEAD-IDENTITY))
 (80 4 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (69 8 (:REWRITE MEMBER-WHEN-ATOM))
 (58 2 (:LINEAR LOGHEAD-UPPER-BOUND))
 (53 53 (:REWRITE SUBSETP-TRANS))
 (52 8 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (40 40 (:TYPE-PRESCRIPTION X86ISA::N64P-RM-LOW-64))
 (40 2 (:REWRITE LOGTAIL-IDENTITY))
 (38 38 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (37 37 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (36 36 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::CR3BITS->PDB$INLINE))
 (28 4 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (24 24 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (21 13 (:REWRITE DEFAULT-CDR))
 (18 12 (:REWRITE DEFAULT-CAR))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (12 4 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (12 4 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (12 2 (:REWRITE X86ISA::CAR-OF-APPEND))
 (11 11 (:REWRITE SUBSETP-MEMBER . 4))
 (11 11 (:REWRITE SUBSETP-MEMBER . 2))
 (11 11 (:REWRITE SUBSETP-MEMBER . 1))
 (11 11 (:REWRITE INTERSECTP-MEMBER . 3))
 (11 11 (:REWRITE INTERSECTP-MEMBER . 2))
 (10 10 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (10 10 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (10 6 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (8 4 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (8 4 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (8 4 (:REWRITE IFIX-WHEN-INTEGERP))
 (8 4 (:DEFINITION X86ISA::APP-VIEW))
 (7 7 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (6 6 (:TYPE-PRESCRIPTION ZIP))
 (6 3 (:REWRITE X86ISA::MEMBER-P-CDR))
 (5 5 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (4 4 (:TYPE-PRESCRIPTION IFIX))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (4 4 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (4 4 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (4 4 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (4 4 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (4 4 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (4 4 (:DEFINITION X86ISA::APP-VIEW$A))
 (4 2 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (3 3 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (3 3 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (3 3 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (3 1 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (1 1 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 )
(X86ISA::PAGE-DIRECTORY-ENTRY-ADDR-IS-AT-THE-THIRD-LEVEL
 (7535 443 (:REWRITE LOGHEAD-IDENTITY))
 (7114 238 (:REWRITE ASH-0))
 (6705 387 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (6318 186 (:REWRITE ZIP-OPEN))
 (5016 186 (:LINEAR LOGHEAD-UPPER-BOUND))
 (4134 636 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (3340 238 (:REWRITE LOGTAIL-IDENTITY))
 (2226 318 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (1976 6 (:DEFINITION REMOVE-DUPLICATES-EQUAL))
 (1606 512 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (1272 159 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (1272 159 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (1191 53 (:DEFINITION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX))
 (1034 3 (:REWRITE MEMBER-OF-APPEND))
 (990 990 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (954 954 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (886 443 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (800 425 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (771 21 (:REWRITE SUBSETP-CAR-MEMBER))
 (764 764 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (761 63 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (708 59 (:DEFINITION BINARY-APPEND))
 (536 68 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (535 118 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (518 518 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (514 9 (:DEFINITION MEMBER-EQUAL))
 (505 21 (:REWRITE SUBSETP-MEMBER . 3))
 (469 3 (:REWRITE MEMBER-OF-REMOVE-DUPLICATES-EQUAL))
 (466 466 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (437 38 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR8BITS-P))
 (350 238 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (340 140 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (323 19 (:REWRITE X86ISA::CR8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (318 318 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (318 318 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (318 159 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (318 159 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 316 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (316 316 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (316 316 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (316 316 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (316 316 (:REWRITE CONSP-BY-LEN))
 (304 6 (:REWRITE SUBSETP-OF-APPEND-WHEN-SUBSET-OF-EITHER))
 (250 14 (:REWRITE CONSP-OF-APPEND))
 (243 173 (:REWRITE DEFAULT-CDR))
 (238 3 (:REWRITE X86ISA::CDR-APPEND-IS-APPEND-CDR))
 (237 4 (:REWRITE SUBSETP-APPEND1))
 (235 167 (:REWRITE DEFAULT-CAR))
 (215 215 (:TYPE-PRESCRIPTION X86ISA::GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (215 215 (:TYPE-PRESCRIPTION X86ISA::CONSP-GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (209 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (200 100 (:DEFINITION X86ISA::APP-VIEW))
 (199 63 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (188 188 (:TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQUAL))
 (186 186 (:TYPE-PRESCRIPTION ZIP))
 (171 38 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-4BITS-P))
 (160 63 (:REWRITE SUBSETP-TRANS2))
 (148 148 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (144 18 (:REWRITE MEMBER-WHEN-ATOM))
 (142 71 (:REWRITE X86ISA::MEMBER-P-CDR))
 (140 140 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (140 140 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (132 132 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (132 38 (:TYPE-PRESCRIPTION X86ISA::CONSP-APPEND))
 (118 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (112 112 (:TYPE-PRESCRIPTION IFIX))
 (102 6 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (100 100 (:DEFINITION X86ISA::APP-VIEW$A))
 (77 77 (:TYPE-PRESCRIPTION NATP))
 (77 77 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (76 76 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (75 75 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY))
 (71 71 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (71 71 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (71 71 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (63 63 (:REWRITE SUBSETP-TRANS))
 (61 61 (:REWRITE X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-WITH-DIFFERENT-X86-ENTRIES))
 (57 57 (:TYPE-PRESCRIPTION X86ISA::CR8BITS-P$INLINE))
 (57 57 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (57 57 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (57 19 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (57 19 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (51 51 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (48 16 (:REWRITE DEFAULT-+-2))
 (38 38 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::4BITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (38 38 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (38 38 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (38 38 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (38 19 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 (37 37 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (29 29 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (21 21 (:REWRITE SUBSETP-MEMBER . 4))
 (21 21 (:REWRITE SUBSETP-MEMBER . 2))
 (21 21 (:REWRITE SUBSETP-MEMBER . 1))
 (21 21 (:REWRITE INTERSECTP-MEMBER . 3))
 (21 21 (:REWRITE INTERSECTP-MEMBER . 2))
 (17 17 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (16 16 (:REWRITE X86ISA::MEMBER-P-AND-MULT-8-QWORD-PADDR-LISTP))
 (16 16 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->REFERENCE-ADDR-OF-WRITE-WITH-MASK))
 (16 16 (:REWRITE DEFAULT-+-1))
 (15 15 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (12 12 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (12 2 (:REWRITE X86ISA::CAR-OF-APPEND))
 (11 11 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (11 11 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (8 8 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGIOR-FOR-NATURALS))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 )
(X86ISA::PAGE-DIRECTORY-ENTRY-ADDR-IS-A-MEMBER-OF-GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES
 (1822 4 (:DEFINITION REMOVE-DUPLICATES-EQUAL))
 (1034 3 (:REWRITE MEMBER-OF-APPEND))
 (731 59 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (717 17 (:REWRITE SUBSETP-CAR-MEMBER))
 (501 17 (:REWRITE SUBSETP-MEMBER . 3))
 (469 3 (:REWRITE MEMBER-OF-REMOVE-DUPLICATES-EQUAL))
 (440 7 (:DEFINITION MEMBER-EQUAL))
 (304 6 (:REWRITE SUBSETP-OF-APPEND-WHEN-SUBSET-OF-EITHER))
 (250 14 (:REWRITE CONSP-OF-APPEND))
 (244 9 (:REWRITE ASH-0))
 (238 3 (:REWRITE X86ISA::CDR-APPEND-IS-APPEND-CDR))
 (237 4 (:REWRITE SUBSETP-APPEND1))
 (220 10 (:REWRITE LOGHEAD-IDENTITY))
 (208 9 (:REWRITE ZIP-OPEN))
 (200 10 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (195 59 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (180 180 (:TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQUAL))
 (178 6 (:DEFINITION BINARY-APPEND))
 (156 59 (:REWRITE SUBSETP-TRANS2))
 (145 5 (:LINEAR LOGHEAD-UPPER-BOUND))
 (134 134 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (134 134 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (134 134 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (134 134 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (134 134 (:REWRITE CONSP-BY-LEN))
 (132 38 (:TYPE-PRESCRIPTION X86ISA::CONSP-APPEND))
 (130 20 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (124 124 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (118 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (114 14 (:REWRITE MEMBER-WHEN-ATOM))
 (111 12 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (105 105 (:TYPE-PRESCRIPTION X86ISA::GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (105 105 (:TYPE-PRESCRIPTION X86ISA::CONSP-GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (102 6 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (100 100 (:TYPE-PRESCRIPTION X86ISA::N64P-RM-LOW-64))
 (100 5 (:REWRITE LOGTAIL-IDENTITY))
 (70 10 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (69 69 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX))
 (60 60 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (59 59 (:REWRITE SUBSETP-TRANS))
 (51 51 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (50 50 (:TYPE-PRESCRIPTION LOGHEAD-TYPE))
 (40 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (40 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (38 38 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (37 37 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (33 25 (:REWRITE DEFAULT-CDR))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::CR3BITS->PDB$INLINE))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (30 10 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (30 4 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (27 21 (:REWRITE DEFAULT-CAR))
 (25 25 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (21 7 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (20 10 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (20 10 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (20 10 (:REWRITE IFIX-WHEN-INTEGERP))
 (19 19 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (17 17 (:REWRITE SUBSETP-MEMBER . 4))
 (17 17 (:REWRITE SUBSETP-MEMBER . 2))
 (17 17 (:REWRITE SUBSETP-MEMBER . 1))
 (17 17 (:REWRITE INTERSECTP-MEMBER . 3))
 (17 17 (:REWRITE INTERSECTP-MEMBER . 2))
 (15 9 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (14 7 (:REWRITE X86ISA::MEMBER-P-CDR))
 (14 7 (:DEFINITION X86ISA::APP-VIEW))
 (12 2 (:REWRITE X86ISA::CAR-OF-APPEND))
 (11 11 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (10 10 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (10 10 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (10 10 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (10 5 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (10 5 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (9 9 (:TYPE-PRESCRIPTION ZIP))
 (7 7 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (7 7 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (7 7 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (7 7 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (7 7 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (7 7 (:DEFINITION X86ISA::APP-VIEW$A))
 (6 6 (:TYPE-PRESCRIPTION IFIX))
 (4 4 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (3 3 (:REWRITE X86ISA::MEMBER-P-WHEN-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-THEN-MEMBER-P-ENTRIES-AUX))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 )
(X86ISA::PAGE-TABLE-ENTRY-ADDR-IS-AT-THE-FOURTH-LEVEL
 (2554 166 (:REWRITE LOGHEAD-IDENTITY))
 (2449 85 (:REWRITE ASH-0))
 (2245 143 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (2166 66 (:REWRITE ZIP-OPEN))
 (1899 5 (:DEFINITION REMOVE-DUPLICATES-EQUAL))
 (1704 66 (:LINEAR LOGHEAD-UPPER-BOUND))
 (1326 204 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (1267 56 (:DEFINITION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX))
 (1249 85 (:REWRITE LOGTAIL-IDENTITY))
 (1034 3 (:REWRITE MEMBER-OF-APPEND))
 (746 61 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (744 19 (:REWRITE SUBSETP-CAR-MEMBER))
 (738 62 (:DEFINITION BINARY-APPEND))
 (715 223 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (714 102 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (559 124 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (503 19 (:REWRITE SUBSETP-MEMBER . 3))
 (483 66 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (483 66 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (477 8 (:DEFINITION MEMBER-EQUAL))
 (469 3 (:REWRITE MEMBER-OF-REMOVE-DUPLICATES-EQUAL))
 (390 390 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (352 44 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (345 30 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR8BITS-P))
 (332 166 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (320 173 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (306 306 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (304 6 (:REWRITE SUBSETP-OF-APPEND-WHEN-SUBSET-OF-EITHER))
 (297 297 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (290 290 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (290 290 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (290 290 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (290 290 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (290 290 (:REWRITE CONSP-BY-LEN))
 (255 15 (:REWRITE X86ISA::CR8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (250 14 (:REWRITE CONSP-OF-APPEND))
 (238 3 (:REWRITE X86ISA::CDR-APPEND-IS-APPEND-CDR))
 (237 4 (:REWRITE SUBSETP-APPEND1))
 (217 163 (:REWRITE DEFAULT-CDR))
 (210 158 (:REWRITE DEFAULT-CAR))
 (204 204 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (197 61 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (186 186 (:TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQUAL))
 (185 185 (:TYPE-PRESCRIPTION X86ISA::GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (185 185 (:TYPE-PRESCRIPTION X86ISA::CONSP-GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (185 185 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (165 15 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (159 65 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (158 61 (:REWRITE SUBSETP-TRANS2))
 (137 85 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (135 30 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-4BITS-P))
 (134 134 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (132 132 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (132 132 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (132 66 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (132 66 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (132 38 (:TYPE-PRESCRIPTION X86ISA::CONSP-APPEND))
 (129 16 (:REWRITE MEMBER-WHEN-ATOM))
 (128 128 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (118 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (102 6 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (94 47 (:REWRITE X86ISA::MEMBER-P-CDR))
 (94 47 (:DEFINITION X86ISA::APP-VIEW))
 (66 66 (:TYPE-PRESCRIPTION ZIP))
 (65 65 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (65 65 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (61 61 (:REWRITE SUBSETP-TRANS))
 (60 60 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (60 60 (:REWRITE X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-WITH-DIFFERENT-X86-ENTRIES))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY))
 (52 52 (:TYPE-PRESCRIPTION IFIX))
 (49 49 (:TYPE-PRESCRIPTION NATP))
 (49 49 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (47 47 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (47 47 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (47 47 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (47 47 (:DEFINITION X86ISA::APP-VIEW$A))
 (45 45 (:TYPE-PRESCRIPTION X86ISA::CR8BITS-P$INLINE))
 (45 45 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (45 15 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (45 15 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (40 40 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (38 38 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (37 37 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::4BITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (30 30 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (30 30 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (30 30 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (30 15 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 15 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 (24 8 (:REWRITE DEFAULT-+-2))
 (19 19 (:REWRITE SUBSETP-MEMBER . 4))
 (19 19 (:REWRITE SUBSETP-MEMBER . 2))
 (19 19 (:REWRITE SUBSETP-MEMBER . 1))
 (19 19 (:REWRITE INTERSECTP-MEMBER . 3))
 (19 19 (:REWRITE INTERSECTP-MEMBER . 2))
 (18 18 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (16 16 (:REWRITE X86ISA::MEMBER-P-AND-MULT-8-QWORD-PADDR-LISTP))
 (15 15 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (13 13 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (12 2 (:REWRITE X86ISA::CAR-OF-APPEND))
 (11 11 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (8 8 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->REFERENCE-ADDR-OF-WRITE-WITH-MASK))
 (8 8 (:REWRITE DEFAULT-+-1))
 (7 7 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (7 7 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (7 7 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 (4 4 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGIOR-FOR-NATURALS))
 )
(X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-SUBSETP-EQUAL-ENTRIES-AUX
 (160 15 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (104 17 (:REWRITE SUBSETP-TRANS))
 (103 15 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (88 8 (:DEFINITION BINARY-APPEND))
 (80 16 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (69 69 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX))
 (64 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (58 58 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (58 58 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (58 58 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (58 58 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (58 58 (:REWRITE CONSP-BY-LEN))
 (35 11 (:REWRITE SUBSETP-MEMBER . 3))
 (31 31 (:REWRITE DEFAULT-CAR))
 (27 2 (:REWRITE SUBSETP-CAR-MEMBER))
 (25 25 (:REWRITE X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-WITH-DIFFERENT-X86-ENTRIES))
 (24 12 (:TYPE-PRESCRIPTION X86ISA::CONSP-APPEND))
 (22 22 (:REWRITE DEFAULT-CDR))
 (18 18 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (11 11 (:REWRITE SUBSETP-MEMBER . 4))
 (11 11 (:REWRITE SUBSETP-MEMBER . 2))
 (11 11 (:REWRITE SUBSETP-MEMBER . 1))
 (11 11 (:REWRITE INTERSECTP-MEMBER . 3))
 (11 11 (:REWRITE INTERSECTP-MEMBER . 2))
 (2 2 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 )
(X86ISA::SUBSETP-EQUAL-AND-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX-1
 (840 38 (:DEFINITION MEMBER-EQUAL))
 (419 36 (:REWRITE SUBSETP-CAR-MEMBER))
 (351 57 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (275 40 (:REWRITE MEMBER-WHEN-ATOM))
 (223 75 (:REWRITE SUBSETP-MEMBER . 2))
 (218 60 (:REWRITE SUBSETP-TRANS))
 (193 193 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (193 193 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (193 193 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (193 193 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (193 193 (:REWRITE CONSP-BY-LEN))
 (169 169 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX))
 (158 13 (:DEFINITION BINARY-APPEND))
 (138 26 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (123 10 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (112 26 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (89 89 (:REWRITE DEFAULT-CAR))
 (77 77 (:REWRITE DEFAULT-CDR))
 (75 75 (:REWRITE SUBSETP-MEMBER . 1))
 (59 59 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (40 40 (:REWRITE SUBSETP-MEMBER . 4))
 (40 40 (:REWRITE SUBSETP-MEMBER . 3))
 (40 40 (:REWRITE INTERSECTP-MEMBER . 3))
 (40 40 (:REWRITE INTERSECTP-MEMBER . 2))
 (18 18 (:REWRITE X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-WITH-DIFFERENT-X86-ENTRIES))
 )
(X86ISA::SUBSETP-EQUAL-AND-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX-2
 (5981 657 (:REWRITE SUBSETP-TRANS))
 (4802 324 (:REWRITE SUBSETP-CAR-MEMBER))
 (4475 170 (:DEFINITION MEMBER-EQUAL))
 (3647 639 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (3070 163 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1307 7 (:REWRITE MEMBER-OF-APPEND))
 (1070 1070 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX))
 (999 999 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (999 999 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (999 999 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (999 999 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (999 999 (:REWRITE CONSP-BY-LEN))
 (785 366 (:REWRITE SUBSETP-MEMBER . 2))
 (496 31 (:REWRITE CONSP-OF-APPEND))
 (479 30 (:DEFINITION BINARY-APPEND))
 (476 56 (:REWRITE SUBSETP-MEMBER . 3))
 (368 115 (:TYPE-PRESCRIPTION X86ISA::CONSP-APPEND))
 (366 366 (:REWRITE SUBSETP-MEMBER . 1))
 (356 356 (:REWRITE DEFAULT-CAR))
 (356 60 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (341 341 (:REWRITE DEFAULT-CDR))
 (328 60 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (307 42 (:REWRITE MEMBER-WHEN-ATOM))
 (303 303 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (115 115 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (77 77 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (56 56 (:REWRITE SUBSETP-MEMBER . 4))
 (56 56 (:REWRITE INTERSECTP-MEMBER . 3))
 (56 56 (:REWRITE INTERSECTP-MEMBER . 2))
 (36 36 (:REWRITE X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-WITH-DIFFERENT-X86-ENTRIES))
 (16 16 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 )
(X86ISA::SET-EQUIV-AND-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX-HELPER
 (275 2 (:REWRITE SUBSETP-OF-APPEND-WHEN-SUBSET-OF-EITHER))
 (185 29 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (148 29 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (146 29 (:REWRITE SUBSETP-MEMBER . 2))
 (78 3 (:DEFINITION BINARY-APPEND))
 (70 70 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (70 70 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (70 70 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (70 70 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (70 70 (:REWRITE CONSP-BY-LEN))
 (62 2 (:REWRITE SUBSETP-CONS-2))
 (58 58 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX))
 (54 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (48 6 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (35 5 (:REWRITE SUBSETP-MEMBER . 4))
 (34 34 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY))
 (16 1 (:REWRITE CONSP-OF-APPEND))
 (15 15 (:REWRITE DEFAULT-CDR))
 (15 15 (:REWRITE DEFAULT-CAR))
 (13 2 (:REWRITE MEMBER-WHEN-ATOM))
 (8 8 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (8 2 (:TYPE-PRESCRIPTION X86ISA::CONSP-APPEND))
 (5 5 (:REWRITE SUBSETP-MEMBER . 3))
 (5 5 (:REWRITE INTERSECTP-MEMBER . 3))
 (5 5 (:REWRITE INTERSECTP-MEMBER . 2))
 (3 3 (:REWRITE X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-WITH-DIFFERENT-X86-ENTRIES))
 (2 2 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (2 2 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (1 1 (:REWRITE MEMBER-OF-CONS))
 )
(X86ISA::SET-EQUIV-AND-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX-CONG
 (355 31 (:DEFINITION BINARY-APPEND))
 (286 62 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (264 62 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (94 94 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX))
 (86 86 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (86 86 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (86 86 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (86 86 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (86 86 (:REWRITE CONSP-BY-LEN))
 (70 70 (:REWRITE DEFAULT-CAR))
 (69 69 (:REWRITE DEFAULT-CDR))
 (44 44 (:REWRITE X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-WITH-DIFFERENT-X86-ENTRIES))
 (35 35 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (1 1 (:REWRITE SUBSETP-TRANS2))
 (1 1 (:REWRITE SUBSETP-TRANS))
 )
(X86ISA::SET-EQUIV-IMPLIES-IFF-MEMBER-P-2-CONG)
(X86ISA::MEMBER-P-AFTER-REMOVE-DUPLICATES-EQUAL-OF-SUPERIOR-PADDRS-IN-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX-NEW)
(X86ISA::PAGE-TABLE-ENTRY-ADDR-IS-A-MEMBER-OF-GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES
 (1121 36 (:REWRITE ASH-0))
 (1100 50 (:REWRITE LOGHEAD-IDENTITY))
 (1000 50 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (977 36 (:REWRITE ZIP-OPEN))
 (725 25 (:LINEAR LOGHEAD-UPPER-BOUND))
 (650 100 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (500 500 (:TYPE-PRESCRIPTION X86ISA::N64P-RM-LOW-64))
 (500 25 (:REWRITE LOGTAIL-IDENTITY))
 (350 50 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (300 300 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (231 3 (:DEFINITION REMOVE-DUPLICATES-EQUAL))
 (200 25 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (200 25 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (150 150 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (150 50 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (125 125 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (118 18 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (116 40 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (111 3 (:DEFINITION MEMBER-EQUAL))
 (100 50 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (100 50 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (100 50 (:REWRITE IFIX-WHEN-INTEGERP))
 (88 88 (:TYPE-PRESCRIPTION X86ISA::CR3BITS->PDB$INLINE))
 (86 86 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (81 6 (:REWRITE SUBSETP-CAR-MEMBER))
 (76 38 (:DEFINITION X86ISA::APP-VIEW))
 (62 36 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (56 3 (:DEFINITION BINARY-APPEND))
 (50 50 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (50 50 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (50 50 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (50 50 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (50 25 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (50 25 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 6 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (45 6 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (45 6 (:REWRITE MEMBER-WHEN-ATOM))
 (42 42 (:TYPE-PRESCRIPTION X86ISA::GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX))
 (42 21 (:REWRITE X86ISA::MEMBER-P-CDR))
 (40 40 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (40 40 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (38 38 (:DEFINITION X86ISA::APP-VIEW$A))
 (37 37 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (37 37 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (37 37 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (37 37 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (37 37 (:REWRITE CONSP-BY-LEN))
 (36 36 (:TYPE-PRESCRIPTION ZIP))
 (33 33 (:REWRITE X86ISA::SET-EQUIV-AND-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-ENTRIES-AUX-HELPER))
 (26 26 (:TYPE-PRESCRIPTION IFIX))
 (21 21 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (21 21 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (21 21 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (18 18 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (17 15 (:REWRITE DEFAULT-CDR))
 (16 16 (:REWRITE X86ISA::MEMBER-P-WHEN-GATHER-QWORD-ADDRESSES-CORRESPONDING-TO-1-ENTRY-THEN-MEMBER-P-ENTRIES-AUX))
 (15 15 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (14 12 (:REWRITE DEFAULT-CAR))
 (12 12 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (11 11 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (10 10 (:TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQUAL))
 (9 9 (:TYPE-PRESCRIPTION X86ISA::GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (9 9 (:TYPE-PRESCRIPTION X86ISA::CONSP-GATHER-PML4-TABLE-QWORD-ADDRESSES))
 (6 6 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (6 6 (:REWRITE SUBSETP-TRANS2))
 (6 6 (:REWRITE SUBSETP-TRANS))
 (6 6 (:REWRITE SUBSETP-MEMBER . 4))
 (6 6 (:REWRITE SUBSETP-MEMBER . 3))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 (6 6 (:REWRITE INTERSECTP-MEMBER . 3))
 (6 6 (:REWRITE INTERSECTP-MEMBER . 2))
 (6 6 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (4 4 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (4 4 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (4 4 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (4 4 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (3 3 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (3 3 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 )
(X86ISA::PML4-TABLE-ENTRY-ADDRESSES-SUBSET-OF-OPEN-QWORD-PADDR-LIST-GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES
 (107 1 (:DEFINITION X86ISA::OPEN-QWORD-PADDR-LIST))
 (61 7 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (61 5 (:REWRITE IFIX-WHEN-INTEGERP))
 (54 1 (:DEFINITION BINARY-APPEND))
 (52 2 (:DEFINITION X86ISA::ADDR-RANGE))
 (42 2 (:DEFINITION INTEGER-LISTP))
 (33 1 (:REWRITE X86ISA::CAR-ADDR-RANGE))
 (16 16 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (16 4 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (16 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (13 5 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (12 2 (:REWRITE ASH-0))
 (7 1 (:REWRITE ZIP-OPEN))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::TRUE-LISTP-ADDR-RANGE))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CONSP-ADDR-RANGE))
 (6 4 (:REWRITE DEFAULT-CDR))
 (5 5 (:TYPE-PRESCRIPTION X86ISA::NATP-PML4-TABLE-ENTRY-ADDR))
 (4 4 (:REWRITE X86ISA::NEG-ADDR-RANGE=NIL))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (4 4 (:REWRITE CONSP-BY-LEN))
 (4 2 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (4 2 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (3 2 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (2 2 (:TYPE-PRESCRIPTION IFIX))
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (2 1 (:REWRITE X86ISA::CDR-ADDR-RANGE))
 (1 1 (:TYPE-PRESCRIPTION ZIP))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (1 1 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 )
(X86ISA::PAGE-DIR-PTR-TABLE-ENTRY-ADDRESSES-SUBSET-OF-OPEN-QWORD-PADDR-LIST-GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES
 (124 6 (:REWRITE ASH-0))
 (107 1 (:DEFINITION X86ISA::OPEN-QWORD-PADDR-LIST))
 (100 6 (:REWRITE ZIP-OPEN))
 (88 4 (:REWRITE LOGHEAD-IDENTITY))
 (80 4 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (69 9 (:REWRITE IFIX-WHEN-INTEGERP))
 (61 7 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (58 2 (:LINEAR LOGHEAD-UPPER-BOUND))
 (54 1 (:DEFINITION BINARY-APPEND))
 (52 8 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (52 2 (:DEFINITION X86ISA::ADDR-RANGE))
 (42 2 (:DEFINITION INTEGER-LISTP))
 (40 40 (:TYPE-PRESCRIPTION X86ISA::N64P-RM-LOW-64))
 (40 2 (:REWRITE LOGTAIL-IDENTITY))
 (33 1 (:REWRITE X86ISA::CAR-ADDR-RANGE))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::CR3BITS->PDB$INLINE))
 (28 4 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (24 24 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (21 9 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (16 16 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (16 4 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (16 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (12 4 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (12 4 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (10 10 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (10 10 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (10 6 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (8 4 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (8 4 (:DEFINITION X86ISA::APP-VIEW))
 (6 6 (:TYPE-PRESCRIPTION ZIP))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::TRUE-LISTP-ADDR-RANGE))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CONSP-ADDR-RANGE))
 (6 4 (:REWRITE DEFAULT-CDR))
 (5 5 (:TYPE-PRESCRIPTION X86ISA::NATP-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (5 5 (:TYPE-PRESCRIPTION IFIX))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (4 4 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (4 4 (:REWRITE X86ISA::NEG-ADDR-RANGE=NIL))
 (4 4 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (4 4 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (4 4 (:REWRITE CONSP-BY-LEN))
 (4 4 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (4 4 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (4 4 (:DEFINITION X86ISA::APP-VIEW$A))
 (4 2 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (4 2 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE DEFAULT-+-2))
 (4 2 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (3 3 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 1 (:REWRITE X86ISA::CDR-ADDR-RANGE))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (1 1 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 )
(X86ISA::PAGE-DIRECTORY-ENTRY-ADDRESSES-SUBSET-OF-OPEN-QWORD-PADDR-LIST-GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES
 (296 12 (:REWRITE ASH-0))
 (264 12 (:REWRITE LOGHEAD-IDENTITY))
 (251 11 (:REWRITE ZIP-OPEN))
 (240 12 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (174 6 (:LINEAR LOGHEAD-UPPER-BOUND))
 (156 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (120 120 (:TYPE-PRESCRIPTION X86ISA::N64P-RM-LOW-64))
 (120 6 (:REWRITE LOGTAIL-IDENTITY))
 (107 1 (:DEFINITION X86ISA::OPEN-QWORD-PADDR-LIST))
 (85 17 (:REWRITE IFIX-WHEN-INTEGERP))
 (84 12 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (72 72 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (61 7 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (54 1 (:DEFINITION BINARY-APPEND))
 (52 2 (:DEFINITION X86ISA::ADDR-RANGE))
 (48 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (48 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (42 2 (:DEFINITION INTEGER-LISTP))
 (40 40 (:TYPE-PRESCRIPTION X86ISA::CR3BITS->PDB$INLINE))
 (37 17 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (36 36 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (36 12 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (33 1 (:REWRITE X86ISA::CAR-ADDR-RANGE))
 (30 30 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (26 10 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (24 24 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (24 12 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (19 12 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (16 16 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (16 8 (:DEFINITION X86ISA::APP-VIEW))
 (16 4 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (16 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (12 12 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (12 12 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (12 6 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (11 11 (:TYPE-PRESCRIPTION ZIP))
 (10 10 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (10 10 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (8 8 (:TYPE-PRESCRIPTION IFIX))
 (8 8 (:DEFINITION X86ISA::APP-VIEW$A))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::TRUE-LISTP-ADDR-RANGE))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CONSP-ADDR-RANGE))
 (6 6 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (6 4 (:REWRITE DEFAULT-CDR))
 (5 5 (:TYPE-PRESCRIPTION X86ISA::NATP-PAGE-DIRECTORY-ENTRY-ADDR))
 (4 4 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (4 4 (:REWRITE X86ISA::NEG-ADDR-RANGE=NIL))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (4 4 (:REWRITE CONSP-BY-LEN))
 (4 2 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (4 2 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 1 (:REWRITE X86ISA::CDR-ADDR-RANGE))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (1 1 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 )
(X86ISA::PAGE-TABLE-ENTRY-ADDRESSES-SUBSET-OF-OPEN-QWORD-PADDR-LIST-GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES
 (548 20 (:REWRITE ASH-0))
 (528 24 (:REWRITE LOGHEAD-IDENTITY))
 (480 24 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (474 18 (:REWRITE ZIP-OPEN))
 (348 12 (:LINEAR LOGHEAD-UPPER-BOUND))
 (312 48 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (240 240 (:TYPE-PRESCRIPTION X86ISA::N64P-RM-LOW-64))
 (240 12 (:REWRITE LOGTAIL-IDENTITY))
 (168 24 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (144 144 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (109 29 (:REWRITE IFIX-WHEN-INTEGERP))
 (107 1 (:DEFINITION X86ISA::OPEN-QWORD-PADDR-LIST))
 (96 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (96 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (72 72 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (72 24 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (61 29 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (61 7 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (60 60 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (54 1 (:DEFINITION BINARY-APPEND))
 (52 2 (:DEFINITION X86ISA::ADDR-RANGE))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::CR3BITS->PDB$INLINE))
 (48 24 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (44 44 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (44 18 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (42 2 (:DEFINITION INTEGER-LISTP))
 (33 1 (:REWRITE X86ISA::CAR-ADDR-RANGE))
 (31 20 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (26 13 (:DEFINITION X86ISA::APP-VIEW))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (24 24 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (24 24 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (24 12 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (18 18 (:TYPE-PRESCRIPTION ZIP))
 (18 18 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (18 18 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (16 16 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (16 4 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (16 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (13 13 (:DEFINITION X86ISA::APP-VIEW$A))
 (12 12 (:TYPE-PRESCRIPTION IFIX))
 (8 8 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::TRUE-LISTP-ADDR-RANGE))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CONSP-ADDR-RANGE))
 (6 6 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (6 4 (:REWRITE DEFAULT-CDR))
 (5 5 (:TYPE-PRESCRIPTION X86ISA::NATP-PAGE-TABLE-ENTRY-ADDR))
 (4 4 (:REWRITE X86ISA::NEG-ADDR-RANGE=NIL))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (4 4 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (4 4 (:REWRITE CONSP-BY-LEN))
 (4 2 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (4 2 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 1 (:REWRITE X86ISA::CDR-ADDR-RANGE))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (1 1 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 )