(X86ISA::MULTIPLE-OF-8-DISJOINT-WITH-ADDR-RANGE-AND-OPEN-QWORD-PADDR-LIST-TO-MEMBER-P
 (2123 69 (:REWRITE DEFAULT-+-2))
 (2085 41 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (2072 41 (:REWRITE ACL2-NUMBERP-OF-CAR-WHEN-ACL2-NUMBER-LISTP))
 (2044 148 (:REWRITE RATIONALP-OF-CAR-WHEN-RATIONAL-LISTP))
 (2024 22 (:DEFINITION ACL2-NUMBER-LISTP))
 (1871 82 (:DEFINITION RATIONAL-LISTP))
 (1764 161 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (1534 72 (:DEFINITION INTEGER-LISTP))
 (1216 2 (:REWRITE X86ISA::NOT-MEMBER-P-ADDR-RANGE))
 (1043 47 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (777 178 (:REWRITE RATIONAL-LISTP-WHEN-NOT-CONSP))
 (668 144 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (607 9 (:REWRITE DEFAULT-<-2))
 (583 123 (:REWRITE RATIONAL-LISTP-OF-CDR-WHEN-RATIONAL-LISTP))
 (482 27 (:DEFINITION X86ISA::ADDR-RANGE))
 (473 37 (:REWRITE LOGHEAD-IDENTITY))
 (400 7 (:DEFINITION BINARY-APPEND))
 (326 98 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (317 317 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (317 317 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (317 317 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (317 317 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (317 317 (:REWRITE CONSP-BY-LEN))
 (295 277 (:REWRITE DEFAULT-CDR))
 (284 284 (:REWRITE DEFAULT-CAR))
 (280 56 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (277 277 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (265 18 (:REWRITE X86ISA::CDR-ADDR-RANGE))
 (250 58 (:REWRITE UNSIGNED-BYTE-P-OF-CAR-WHEN-UNSIGNED-BYTE-LISTP))
 (225 31 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (221 44 (:REWRITE ACL2-NUMBER-LISTP-WHEN-NOT-CONSP))
 (196 28 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (185 37 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-3BITS-P))
 (175 4 (:REWRITE X86ISA::DISJOINT-P-TWO-ADDR-RANGES-THM-1))
 (145 31 (:REWRITE ACL2-NUMBER-LISTP-OF-CDR-WHEN-ACL2-NUMBER-LISTP))
 (112 112 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (112 14 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (109 19 (:REWRITE BITOPS::BASIC-UNSIGNED-BYTE-P-OF-+))
 (103 73 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (96 96 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-LISTP))
 (84 84 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (77 77 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (74 74 (:TYPE-PRESCRIPTION X86ISA::3BITS-P))
 (74 37 (:REWRITE X86ISA::3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (69 69 (:REWRITE DEFAULT-+-1))
 (65 5 (:REWRITE X86ISA::OPEN-QWORD-PADDR-LIST-AND-SUBSET-P))
 (63 9 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-0))
 (54 54 (:REWRITE X86ISA::NEG-ADDR-RANGE=NIL))
 (48 48 (:REWRITE UNSIGNED-BYTE-LISTP-WHEN-TAKE-AND-NTHCDR))
 (48 48 (:REWRITE UNSIGNED-BYTE-LISTP-WHEN-NOT-CONSP))
 (41 41 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (35 35 (:TYPE-PRESCRIPTION X86ISA::OPEN-QWORD-PADDR-LIST))
 (33 33 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (33 33 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (33 11 (:REWRITE FOLD-CONSTS-IN-+))
 (32 1 (:REWRITE X86ISA::SUBSET-P-OF-APPEND-1))
 (29 29 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (29 29 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (23 23 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P-PHYSICAL-ADDRESS-LISTP))
 (23 23 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 (12 6 (:REWRITE X86ISA::SUBSET-P-CDR-Y))
 (11 11 (:TYPE-PRESCRIPTION IFIX))
 (9 9 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-3))
 (9 9 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-2))
 (9 9 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-1))
 (9 9 (:REWRITE DEFAULT-<-1))
 (8 2 (:REWRITE IFIX-EQUAL-TO-NONZERO))
 (7 4 (:REWRITE X86ISA::NOT-DISJOINT-P-TWO-ADDR-RANGES-THM))
 (7 4 (:REWRITE X86ISA::DISJOINT-P-TWO-ADDR-RANGES-THM-0))
 (6 2 (:REWRITE X86ISA::MEMBER-P-ADDR-RANGE))
 (5 1 (:REWRITE NATP-OF-CAR-WHEN-NAT-LISTP))
 (4 4 (:TYPE-PRESCRIPTION ZIP))
 (4 4 (:REWRITE X86ISA::DISJOINT-P-TWO-ADDR-RANGES-THM-3))
 (4 4 (:REWRITE X86ISA::DISJOINT-P-TWO-ADDR-RANGES-THM-2))
 (3 1 (:REWRITE NATP-WHEN-INTEGERP))
 (3 1 (:REWRITE NATP-WHEN-GTE-0))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE ZIP-OPEN))
 (2 2 (:REWRITE X86ISA::NOT-MEMBER-P-ADDR-RANGE-FROM-NOT-MEMBER-P-ADDR-RANGE))
 (2 2 (:REWRITE X86ISA::MEMBER-P-ADDR-RANGE-FROM-MEMBER-P-ADDR-RANGE))
 (2 2 (:REWRITE IFIX-EQUAL-TO-NONZERO-CONST))
 (1 1 (:REWRITE NAT-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (1 1 (:REWRITE NAT-LISTP-WHEN-NOT-CONSP))
 (1 1 (:INDUCTION BITOPS::UNSIGNED-BYTE-P-INDUCT))
 )
(X86ISA::PAGE-PRESENT=0-AND-PAGING-ENTRY-NO-PAGE-FAULT-P
 (138 4 (:REWRITE LOGHEAD-IDENTITY))
 (18 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (18 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (18 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (18 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (18 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (18 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (18 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (18 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (13 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (11 8 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (6 3 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 2 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (5 5 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (5 5 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (5 1 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (4 2 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 1 (:LINEAR LOGHEAD-UPPER-BOUND))
 (3 3 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (2 2 (:TYPE-PRESCRIPTION BITP))
 (2 1 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (1 1 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (1 1 (:REWRITE IFIX-WHEN-INTEGERP))
 (1 1 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->P-OF-WRITE-WITH-MASK))
 )
(X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES-PAGING-ENTRY-NO-PAGE-FAULT-P
 (316 5 (:REWRITE LOGHEAD-IDENTITY))
 (244 4 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (207 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (192 3 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (74 74 (:TYPE-PRESCRIPTION IFIX))
 (54 54 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (24 24 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (23 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (23 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (23 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (23 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (23 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (23 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (23 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (23 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (23 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (23 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (23 5 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (21 7 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (18 6 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (18 6 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (18 2 (:REWRITE LOGTAIL-IDENTITY))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-13BITS-P))
 (9 9 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (8 4 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (7 7 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (6 6 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (6 6 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (6 6 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (6 6 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (6 3 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE DEFAULT-<-1))
 (6 3 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 2 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::13BITS-P))
 (4 4 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (4 4 (:REWRITE IFIX-WHEN-INTEGERP))
 (4 2 (:REWRITE X86ISA::13BITS-P-WHEN-UNSIGNED-BYTE-P))
 (3 3 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 )
(X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-PAGING-ENTRY-NO-PAGE-FAULT-P
 (120663 534 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-REFLEXIVE))
 (119327 401 (:DEFINITION X86ISA::QWORD-PADDR-LISTP))
 (96952 268 (:DEFINITION X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES))
 (63078 1203 (:DEFINITION X86ISA::PHYSICAL-ADDRESS-P$INLINE))
 (47963 2185 (:REWRITE LOGHEAD-IDENTITY))
 (45957 401 (:REWRITE DEFAULT-+-2))
 (45835 802 (:REWRITE X86ISA::ADDING-7-TO-BASE-ADDR-LEMMA))
 (32481 1488 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (31661 1069 (:REWRITE ACL2-NUMBERP-OF-CAR-WHEN-ACL2-NUMBER-LISTP))
 (30993 2672 (:REWRITE RATIONALP-OF-CAR-WHEN-RATIONAL-LISTP))
 (29900 2313 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (28989 668 (:DEFINITION ACL2-NUMBER-LISTP))
 (26988 2138 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (24581 1603 (:DEFINITION RATIONAL-LISTP))
 (21644 1336 (:DEFINITION INTEGER-LISTP))
 (12950 1082 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (12289 12289 (:TYPE-PRESCRIPTION RATIONAL-LISTP))
 (11750 2137 (:REWRITE RATIONAL-LISTP-OF-CDR-WHEN-RATIONAL-LISTP))
 (11216 1870 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (10420 10420 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (9880 935 (:REWRITE ACL2-NUMBER-LISTP-OF-CDR-WHEN-ACL2-NUMBER-LISTP))
 (9086 3740 (:REWRITE RATIONAL-LISTP-WHEN-NOT-CONSP))
 (8552 3206 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (8421 2005 (:REWRITE UNSIGNED-BYTE-P-OF-CAR-WHEN-UNSIGNED-BYTE-LISTP))
 (8421 1604 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (6015 802 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (5210 5210 (:TYPE-PRESCRIPTION ACL2-NUMBER-LISTP))
 (4945 4945 (:REWRITE DEFAULT-CAR))
 (4660 4660 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (4544 4544 (:REWRITE DEFAULT-CDR))
 (4411 802 (:REWRITE BITOPS::BASIC-UNSIGNED-BYTE-P-OF-+))
 (4276 1603 (:REWRITE ACL2-NUMBER-LISTP-WHEN-NOT-CONSP))
 (4010 802 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-3BITS-P))
 (3840 640 (:REWRITE IFIX-NEGATIVE-TO-NEGP))
 (3840 320 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (3840 320 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (3208 3208 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-LISTP))
 (2970 1082 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (2807 401 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-0))
 (2760 552 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (2760 552 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (2674 2674 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (2674 2674 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (2674 2674 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (2674 2674 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (2674 2674 (:REWRITE CONSP-BY-LEN))
 (2406 2406 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (2277 669 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES))
 (2272 2272 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (2152 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (2005 2005 (:TYPE-PRESCRIPTION X86ISA::QWORD-PADDR-LISTP))
 (2005 2005 (:REWRITE X86ISA::MEMBER-P-AND-MULT-8-QWORD-PADDR-LISTP))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (1920 640 (:REWRITE NEGP-WHEN-LESS-THAN-0))
 (1840 368 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (1608 1608 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (1604 1604 (:TYPE-PRESCRIPTION X86ISA::3BITS-P))
 (1604 1604 (:REWRITE UNSIGNED-BYTE-LISTP-WHEN-TAKE-AND-NTHCDR))
 (1604 1604 (:REWRITE UNSIGNED-BYTE-LISTP-WHEN-NOT-CONSP))
 (1604 802 (:REWRITE X86ISA::3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1478 1059 (:REWRITE DEFAULT-<-1))
 (1397 941 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (1335 1335 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (1289 1289 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1280 320 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (1197 1197 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1104 1104 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (1104 1104 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (1104 552 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1104 552 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1082 1082 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (1082 1082 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (1082 1082 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (1074 536 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (1059 1059 (:REWRITE DEFAULT-<-2))
 (970 392 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (786 786 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (784 392 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (736 736 (:TYPE-PRESCRIPTION BITP))
 (736 368 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (640 640 (:TYPE-PRESCRIPTION NEGP))
 (640 640 (:REWRITE NEGP-WHEN-INTEGERP))
 (603 67 (:REWRITE LOGTAIL-IDENTITY))
 (589 73 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (538 269 (:DEFINITION X86ISA::APP-VIEW))
 (536 536 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-TRANSITIVE))
 (536 536 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (536 536 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (401 401 (:TYPE-PRESCRIPTION X86ISA::PHYSICAL-ADDRESS-P$INLINE))
 (401 401 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P-PHYSICAL-ADDRESS-LISTP))
 (401 401 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 (401 401 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-3))
 (401 401 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-2))
 (401 401 (:REWRITE X86ISA::PHYSICAL-ADDRESS-P-LIMITS-THM-1))
 (401 401 (:REWRITE DEFAULT-+-1))
 (398 199 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (335 67 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-13BITS-P))
 (272 269 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AND-SET-ACCESSED-AND/OR-DIRTY-BIT))
 (269 269 (:DEFINITION X86ISA::APP-VIEW$A))
 (199 199 (:TYPE-PRESCRIPTION NATP))
 (199 199 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (134 134 (:TYPE-PRESCRIPTION X86ISA::13BITS-P))
 (134 67 (:REWRITE X86ISA::13BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 2 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (3 3 (:TYPE-PRESCRIPTION X86ISA::XLATE-EQUIV-ENTRIES))
 )
(X86ISA::MV-NTH-0-PAGING-ENTRY-NO-PAGE-FAULT-P-WITH-XLATE-EQUIV-ENTRIES-CONG
 (97980 41059 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (89625 19725 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (80712 13452 (:REWRITE IFIX-NEGATIVE-TO-NEGP))
 (80712 6726 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (80712 6726 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (40356 13452 (:REWRITE NEGP-WHEN-LESS-THAN-0))
 (32247 3583 (:REWRITE LOGTAIL-IDENTITY))
 (28248 20850 (:REWRITE DEFAULT-<-1))
 (26904 6726 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (25394 20010 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (20956 1612 (:REWRITE X86ISA::LOGHEAD-UNEQUAL))
 (20850 20850 (:REWRITE DEFAULT-<-2))
 (19725 19725 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (19725 19725 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (19725 19725 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (18971 18971 (:TYPE-PRESCRIPTION NATP))
 (18971 18971 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (18843 18843 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (18134 18134 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (13452 13452 (:TYPE-PRESCRIPTION NEGP))
 (13452 13452 (:REWRITE NEGP-WHEN-INTEGERP))
 (12896 1612 (:REWRITE BITOPS::SIGNED-BYTE-P-OF-LOGTAIL))
 (10749 10749 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (9855 1971 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-13BITS-P))
 (8060 1612 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (7398 7398 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3942 3942 (:TYPE-PRESCRIPTION X86ISA::13BITS-P))
 (3942 1971 (:REWRITE X86ISA::13BITS-P-WHEN-UNSIGNED-BYTE-P))
 (3583 3583 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (3224 3224 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (3224 3224 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (3224 3224 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (3224 3224 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (3224 3224 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (3224 1612 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (1612 1612 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 )
(X86ISA::MV-NTH-2-PAGING-ENTRY-NO-PAGE-FAULT-P-WITH-XLATE-EQUIV-ENTRIES-CONG
 (3751043 54934 (:REWRITE LOGHEAD-IDENTITY))
 (2832228 25172 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (2489819 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (2315282 34015 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (278055 25043 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (266731 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (266731 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (266731 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (266731 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (266731 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (266731 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (266731 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (266731 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (266731 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (266731 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (266731 58179 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (140107 57383 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (103296 17216 (:REWRITE IFIX-NEGATIVE-TO-NEGP))
 (103296 8608 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (103296 8608 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (92194 92194 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (84318 84318 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (68030 68030 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (68030 68030 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (68030 68030 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (68030 68030 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (68030 68030 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (68030 68030 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (68030 68030 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (68030 68030 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (68030 68030 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (68030 68030 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (68030 68030 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (68030 34015 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (68030 34015 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (68030 34015 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (68030 34015 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (68030 34015 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (68030 34015 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (68030 34015 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (68030 34015 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (68030 34015 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (68030 34015 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (68030 34015 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (63684 51060 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (58840 11768 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (58840 11768 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (51648 17216 (:REWRITE NEGP-WHEN-LESS-THAN-0))
 (47016 5224 (:REWRITE LOGTAIL-IDENTITY))
 (40695 8139 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (36272 26744 (:REWRITE DEFAULT-<-1))
 (34432 8608 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (30680 2360 (:REWRITE X86ISA::LOGHEAD-UNEQUAL))
 (27572 27572 (:TYPE-PRESCRIPTION NATP))
 (27572 27572 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (27065 27065 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (26744 26744 (:REWRITE DEFAULT-<-2))
 (26175 26175 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (25043 25043 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (25043 25043 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (25043 25043 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (23536 23536 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (23536 23536 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (23536 11768 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (23536 11768 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (18880 2360 (:REWRITE BITOPS::SIGNED-BYTE-P-OF-LOGTAIL))
 (17216 17216 (:TYPE-PRESCRIPTION NEGP))
 (17216 17216 (:REWRITE NEGP-WHEN-INTEGERP))
 (16278 16278 (:TYPE-PRESCRIPTION BITP))
 (16278 8139 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (14320 2864 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-13BITS-P))
 (11800 2360 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (9528 9528 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (5728 5728 (:TYPE-PRESCRIPTION X86ISA::13BITS-P))
 (5728 2864 (:REWRITE X86ISA::13BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4720 4720 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (4720 4720 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (4720 4720 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (4720 4720 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (4720 4720 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (4720 2360 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (2360 2360 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 )
(X86ISA::MV-NTH-0-PAGING-ENTRY-NO-PAGE-FAULT-P-WITH-XLATE-EQUIV-STRUCTURES-CONG
 (632 10 (:REWRITE LOGHEAD-IDENTITY))
 (488 8 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (414 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (384 6 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (148 148 (:TYPE-PRESCRIPTION IFIX))
 (108 108 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (46 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (46 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (46 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (46 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (46 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (46 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (46 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (46 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (46 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (46 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (46 10 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (42 14 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (36 12 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (36 4 (:REWRITE LOGTAIL-IDENTITY))
 (24 24 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (20 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-13BITS-P))
 (18 18 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (16 8 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (14 14 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (12 12 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (12 12 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (12 12 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (12 12 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (12 6 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE DEFAULT-<-1))
 (12 6 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 4 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (8 8 (:TYPE-PRESCRIPTION NATP))
 (8 8 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::13BITS-P))
 (8 8 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (8 8 (:REWRITE IFIX-WHEN-INTEGERP))
 (8 4 (:REWRITE X86ISA::13BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 6 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (6 6 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 )
(X86ISA::MV-NTH-2-PAGING-ENTRY-NO-PAGE-FAULT-P-WITH-XLATE-EQUIV-STRUCTURES
 (94789 5818 (:REWRITE LOGHEAD-IDENTITY))
 (25101 2010 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (21513 21513 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (10371 6070 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (7818 7818 (:TYPE-PRESCRIPTION X86ISA::N64P-XR-CTR))
 (7450 1334 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (7450 1334 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (6984 1164 (:REWRITE IFIX-NEGATIVE-TO-NEGP))
 (6984 582 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (6984 582 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (5469 2010 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (4863 4863 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (4684 4684 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (3947 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (3763 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (3763 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (3763 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (3763 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (3763 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (3763 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (3763 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (3763 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (3763 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (3763 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (3763 753 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (3585 3585 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (3580 716 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (3492 1164 (:REWRITE NEGP-WHEN-LESS-THAN-0))
 (2748 1956 (:REWRITE DEFAULT-<-1))
 (2668 2668 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (2668 2668 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (2668 1334 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2668 1334 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2508 1702 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (2346 2346 (:TYPE-PRESCRIPTION X86ISA::N64P-XR-MSR))
 (2328 582 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (2080 260 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (2080 260 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (2080 260 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (2080 260 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR4BITS-P))
 (2080 260 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (2080 260 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (2080 260 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-22BITS-P))
 (2010 2010 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (2010 2010 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (2010 2010 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (1956 1956 (:REWRITE DEFAULT-<-2))
 (1688 751 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1504 1504 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (1502 1502 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (1502 1502 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (1502 1502 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (1502 1502 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (1502 1502 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (1502 1502 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (1502 1502 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (1502 1502 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (1502 1502 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (1502 1502 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (1502 1502 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (1502 751 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1502 751 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1502 751 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1502 751 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1502 751 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1502 751 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1502 751 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1502 751 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1502 751 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1502 751 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1502 751 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1432 1432 (:TYPE-PRESCRIPTION BITP))
 (1432 716 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (1164 1164 (:TYPE-PRESCRIPTION NEGP))
 (1164 1164 (:REWRITE NEGP-WHEN-INTEGERP))
 (1161 129 (:REWRITE LOGTAIL-IDENTITY))
 (899 135 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (792 792 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (786 786 (:REWRITE X86ISA::SEGMENT-SELECTORBITS->RPL-OF-WRITE-WITH-MASK))
 (786 786 (:REWRITE X86ISA::RFLAGSBITS->AC-OF-WRITE-WITH-MASK))
 (786 786 (:REWRITE X86ISA::IA32_EFERBITS->NXE-OF-WRITE-WITH-MASK))
 (786 786 (:REWRITE X86ISA::CR4BITS->SMEP-OF-WRITE-WITH-MASK))
 (786 786 (:REWRITE X86ISA::CR4BITS->SMAP-OF-WRITE-WITH-MASK))
 (786 786 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (786 786 (:REWRITE X86ISA::CR0BITS->WP-OF-WRITE-WITH-MASK))
 (770 385 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (645 129 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-13BITS-P))
 (520 520 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (520 520 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (520 520 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (520 520 (:TYPE-PRESCRIPTION X86ISA::CR4BITS-P$INLINE))
 (520 520 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (520 520 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (520 520 (:TYPE-PRESCRIPTION X86ISA::22BITS-P))
 (520 260 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (520 260 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (520 260 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (520 260 (:REWRITE X86ISA::CR4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (520 260 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (520 260 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (520 260 (:REWRITE X86ISA::22BITS-P-WHEN-UNSIGNED-BYTE-P))
 (385 385 (:TYPE-PRESCRIPTION NATP))
 (385 385 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (258 258 (:TYPE-PRESCRIPTION X86ISA::13BITS-P))
 (258 129 (:REWRITE X86ISA::13BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 2 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 )
(X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-TABLE-ENTRY-ADDR
 (18 2 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (4 4 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (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 2 (:REWRITE X86ISA::MEMBER-P-CDR))
 (2 2 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (2 2 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (2 2 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (2 2 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (2 2 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (2 2 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (2 2 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (2 2 (:REWRITE CONSP-BY-LEN))
 (1 1 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AND-SET-ACCESSED-AND/OR-DIRTY-BIT))
 )
(X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-TABLE-ENTRY-ADDR
 (40 2 (:REWRITE LOGTAIL-IDENTITY))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (8 4 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (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-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (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 2 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (4 2 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:DEFINITION X86ISA::APP-VIEW))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (2 2 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (2 2 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (2 2 (:DEFINITION X86ISA::APP-VIEW$A))
 )
(X86ISA::XLATE-EQUIV-MEMORY-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-TABLE-ENTRY-ADDR-CONG
 (713 7 (:DEFINITION X86ISA::OPEN-QWORD-PADDR-LIST))
 (403 35 (:REWRITE IFIX-WHEN-INTEGERP))
 (391 49 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (360 7 (:DEFINITION BINARY-APPEND))
 (346 14 (:DEFINITION X86ISA::ADDR-RANGE))
 (282 14 (:DEFINITION INTEGER-LISTP))
 (213 7 (:REWRITE X86ISA::CAR-ADDR-RANGE))
 (112 112 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (112 28 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (112 14 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (100 100 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (79 35 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (75 11 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (42 42 (:TYPE-PRESCRIPTION X86ISA::TRUE-LISTP-ADDR-RANGE))
 (42 42 (:TYPE-PRESCRIPTION X86ISA::CONSP-ADDR-RANGE))
 (42 28 (:REWRITE DEFAULT-CDR))
 (36 36 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (36 36 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (36 36 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (36 36 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (36 36 (:REWRITE CONSP-BY-LEN))
 (32 16 (:REWRITE DEFAULT-+-2))
 (28 28 (:REWRITE X86ISA::NEG-ADDR-RANGE=NIL))
 (28 14 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (26 14 (:REWRITE X86ISA::MEMBER-P-AND-MULT-8-QWORD-PADDR-LISTP))
 (22 22 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (22 22 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (22 11 (:REWRITE X86ISA::MEMBER-P-CDR))
 (21 21 (:REWRITE DEFAULT-CAR))
 (21 21 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (16 16 (:REWRITE DEFAULT-+-1))
 (14 7 (:REWRITE X86ISA::CDR-ADDR-RANGE))
 (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))
 (8 8 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (8 4 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (7 7 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 (7 7 (:TYPE-PRESCRIPTION IFIX))
 (7 7 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 )
(X86ISA::XLATE-EQUIV-MEMORY-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-TABLE-ENTRY-ADDR-CONG
 (40 2 (:REWRITE LOGTAIL-IDENTITY))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (8 4 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (6 3 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AND-SET-ACCESSED-AND/OR-DIRTY-BIT))
 (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-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (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 2 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (4 2 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:DEFINITION X86ISA::APP-VIEW))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-TABLE-ENTRY-ADDR))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-TABLE-ENTRY-ADDR))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (2 2 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (2 2 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (2 2 (:DEFINITION X86ISA::APP-VIEW$A))
 )
(X86ISA::IA32E-LA-TO-PA-PAGE-TABLE-IN-APP-VIEW)
(X86ISA::XLATE-EQUIV-ENTRIES-AND-IA32E-PTE-4K-PAGEBITS->PAGE)
(X86ISA::XLATE-EQUIV-MEMORY-AND-IA32E-LA-TO-PA-PAGE-TABLE
 (2742 6 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-2))
 (2340 6 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 2))
 (2064 12 (:LINEAR X86ISA::RM-LOW-64-LOGAND-LOGIOR-HELPER-1))
 (2040 12 (:DEFINITION X86ISA::N64P$INLINE))
 (2024 40 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (1784 28 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (872 88 (:REWRITE LOGHEAD-IDENTITY))
 (828 72 (:REWRITE UNSIGNED-BYTE-P-OF-ASH))
 (674 14 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (570 30 (:LINEAR LOGHEAD-UPPER-BOUND))
 (490 46 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (372 60 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (308 40 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (308 40 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (308 40 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (308 40 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (308 40 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (308 40 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (308 40 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (308 40 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (300 24 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (276 36 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (276 36 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (276 36 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (260 52 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (260 52 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (252 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR8BITS-P))
 (244 244 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (194 14 (:REWRITE X86ISA::PAGE-PRESENT=0-AND-PAGING-ENTRY-NO-PAGE-FAULT-P))
 (192 36 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (186 6 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-1))
 (180 12 (:REWRITE X86ISA::CR8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (168 66 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (164 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (160 24 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (144 116 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (132 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTORBITS-P))
 (132 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P))
 (132 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTORBITS-P))
 (132 6 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (116 116 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (112 112 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (108 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-4BITS-P))
 (108 6 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-2))
 (104 104 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (104 104 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (104 52 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (104 52 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (104 16 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (96 96 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (92 20 (:REWRITE LOGEXT-IDENTITY))
 (82 82 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (82 42 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (68 68 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (68 8 (:REWRITE ASH-0))
 (66 6 (:REWRITE BITOPS::ASH-<-0))
 (60 20 (:LINEAR X86ISA::N01P-PAGE-PRESENT))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (56 28 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (56 28 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (56 28 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (56 28 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (56 28 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (56 28 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (56 28 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (56 28 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (48 48 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (48 24 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 18 (:REWRITE DEFAULT-<-1))
 (46 46 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (46 46 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (42 6 (:REWRITE ZIP-OPEN))
 (40 40 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (38 14 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (36 36 (:TYPE-PRESCRIPTION X86ISA::CR8BITS-P$INLINE))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (32 32 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (32 32 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (32 32 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (32 32 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (32 16 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 (28 4 (:REWRITE X86ISA::LOGEXT-LOGHEAD-IDENTITY))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTORBITS-P))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTORBITS-P))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::4BITS-P))
 (24 12 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::CALL-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (20 4 (:REWRITE X86ISA::ACCESSED-BIT-SET-ACCESSED-BIT-IDENTITY))
 (18 18 (:REWRITE DEFAULT-<-2))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (16 16 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (14 14 (:REWRITE X86ISA::MV-NTH-0-PAGING-ENTRY-NO-PAGE-FAULT-P-AND-SIMILAR-ENTRIES))
 (14 14 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (14 14 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (12 6 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (12 4 (:REWRITE X86ISA::MV-NTH-2-PAGING-ENTRY-NO-PAGE-FAULT-P-DOES-NOT-MODIFY-X86-IF-NO-FAULT))
 (12 4 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-TABLE-IN-APP-VIEW))
 (10 10 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-TABLE-ENTRY-ADDR))
 (10 10 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (8 8 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (8 8 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS->PAGE-OF-WRITE-WITH-MASK))
 (8 8 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->A-OF-WRITE-WITH-MASK))
 (8 4 (:REWRITE BITOPS::SIGNED-BYTE-P-OF-LOGHEAD))
 (6 6 (:TYPE-PRESCRIPTION ZIP))
 (6 6 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGIOR-FOR-NATURALS))
 (6 6 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::N01P-ACCESSED-BIT))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::ACCESSED-BIT))
 (4 4 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->D-OF-WRITE-WITH-MASK))
 )
(X86ISA::XLATE-EQUIV-MEMORY-AND-MV-NTH-0-IA32E-LA-TO-PA-PAGE-TABLE-CONG)
(X86ISA::XLATE-EQUIV-MEMORY-AND-MV-NTH-1-IA32E-LA-TO-PA-PAGE-TABLE-CONG)
(X86ISA::XLATE-EQUIV-STRUCTURES-AND-MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE
 (6338 848 (:REWRITE LOGHEAD-IDENTITY))
 (5008 168 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (3432 176 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (3344 176 (:LINEAR LOGHEAD-UPPER-BOUND))
 (2200 176 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (1552 1040 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (1468 284 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (1468 284 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (1414 14 (:DEFINITION X86ISA::OPEN-QWORD-PADDR-LIST))
 (1058 1058 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1026 1026 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (924 200 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (886 886 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (770 98 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (726 198 (:REWRITE LOGEXT-IDENTITY))
 (714 14 (:DEFINITION BINARY-APPEND))
 (686 28 (:DEFINITION X86ISA::ADDR-RANGE))
 (576 576 (:TYPE-PRESCRIPTION X86ISA::N64P-XR-CTR))
 (568 568 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (568 568 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (568 284 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (568 284 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (560 28 (:DEFINITION INTEGER-LISTP))
 (544 90 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (466 92 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (430 430 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (420 24 (:REWRITE X86ISA::PAGE-PRESENT=0-AND-PAGING-ENTRY-NO-PAGE-FAULT-P))
 (420 14 (:REWRITE X86ISA::CAR-ADDR-RANGE))
 (272 174 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (270 270 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (264 136 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (260 36 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (224 224 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (224 56 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (224 28 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (190 90 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (182 182 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (180 180 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (180 180 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (180 180 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (180 180 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (178 82 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (176 176 (:TYPE-PRESCRIPTION X86ISA::PAGE-PRESENT))
 (176 176 (:TYPE-PRESCRIPTION X86ISA::N64P-XR-MSR))
 (176 176 (:TYPE-PRESCRIPTION X86ISA::N01P-PAGE-PRESENT))
 (176 176 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (176 176 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (166 20 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (166 20 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (166 20 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (166 20 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (166 20 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (136 136 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (136 136 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (132 44 (:LINEAR X86ISA::N01P-PAGE-PRESENT))
 (128 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR4BITS-P))
 (128 16 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-22BITS-P))
 (102 8 (:REWRITE UNSIGNED-BYTE-P-OF-ASH))
 (98 98 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (90 90 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (90 90 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (84 84 (:TYPE-PRESCRIPTION X86ISA::TRUE-LISTP-ADDR-RANGE))
 (84 84 (:TYPE-PRESCRIPTION X86ISA::CONSP-ADDR-RANGE))
 (84 84 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (84 84 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (84 84 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (84 84 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (84 84 (:REWRITE CONSP-BY-LEN))
 (84 56 (:REWRITE DEFAULT-CDR))
 (80 80 (:REWRITE X86ISA::SEGMENT-SELECTORBITS->RPL-OF-WRITE-WITH-MASK))
 (80 80 (:REWRITE X86ISA::RFLAGSBITS->AC-OF-WRITE-WITH-MASK))
 (80 80 (:REWRITE X86ISA::IA32_EFERBITS->NXE-OF-WRITE-WITH-MASK))
 (80 80 (:REWRITE X86ISA::CR4BITS->SMEP-OF-WRITE-WITH-MASK))
 (80 80 (:REWRITE X86ISA::CR4BITS->SMAP-OF-WRITE-WITH-MASK))
 (80 80 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (80 80 (:REWRITE X86ISA::CR0BITS->WP-OF-WRITE-WITH-MASK))
 (72 36 (:REWRITE X86ISA::MEMBER-P-CDR))
 (62 62 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-TABLE-ENTRY-ADDR))
 (62 62 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (56 56 (:REWRITE X86ISA::NEG-ADDR-RANGE=NIL))
 (56 28 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (56 28 (:REWRITE DEFAULT-+-2))
 (42 42 (:REWRITE DEFAULT-CAR))
 (42 42 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (42 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR8BITS-P))
 (40 40 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (40 40 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (40 40 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (40 40 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (40 40 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (40 20 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (40 20 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (40 20 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (40 20 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (40 20 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (36 36 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (36 36 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (36 36 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::CR4BITS-P$INLINE))
 (32 32 (:TYPE-PRESCRIPTION X86ISA::22BITS-P))
 (32 16 (:REWRITE X86ISA::CR4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (32 16 (:REWRITE X86ISA::22BITS-P-WHEN-UNSIGNED-BYTE-P))
 (30 2 (:REWRITE X86ISA::CR8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (28 28 (:REWRITE X86ISA::MEMBER-P-AND-MULT-8-QWORD-PADDR-LISTP))
 (28 28 (:REWRITE DEFAULT-+-1))
 (28 14 (:REWRITE X86ISA::CDR-ADDR-RANGE))
 (24 24 (:REWRITE X86ISA::MV-NTH-0-PAGING-ENTRY-NO-PAGE-FAULT-P-AND-SIMILAR-ENTRIES))
 (24 12 (:REWRITE X86ISA::DIRTY-BIT-SET-DIRTY-BIT-IDENTITY))
 (22 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (22 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTORBITS-P))
 (22 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P))
 (22 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (22 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTORBITS-P))
 (22 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (22 2 (:REWRITE ASH-0))
 (20 20 (:REWRITE X86ISA::ACCESSED-BIT-SET-ACCESSED-BIT-IDENTITY))
 (18 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-4BITS-P))
 (14 14 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 (14 2 (:REWRITE ZIP-OPEN))
 (14 2 (:REWRITE X86ISA::LOGEXT-LOGHEAD-IDENTITY))
 (12 4 (:REWRITE X86ISA::MV-NTH-2-PAGING-ENTRY-NO-PAGE-FAULT-P-WITH-XLATE-EQUIV-STRUCTURES))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::X86P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-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::IA32E-PAGE-TABLESBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (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::16BITS-P))
 (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::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::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::FP-STATUSBITS-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::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::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CR8BITS-P$INLINE))
 (6 2 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-TABLE-IN-APP-VIEW))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTORBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTORBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::4BITS-P))
 (4 4 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-TRANSITIVE))
 (4 4 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (4 4 (:REWRITE X86ISA::DIRTY-BIT-SET-ACCESSED-BIT))
 (4 2 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE BITOPS::SIGNED-BYTE-P-OF-LOGHEAD))
 (4 2 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CALL-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 2 (:TYPE-PRESCRIPTION ZIP))
 (2 2 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS->PAGE-OF-WRITE-WITH-MASK))
 )
(X86ISA::XLATE-EQUIV-STRUCTURES-AND-TWO-MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE-CONG)
(X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-PAGING-ENTRY-NO-PAGE-FAULT-P
 (36735 1383 (:REWRITE LOGHEAD-IDENTITY))
 (12950 1082 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (3840 640 (:REWRITE IFIX-NEGATIVE-TO-NEGP))
 (3840 320 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (3840 320 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (2970 1082 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (2760 552 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (2760 552 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (2152 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (2110 1511 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (1968 394 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (1920 640 (:REWRITE NEGP-WHEN-LESS-THAN-0))
 (1840 368 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (1478 1059 (:REWRITE DEFAULT-<-1))
 (1452 1452 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (1397 941 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (1280 320 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (1104 1104 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (1104 1104 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (1104 552 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1104 552 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1082 1082 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (1082 1082 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (1082 1082 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (1059 1059 (:REWRITE DEFAULT-<-2))
 (970 392 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (888 888 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (796 796 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (786 786 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (784 784 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (784 392 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (784 392 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (736 736 (:TYPE-PRESCRIPTION BITP))
 (736 368 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (640 640 (:TYPE-PRESCRIPTION NEGP))
 (640 640 (:REWRITE NEGP-WHEN-INTEGERP))
 (603 67 (:REWRITE LOGTAIL-IDENTITY))
 (589 73 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (419 419 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (398 199 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (335 67 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-13BITS-P))
 (199 199 (:TYPE-PRESCRIPTION NATP))
 (199 199 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (134 134 (:TYPE-PRESCRIPTION X86ISA::13BITS-P))
 (134 67 (:REWRITE X86ISA::13BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 2 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 )
(X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-WITH-MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE
 (2149 59 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (2030 215 (:REWRITE LOGHEAD-IDENTITY))
 (1469 63 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (1444 76 (:LINEAR LOGHEAD-UPPER-BOUND))
 (950 76 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (580 116 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (580 116 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (384 70 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (369 292 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (297 69 (:REWRITE LOGEXT-IDENTITY))
 (292 292 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (270 270 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (236 39 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (232 232 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (232 232 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (232 116 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (232 116 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (209 209 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (203 40 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (172 10 (:REWRITE X86ISA::PAGE-PRESENT=0-AND-PAGING-ENTRY-NO-PAGE-FAULT-P))
 (167 167 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (117 117 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (105 62 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (104 46 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (83 39 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (81 9 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (79 79 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (78 78 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (78 78 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (78 78 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (78 78 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (63 63 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (63 63 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (54 18 (:LINEAR X86ISA::N01P-PAGE-PRESENT))
 (51 4 (:REWRITE UNSIGNED-BYTE-P-OF-ASH))
 (46 46 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (46 46 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (43 43 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (39 39 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (39 39 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (27 27 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (21 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR8BITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (19 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (18 18 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-TABLE-ENTRY-ADDR))
 (18 18 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (18 9 (:REWRITE X86ISA::MEMBER-P-CDR))
 (15 1 (:REWRITE X86ISA::CR8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTORBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTORBITS-P))
 (11 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (11 1 (:REWRITE ASH-0))
 (10 10 (:REWRITE X86ISA::MV-NTH-0-PAGING-ENTRY-NO-PAGE-FAULT-P-AND-SIMILAR-ENTRIES))
 (10 4 (:REWRITE X86ISA::DIRTY-BIT-SET-DIRTY-BIT-IDENTITY))
 (9 9 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (9 9 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (9 9 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (9 9 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (9 9 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (9 9 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (9 9 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (9 9 (:REWRITE CONSP-BY-LEN))
 (9 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-4BITS-P))
 (7 1 (:REWRITE ZIP-OPEN))
 (7 1 (:REWRITE X86ISA::LOGEXT-LOGHEAD-IDENTITY))
 (6 6 (:REWRITE X86ISA::ACCESSED-BIT-SET-ACCESSED-BIT-IDENTITY))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (4 2 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 (3 3 (:TYPE-PRESCRIPTION X86ISA::CR8BITS-P$INLINE))
 (3 1 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-TABLE-IN-APP-VIEW))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::4BITS-P))
 (2 2 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (2 2 (:REWRITE X86ISA::DIRTY-BIT-SET-ACCESSED-BIT))
 (2 1 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE BITOPS::SIGNED-BYTE-P-OF-LOGHEAD))
 (2 1 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CALL-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1 1 (:TYPE-PRESCRIPTION ZIP))
 (1 1 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS->PAGE-OF-WRITE-WITH-MASK))
 )
(X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-WITH-TWO-MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE
 (112 2 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (104 10 (:REWRITE LOGHEAD-IDENTITY))
 (76 4 (:LINEAR LOGHEAD-UPPER-BOUND))
 (76 2 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (50 4 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (36 36 (:TYPE-PRESCRIPTION LOGHEAD-TYPE))
 (32 32 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (30 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (30 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (18 14 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (18 2 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (18 2 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (14 14 (:TYPE-PRESCRIPTION NFIX))
 (14 14 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (14 2 (:REWRITE LOGEXT-IDENTITY))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (12 6 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 2 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (10 10 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (8 8 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (8 8 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (8 4 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (6 6 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (6 2 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-TABLE-IN-APP-VIEW))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (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))
 (4 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGHEAD))
 (4 2 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::MEMBER-P-CDR))
 (4 2 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (4 2 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (4 2 (:DEFINITION X86ISA::APP-VIEW))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (2 2 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (2 2 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (2 2 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (2 2 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (2 2 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (2 2 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (2 2 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (2 2 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (2 2 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (2 2 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (2 2 (:REWRITE CONSP-BY-LEN))
 (2 2 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (2 2 (:DEFINITION X86ISA::APP-VIEW$A))
 )
(X86ISA::XLATE-EQUIV-MEMORY-WITH-MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE
 (224 4 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (208 20 (:REWRITE LOGHEAD-IDENTITY))
 (152 8 (:LINEAR LOGHEAD-UPPER-BOUND))
 (152 4 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (100 8 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (72 72 (:TYPE-PRESCRIPTION LOGHEAD-TYPE))
 (64 64 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (36 28 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (36 4 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (36 4 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (28 28 (:TYPE-PRESCRIPTION NFIX))
 (28 28 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (28 4 (:REWRITE LOGEXT-IDENTITY))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (24 12 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (24 4 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (20 20 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (20 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (16 16 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (16 16 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (16 8 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (12 12 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (8 8 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (8 8 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (8 8 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (8 8 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (8 4 (:REWRITE UNSIGNED-BYTE-P-OF-LOGHEAD))
 (8 4 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::MEMBER-P-CDR))
 (8 4 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (4 4 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (4 4 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (4 4 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (4 4 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (4 4 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (4 4 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (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::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (4 2 (:DEFINITION X86ISA::MARKING-VIEW))
 (3 1 (:REWRITE X86ISA::XR-IA32E-LA-TO-PA-PAGE-TABLE-IN-NON-MARKING-VIEW))
 (3 1 (:REWRITE X86ISA::MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE-SYSTEM-LEVEL-NON-MARKING-VIEW))
 (2 2 (:DEFINITION X86ISA::MARKING-VIEW$A))
 )
(X86ISA::XLATE-EQUIV-MEMORY-WITH-TWO-MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE
 (672 12 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (624 60 (:REWRITE LOGHEAD-IDENTITY))
 (456 24 (:LINEAR LOGHEAD-UPPER-BOUND))
 (456 12 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (300 24 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (216 216 (:TYPE-PRESCRIPTION LOGHEAD-TYPE))
 (192 192 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (180 36 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (180 36 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (108 84 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (108 12 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (108 12 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (84 84 (:TYPE-PRESCRIPTION NFIX))
 (84 84 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (84 12 (:REWRITE LOGEXT-IDENTITY))
 (72 72 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (72 72 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (72 36 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (72 36 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (72 12 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (60 60 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (48 48 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (48 48 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (48 24 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (36 36 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (36 36 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (26 13 (:DEFINITION X86ISA::MARKING-VIEW))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (24 24 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (24 24 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (24 24 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (24 24 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (24 24 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (24 12 (:REWRITE UNSIGNED-BYTE-P-OF-LOGHEAD))
 (24 12 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::MEMBER-P-CDR))
 (24 12 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (24 12 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (24 8 (:REWRITE X86ISA::XR-IA32E-LA-TO-PA-PAGE-TABLE-IN-NON-MARKING-VIEW))
 (18 8 (:REWRITE X86ISA::MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE-SYSTEM-LEVEL-NON-MARKING-VIEW))
 (13 13 (:DEFINITION X86ISA::MARKING-VIEW$A))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (12 12 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (12 12 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (12 12 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (12 12 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (12 12 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (12 12 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (12 12 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (12 12 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (12 12 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (12 12 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (12 12 (:REWRITE CONSP-BY-LEN))
 (12 12 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 )
(X86ISA::TWO-PAGE-TABLE-WALKS-IA32E-LA-TO-PA-PAGE-TABLE
 (56 1 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (52 5 (:REWRITE LOGHEAD-IDENTITY))
 (38 2 (:LINEAR LOGHEAD-UPPER-BOUND))
 (38 1 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (25 2 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (18 18 (:TYPE-PRESCRIPTION LOGHEAD-TYPE))
 (16 16 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (15 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (15 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (9 7 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (9 1 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (9 1 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (8 6 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-TABLE-IN-APP-VIEW))
 (7 7 (:TYPE-PRESCRIPTION NFIX))
 (7 7 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (7 1 (:REWRITE LOGEXT-IDENTITY))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (6 3 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 1 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (5 5 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (5 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (4 4 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (4 4 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (4 2 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (3 3 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (3 3 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (2 2 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (2 1 (:REWRITE UNSIGNED-BYTE-P-OF-LOGHEAD))
 (2 1 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MEMBER-P-CDR))
 (2 1 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (2 1 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (2 1 (:DEFINITION X86ISA::APP-VIEW))
 (1 1 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (1 1 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (1 1 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (1 1 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (1 1 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (1 1 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (1 1 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (1 1 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (1 1 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (1 1 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (1 1 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (1 1 (:REWRITE CONSP-BY-LEN))
 (1 1 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (1 1 (:DEFINITION X86ISA::APP-VIEW$A))
 )
(X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES-WITH-XLATE-EQUIV-STRUCTURES
 (6775 2 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES))
 (5360 424 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (4960 88 (:REWRITE SUBSETP-CAR-MEMBER))
 (3832 88 (:REWRITE SUBSETP-MEMBER . 3))
 (2632 32 (:DEFINITION MEMBER-EQUAL))
 (2432 48 (:REWRITE SUBSETP-OF-APPEND-WHEN-SUBSET-OF-EITHER))
 (2000 112 (:REWRITE CONSP-OF-APPEND))
 (1896 32 (:REWRITE SUBSETP-APPEND1))
 (1424 48 (:DEFINITION BINARY-APPEND))
 (1384 424 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1200 424 (:REWRITE SUBSETP-TRANS2))
 (944 16 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (896 896 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (868 868 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (868 868 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (868 868 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (868 868 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (868 868 (:REWRITE CONSP-BY-LEN))
 (856 96 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (816 48 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (552 64 (:REWRITE MEMBER-WHEN-ATOM))
 (424 424 (:REWRITE SUBSETP-TRANS))
 (378 16 (:REWRITE LOGHEAD-IDENTITY))
 (288 288 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (168 104 (:REWRITE DEFAULT-CDR))
 (144 96 (:REWRITE DEFAULT-CAR))
 (108 108 (:TYPE-PRESCRIPTION X86ISA::N64P-XR-CTR))
 (88 88 (:REWRITE SUBSETP-MEMBER . 4))
 (88 88 (:REWRITE SUBSETP-MEMBER . 2))
 (88 88 (:REWRITE SUBSETP-MEMBER . 1))
 (88 88 (:REWRITE INTERSECTP-MEMBER . 3))
 (88 88 (:REWRITE INTERSECTP-MEMBER . 2))
 (68 68 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (48 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR4BITS-P))
 (48 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-22BITS-P))
 (40 40 (:REWRITE CONSP-OF-CDDR-BY-LEN))
 (32 16 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (28 28 (:TYPE-PRESCRIPTION X86ISA::N64P-XR-MSR))
 (16 16 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (16 16 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (16 16 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (14 14 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::CR4BITS-P$INLINE))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::22BITS-P))
 (12 6 (:REWRITE X86ISA::CR4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::22BITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::12BITS-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::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 4 (:REWRITE X86ISA::SEGMENT-SELECTORBITS->RPL-OF-WRITE-WITH-MASK))
 (4 4 (:REWRITE X86ISA::RFLAGSBITS->AC-OF-WRITE-WITH-MASK))
 (4 4 (:REWRITE X86ISA::IA32_EFERBITS->NXE-OF-WRITE-WITH-MASK))
 (4 4 (:REWRITE X86ISA::CR4BITS->SMEP-OF-WRITE-WITH-MASK))
 (4 4 (:REWRITE X86ISA::CR4BITS->SMAP-OF-WRITE-WITH-MASK))
 (4 4 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (4 4 (:REWRITE X86ISA::CR0BITS->WP-OF-WRITE-WITH-MASK))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-TRANSITIVE))
 )
(X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES-WITH-XLATE-EQUIV-MEMORY-CONG)
(X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES-MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE
 (3 1 (:REWRITE X86ISA::XLATE-EQUIV-MEMORY-WITH-MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE))
 (3 1 (:REWRITE X86ISA::MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE-SYSTEM-LEVEL-NON-MARKING-VIEW))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::64-BIT-MODEP))
 (2 1 (:DEFINITION X86ISA::MARKING-VIEW))
 (1 1 (:DEFINITION X86ISA::MARKING-VIEW$A))
 )
(X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE
 (9 9 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-TRANSITIVE))
 (9 3 (:REWRITE X86ISA::MV-NTH-2-IA32E-LA-TO-PA-PAGE-TABLE-SYSTEM-LEVEL-NON-MARKING-VIEW))
 (6 3 (:DEFINITION X86ISA::MARKING-VIEW))
 (3 3 (:DEFINITION X86ISA::MARKING-VIEW$A))
 )