File: paging-basics%40useless-runes.lsp

package info (click to toggle)
acl2 8.5dfsg-5
links: PTS
area: main
in suites: bookworm
size: 991,452 kB
sloc: lisp: 15,567,759; javascript: 22,820; cpp: 13,929; ansic: 12,092; perl: 7,150; java: 4,405; xml: 3,884; makefile: 3,507; sh: 3,187; ruby: 2,633; ml: 763; python: 746; yacc: 723; awk: 295; csh: 186; php: 171; lex: 154; tcl: 49; asm: 23; haskell: 17
file content (1518 lines) | stat: -rw-r--r-- 83,176 bytes
(X86ISA::LOGHEAD-1-BOOL->BIT-RULE
 (20 2 (:LINEAR LOGHEAD-UPPER-BOUND))
 (6 3 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (3 3 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (3 3 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 )
(X86ISA::LOW-3-BITS-0-ADD-7-PRESERVE-BOUND
 (618 618 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (618 618 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (618 618 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (503 9 (:REWRITE CANCEL-MOD-+))
 (270 54 (:TYPE-PRESCRIPTION MOD-ZERO . 2))
 (255 38 (:REWRITE INTEGERP-MINUS-X))
 (234 167 (:REWRITE DEFAULT-TIMES-2))
 (217 9 (:REWRITE MOD-X-Y-=-X . 4))
 (216 9 (:REWRITE MOD-X-Y-=-X . 3))
 (210 9 (:REWRITE MOD-X-Y-=-X+Y . 2))
 (208 9 (:REWRITE MOD-ZERO . 3))
 (198 54 (:TYPE-PRESCRIPTION MOD-POSITIVE . 2))
 (198 54 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 2))
 (176 167 (:REWRITE DEFAULT-TIMES-1))
 (161 18 (:REWRITE |(* (- x) y)|))
 (138 9 (:REWRITE MOD-X-Y-=-X-Y . 2))
 (127 107 (:TYPE-PRESCRIPTION NOT-INTEGERP-4A))
 (110 9 (:REWRITE MOD-ZERO . 4))
 (107 107 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (107 107 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (107 107 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (106 12 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (106 12 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (105 9 (:REWRITE DEFAULT-MOD-RATIO))
 (96 3 (:REWRITE MOD-X-Y-=-X-Y . 1))
 (94 18 (:REWRITE DEFAULT-MINUS))
 (92 17 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (85 18 (:REWRITE |(- (* c x))|))
 (82 82 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (78 3 (:REWRITE MOD-ZERO . 1))
 (71 3 (:LINEAR MOD-BOUNDS-3))
 (70 4 (:REWRITE IFIX-NEGATIVE-TO-NEGP))
 (66 2 (:REWRITE IFIX-POSITIVE-TO-NON-ZP))
 (62 4 (:REWRITE NEGP-WHEN-INTEGERP))
 (62 2 (:REWRITE ZP-WHEN-INTEGERP))
 (54 54 (:TYPE-PRESCRIPTION MOD-ZERO . 3))
 (54 54 (:TYPE-PRESCRIPTION MOD-POSITIVE . 1))
 (54 54 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 1))
 (53 53 (:TYPE-PRESCRIPTION MOD-NONPOSITIVE))
 (53 53 (:TYPE-PRESCRIPTION INTEGERP-MOD-2))
 (49 47 (:REWRITE DEFAULT-PLUS-1))
 (49 41 (:REWRITE DEFAULT-LESS-THAN-1))
 (49 9 (:REWRITE MOD-X-Y-=-X . 2))
 (49 9 (:REWRITE |(mod (+ x (mod a b)) y)|))
 (49 9 (:REWRITE |(mod (+ x (- (mod a b))) y)|))
 (49 3 (:REWRITE MOD-X-Y-=-X+Y . 1))
 (47 47 (:REWRITE DEFAULT-PLUS-2))
 (47 9 (:REWRITE MOD-X-Y-=-X-Y . 3))
 (47 9 (:REWRITE MOD-X-Y-=-X+Y . 3))
 (47 9 (:REWRITE MOD-CANCEL-*-REWRITING-GOAL-LITERAL))
 (47 9 (:REWRITE MOD-CANCEL-*-CONST))
 (47 9 (:REWRITE |(mod (* x (/ y)) z) rewriting-goal-literal|))
 (43 41 (:REWRITE DEFAULT-LESS-THAN-2))
 (41 41 (:REWRITE THE-FLOOR-BELOW))
 (41 41 (:REWRITE THE-FLOOR-ABOVE))
 (41 31 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (39 3 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (38 36 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (34 34 (:REWRITE CONSTANT-<-INTEGERP))
 (34 34 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (34 34 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (34 34 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (34 34 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (34 34 (:REWRITE |(< c (- x))|))
 (34 34 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (34 34 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (34 34 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (34 34 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (34 34 (:REWRITE |(< (/ x) (/ y))|))
 (34 34 (:REWRITE |(< (- x) c)|))
 (34 34 (:REWRITE |(< (- x) (- y))|))
 (32 6 (:LINEAR MOD-BOUNDS-2))
 (30 1 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (30 1 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (29 29 (:REWRITE REDUCE-INTEGERP-+))
 (29 29 (:META META-INTEGERP-CORRECT))
 (27 3 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (27 3 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (21 21 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (17 17 (:TYPE-PRESCRIPTION RATIONALP-MOD))
 (17 17 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (15 3 (:TYPE-PRESCRIPTION FLOOR-ZERO . 4))
 (15 3 (:TYPE-PRESCRIPTION FLOOR-ZERO . 3))
 (15 3 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (15 3 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (15 3 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (15 3 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (15 3 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (15 3 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (15 3 (:REWRITE MOD-ZERO . 2))
 (13 13 (:REWRITE |(equal c (/ x))|))
 (13 13 (:REWRITE |(equal (/ x) (/ y))|))
 (13 13 (:REWRITE |(equal (- x) (- y))|))
 (12 12 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (12 12 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (12 12 (:REWRITE |(equal c (- x))|))
 (12 12 (:REWRITE |(equal (- x) c)|))
 (11 9 (:REWRITE DEFAULT-MOD-1))
 (9 9 (:REWRITE THIS-NEEDS-TO-BE-ADDED-TO-QUOTIENT-REMAINDER-LEMMAS))
 (9 9 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (9 9 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (9 9 (:REWRITE MOD-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (9 9 (:REWRITE DEFAULT-MOD-2))
 (9 9 (:REWRITE |(mod x (- y))| . 3))
 (9 9 (:REWRITE |(mod x (- y))| . 2))
 (9 9 (:REWRITE |(mod x (- y))| . 1))
 (9 9 (:REWRITE |(mod x (* y (/ z))) rewriting-goal-literal|))
 (9 9 (:REWRITE |(mod x (* y (/ z))) not rewriting-goal-literal|))
 (9 9 (:REWRITE |(mod (- x) y)| . 3))
 (9 9 (:REWRITE |(mod (- x) y)| . 2))
 (9 9 (:REWRITE |(mod (- x) y)| . 1))
 (9 9 (:REWRITE |(mod (* x (/ y)) z) not rewriting-goal-literal|))
 (9 9 (:REWRITE |(< (/ x) 0)|))
 (9 9 (:REWRITE |(< (* x y) 0)|))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE |(< 0 (* x y))|))
 (6 6 (:REWRITE |(< 0 (/ x))|))
 (6 2 (:REWRITE IFIX-EQUAL-TO-0))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (4 4 (:REWRITE NEGP-WHEN-LESS-THAN-0))
 (3 3 (:REWRITE |(equal (mod (+ x y) z) x)|))
 (2 2 (:TYPE-PRESCRIPTION ZIP))
 (2 2 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (2 2 (:REWRITE ZP-WHEN-GT-0))
 (2 2 (:REWRITE ZIP-OPEN))
 (2 2 (:REWRITE IFIX-EQUAL-TO-NONZERO-CONST))
 (2 2 (:REWRITE IFIX-EQUAL-TO-NONZERO))
 (2 2 (:REWRITE |(< (+ c/d x) y)|))
 (1 1 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (1 1 (:REWRITE DEFAULT-DIVIDE))
 (1 1 (:REWRITE |(not (equal x (/ y)))|))
 (1 1 (:REWRITE |(equal x (/ y))|))
 (1 1 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (1 1 (:REWRITE |(< (+ (- c) x) y)|))
 )
(X86ISA::RM-LOW-64-LOGAND-LOGIOR-HELPER-1
 (88 1 (:REWRITE UNSIGNED-BYTE-P-OF-LOGAND-2))
 (73 13 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (73 13 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (73 13 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (73 13 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (73 13 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (73 13 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (73 13 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (73 13 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (69 2 (:REWRITE DIFFERENCE-UNSIGNED-BYTE-P))
 (48 11 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (48 11 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (48 11 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (24 24 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (20 14 (:REWRITE DEFAULT-<-1))
 (20 8 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (20 8 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (18 18 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (18 18 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (18 18 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (18 18 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (18 18 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (18 18 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (18 18 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (18 18 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (18 9 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (18 9 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (18 9 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (18 9 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (18 9 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (18 9 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (18 9 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (18 9 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (14 14 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (14 14 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (14 14 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (14 14 (:REWRITE DEFAULT-<-2))
 (14 7 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (14 7 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (14 7 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (13 13 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (12 8 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (8 8 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (8 8 (:REWRITE X86ISA::NEGATIVE-LOGAND-TO-POSITIVE-LOGAND-WITH-INTEGERP-X))
 (8 8 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (6 2 (:REWRITE NATP-WHEN-GTE-0))
 (4 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 2 (:TYPE-PRESCRIPTION X86ISA::RM-LOW-64-LOGAND-LOGIOR-HELPER-1))
 (2 2 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (2 2 (:REWRITE NATP-WHEN-INTEGERP))
 )
(X86ISA::PML4-TABLE-BASE-ADDR)
(X86ISA::N52P-OF-PML4-TABLE-BASE-ADDR
 (11 1 (:REWRITE ASH-0))
 (7 1 (:REWRITE ZIP-OPEN))
 (2 1 (:REWRITE RIGHT-SHIFT-TO-LOGTAIL))
 (1 1 (:TYPE-PRESCRIPTION ZIP))
 (1 1 (:TYPE-PRESCRIPTION IFIX))
 (1 1 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (1 1 (:REWRITE X86ISA::CR3BITS->PDB-OF-WRITE-WITH-MASK))
 )
(X86ISA::PML4-TABLE-BASE-ADDR-AND-MV-NTH-1-WB)
(X86ISA::PAGE-DIR-PTR-TABLE-BASE-ADDR)
(X86ISA::PAGE-DIRECTORY-BASE-ADDR)
(X86ISA::PAGE-TABLE-BASE-ADDR)
(X86ISA::LOGHEAD-SMALLER-EQUALITY
 (7429 47 (:REWRITE LOGHEAD-IDENTITY))
 (7352 127 (:DEFINITION UNSIGNED-BYTE-P**))
 (4616 93 (:DEFINITION INTEGER-RANGE-P))
 (4526 105 (:DEFINITION UNSIGNED-BYTE-P))
 (2798 1279 (:TYPE-PRESCRIPTION BITOPS::LOGCDR-NATP))
 (2765 137 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (2567 134 (:REWRITE UNSIGNED-BYTE-P-PLUS))
 (1918 144 (:REWRITE BITOPS::LOGCDR-OF-BIT))
 (1643 53 (:REWRITE BITOPS::LOGCAR-OF-BIT))
 (1345 142 (:REWRITE BITOPS::LOGCDR-<-CONST))
 (1252 1252 (:TYPE-PRESCRIPTION LOGCDR-TYPE))
 (1227 60 (:REWRITE BITOPS::UNSIGNED-BYTE-P-OF-0-X))
 (898 7 (:REWRITE X86ISA::LOGHEAD-UNEQUAL))
 (835 835 (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P))
 (639 362 (:REWRITE DEFAULT-<-1))
 (533 7 (:DEFINITION SIGNED-BYTE-P**))
 (528 528 (:LINEAR BITOPS::LOGCDR-<=-LOGCDR))
 (528 362 (:REWRITE DEFAULT-<-2))
 (437 3 (:REWRITE BITOPS::SIGNED-BYTE-P-OF-LOGCDR))
 (427 7 (:DEFINITION SIGNED-BYTE-P))
 (391 391 (:TYPE-PRESCRIPTION BITP))
 (378 378 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (300 50 (:REWRITE IFIX-NEGATIVE-TO-NEGP))
 (230 78 (:REWRITE ZP-WHEN-GT-0))
 (214 214 (:REWRITE EXPT-WITH-VIOLATED-GUARDS))
 (204 57 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (160 96 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (156 4 (:REWRITE BFIX-WHEN-NOT-1))
 (150 50 (:REWRITE NEGP-WHEN-LESS-THAN-0))
 (132 4 (:LINEAR BITOPS::LOGCAR-BOUND))
 (127 67 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (119 119 (:REWRITE DEFAULT-+-2))
 (119 119 (:REWRITE DEFAULT-+-1))
 (114 44 (:TYPE-PRESCRIPTION BITOPS::LOGCONS-POSP-1))
 (89 89 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (89 89 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (89 89 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 (88 44 (:TYPE-PRESCRIPTION BITOPS::LOGCONS-POSP-2))
 (81 25 (:REWRITE FOLD-CONSTS-IN-+))
 (73 73 (:LINEAR BITOPS::EXPT-2-LOWER-BOUND-BY-LOGBITP))
 (67 67 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (60 60 (:LINEAR X86ISA::SIGNED-BYTE-P-OF-TRUNCATE-WHEN-Y-IS-POSITIVE))
 (60 60 (:LINEAR X86ISA::SIGNED-BYTE-P-OF-TRUNCATE-WHEN-Y-IS-NEGATIVE))
 (60 60 (:LINEAR X86ISA::SIGNED-BYTE-P-OF-TRUNCATE))
 (60 60 (:LINEAR X86ISA::SIGNED-BYTE-P-OF-REM))
 (52 52 (:TYPE-PRESCRIPTION BIT->BOOL$INLINE))
 (50 50 (:TYPE-PRESCRIPTION NEGP))
 (50 50 (:REWRITE NEGP-WHEN-INTEGERP))
 (49 7 (:REWRITE POSP-REDEFINITION))
 (44 44 (:TYPE-PRESCRIPTION POSP))
 (29 29 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (21 7 (:REWRITE DEFAULT-UNARY-MINUS))
 (17 17 (:REWRITE ZP-OPEN))
 (17 17 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (16 16 (:REWRITE NATP-WHEN-INTEGERP))
 (14 14 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (9 3 (:REWRITE IFIX-EQUAL-TO-0))
 (8 4 (:REWRITE BFIX-WHEN-NOT-BITP))
 (8 4 (:REWRITE BFIX-WHEN-NOT-BIT->BOOL))
 (8 4 (:REWRITE BFIX-WHEN-BIT->BOOL))
 (6 6 (:REWRITE IFIX-EQUAL-TO-NONZERO))
 (6 3 (:REWRITE UNICITY-OF-0))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 3 (:TYPE-PRESCRIPTION ZIP))
 (3 3 (:REWRITE ZIP-OPEN))
 (3 3 (:REWRITE IFIX-EQUAL-TO-NONZERO-CONST))
 (3 3 (:DEFINITION FIX))
 (2 2 (:REWRITE BITOPS::LOGCONS-EQUAL-CONSTANT))
 )
(X86ISA::LOGBITP-N-OF-SET-ACCESSED-BIT
 (1606 28 (:REWRITE LOGHEAD-IDENTITY))
 (1100 33 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (690 25 (:REWRITE BITOPS::LOGBITP-NONZERO-OF-BIT))
 (540 17 (:REWRITE BITOPS::LOGBITP-WHEN-BIT))
 (131 118 (:REWRITE DEFAULT-<-1))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (118 118 (:REWRITE DEFAULT-<-2))
 (115 23 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (115 23 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (115 23 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (112 32 (:REWRITE BITOPS::LOGBITP-OF-MASK))
 (93 93 (:TYPE-PRESCRIPTION BITP))
 (92 32 (:REWRITE BITOPS::LOGBITP-OF-CONST))
 (84 31 (:REWRITE BITOPS::LOGBITP-WHEN-BITMASKP))
 (80 20 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
 (74 29 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (65 3 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (59 59 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (57 57 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (50 10 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (48 24 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (46 46 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (46 46 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (46 46 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (46 23 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (46 23 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (46 23 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (43 7 (:REWRITE BITOPS::LOGBITP-OF-LOGHEAD-OUT-OF-BOUNDS))
 (43 7 (:REWRITE BITOPS::LOGBITP-OF-LOGHEAD-IN-BOUNDS))
 (33 33 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (32 32 (:REWRITE BITOPS::NORMALIZE-LOGBITP-WHEN-MODS-EQUAL))
 (32 32 (:REWRITE BITOPS::LOGBITP-OF-NEGATIVE-CONST))
 (31 31 (:REWRITE NFIX-WHEN-NOT-NATP))
 (30 29 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (29 29 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (25 25 (:TYPE-PRESCRIPTION BITOPS::INTEGER-LENGTH-TYPE-PRESCRIPTION-STRONG-NEGATIVE))
 (25 25 (:TYPE-PRESCRIPTION BITOPS::INTEGER-LENGTH-TYPE-PRESCRIPTION-STRONG))
 (25 25 (:TYPE-PRESCRIPTION INTEGER-LENGTH))
 (24 3 (:REWRITE BFIX-WHEN-NOT-1))
 (24 1 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (15 15 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (13 13 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (12 4 (:REWRITE ZP-WHEN-GT-0))
 (11 11 (:REWRITE NATP-WHEN-INTEGERP))
 (10 10 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NATP))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (9 1 (:REWRITE EQUAL-1-OF-BOOL->BIT))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX2-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SIB-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MODR/M-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE3-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-8BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (6 6 (:TYPE-PRESCRIPTION BIT->BOOL$INLINE))
 (6 3 (:REWRITE BFIX-WHEN-NOT-BITP))
 (6 3 (:REWRITE BFIX-WHEN-NOT-BIT->BOOL))
 (6 3 (:REWRITE BFIX-WHEN-BIT->BOOL))
 (5 5 (:TYPE-PRESCRIPTION LOGNOT))
 (5 2 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (5 2 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (4 2 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (3 3 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (3 3 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (3 3 (:REWRITE BITOPS::B-AND-EQUAL-1-IN-HYP))
 (3 1 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX2-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SIB-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MODR/M-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE3-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::8BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX2-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SIB-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MODR/M-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (2 1 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE3-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 )
(X86ISA::LOGBITP-N-OF-SET-DIRTY-BIT
 (1578 26 (:REWRITE LOGHEAD-IDENTITY))
 (1063 28 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (676 24 (:REWRITE BITOPS::LOGBITP-NONZERO-OF-BIT))
 (512 15 (:REWRITE BITOPS::LOGBITP-WHEN-BIT))
 (135 122 (:REWRITE DEFAULT-<-1))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (123 24 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (122 122 (:REWRITE DEFAULT-<-2))
 (115 23 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (115 23 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (115 23 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (110 30 (:REWRITE BITOPS::LOGBITP-OF-MASK))
 (90 30 (:REWRITE BITOPS::LOGBITP-OF-CONST))
 (81 30 (:REWRITE BITOPS::LOGBITP-WHEN-BITMASKP))
 (80 80 (:TYPE-PRESCRIPTION BITP))
 (80 20 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
 (65 3 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (58 24 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (57 57 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (52 52 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (50 10 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (48 48 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (48 24 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (48 24 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (46 46 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (46 46 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (46 46 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (46 23 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (46 23 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (46 23 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (43 7 (:REWRITE BITOPS::LOGBITP-OF-LOGHEAD-OUT-OF-BOUNDS))
 (43 7 (:REWRITE BITOPS::LOGBITP-OF-LOGHEAD-IN-BOUNDS))
 (31 31 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (30 30 (:REWRITE BITOPS::NORMALIZE-LOGBITP-WHEN-MODS-EQUAL))
 (30 30 (:REWRITE BITOPS::LOGBITP-OF-NEGATIVE-CONST))
 (28 28 (:REWRITE NFIX-WHEN-NOT-NATP))
 (28 27 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (27 27 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (25 25 (:TYPE-PRESCRIPTION BITOPS::INTEGER-LENGTH-TYPE-PRESCRIPTION-STRONG-NEGATIVE))
 (25 25 (:TYPE-PRESCRIPTION BITOPS::INTEGER-LENGTH-TYPE-PRESCRIPTION-STRONG))
 (25 25 (:TYPE-PRESCRIPTION INTEGER-LENGTH))
 (24 3 (:REWRITE BFIX-WHEN-NOT-1))
 (24 1 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (13 13 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (12 12 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (11 11 (:REWRITE NATP-WHEN-INTEGERP))
 (10 10 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NATP))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (9 1 (:REWRITE EQUAL-1-OF-BOOL->BIT))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX2-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SIB-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MODR/M-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE3-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-8BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (6 6 (:TYPE-PRESCRIPTION BIT->BOOL$INLINE))
 (6 3 (:REWRITE BFIX-WHEN-NOT-BITP))
 (6 3 (:REWRITE BFIX-WHEN-NOT-BIT->BOOL))
 (6 3 (:REWRITE BFIX-WHEN-BIT->BOOL))
 (5 5 (:TYPE-PRESCRIPTION LOGNOT))
 (5 2 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (5 2 (:REWRITE BITOPS::LOGAND-WITH-BITMASK))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (4 2 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (3 3 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (3 3 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (3 3 (:REWRITE BITOPS::B-AND-EQUAL-1-IN-HYP))
 (3 1 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX2-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SIB-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MODR/M-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE3-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::8BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX2-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SIB-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MODR/M-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (2 1 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE3-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 )
(X86ISA::LOGBITP-N-OF-SET-DIRTY-AND-ACCESSED-BITS
 (240 4 (:REWRITE BITOPS::LOGBITP-NONZERO-OF-BIT))
 (216 4 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (195 5 (:DEFINITION UNSIGNED-BYTE-P))
 (190 5 (:DEFINITION INTEGER-RANGE-P))
 (70 1 (:LINEAR LOGHEAD-UPPER-BOUND))
 (61 7 (:REWRITE X86ISA::ACCESSED-BIT-SET-ACCESSED-BIT-IDENTITY))
 (50 4 (:LINEAR X86ISA::N64P-SET-ACCESSED-BIT))
 (30 30 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS->A$INLINE))
 (30 3 (:REWRITE X86ISA::DIRTY-BIT-SET-DIRTY-BIT-IDENTITY))
 (25 2 (:LINEAR X86ISA::N64P-SET-DIRTY-BIT))
 (15 15 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS->D$INLINE))
 (12 12 (:TYPE-PRESCRIPTION BITP))
 (12 8 (:REWRITE DEFAULT-<-1))
 (12 6 (:DEFINITION X86ISA::ACCESSED-BIT))
 (12 4 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (12 4 (:REWRITE BITOPS::LOGBITP-WHEN-BITMASKP))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (8 8 (:TYPE-PRESCRIPTION BITMASKP$INLINE))
 (8 8 (:REWRITE DEFAULT-<-2))
 (7 1 (:REWRITE BITOPS::LOGBITP-OF-LOGHEAD-OUT-OF-BOUNDS))
 (7 1 (:REWRITE BITOPS::LOGBITP-OF-LOGHEAD-IN-BOUNDS))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::N01P-ACCESSED-BIT))
 (6 6 (:TYPE-PRESCRIPTION X86ISA::ACCESSED-BIT))
 (6 6 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (6 6 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->A-OF-WRITE-WITH-MASK))
 (6 3 (:DEFINITION X86ISA::DIRTY-BIT))
 (5 5 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (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::DATA-SEGMENT-DESCRIPTORBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (4 4 (:REWRITE BITOPS::NORMALIZE-LOGBITP-WHEN-MODS-EQUAL))
 (4 4 (:REWRITE BITOPS::LOGBITP-OF-NEGATIVE-CONST))
 (4 4 (:REWRITE BITOPS::LOGBITP-OF-MASK))
 (4 4 (:REWRITE BITOPS::LOGBITP-OF-CONST))
 (4 4 (:META BITOPS::OPEN-LOGBITP-OF-CONST-LITE-META))
 (4 3 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (4 2 (:REWRITE X86ISA::XCR0BITS-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::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (3 3 (:TYPE-PRESCRIPTION X86ISA::N01P-DIRTY-BIT))
 (3 3 (:TYPE-PRESCRIPTION X86ISA::DIRTY-BIT))
 (3 3 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (3 3 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->D-OF-WRITE-WITH-MASK))
 (2 2 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (2 2 (:REWRITE NFIX-WHEN-NOT-NATP))
 (2 2 (:REWRITE NFIX-WHEN-NATP))
 (2 1 (:REWRITE UNSIGNED-BYTE-P-OF-LOGHEAD))
 (1 1 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 )
(X86ISA::LOGTAIL-N-OF-SET-ACCESSED-BIT
 (8598 44 (:REWRITE LOGHEAD-IDENTITY))
 (7672 114 (:REWRITE UNSIGNED-BYTE-P-PLUS))
 (7615 91 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (7554 51 (:REWRITE BITOPS::LOGBITP-WHEN-BIT))
 (6610 12 (:LINEAR X86ISA::RM-LOW-64-LOGAND-LOGIOR-HELPER-1))
 (6586 12 (:DEFINITION X86ISA::N64P$INLINE))
 (3297 50 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (3210 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (2598 82 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1818 6 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-2))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (954 702 (:REWRITE DEFAULT-<-2))
 (896 702 (:REWRITE DEFAULT-<-1))
 (884 80 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (884 80 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (884 80 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (584 149 (:REWRITE NFIX-WHEN-NOT-NATP))
 (494 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGAND-2))
 (445 28 (:REWRITE LOGTAIL-IDENTITY))
 (440 35 (:REWRITE BITOPS::LOGBITP-NONZERO-OF-BIT))
 (404 82 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (376 68 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (376 68 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (376 68 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (291 291 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (282 47 (:REWRITE IFIX-NEGATIVE-TO-NEGP))
 (253 253 (:TYPE-PRESCRIPTION BITP))
 (244 222 (:REWRITE EXPT-WITH-VIOLATED-GUARDS))
 (215 78 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (208 43 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (176 176 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (171 124 (:REWRITE DEFAULT-+-1))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (160 8 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (158 8 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 2))
 (155 46 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (151 51 (:REWRITE BITOPS::LOGBITP-WHEN-BITMASKP))
 (145 68 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (144 8 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-2))
 (141 47 (:REWRITE NEGP-WHEN-LESS-THAN-0))
 (138 138 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (138 138 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (138 138 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (136 124 (:REWRITE DEFAULT-+-2))
 (136 8 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (134 54 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (113 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGIOR))
 (113 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGAND-1))
 (104 42 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (92 92 (:LINEAR BITOPS::EXPT-2-LOWER-BOUND-BY-LOGBITP))
 (88 8 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (84 42 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (72 6 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-1))
 (56 56 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
 (53 46 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (51 51 (:REWRITE BITOPS::NORMALIZE-LOGBITP-WHEN-MODS-EQUAL))
 (51 51 (:REWRITE BITOPS::LOGBITP-OF-NEGATIVE-CONST))
 (51 51 (:REWRITE BITOPS::LOGBITP-OF-MASK))
 (51 51 (:REWRITE BITOPS::LOGBITP-OF-CONST))
 (47 47 (:TYPE-PRESCRIPTION NEGP))
 (47 47 (:REWRITE NEGP-WHEN-INTEGERP))
 (43 43 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (43 43 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (42 42 (:DEFINITION FIX))
 (34 34 (:TYPE-PRESCRIPTION BIT->BOOL$INLINE))
 (34 17 (:REWRITE BFIX-WHEN-NOT-BIT->BOOL))
 (34 17 (:REWRITE BFIX-WHEN-BIT->BOOL))
 (32 16 (:REWRITE BFIX-WHEN-NOT-BITP))
 (28 28 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NATP))
 (28 28 (:TYPE-PRESCRIPTION BITOPS::LOGAND-NATP-TYPE-1))
 (27 27 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (25 21 (:REWRITE DEFAULT-UNARY-MINUS))
 (24 1 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (13 13 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX2-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SIB-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MODR/M-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE3-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-8BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (7 7 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 (6 6 (:REWRITE BITOPS::B-IOR-EQUAL-1-IN-CONCL))
 (6 6 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGIOR-FOR-NATURALS))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (4 4 (:REWRITE BITOPS::B-AND-EQUAL-1-IN-HYP))
 (4 2 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:LINEAR BITOPS::B-AND-BOUND))
 (3 1 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX2-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SIB-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MODR/M-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE3-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::8BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX2-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SIB-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MODR/M-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE3-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 )
(X86ISA::LOGTAIL-N-OF-SET-DIRTY-BIT
 (8598 44 (:REWRITE LOGHEAD-IDENTITY))
 (7672 114 (:REWRITE UNSIGNED-BYTE-P-PLUS))
 (7615 91 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (7554 51 (:REWRITE BITOPS::LOGBITP-WHEN-BIT))
 (6610 12 (:LINEAR X86ISA::RM-LOW-64-LOGAND-LOGIOR-HELPER-1))
 (6586 12 (:DEFINITION X86ISA::N64P$INLINE))
 (3297 50 (:REWRITE UNSIGNED-BYTE-P-OF-LOGTAIL))
 (3210 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (2598 82 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (1818 6 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-2))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (1074 94 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (954 702 (:REWRITE DEFAULT-<-2))
 (896 702 (:REWRITE DEFAULT-<-1))
 (884 80 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (884 80 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (884 80 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (584 149 (:REWRITE NFIX-WHEN-NOT-NATP))
 (494 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGAND-2))
 (445 28 (:REWRITE LOGTAIL-IDENTITY))
 (440 35 (:REWRITE BITOPS::LOGBITP-NONZERO-OF-BIT))
 (404 82 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (404 82 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (376 68 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (376 68 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (376 68 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (291 291 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (282 47 (:REWRITE IFIX-NEGATIVE-TO-NEGP))
 (253 253 (:TYPE-PRESCRIPTION BITP))
 (244 222 (:REWRITE EXPT-WITH-VIOLATED-GUARDS))
 (215 78 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (208 43 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (176 176 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (171 124 (:REWRITE DEFAULT-+-1))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (166 166 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (160 8 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (158 8 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 2))
 (155 46 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (151 51 (:REWRITE BITOPS::LOGBITP-WHEN-BITMASKP))
 (145 68 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (144 8 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-2))
 (141 47 (:REWRITE NEGP-WHEN-LESS-THAN-0))
 (138 138 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (138 138 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (138 138 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (136 124 (:REWRITE DEFAULT-+-2))
 (136 8 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (134 54 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (113 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGIOR))
 (113 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGAND-1))
 (104 42 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (92 92 (:LINEAR BITOPS::EXPT-2-LOWER-BOUND-BY-LOGBITP))
 (88 8 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (84 42 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (72 6 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-1))
 (56 56 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
 (53 46 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (51 51 (:REWRITE BITOPS::NORMALIZE-LOGBITP-WHEN-MODS-EQUAL))
 (51 51 (:REWRITE BITOPS::LOGBITP-OF-NEGATIVE-CONST))
 (51 51 (:REWRITE BITOPS::LOGBITP-OF-MASK))
 (51 51 (:REWRITE BITOPS::LOGBITP-OF-CONST))
 (47 47 (:TYPE-PRESCRIPTION NEGP))
 (47 47 (:REWRITE NEGP-WHEN-INTEGERP))
 (43 43 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (43 43 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (42 42 (:DEFINITION FIX))
 (34 34 (:TYPE-PRESCRIPTION BIT->BOOL$INLINE))
 (34 17 (:REWRITE BFIX-WHEN-NOT-BIT->BOOL))
 (34 17 (:REWRITE BFIX-WHEN-BIT->BOOL))
 (32 16 (:REWRITE BFIX-WHEN-NOT-BITP))
 (28 28 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NATP))
 (28 28 (:TYPE-PRESCRIPTION BITOPS::LOGAND-NATP-TYPE-1))
 (27 27 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (25 21 (:REWRITE DEFAULT-UNARY-MINUS))
 (24 1 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-1))
 (13 13 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX2-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SIB-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MODR/M-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE3-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-8BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (7 7 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 (6 6 (:REWRITE BITOPS::B-IOR-EQUAL-1-IN-CONCL))
 (6 6 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGIOR-FOR-NATURALS))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (4 4 (:REWRITE BITOPS::B-AND-EQUAL-1-IN-HYP))
 (4 2 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:LINEAR BITOPS::B-AND-BOUND))
 (3 1 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX2-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SIB-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MODR/M-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE3-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::8BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX2-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SIB-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MODR/M-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE3-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 )
(X86ISA::LOGTAIL-N-OF-SET-DIRTY-AND-ACCESSED-BITS
 (74 2 (:REWRITE LOGTAIL-IDENTITY))
 (68 2 (:DEFINITION UNSIGNED-BYTE-P))
 (62 2 (:DEFINITION INTEGER-RANGE-P))
 (30 3 (:REWRITE X86ISA::DIRTY-BIT-SET-DIRTY-BIT-IDENTITY))
 (27 2 (:LINEAR X86ISA::N64P-SET-DIRTY-BIT))
 (15 15 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS->D$INLINE))
 (11 2 (:REWRITE X86ISA::ACCESSED-BIT-SET-ACCESSED-BIT-IDENTITY))
 (8 8 (:TYPE-PRESCRIPTION RATIONALP-EXPT-TYPE-PRESCRIPTION))
 (8 8 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE))
 (7 3 (:REWRITE DEFAULT-<-2))
 (6 3 (:DEFINITION X86ISA::DIRTY-BIT))
 (5 5 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS->A$INLINE))
 (5 3 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE EXPT-WITH-VIOLATED-GUARDS))
 (3 3 (:TYPE-PRESCRIPTION X86ISA::N01P-DIRTY-BIT))
 (3 3 (:TYPE-PRESCRIPTION X86ISA::DIRTY-BIT))
 (3 3 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->D-OF-WRITE-WITH-MASK))
 (2 2 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (2 2 (:LINEAR BITOPS::EXPT-2-LOWER-BOUND-BY-LOGBITP))
 (2 1 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (2 1 (:DEFINITION X86ISA::ACCESSED-BIT))
 (1 1 (:TYPE-PRESCRIPTION X86ISA::N01P-ACCESSED-BIT))
 (1 1 (:TYPE-PRESCRIPTION X86ISA::ACCESSED-BIT))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (1 1 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->A-OF-WRITE-WITH-MASK))
 )
(X86ISA::LOGHEAD-N-OF-SET-ACCESSED-BIT
 (5528 91 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (5423 49 (:REWRITE BITOPS::LOGBITP-WHEN-BIT))
 (3910 12 (:LINEAR X86ISA::RM-LOW-64-LOGAND-LOGIOR-HELPER-1))
 (3886 12 (:DEFINITION X86ISA::N64P$INLINE))
 (1444 75 (:REWRITE LOGHEAD-IDENTITY))
 (1228 51 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (1026 39 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (886 6 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-2))
 (561 409 (:REWRITE DEFAULT-<-2))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (513 409 (:REWRITE DEFAULT-<-1))
 (450 30 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (450 30 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (450 30 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (448 37 (:REWRITE BITOPS::LOGBITP-NONZERO-OF-BIT))
 (316 39 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (294 28 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (294 28 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (294 28 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (257 257 (:TYPE-PRESCRIPTION BITP))
 (234 78 (:REWRITE NFIX-WHEN-NOT-NATP))
 (227 84 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (218 6 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-1))
 (182 182 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (164 164 (:REWRITE EXPT-WITH-VIOLATED-GUARDS))
 (160 8 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (158 8 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 2))
 (154 43 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (145 49 (:REWRITE BITOPS::LOGBITP-WHEN-BITMASKP))
 (144 8 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-2))
 (143 42 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (136 87 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (136 8 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (134 8 (:REWRITE BFIX-WHEN-NOT-1))
 (128 51 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (112 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGIOR))
 (105 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGAND-2))
 (105 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGAND-1))
 (104 42 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (92 92 (:REWRITE NATP-WHEN-INTEGERP))
 (88 8 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (58 58 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (58 58 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (58 58 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (57 57 (:LINEAR BITOPS::EXPT-2-LOWER-BOUND-BY-LOGBITP))
 (54 18 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (49 49 (:REWRITE BITOPS::NORMALIZE-LOGBITP-WHEN-MODS-EQUAL))
 (49 49 (:REWRITE BITOPS::LOGBITP-OF-NEGATIVE-CONST))
 (49 49 (:REWRITE BITOPS::LOGBITP-OF-MASK))
 (49 49 (:REWRITE BITOPS::LOGBITP-OF-CONST))
 (43 43 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (43 43 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (40 7 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (39 39 (:REWRITE INEQUALITY-WITH-NFIX-HYP-1))
 (36 36 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
 (36 36 (:TYPE-PRESCRIPTION ASH))
 (33 33 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (24 24 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (18 18 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NATP))
 (18 18 (:TYPE-PRESCRIPTION LOGNOT))
 (18 18 (:TYPE-PRESCRIPTION BITOPS::LOGAND-NATP-TYPE-1))
 (18 18 (:TYPE-PRESCRIPTION BINARY-LOGIOR))
 (18 18 (:TYPE-PRESCRIPTION BINARY-LOGAND))
 (16 16 (:TYPE-PRESCRIPTION BIT->BOOL$INLINE))
 (16 8 (:REWRITE BFIX-WHEN-NOT-BITP))
 (16 8 (:REWRITE BFIX-WHEN-NOT-BIT->BOOL))
 (16 8 (:REWRITE BFIX-WHEN-BIT->BOOL))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (9 9 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX2-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SIB-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MODR/M-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE3-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-8BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (6 6 (:REWRITE BITOPS::B-IOR-EQUAL-1-IN-CONCL))
 (6 6 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGIOR-FOR-NATURALS))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (4 4 (:REWRITE BITOPS::B-AND-EQUAL-1-IN-HYP))
 (4 2 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:LINEAR BITOPS::B-AND-BOUND))
 (3 3 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX2-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SIB-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MODR/M-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE3-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::8BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX2-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SIB-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MODR/M-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE3-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:LINEAR BITOPS::B-NOT-BOUND))
 )
(X86ISA::LOGHEAD-N-OF-SET-DIRTY-BIT
 (5528 91 (:REWRITE FTY::BITP-WHEN-UNSIGNED-BYTE-P-1))
 (5423 49 (:REWRITE BITOPS::LOGBITP-WHEN-BIT))
 (3910 12 (:LINEAR X86ISA::RM-LOW-64-LOGAND-LOGIOR-HELPER-1))
 (3886 12 (:DEFINITION X86ISA::N64P$INLINE))
 (1444 75 (:REWRITE LOGHEAD-IDENTITY))
 (1228 51 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PTE-4K-PAGEBITS-P))
 (1026 39 (:REWRITE X86ISA::IA32E-PTE-4K-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (886 6 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-2))
 (561 409 (:REWRITE DEFAULT-<-2))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PML4EBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-PG-DIRBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDPTE-1GB-PAGEBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-PG-TABLEBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PDE-2MB-PAGEBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32E-PAGE-TABLESBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTORBITS-P))
 (538 41 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTORBITS-P))
 (513 409 (:REWRITE DEFAULT-<-1))
 (450 30 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-XCR0BITS-P))
 (450 30 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR3BITS-P))
 (450 30 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-64BITS-P))
 (448 37 (:REWRITE BITOPS::LOGBITP-NONZERO-OF-BIT))
 (316 39 (:REWRITE X86ISA::IA32E-PML4EBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::IA32E-PDPTE-PG-DIRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::IA32E-PDE-PG-TABLEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::IA32E-PDE-2MB-PAGEBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (316 39 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (294 28 (:REWRITE X86ISA::XCR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (294 28 (:REWRITE X86ISA::CR3BITS-P-WHEN-UNSIGNED-BYTE-P))
 (294 28 (:REWRITE X86ISA::64BITS-P-WHEN-UNSIGNED-BYTE-P))
 (257 257 (:TYPE-PRESCRIPTION BITP))
 (234 78 (:REWRITE NFIX-WHEN-NOT-NATP))
 (227 84 (:REWRITE FTY::UNSIGNED-BYTE-P-1-WHEN-BITP))
 (218 6 (:LINEAR BITOPS::LOGIOR-<-0-LINEAR-1))
 (182 182 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (164 164 (:REWRITE EXPT-WITH-VIOLATED-GUARDS))
 (160 8 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 1))
 (158 8 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGAND . 2))
 (154 43 (:REWRITE X86ISA::LOGAND-IDENTITY-LEMMA-FOR-BASE-ADDR))
 (145 49 (:REWRITE BITOPS::LOGBITP-WHEN-BITMASKP))
 (144 8 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-2))
 (143 42 (:REWRITE UNSIGNED-BYTE-P-LOGHEAD))
 (136 87 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (136 8 (:LINEAR BITOPS::LOGAND->=-0-LINEAR-1))
 (134 8 (:REWRITE BFIX-WHEN-NOT-1))
 (128 51 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
 (112 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGIOR))
 (105 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGAND-2))
 (105 2 (:REWRITE UNSIGNED-BYTE-P-OF-LOGAND-1))
 (104 42 (:REWRITE BITOPS::LOGAND-WITH-NEGATED-BITMASK))
 (92 92 (:REWRITE NATP-WHEN-INTEGERP))
 (88 8 (:LINEAR BITOPS::LOGAND-<-0-LINEAR))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PTE-4K-PAGEBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PML4EBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-PG-DIRBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDPTE-1GB-PAGEBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-PG-TABLEBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PDE-2MB-PAGEBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTORBITS-P))
 (80 80 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTORBITS-P))
 (58 58 (:TYPE-PRESCRIPTION X86ISA::XCR0BITS-P$INLINE))
 (58 58 (:TYPE-PRESCRIPTION X86ISA::CR3BITS-P$INLINE))
 (58 58 (:TYPE-PRESCRIPTION X86ISA::64BITS-P))
 (57 57 (:LINEAR BITOPS::EXPT-2-LOWER-BOUND-BY-LOGBITP))
 (54 18 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (49 49 (:REWRITE BITOPS::NORMALIZE-LOGBITP-WHEN-MODS-EQUAL))
 (49 49 (:REWRITE BITOPS::LOGBITP-OF-NEGATIVE-CONST))
 (49 49 (:REWRITE BITOPS::LOGBITP-OF-MASK))
 (49 49 (:REWRITE BITOPS::LOGBITP-OF-CONST))
 (43 43 (:REWRITE X86ISA::WEED-OUT-IRRELEVANT-LOGAND-WHEN-FIRST-OPERAND-CONSTANT))
 (43 43 (:REWRITE X86ISA::LOGAND-REDUNDANT))
 (40 7 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (39 39 (:REWRITE INEQUALITY-WITH-NFIX-HYP-1))
 (36 36 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
 (36 36 (:TYPE-PRESCRIPTION ASH))
 (33 33 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (24 24 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (18 18 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NATP))
 (18 18 (:TYPE-PRESCRIPTION LOGNOT))
 (18 18 (:TYPE-PRESCRIPTION BITOPS::LOGAND-NATP-TYPE-1))
 (18 18 (:TYPE-PRESCRIPTION BINARY-LOGIOR))
 (18 18 (:TYPE-PRESCRIPTION BINARY-LOGAND))
 (16 16 (:TYPE-PRESCRIPTION BIT->BOOL$INLINE))
 (16 8 (:REWRITE BFIX-WHEN-NOT-BITP))
 (16 8 (:REWRITE BFIX-WHEN-NOT-BIT->BOOL))
 (16 8 (:REWRITE BFIX-WHEN-BIT->BOOL))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-IA32_EFERBITS-P))
 (10 2 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-12BITS-P))
 (9 9 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX3-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-VEX2-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SIB-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-SEGMENT-SELECTORBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-RFLAGSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MXCSRBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-MODR/M-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-FP-STATUSBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-PREFIXES-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE3-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE2-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-EVEX-BYTE1-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-8BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-32BITS-P))
 (8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-16BITS-P))
 (6 6 (:REWRITE BITOPS::B-IOR-EQUAL-1-IN-CONCL))
 (6 6 (:LINEAR BITOPS::UPPER-BOUND-OF-LOGIOR-FOR-NATURALS))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::IA32_EFERBITS-P$INLINE))
 (4 4 (:TYPE-PRESCRIPTION X86ISA::12BITS-P))
 (4 4 (:REWRITE BITOPS::B-AND-EQUAL-1-IN-HYP))
 (4 2 (:REWRITE X86ISA::IA32_EFERBITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:REWRITE X86ISA::12BITS-P-WHEN-UNSIGNED-BYTE-P))
 (4 2 (:LINEAR BITOPS::B-AND-BOUND))
 (3 3 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX3-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::VEX2-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SIB-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::SEGMENT-SELECTORBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::RFLAGSBITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MXCSRBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::MODR/M-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::FP-STATUSBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-PREFIXES-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE3-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE2-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::EVEX-BYTE1-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::8BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::32BITS-P))
 (2 2 (:TYPE-PRESCRIPTION X86ISA::16BITS-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX3-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::VEX2-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SYSTEM-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SIB-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::SEGMENT-SELECTORBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::RFLAGSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MXCSRBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::MODR/M-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::INTERRUPT/TRAP-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::FP-STATUSBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-PREFIXES-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE3-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE2-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::EVEX-BYTE1-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::DATA-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CODE-SEGMENT-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::CALL-GATE-DESCRIPTOR-ATTRIBUTESBITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::8BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::32BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:REWRITE X86ISA::16BITS-P-WHEN-UNSIGNED-BYTE-P))
 (2 1 (:LINEAR BITOPS::B-NOT-BOUND))
 )
(X86ISA::LOGHEAD-N-OF-SET-DIRTY-AND-ACCESSED-BITS
 (257 9 (:DEFINITION INTEGER-RANGE-P))
 (226 8 (:DEFINITION UNSIGNED-BYTE-P))
 (81 6 (:LINEAR X86ISA::N64P-SET-DIRTY-BIT))
 (70 7 (:REWRITE X86ISA::DIRTY-BIT-SET-DIRTY-BIT-IDENTITY))
 (69 1 (:REWRITE X86ISA::LOGHEAD-UNEQUAL))
 (65 1 (:DEFINITION SIGNED-BYTE-P))
 (43 43 (:TYPE-PRESCRIPTION X86ISA::N64P-SET-DIRTY-BIT))
 (38 18 (:REWRITE DEFAULT-<-2))
 (35 35 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS->D$INLINE))
 (30 30 (:REWRITE EXPT-WITH-VIOLATED-GUARDS))
 (24 18 (:REWRITE DEFAULT-<-1))
 (18 11 (:REWRITE X86ISA::LOGHEAD-OF-NON-INTEGERP))
 (14 7 (:DEFINITION X86ISA::DIRTY-BIT))
 (14 2 (:REWRITE BITOPS::LOGHEAD-OF-LOGHEAD-2))
 (11 11 (:REWRITE X86ISA::LOGHEAD-ZERO-SMALLER))
 (11 2 (:REWRITE X86ISA::ACCESSED-BIT-SET-ACCESSED-BIT-IDENTITY))
 (8 8 (:TYPE-PRESCRIPTION X86ISA::N64P-SET-ACCESSED-BIT))
 (8 8 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
 (8 8 (:LINEAR BITOPS::EXPT-2-LOWER-BOUND-BY-LOGBITP))
 (7 7 (:TYPE-PRESCRIPTION X86ISA::N01P-DIRTY-BIT))
 (7 7 (:TYPE-PRESCRIPTION X86ISA::DIRTY-BIT))
 (7 7 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->D-OF-WRITE-WITH-MASK))
 (5 5 (:TYPE-PRESCRIPTION X86ISA::IA32E-PAGE-TABLESBITS->A$INLINE))
 (4 4 (:REWRITE NFIX-WHEN-NOT-NATP))
 (4 4 (:LINEAR X86ISA::SIGNED-BYTE-P-OF-TRUNCATE-WHEN-Y-IS-POSITIVE))
 (4 4 (:LINEAR X86ISA::SIGNED-BYTE-P-OF-TRUNCATE-WHEN-Y-IS-NEGATIVE))
 (4 4 (:LINEAR X86ISA::SIGNED-BYTE-P-OF-TRUNCATE))
 (4 4 (:LINEAR X86ISA::SIGNED-BYTE-P-OF-REM))
 (3 1 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 1 (:DEFINITION X86ISA::ACCESSED-BIT))
 (1 1 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
 (1 1 (:TYPE-PRESCRIPTION X86ISA::N01P-ACCESSED-BIT))
 (1 1 (:TYPE-PRESCRIPTION X86ISA::ACCESSED-BIT))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
 (1 1 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
 (1 1 (:REWRITE X86ISA::IA32E-PAGE-TABLESBITS->A-OF-WRITE-WITH-MASK))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(X86ISA::ACCESSED-BIT-SET-ACCESSED-BIT)
(X86ISA::ACCESSED-BIT-SET-DIRTY-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )
(X86ISA::DIRTY-BIT-SET-DIRTY-BIT)
(X86ISA::DIRTY-BIT-SET-ACCESSED-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )
(X86ISA::PAGE-SIZE-SET-ACCESSED-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )
(X86ISA::PAGE-SIZE-SET-DIRTY-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )
(X86ISA::PAGE-PRESENT-SET-ACCESSED-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )
(X86ISA::PAGE-PRESENT-SET-DIRTY-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )
(X86ISA::PAGE-READ-WRITE-SET-ACCESSED-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )
(X86ISA::PAGE-READ-WRITE-SET-DIRTY-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )
(X86ISA::PAGE-USER-SUPERVISOR-SET-ACCESSED-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )
(X86ISA::PAGE-USER-SUPERVISOR-SET-DIRTY-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )
(X86ISA::PAGE-EXECUTE-DISABLE-SET-ACCESSED-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )
(X86ISA::PAGE-EXECUTE-DISABLE-SET-DIRTY-BIT
 (2 2 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:TYPE-PRESCRIPTION BITOPS::LOGNOT-NEGP))
 (1 1 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (1 1 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
 )