(X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIR-PTR-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-DIR-PTR-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))
 (2 1 (:REWRITE X86ISA::MEMBER-P-CDR))
 (1 1 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 )
(X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-21-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR
 (8 4 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (8 2 (:REWRITE LOGTAIL-IDENTITY))
 (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 (: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))
 (2 1 (:REWRITE X86ISA::MEMBER-P-CDR))
 (1 1 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 )
(X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-30-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR
 (8 4 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (8 2 (:REWRITE LOGTAIL-IDENTITY))
 (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 (: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))
 (2 1 (:REWRITE X86ISA::MEMBER-P-CDR))
 (1 1 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 )
(X86ISA::XLATE-EQUIV-MEMORY-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIR-PTR-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))
 (24 12 (:REWRITE X86ISA::MEMBER-P-CDR))
 (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))
 (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))
 (12 12 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (11 11 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (11 11 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (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-DIR-PTR-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-DIR-PTR-TABLE-ENTRY-ADDR))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-DIR-PTR-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::XLATE-EQUIV-MEMORY-AND-LOGTAIL-21-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR-CONG
 (8 4 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (8 2 (:REWRITE LOGTAIL-IDENTITY))
 (6 3 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AND-SET-ACCESSED-AND/OR-DIRTY-BIT))
 (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 (:DEFINITION X86ISA::APP-VIEW))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-21-RM-LOW-64-WITH-PAGE-DIR-PTR-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::XLATE-EQUIV-MEMORY-AND-LOGTAIL-30-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR-CONG
 (8 4 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (8 2 (:REWRITE LOGTAIL-IDENTITY))
 (6 3 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AND-SET-ACCESSED-AND/OR-DIRTY-BIT))
 (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 (:DEFINITION X86ISA::APP-VIEW))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-30-RM-LOW-64-WITH-PAGE-DIR-PTR-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-DIR-PTR-TABLE-IN-APP-VIEW)
(X86ISA::XLATE-EQUIV-ENTRIES-AND-IA32E-PDPTE-PG-DIRBITS->PD)
(X86ISA::XLATE-EQUIV-ENTRIES-AND-IA32E-PDPTE-1GB-PAGEBITS->PAGE
 (20855 354 (:REWRITE LOGHEAD-IDENTITY))
 (8160 192 (:REWRITE X86ISA::GREATER-LOGBITP-OF-UNSIGNED-BYTE-P . 2))
 (4578 75 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (4474 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (3536 280 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1530 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (1530 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (1530 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (1530 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (1530 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (1530 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (1530 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (1530 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (1530 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (1530 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (1530 314 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (1312 1312 (:TYPE-PRESCRIPTION IFIX))
 (864 96 (:REWRITE BITOPS::LOGBITP-NONZERO-OF-BIT))
 (816 34 (:REWRITE LOGTAIL-IDENTITY))
 (688 412 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (632 124 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (592 592 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (576 192 (:REWRITE BITOPS::LOGBITP-WHEN-BITMASKP))
 (560 560 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (560 560 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (560 560 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (560 560 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (560 560 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (560 560 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (560 560 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (560 560 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (560 560 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (560 560 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (560 560 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (560 280 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (560 280 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (560 280 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (560 280 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (560 280 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (560 280 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (560 280 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (560 280 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (560 280 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (560 280 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (560 280 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (544 544 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (412 412 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (384 384 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (384 192 (:REWRITE DEFAULT-<-1))
 (348 38 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (344 344 (:TYPE-PRESCRIPTION BITP))
 (340 340 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (340 340 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (332 124 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (273 42 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (246 24 (:REWRITE X86ISA::LOGHEAD-UNEQUAL))
 (234 24 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (192 192 (:REWRITE BITOPS::NORMALIZE-LOGBITP-WHEN-MODS-EQUAL))
 (192 192 (:REWRITE X86ISA::GREATER-LOGBITP-OF-UNSIGNED-BYTE-P . 1))
 (192 192 (:REWRITE DEFAULT-<-2))
 (192 96 (:REWRITE BITOPS::LOGBITP-OF-LOGHEAD-OUT-OF-BOUNDS))
 (176 38 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (147 25 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (118 58 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (104 13 (:REWRITE BITOPS::SIGNED-BYTE-P-OF-LOGTAIL))
 (98 88 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (98 88 (:REWRITE IFIX-WHEN-INTEGERP))
 (96 96 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (67 67 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (66 66 (:TYPE-PRESCRIPTION NATP))
 (66 66 (:TYPE-PRESCRIPTION LOGTAIL-TYPE))
 (62 62 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE2-P))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE1-P))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX2-BYTE1-P))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SIB-P))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MODR/M-P))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE3-P))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE2-P))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE1-P))
 (60 12 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-8BITS-P))
 (48 48 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (48 24 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (37 37 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (37 37 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (37 37 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (28 18 (:REWRITE UNSIGNED-BYTE-P-OF-LOGHEAD))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE2-P$INLINE))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE1-P$INLINE))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::VEX2-BYTE1-P$INLINE))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::SIB-P$INLINE))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::MODR/M-P$INLINE))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE3-P$INLINE))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE2-P$INLINE))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE1-P$INLINE))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::8BITS-P))
 (24 24 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (24 12 (:REWRITE X86ISA::VEX3-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::VEX3-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::VEX2-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::SIB-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::MODR/M-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::EVEX-BYTE3-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::EVEX-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::EVEX-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (24 12 (:REWRITE X86ISA::8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (18 18 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 )
(X86ISA::XLATE-EQUIV-MEMORY-AND-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE
 (12580 37 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-2))
 (11766 74 (:LINEAR X86ISA::RM-LOW-64-LOGAND-LOGIOR-HELPER-1))
 (11618 74 (:DEFINITION X86ISA::N64P$INLINE))
 (11024 196 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (10101 37 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 2))
 (9938 122 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (5400 799 (:REWRITE LOGHEAD-IDENTITY))
 (5363 358 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (4064 697 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (4005 228 (:LINEAR LOGHEAD-UPPER-BOUND))
 (2275 182 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (1470 280 (:REWRITE UNSIGNED-BYTE-P-OF-ASH))
 (1449 1449 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1404 196 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (1404 196 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (1404 196 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (1404 196 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (1404 196 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (1404 196 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (1404 196 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (1404 196 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (1372 192 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (1372 192 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (1372 192 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (1365 273 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (1365 273 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (1294 1054 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (1207 439 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (1168 693 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (1047 1047 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (1001 1001 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (981 435 (:REWRITE LOGEXT-IDENTITY))
 (972 972 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (972 51 (:REWRITE X86ISA::PAGE-DIRECTORY-LOWER-12-BITS-ERROR))
 (897 51 (:REWRITE X86ISA::PAGE-PRESENT=0-AND-PAGING-ENTRY-NO-PAGE-FAULT-P))
 (814 37 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (788 283 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (777 37 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-1))
 (697 697 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (697 697 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (666 37 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-2))
 (578 95 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (576 362 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (572 88 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-2BITS-P))
 (546 546 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (546 546 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (546 273 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (546 273 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (516 48 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (516 48 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (516 48 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (516 48 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (516 48 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (487 167 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-DIRECTORY-IN-APP-VIEW))
 (484 44 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTORBITS-P))
 (484 44 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P))
 (484 44 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTORBITS-P))
 (475 475 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (455 91 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (407 37 (:REWRITE BITOPS::ASH-<-0))
 (379 39 (:REWRITE ASH-0))
 (376 376 (:TYPE-PRESCRIPTION X86ISA::PAGE-PRESENT))
 (376 376 (:TYPE-PRESCRIPTION X86ISA::N01P-PAGE-PRESENT))
 (362 362 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (362 362 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (353 353 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (353 353 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (318 318 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (308 44 (:REWRITE X86ISA::2BITS-P-WHEN-UNSIGNED-BYTE-P))
 (304 119 (:REWRITE DEFAULT-<-1))
 (293 293 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (282 94 (:LINEAR X86ISA::N01P-PAGE-PRESENT))
 (244 244 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (244 244 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (244 244 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (244 244 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (244 244 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (244 244 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (244 244 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (244 244 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (244 122 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (244 122 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (244 122 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (244 122 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (244 122 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (244 122 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (244 122 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (244 122 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (238 34 (:REWRITE ZIP-OPEN))
 (236 236 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (236 236 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (236 236 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (236 118 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (236 118 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (236 118 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (216 216 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS->PD$INLINE))
 (202 27 (:REWRITE BITOPS::CANCEL-LOGEXT-UNDER-LOGHEAD))
 (194 194 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (194 194 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (194 194 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (194 194 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (182 182 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (182 91 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (143 28 (:REWRITE X86ISA::PAGE-DIRECTORY-LOWER-12-BITS-VALUE-OF-ADDRESS-WHEN-ERROR))
 (135 24 (:REWRITE X86ISA::PAGE-DIRECTORY-LOWER-12-BITS))
 (132 132 (:TYPE-PRESCRIPTION X86ISA::2BITS-P))
 (119 119 (:REWRITE DEFAULT-<-2))
 (114 18 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (96 96 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (96 96 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (96 96 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (96 96 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (96 96 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (96 48 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (96 48 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (96 48 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (96 48 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (96 48 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (95 95 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (95 95 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (88 88 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTORBITS-P))
 (88 88 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P))
 (88 88 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTORBITS-P))
 (88 44 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (88 44 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (88 44 (:REWRITE X86ISA::CALL-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (74 37 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (51 51 (:REWRITE X86ISA::MV-NTH-0-PAGING-ENTRY-NO-PAGE-FAULT-P-AND-SIMILAR-ENTRIES))
 (45 45 (:TYPE-PRESCRIPTION BITP-LOGHEAD-1))
 (40 8 (:REWRITE X86ISA::ACCESSED-BIT-SET-ACCESSED-BIT-IDENTITY))
 (37 37 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGIOR-FOR-NATURALS))
 (37 37 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (36 36 (:TYPE-PRESCRIPTION BITP))
 (36 18 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (35 35 (:REWRITE BITOPS::LOGHEAD-OF-0-I))
 (34 34 (:TYPE-PRESCRIPTION ZIP))
 (32 8 (:REWRITE X86ISA::XR-AND-IA32E-LA-TO-PA-PAGE-DIRECTORY-IN-NON-MARKING-VIEW))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (32 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (29 29 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS->PD-OF-WRITE-WITH-MASK))
 (28 4 (:REWRITE X86ISA::LOGHEAD-UNEQUAL))
 (28 4 (:REWRITE X86ISA::LOGEXT-LOGHEAD-IDENTITY))
 (27 27 (:TYPE-PRESCRIPTION LOGEXT-TYPE))
 (17 17 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->A-OF-WRITE-WITH-MASK))
 (16 4 (:REWRITE X86ISA::MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIRECTORY-SYSTEM-LEVEL-NON-MARKING-VIEW))
 (12 4 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE-IN-APP-VIEW))
 (10 10 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS->PAGE-OF-WRITE-WITH-MASK))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::N01P-ACCESSED-BIT))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-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::ACCESSED-BIT))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (8 8 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (8 4 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE BITOPS::SIGNED-BYTE-P-OF-LOGHEAD))
 (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::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-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))
 (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-DIR-PTR-TABLE-CONG)
(X86ISA::XLATE-EQUIV-MEMORY-AND-MV-NTH-1-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE-CONG)
(X86ISA::XLATE-EQUIV-STRUCTURES-AND-MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE
 (10556 1732 (:REWRITE LOGHEAD-IDENTITY))
 (8650 620 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (6357 955 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (5548 292 (:LINEAR LOGHEAD-UPPER-BOUND))
 (3650 292 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (2904 2061 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (2863 2863 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (2382 462 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (2382 462 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (2186 2186 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (2044 2044 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (1917 729 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (1717 17 (:DEFINITION X86ISA::OPEN-QWORD-PADDR-LIST))
 (1603 727 (:REWRITE LOGEXT-IDENTITY))
 (1421 953 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (955 955 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (955 955 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (935 119 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (924 924 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (924 924 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (924 462 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (924 462 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (894 894 (:TYPE-PRESCRIPTION X86ISA::N64P-XR-CTR))
 (892 148 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (867 17 (:DEFINITION BINARY-APPEND))
 (862 582 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (833 34 (:DEFINITION X86ISA::ADDR-RANGE))
 (730 146 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (680 680 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (680 34 (:DEFINITION INTEGER-LISTP))
 (582 582 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (582 582 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (572 32 (:REWRITE X86ISA::PAGE-PRESENT=0-AND-PAGING-ENTRY-NO-PAGE-FAULT-P))
 (510 17 (:REWRITE X86ISA::CAR-ADDR-RANGE))
 (494 494 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (468 468 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (444 444 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (343 47 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (296 296 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (296 296 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (296 296 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (296 296 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (292 292 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (292 146 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (274 274 (:TYPE-PRESCRIPTION X86ISA::N64P-XR-MSR))
 (272 272 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (272 68 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (272 34 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (255 55 (:REWRITE ASH-0))
 (240 240 (:TYPE-PRESCRIPTION X86ISA::PAGE-PRESENT))
 (240 240 (:TYPE-PRESCRIPTION X86ISA::N01P-PAGE-PRESENT))
 (230 28 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (230 28 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (230 28 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (230 28 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (230 28 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (211 97 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (192 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR4BITS-P))
 (192 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-22BITS-P))
 (180 60 (:LINEAR X86ISA::N01P-PAGE-PRESENT))
 (158 14 (:REWRITE X86ISA::PAGE-DIRECTORY-LOWER-12-BITS-ERROR))
 (148 148 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (148 148 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (144 144 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS->PD$INLINE))
 (140 20 (:REWRITE ZIP-OPEN))
 (130 130 (:REWRITE X86ISA::SEGMENT-SELECTORBITS->RPL-OF-WRITE-WITH-MASK))
 (130 130 (:REWRITE X86ISA::RFLAGSBITS->AC-OF-WRITE-WITH-MASK))
 (130 130 (:REWRITE X86ISA::IA32_EFERBITS->NXE-OF-WRITE-WITH-MASK))
 (130 130 (:REWRITE X86ISA::CR4BITS->SMEP-OF-WRITE-WITH-MASK))
 (130 130 (:REWRITE X86ISA::CR4BITS->SMAP-OF-WRITE-WITH-MASK))
 (130 130 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 (130 130 (:REWRITE X86ISA::CR0BITS->WP-OF-WRITE-WITH-MASK))
 (107 69 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-DIRECTORY-IN-APP-VIEW))
 (105 105 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (105 105 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (105 105 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (105 105 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (105 105 (:REWRITE CONSP-BY-LEN))
 (102 102 (:TYPE-PRESCRIPTION X86ISA::TRUE-LISTP-ADDR-RANGE))
 (102 102 (:TYPE-PRESCRIPTION X86ISA::CONSP-ADDR-RANGE))
 (102 68 (:REWRITE DEFAULT-CDR))
 (102 51 (:REWRITE X86ISA::MEMBER-P-CDR))
 (68 68 (:REWRITE X86ISA::NEG-ADDR-RANGE=NIL))
 (68 34 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (68 34 (:REWRITE DEFAULT-+-2))
 (68 30 (:REWRITE X86ISA::MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIRECTORY-SYSTEM-LEVEL-NON-MARKING-VIEW))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (56 56 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (56 28 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (56 28 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (56 28 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (56 28 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (56 28 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (53 53 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS->PD-OF-WRITE-WITH-MASK))
 (51 51 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (51 51 (:REWRITE DEFAULT-CAR))
 (51 51 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (50 6 (:REWRITE UNSIGNED-BYTE-P-OF-ASH))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::CR4BITS-P$INLINE))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::22BITS-P))
 (48 24 (:REWRITE X86ISA::CR4BITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::22BITS-P-WHEN-UNSIGNED-BYTE-P))
 (47 47 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (47 47 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (39 23 (:REWRITE X86ISA::XLATE-EQUIV-MEMORY-WITH-MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIRECTORY))
 (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-DATA-SEGMENT-DESCRIPTORBITS-P))
 (38 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (36 6 (:REWRITE BITOPS::CANCEL-LOGEXT-UNDER-LOGHEAD))
 (34 34 (:REWRITE X86ISA::MEMBER-P-AND-MULT-8-QWORD-PADDR-LISTP))
 (34 34 (:REWRITE DEFAULT-+-1))
 (34 17 (:REWRITE X86ISA::CDR-ADDR-RANGE))
 (32 32 (:REWRITE X86ISA::MV-NTH-0-PAGING-ENTRY-NO-PAGE-FAULT-P-AND-SIMILAR-ENTRIES))
 (26 26 (:REWRITE X86ISA::ACCESSED-BIT-SET-ACCESSED-BIT-IDENTITY))
 (26 6 (:REWRITE X86ISA::PAGE-DIRECTORY-LOWER-12-BITS-VALUE-OF-ADDRESS-WHEN-ERROR))
 (26 6 (:REWRITE X86ISA::PAGE-DIRECTORY-LOWER-12-BITS))
 (26 4 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-2BITS-P))
 (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))
 (20 20 (:TYPE-PRESCRIPTION ZIP))
 (17 17 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::64-BIT-MODEP))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (16 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (14 2 (:REWRITE X86ISA::LOGEXT-LOGHEAD-IDENTITY))
 (14 2 (:REWRITE X86ISA::2BITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 12 (:REWRITE BITOPS::LOGHEAD-OF-0-I))
 (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::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::DATA-SEGMENT-DESCRIPTORBITS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-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::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (8 4 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::N52P-MV-NTH-1-IA32E-LA-TO-PA-PAGE-DIRECTORY))
 (6 6 (:TYPE-PRESCRIPTION LOGEXT-TYPE))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::2BITS-P))
 (6 2 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-DIR-PTR-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::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTORBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::16BITS-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 X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE BITOPS::SIGNED-BYTE-P-OF-LOGHEAD))
 (4 2 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CALL-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 2 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS->PAGE-OF-WRITE-WITH-MASK))
 )
(X86ISA::XLATE-EQUIV-STRUCTURES-AND-TWO-MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE-CONG)
(X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-WITH-MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE
 (13119 585 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (11370 550 (:LINEAR LOGHEAD-UPPER-BOUND))
 (9294 858 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (5700 456 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (4140 774 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (4140 774 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (3661 121 (:REWRITE ASH-0))
 (3600 180 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (3480 588 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (3261 93 (:REWRITE ZIP-OPEN))
 (3157 2224 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (2798 2798 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (2224 2224 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (2101 733 (:REWRITE LOGEXT-IDENTITY))
 (2069 2069 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1828 118 (:REWRITE LOGTAIL-IDENTITY))
 (1716 408 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (1548 1548 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (1548 1548 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (1548 774 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1548 774 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (1437 855 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (1406 1406 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (1392 231 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (1022 580 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (996 996 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (858 858 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (858 858 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (697 697 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (668 38 (:REWRITE X86ISA::PAGE-PRESENT=0-AND-PAGING-ENTRY-NO-PAGE-FAULT-P))
 (639 71 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (582 582 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (580 580 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (580 580 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (464 464 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (464 464 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (464 464 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (464 464 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (416 208 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (396 198 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (390 390 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (360 16 (:REWRITE X86ISA::PAGE-DIRECTORY-LOWER-12-BITS-ERROR))
 (255 255 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (213 213 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (210 70 (:LINEAR X86ISA::N01P-PAGE-PRESENT))
 (178 89 (:REWRITE X86ISA::MEMBER-P-CDR))
 (101 101 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (93 93 (:TYPE-PRESCRIPTION ZIP))
 (92 50 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-DIRECTORY-IN-APP-VIEW))
 (89 89 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (71 71 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (71 71 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (71 71 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (71 71 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (71 71 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (71 71 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (71 71 (:REWRITE CONSP-BY-LEN))
 (64 8 (:REWRITE BITOPS::CANCEL-LOGEXT-UNDER-LOGHEAD))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (57 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (52 10 (:REWRITE X86ISA::PAGE-DIRECTORY-LOWER-12-BITS-VALUE-OF-ADDRESS-WHEN-ERROR))
 (52 8 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (48 10 (:REWRITE X86ISA::PAGE-DIRECTORY-LOWER-12-BITS))
 (40 20 (:REWRITE X86ISA::LOGHEAD-ASH-0))
 (39 6 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-2BITS-P))
 (38 38 (:REWRITE X86ISA::MV-NTH-0-PAGING-ENTRY-NO-PAGE-FAULT-P-AND-SIMILAR-ENTRIES))
 (34 10 (:REWRITE X86ISA::XR-AND-IA32E-LA-TO-PA-PAGE-DIRECTORY-IN-NON-MARKING-VIEW))
 (33 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (33 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTORBITS-P))
 (33 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P))
 (33 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (33 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTORBITS-P))
 (33 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (32 14 (:REWRITE X86ISA::MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIRECTORY-SYSTEM-LEVEL-NON-MARKING-VIEW))
 (30 14 (:REWRITE X86ISA::XLATE-EQUIV-MEMORY-WITH-MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIRECTORY))
 (30 12 (:REWRITE X86ISA::DIRTY-BIT-SET-DIRTY-BIT-IDENTITY))
 (24 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (24 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (24 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (24 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (24 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (24 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (24 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (24 3 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (22 22 (:TYPE-PRESCRIPTION X86ISA::N52P-MV-NTH-1-IA32E-LA-TO-PA-PAGE-DIRECTORY))
 (22 22 (:REWRITE X86ISA::ACCESSED-BIT-SET-ACCESSED-BIT-IDENTITY))
 (21 21 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIRECTORY-ENTRY-ADDR))
 (21 3 (:REWRITE X86ISA::LOGEXT-LOGHEAD-IDENTITY))
 (21 3 (:REWRITE X86ISA::2BITS-P-WHEN-UNSIGNED-BYTE-P))
 (20 20 (:TYPE-PRESCRIPTION BITP-LOGHEAD-1))
 (17 17 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-DIRECTORY-ENTRY-ADDR))
 (16 16 (:TYPE-PRESCRIPTION BITP))
 (16 16 (:TYPE-PRESCRIPTION X86ISA::64-BIT-MODEP))
 (16 8 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (14 2 (:REWRITE X86ISA::LOGHEAD-UNEQUAL))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-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::EVEX-PREFIXES-P$INLINE))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (12 12 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (12 12 (:REWRITE BITOPS::LOGHEAD-OF-0-I))
 (12 6 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::IA32E-PML4EBITS-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 X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (12 6 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (9 9 (:TYPE-PRESCRIPTION X86ISA::2BITS-P))
 (9 3 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE-IN-APP-VIEW))
 (8 8 (:TYPE-PRESCRIPTION LOGEXT-TYPE))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTORBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTORBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (6 6 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (6 6 (:REWRITE X86ISA::DIRTY-BIT-SET-ACCESSED-BIT))
 (6 3 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE BITOPS::SIGNED-BYTE-P-OF-LOGHEAD))
 (6 3 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::CALL-GATE-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (6 3 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 (3 3 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS->PAGE-OF-WRITE-WITH-MASK))
 (2 2 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS->PD-OF-WRITE-WITH-MASK))
 )
(X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-WITH-TWO-MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE
 (1744 132 (:REWRITE LOGHEAD-IDENTITY))
 (1224 56 (:LINEAR LOGHEAD-UPPER-BOUND))
 (1192 24 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (1096 20 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (808 8 (:DEFINITION X86ISA::OPEN-QWORD-PADDR-LIST))
 (760 20 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (640 32 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (640 16 (:REWRITE ASH-0))
 (576 16 (:REWRITE ZIP-OPEN))
 (528 528 (:TYPE-PRESCRIPTION LOGHEAD-TYPE))
 (520 72 (:REWRITE IFIX-WHEN-INTEGERP))
 (516 84 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (500 40 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (440 56 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (428 76 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (428 76 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (408 8 (:DEFINITION BINARY-APPEND))
 (392 16 (:DEFINITION X86ISA::ADDR-RANGE))
 (320 320 (:TYPE-PRESCRIPTION X86ISA::N64P-RM-LOW-64))
 (320 16 (:REWRITE LOGTAIL-IDENTITY))
 (320 16 (:DEFINITION INTEGER-LISTP))
 (276 172 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (264 52 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (240 8 (:REWRITE X86ISA::MULTIPLE-OF-8-DISJOINT-WITH-ADDR-RANGE-AND-OPEN-QWORD-PADDR-LIST-TO-MEMBER-P))
 (240 8 (:REWRITE X86ISA::CAR-ADDR-RANGE))
 (196 36 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (180 20 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (172 172 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (172 172 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (160 160 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (156 36 (:REWRITE LOGEXT-IDENTITY))
 (152 152 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (152 152 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (152 76 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (152 76 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (152 72 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (140 140 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (136 136 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (136 136 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (128 128 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (128 32 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (128 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (120 20 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (116 116 (:TYPE-PRESCRIPTION NFIX))
 (68 34 (:DEFINITION X86ISA::APP-VIEW))
 (64 32 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (60 60 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (56 40 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (56 24 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (54 18 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE-IN-APP-VIEW))
 (52 52 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (52 52 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (52 52 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (52 52 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (52 52 (:REWRITE CONSP-BY-LEN))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::TRUE-LISTP-ADDR-RANGE))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::CONSP-ADDR-RANGE))
 (48 32 (:REWRITE DEFAULT-CDR))
 (48 16 (:REWRITE X86ISA::MEMBER-P-AND-MULT-8-QWORD-PADDR-LISTP))
 (40 40 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (40 40 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (40 40 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (40 40 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (40 20 (:REWRITE UNSIGNED-BYTE-P-OF-LOGHEAD))
 (40 20 (:REWRITE X86ISA::MEMBER-P-CDR))
 (34 34 (:DEFINITION X86ISA::APP-VIEW$A))
 (32 32 (:REWRITE X86ISA::NEG-ADDR-RANGE=NIL))
 (32 16 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (32 16 (:REWRITE DEFAULT-+-2))
 (28 20 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (28 20 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::NATP-PAGE-DIRECTORY-ENTRY-ADDR))
 (24 24 (:TYPE-PRESCRIPTION X86ISA::NATP-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (24 24 (:REWRITE X86ISA::MULT-8-QWORD-PADDR-LISTP-GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (24 24 (:REWRITE DEFAULT-CAR))
 (24 24 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (24 24 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (20 20 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (20 20 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (20 20 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (20 20 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (20 20 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (20 20 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (20 20 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (20 20 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (20 16 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (16 16 (:TYPE-PRESCRIPTION ZIP))
 (16 16 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (16 16 (:REWRITE DEFAULT-+-1))
 (16 8 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P-PHYSICAL-ADDRESS-LISTP))
 (16 8 (:REWRITE X86ISA::CDR-ADDR-RANGE))
 (12 12 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::PHYSICAL-ADDRESS-P$INLINE))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::DISJOINT-P))
 (8 8 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (4 4 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIRECTORY-ENTRY-ADDR))
 (4 4 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (4 4 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-DIRECTORY-ENTRY-ADDR))
 )
(X86ISA::XLATE-EQUIV-MEMORY-WITH-MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE
 (1968 158 (:REWRITE LOGHEAD-IDENTITY))
 (1448 26 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (1394 66 (:LINEAR LOGHEAD-UPPER-BOUND))
 (988 26 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (650 52 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (608 608 (:TYPE-PRESCRIPTION LOGHEAD-TYPE))
 (584 584 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (560 28 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (560 14 (:REWRITE ASH-0))
 (504 14 (:REWRITE ZIP-OPEN))
 (502 92 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (502 92 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (494 82 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (318 210 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (280 280 (:TYPE-PRESCRIPTION X86ISA::N64P-RM-LOW-64))
 (280 14 (:REWRITE LOGTAIL-IDENTITY))
 (252 44 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (248 54 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (210 210 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (206 206 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (200 44 (:REWRITE LOGEXT-IDENTITY))
 (184 184 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (184 184 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (184 92 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (184 92 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (174 174 (:TYPE-PRESCRIPTION NFIX))
 (174 174 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (162 18 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (158 158 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (156 26 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (136 136 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (96 52 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (78 78 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (56 28 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (56 28 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (56 28 (:REWRITE IFIX-WHEN-INTEGERP))
 (54 54 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (52 52 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (52 52 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (52 52 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (52 52 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (52 26 (:REWRITE UNSIGNED-BYTE-P-OF-LOGHEAD))
 (48 26 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (36 18 (:REWRITE X86ISA::MEMBER-P-CDR))
 (26 26 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (26 26 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (26 26 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (26 26 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (26 26 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (26 26 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (26 26 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (23 14 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (22 22 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (18 18 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (18 18 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (18 18 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (18 18 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (18 18 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (18 18 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (18 18 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (18 18 (:REWRITE CONSP-BY-LEN))
 (14 14 (:TYPE-PRESCRIPTION ZIP))
 (11 11 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (9 9 (:TYPE-PRESCRIPTION IFIX))
 (8 8 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (6 4 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIRECTORY-ENTRY-ADDR))
 (6 4 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (4 2 (:DEFINITION X86ISA::MARKING-VIEW))
 (3 3 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-DIRECTORY-ENTRY-ADDR))
 (3 1 (:REWRITE X86ISA::XR-AND-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE-IN-NON-MARKING-VIEW))
 (3 1 (:REWRITE X86ISA::MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIR-PTR-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-DIR-PTR-TABLE
 (9926 812 (:REWRITE LOGHEAD-IDENTITY))
 (9581 153 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (7000 144 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (6992 328 (:LINEAR LOGHEAD-UPPER-BOUND))
 (6586 62 (:DEFINITION X86ISA::OPEN-QWORD-PADDR-LIST))
 (4806 144 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (4054 462 (:REWRITE IFIX-WHEN-INTEGERP))
 (3734 434 (:REWRITE INTEGERP-OF-CAR-WHEN-INTEGER-LISTP))
 (3324 62 (:DEFINITION BINARY-APPEND))
 (3200 124 (:DEFINITION X86ISA::ADDR-RANGE))
 (3150 252 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (3090 3090 (:TYPE-PRESCRIPTION LOGHEAD-TYPE))
 (3052 88 (:REWRITE ASH-0))
 (3040 152 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (2736 76 (:REWRITE ZIP-OPEN))
 (2606 430 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (2588 124 (:DEFINITION INTEGER-LISTP))
 (2498 454 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (2498 454 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (2022 62 (:REWRITE X86ISA::CAR-ADDR-RANGE))
 (1912 62 (:REWRITE X86ISA::MULTIPLE-OF-8-DISJOINT-WITH-ADDR-RANGE-AND-OPEN-QWORD-PADDR-LIST-TO-MEMBER-P))
 (1644 1064 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (1532 1532 (:TYPE-PRESCRIPTION X86ISA::N64P-RM-LOW-64))
 (1532 88 (:REWRITE LOGTAIL-IDENTITY))
 (1316 278 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (1295 1295 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (1248 240 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (1138 1138 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1094 462 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (1091 155 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (1064 1064 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (996 240 (:REWRITE LOGEXT-IDENTITY))
 (992 992 (:TYPE-PRESCRIPTION INTEGER-LISTP))
 (992 248 (:REWRITE INTEGER-LISTP-WHEN-NOT-CONSP))
 (992 124 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (908 908 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (908 908 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (908 454 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (908 454 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (890 890 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (884 884 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (808 808 (:TYPE-PRESCRIPTION NFIX))
 (756 126 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (708 708 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (430 252 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (378 378 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (372 372 (:TYPE-PRESCRIPTION X86ISA::TRUE-LISTP-ADDR-RANGE))
 (372 372 (:TYPE-PRESCRIPTION X86ISA::CONSP-ADDR-RANGE))
 (372 248 (:REWRITE DEFAULT-CDR))
 (372 124 (:REWRITE X86ISA::MEMBER-P-AND-MULT-8-QWORD-PADDR-LISTP))
 (365 365 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (365 365 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (365 365 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (365 365 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (365 365 (:REWRITE CONSP-BY-LEN))
 (346 173 (:REWRITE X86ISA::MEMBER-P-CDR))
 (328 164 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (252 252 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (252 252 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (252 252 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (252 252 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (252 126 (:REWRITE UNSIGNED-BYTE-P-OF-LOGHEAD))
 (248 248 (:REWRITE X86ISA::NEG-ADDR-RANGE=NIL))
 (248 124 (:REWRITE INTEGER-LISTP-OF-CDR-WHEN-INTEGER-LISTP))
 (248 124 (:REWRITE DEFAULT-+-2))
 (240 240 (:TYPE-PRESCRIPTION X86ISA::NATP-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (234 117 (:DEFINITION X86ISA::MARKING-VIEW))
 (233 144 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (233 144 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (216 72 (:REWRITE X86ISA::XR-AND-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE-IN-NON-MARKING-VIEW))
 (186 186 (:REWRITE X86ISA::MULT-8-QWORD-PADDR-LISTP-GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (186 186 (:REWRITE DEFAULT-CAR))
 (186 186 (:REWRITE CONSP-OF-CDR-BY-LEN))
 (178 178 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (173 173 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (162 72 (:REWRITE X86ISA::MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE-SYSTEM-LEVEL-NON-MARKING-VIEW))
 (155 155 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (155 155 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (153 153 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (144 144 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (144 144 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (144 144 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (132 132 (:TYPE-PRESCRIPTION X86ISA::NATP-PAGE-DIRECTORY-ENTRY-ADDR))
 (131 88 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (126 126 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (126 126 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (124 124 (:REWRITE DEFAULT-+-1))
 (124 62 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P-PHYSICAL-ADDRESS-LISTP))
 (124 62 (:REWRITE X86ISA::CDR-ADDR-RANGE))
 (117 117 (:DEFINITION X86ISA::MARKING-VIEW$A))
 (76 76 (:TYPE-PRESCRIPTION ZIP))
 (72 72 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (62 62 (:TYPE-PRESCRIPTION X86ISA::PHYSICAL-ADDRESS-P$INLINE))
 (62 62 (:TYPE-PRESCRIPTION X86ISA::MEMBER-P-PHYSICAL-ADDRESS-P))
 (62 62 (:TYPE-PRESCRIPTION X86ISA::DISJOINT-P))
 (57 57 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (16 16 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-DIRECTORY-ENTRY-ADDR))
 )
(X86ISA::TWO-PAGE-DIR-PTR-TABLE-WALKS-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE
 (436 33 (:REWRITE LOGHEAD-IDENTITY))
 (306 14 (:LINEAR LOGHEAD-UPPER-BOUND))
 (274 5 (:REWRITE X86ISA::4K-ALIGNED-PHYSICAL-ADDRESS-HELPER))
 (190 5 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (160 8 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (160 4 (:REWRITE ASH-0))
 (144 4 (:REWRITE ZIP-OPEN))
 (130 130 (:TYPE-PRESCRIPTION LOGHEAD-TYPE))
 (129 21 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-PREFIXES-P))
 (125 10 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (107 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (107 19 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::N64P-RM-LOW-64))
 (80 4 (:REWRITE LOGTAIL-IDENTITY))
 (69 43 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (66 13 (:REWRITE X86ISA::PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (49 9 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-AND-LOGEXT-48))
 (43 43 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (41 41 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (40 40 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (39 9 (:REWRITE LOGEXT-IDENTITY))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (38 38 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (38 19 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (38 19 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (34 34 (:TYPE-PRESCRIPTION X86ISA::PREFIXES-P$INLINE))
 (32 32 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (30 5 (:DEFINITION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (29 29 (:TYPE-PRESCRIPTION NFIX))
 (27 3 (:REWRITE X86ISA::MEMBER-P-OF-NOT-A-CONSP))
 (24 18 (:REWRITE X86ISA::IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE-IN-APP-VIEW))
 (16 8 (:TYPE-PRESCRIPTION BITOPS::LOGTAIL-NATP))
 (16 8 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (16 8 (:REWRITE IFIX-WHEN-INTEGERP))
 (15 15 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (14 10 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (14 7 (:DEFINITION X86ISA::APP-VIEW))
 (14 6 (:REWRITE X86ISA::RM-LOW-64-IN-APP-VIEW))
 (10 10 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
 (10 10 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
 (10 10 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (10 10 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (10 5 (:REWRITE UNSIGNED-BYTE-P-OF-LOGHEAD))
 (9 9 (:TYPE-PRESCRIPTION X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES))
 (7 7 (:DEFINITION X86ISA::APP-VIEW$A))
 (7 5 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (7 5 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (6 6 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AUX-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (6 6 (:REWRITE X86ISA::ALL-MEM-EXCEPT-PAGING-STRUCTURES-EQUAL-AND-RM-LOW-64-FROM-REST-OF-MEMORY))
 (6 3 (:REWRITE X86ISA::MEMBER-P-CDR))
 (5 5 (:TYPE-PRESCRIPTION X86ISA::CANONICAL-ADDRESS-P$INLINE))
 (5 5 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (5 5 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (5 5 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (5 5 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
 (5 4 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (4 4 (:TYPE-PRESCRIPTION ZIP))
 (4 4 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (3 3 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (3 3 (:REWRITE X86ISA::SUBSET-P-CONS-MEMBER-P-LEMMA))
 (3 3 (:REWRITE X86ISA::NOT-MEMBER-P-WHEN-DISJOINT-P))
 (3 3 (:REWRITE X86ISA::MEMBER-P-OF-SUBSET-IS-MEMBER-P-OF-SUPERSET))
 (3 3 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 2))
 (3 3 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-PREFIXMAP-P . 1))
 (3 3 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 2))
 (3 3 (:REWRITE VL::CONSP-WHEN-MEMBER-EQUAL-OF-VL-NAMEDB-NAMESET-P . 1))
 (3 3 (:REWRITE CONSP-BY-LEN))
 (2 2 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-IMPLIES-XLATE-EQUIV-ENTRIES))
 (1 1 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIRECTORY-ENTRY-ADDR))
 (1 1 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-XLATE-EQUIV-ENTRIES-RM-LOW-64-WITH-PAGE-DIR-PTR-TABLE-ENTRY-ADDR))
 (1 1 (:REWRITE X86ISA::XLATE-EQUIV-STRUCTURES-AND-LOGTAIL-12-RM-LOW-64-WITH-PAGE-DIRECTORY-ENTRY-ADDR))
 )
(X86ISA::GATHER-ALL-PAGING-STRUCTURE-QWORD-ADDRESSES-MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE
 (3 1 (:REWRITE X86ISA::XLATE-EQUIV-MEMORY-WITH-MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE))
 (3 1 (:REWRITE X86ISA::MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIR-PTR-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-DIR-PTR-TABLE
 (9 9 (:REWRITE X86ISA::XLATE-EQUIV-ENTRIES-AT-QWORD-ADDRESSES-TRANSITIVE))
 (9 3 (:REWRITE X86ISA::MV-NTH-2-IA32E-LA-TO-PA-PAGE-DIR-PTR-TABLE-SYSTEM-LEVEL-NON-MARKING-VIEW))
 (6 3 (:DEFINITION X86ISA::MARKING-VIEW))
 (3 3 (:DEFINITION X86ISA::MARKING-VIEW$A))
 )