(ADE::SIPO-SREG*)
(ADE::SIPO-SREG*$DESTRUCTURE
 (978 30 (:REWRITE ZP-OPEN))
 (780 24 (:DEFINITION BINARY-APPEND))
 (750 24 (:REWRITE CONSP-OF-REPEAT))
 (486 66 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (462 48 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (276 6 (:REWRITE REPEAT-WHEN-ZP))
 (198 36 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (190 34 (:REWRITE DEFAULT-CDR))
 (185 29 (:REWRITE DEFAULT-CAR))
 (180 30 (:REWRITE |(+ c (+ d x))|))
 (105 105 (:TYPE-PRESCRIPTION POSP))
 (84 30 (:DEFINITION NOT))
 (72 72 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (72 72 (:REWRITE NORMALIZE-ADDENDS))
 (72 72 (:REWRITE DEFAULT-+-2))
 (72 72 (:REWRITE DEFAULT-+-1))
 (66 66 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (66 66 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (66 66 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (66 66 (:REWRITE |(< d (+ c x))|))
 (66 66 (:REWRITE |(< (- x) (- y))|))
 (60 60 (:TYPE-PRESCRIPTION REPEAT))
 (48 48 (:REWRITE |(+ 0 x)|))
 (42 42 (:META META-INTEGERP-CORRECT))
 (36 36 (:REWRITE SIMPLIFY-SUMS-<))
 (36 36 (:REWRITE DEFAULT-<-2))
 (36 36 (:REWRITE DEFAULT-<-1))
 (36 24 (:REWRITE REDUCE-INTEGERP-+))
 (30 30 (:REWRITE |(< 0 (- x))|))
 (24 24 (:REWRITE INTEGERP-MINUS-X))
 (6 6 (:TYPE-PRESCRIPTION ZP))
 )
(ADE::NOT-PRIMP-SIPO-SREG
 (72 36 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (72 36 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (72 36 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (36 36 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::SIPO-SREG$NETLIST)
(ADE::SIPO-SREG&
 (504 28 (:DEFINITION ASSOC-EQUAL))
 (116 29 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
 (113 90 (:REWRITE DEFAULT-CAR))
 (86 57 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (86 57 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (86 57 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (77 2 (:DEFINITION ADE::TV-GUARD))
 (58 58 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
 (58 6 (:REWRITE ADE::CONSP-MAKE-TREE))
 (57 57 (:REWRITE |(equal (- x) (- y))|))
 (57 34 (:REWRITE DEFAULT-CDR))
 (29 29 (:REWRITE DEFAULT-SYMBOL-NAME))
 (21 21 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (21 21 (:REWRITE NORMALIZE-ADDENDS))
 (21 21 (:REWRITE DEFAULT-+-2))
 (21 21 (:REWRITE DEFAULT-+-1))
 (18 1 (:DEFINITION ADE::DELETE-TO-EQ))
 (12 12 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE SIMPLIFY-SUMS-<))
 (9 9 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (9 9 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (9 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE DEFAULT-<-1))
 (9 9 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE |(< 0 (- x))|))
 )
(ADE::CHECK-SIPO-SREG$NETLIST-64-7)
(ADE::SIPO-SREG$ST-FORMAT)
(ADE::SIPO-SREG$ST-FORMAT=>CONSTRAINT
 (28 4 (:DEFINITION LEN))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (8 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (8 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (8 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (8 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (4 4 (:REWRITE NORMALIZE-ADDENDS))
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE |(equal (- x) (- y))|))
 (3 3 (:REWRITE SIMPLIFY-SUMS-<))
 (3 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (3 3 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (3 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 )
(ADE::SIPO-SREG$VALID-ST
 (6 6 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE))
 )
(ADE::EXPT-LINEAR-LOWER-<=-INSTANCE
 (2 2 (:REWRITE DEFAULT-EXPT-2))
 (2 2 (:REWRITE DEFAULT-EXPT-1))
 (2 2 (:REWRITE |(expt x (- n))|))
 (2 2 (:REWRITE |(expt 2^i n)|))
 (2 2 (:REWRITE |(expt 1/c n)|))
 (2 2 (:REWRITE |(expt (- x) n)|))
 (2 2 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (1 1 (:LINEAR EXPT->-1-TWO))
 (1 1 (:LINEAR EXPT-<-1-TWO))
 (1 1 (:LINEAR EXPT-<-1-ONE))
 )
(ADE::SIPO-SREG$VALID-ST=>CONSTRAINT
 (128 128 (:LINEAR LEN-WHEN-PREFIXP))
 (64 64 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (32 32 (:REWRITE SIMPLIFY-SUMS-<))
 (32 32 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (32 32 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (32 32 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (32 32 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (32 32 (:REWRITE DEFAULT-<-2))
 (32 32 (:REWRITE DEFAULT-<-1))
 (32 32 (:REWRITE |(< (- x) (- y))|))
 (28 17 (:REWRITE DEFAULT-EXPT-2))
 (28 17 (:REWRITE |(expt 2^i n)|))
 (28 4 (:DEFINITION LEN))
 (21 17 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (21 17 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (21 17 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (20 4 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (17 17 (:REWRITE DEFAULT-EXPT-1))
 (17 17 (:REWRITE |(expt x (- n))|))
 (17 17 (:REWRITE |(expt 1/c n)|))
 (17 17 (:REWRITE |(expt (- x) n)|))
 (17 17 (:REWRITE |(equal (- x) (- y))|))
 (16 16 (:REWRITE NTH-WHEN-PREFIXP))
 (16 4 (:DEFINITION STRIP-CARS))
 (11 7 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE NORMALIZE-ADDENDS))
 (7 7 (:REWRITE DEFAULT-+-1))
 (4 4 (:META META-INTEGERP-CORRECT))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE |(+ 0 x)|))
 )
(ADE::SIPO-SREG$VALID-ST=>ST-FORMAT
 (4 4 (:REWRITE NTH-WHEN-PREFIXP))
 )
(ADE::SIPO-SREG$BIT-IN)
(ADE::SIPO-SREG$IN-ACT
 (12 6 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (6 6 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (5 5 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::SIPO-SREG$IN-ACT-INACTIVE
 (22 6 (:REWRITE ADE::F-GATES=B-GATES))
 (12 12 (:REWRITE NTH-WHEN-PREFIXP))
 (10 10 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 6 (:REWRITE DEFAULT-CAR))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 3 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (3 3 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (3 1 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (2 2 (:TYPE-PRESCRIPTION ADE::BVP))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 1 (:DEFINITION NTHCDR))
 )
(ADE::SIPO-SREG$OUT-ACT
 (12 6 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (6 6 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (5 5 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::SIPO-SREG$OUT-ACT-INACTIVE
 (12 12 (:REWRITE NTH-WHEN-PREFIXP))
 (10 4 (:REWRITE ADE::F-GATES=B-GATES))
 (6 6 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 6 (:REWRITE DEFAULT-CAR))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 1 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (2 2 (:TYPE-PRESCRIPTION ADE::BVP))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 1 (:DEFINITION NTHCDR))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE
 (538 538 (:REWRITE NTH-WHEN-PREFIXP))
 (204 51 (:DEFINITION STRIP-CARS))
 (195 195 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (140 140 (:REWRITE DEFAULT-CDR))
 (112 59 (:REWRITE DEFAULT-+-2))
 (108 108 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (102 102 (:REWRITE DEFAULT-CAR))
 (78 39 (:DEFINITION NTHCDR))
 (72 50 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (72 50 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (72 50 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (64 32 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (59 59 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (59 59 (:REWRITE NORMALIZE-ADDENDS))
 (59 59 (:REWRITE DEFAULT-+-1))
 (50 50 (:REWRITE |(equal (- x) (- y))|))
 (32 18 (:REWRITE |(expt 2^i n)|))
 (24 24 (:LINEAR LEN-WHEN-PREFIXP))
 (22 20 (:REWRITE SIMPLIFY-SUMS-<))
 (22 20 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (22 20 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (22 20 (:REWRITE DEFAULT-<-1))
 (21 3 (:LINEAR EXPT-X->=-X))
 (21 3 (:LINEAR EXPT-X->-X))
 (21 3 (:LINEAR EXPT->-1-ONE))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (20 20 (:REWRITE DEFAULT-<-2))
 (20 20 (:REWRITE |(< (- x) (- y))|))
 (18 18 (:REWRITE |(expt x (- n))|))
 (18 18 (:REWRITE |(expt 1/c n)|))
 (18 18 (:REWRITE |(expt (- x) n)|))
 (17 17 (:REWRITE DEFAULT-EXPT-1))
 (12 12 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (12 2 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (6 6 (:META META-INTEGERP-CORRECT))
 (6 6 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (6 6 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (6 6 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (6 6 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (6 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (3 3 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (3 3 (:LINEAR EXPT->-1-TWO))
 (3 3 (:LINEAR EXPT-<-1-TWO))
 (3 3 (:LINEAR EXPT-<-1-ONE))
 )
(ADE::SIPO-SREG$CNT-OUT=1)
(ADE::LEN-CDR
 (14 7 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE NORMALIZE-ADDENDS))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 1 (:REWRITE SIMPLIFY-SUMS-<))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 1 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE |(< (- x) (- y))|))
 )
(ADE::BOOLEANP-SIPO-SREG$CNT-OUT=1-1
 (546 546 (:REWRITE NTH-WHEN-PREFIXP))
 (209 191 (:REWRITE DEFAULT-CDR))
 (195 195 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (180 162 (:REWRITE DEFAULT-CAR))
 (126 67 (:REWRITE DEFAULT-+-2))
 (102 102 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (82 52 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (82 52 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (82 52 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (67 67 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (67 67 (:REWRITE NORMALIZE-ADDENDS))
 (67 67 (:REWRITE DEFAULT-+-1))
 (64 32 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (52 52 (:REWRITE |(equal (- x) (- y))|))
 (34 19 (:REWRITE |(expt 2^i n)|))
 (26 26 (:LINEAR LEN-WHEN-PREFIXP))
 (22 19 (:REWRITE SIMPLIFY-SUMS-<))
 (22 19 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (22 19 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (21 19 (:REWRITE DEFAULT-<-1))
 (21 3 (:LINEAR EXPT-X->=-X))
 (21 3 (:LINEAR EXPT-X->-X))
 (21 3 (:LINEAR EXPT->-1-ONE))
 (20 19 (:REWRITE DEFAULT-<-2))
 (19 19 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (19 19 (:REWRITE |(expt x (- n))|))
 (19 19 (:REWRITE |(expt 1/c n)|))
 (19 19 (:REWRITE |(expt (- x) n)|))
 (19 19 (:REWRITE |(< (- x) (- y))|))
 (18 18 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (18 18 (:REWRITE DEFAULT-EXPT-1))
 (13 13 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (6 6 (:META META-INTEGERP-CORRECT))
 (6 6 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (6 6 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (6 6 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (6 6 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (6 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (3 3 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (3 3 (:LINEAR EXPT->-1-TWO))
 (3 3 (:LINEAR EXPT-<-1-TWO))
 (3 3 (:LINEAR EXPT-<-1-ONE))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE |(< 0 (- x))|))
 )
(ADE::BOOLEANP-SIPO-SREG$CNT-OUT=1-2
 (960 960 (:REWRITE NTH-WHEN-PREFIXP))
 (476 416 (:REWRITE DEFAULT-CDR))
 (428 368 (:REWRITE DEFAULT-CAR))
 (325 169 (:REWRITE DEFAULT-+-2))
 (234 138 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (234 138 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (234 138 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (192 32 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (169 169 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (169 169 (:REWRITE NORMALIZE-ADDENDS))
 (169 169 (:REWRITE DEFAULT-+-1))
 (138 138 (:REWRITE |(equal (- x) (- y))|))
 (104 104 (:LINEAR LEN-WHEN-PREFIXP))
 (104 24 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (97 70 (:REWRITE |(expt 2^i n)|))
 (84 12 (:LINEAR EXPT-X->=-X))
 (84 12 (:LINEAR EXPT-X->-X))
 (84 12 (:LINEAR EXPT->-1-ONE))
 (70 70 (:REWRITE |(expt x (- n))|))
 (70 70 (:REWRITE |(expt 1/c n)|))
 (70 70 (:REWRITE |(expt (- x) n)|))
 (69 69 (:REWRITE DEFAULT-EXPT-1))
 (64 32 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (64 16 (:REWRITE ADE::BOOLEANP-OF-F-BUF))
 (56 24 (:REWRITE ADE::F-BUF-OF-3VP))
 (52 52 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (40 28 (:REWRITE SIMPLIFY-SUMS-<))
 (40 28 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (40 28 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (36 28 (:REWRITE DEFAULT-<-1))
 (32 32 (:TYPE-PRESCRIPTION ADE::3VP))
 (32 32 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (32 28 (:REWRITE DEFAULT-<-2))
 (28 28 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (28 28 (:REWRITE |(< (- x) (- y))|))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (24 24 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (24 24 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (24 24 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (24 24 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (12 12 (:LINEAR EXPT->-1-TWO))
 (12 12 (:LINEAR EXPT-<-1-TWO))
 (12 12 (:LINEAR EXPT-<-1-ONE))
 (8 8 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (6 6 (:META META-INTEGERP-CORRECT))
 (6 4 (:REWRITE REDUCE-INTEGERP-+))
 (5 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$CNT-OUT=1-1))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:REWRITE |(< 0 (- x))|))
 )
(ADE::SIPO-SREG$DATA-OUT)
(ADE::LEN-SIPO-SREG$DATA-OUT-1
 (7 1 (:DEFINITION LEN))
 (5 5 (:REWRITE NTH-WHEN-PREFIXP))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (3 3 (:REWRITE SIMPLIFY-SUMS-<))
 (3 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (3 3 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (3 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:META META-INTEGERP-CORRECT))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1 1 (:REWRITE NORMALIZE-ADDENDS))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 )
(ADE::LEN-SIPO-SREG$DATA-OUT-2
 (14 14 (:REWRITE NTH-WHEN-PREFIXP))
 (14 2 (:DEFINITION LEN))
 (13 2 (:REWRITE |(expt 2^i n)|))
 (9 7 (:REWRITE DEFAULT-+-2))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (7 7 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE NORMALIZE-ADDENDS))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 6 (:META META-INTEGERP-CORRECT))
 (6 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (3 3 (:REWRITE |(+ 0 x)|))
 (2 2 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE))
 (2 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE |(expt x (- n))|))
 (2 2 (:REWRITE |(expt 1/c n)|))
 (2 2 (:REWRITE |(expt (- x) n)|))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE DEFAULT-EXPT-1))
 )
(ADE::BVP-SIPO-SREG$DATA-OUT-1
 (912 192 (:REWRITE ADE::F-GATES=B-GATES))
 (420 420 (:REWRITE NTH-WHEN-PREFIXP))
 (336 32 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (192 192 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (168 42 (:DEFINITION STRIP-CARS))
 (168 24 (:DEFINITION LEN))
 (128 16 (:REWRITE ADE::LEN-STRIP-CARS))
 (98 98 (:REWRITE DEFAULT-CDR))
 (96 96 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (84 84 (:REWRITE DEFAULT-CAR))
 (64 32 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (64 32 (:DEFINITION NTHCDR))
 (53 53 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE))
 (53 29 (:REWRITE DEFAULT-+-2))
 (42 34 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (42 34 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (42 34 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (34 34 (:REWRITE |(equal (- x) (- y))|))
 (29 29 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (29 29 (:REWRITE NORMALIZE-ADDENDS))
 (29 29 (:REWRITE DEFAULT-+-1))
 (16 16 (:REWRITE SIMPLIFY-SUMS-<))
 (16 16 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (16 16 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (16 16 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (16 16 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (16 16 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE DEFAULT-<-1))
 (16 16 (:REWRITE |(< (- x) (- y))|))
 (13 2 (:REWRITE |(expt 2^i n)|))
 (6 6 (:META META-INTEGERP-CORRECT))
 (6 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (3 3 (:REWRITE |(+ 0 x)|))
 (2 2 (:REWRITE |(expt x (- n))|))
 (2 2 (:REWRITE |(expt 1/c n)|))
 (2 2 (:REWRITE |(expt (- x) n)|))
 (1 1 (:REWRITE DEFAULT-EXPT-1))
 )
(ADE::BVP-SIPO-SREG$DATA-OUT-2
 (760 152 (:REWRITE ADE::F-GATES=B-GATES))
 (432 432 (:REWRITE NTH-WHEN-PREFIXP))
 (336 32 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (192 48 (:DEFINITION STRIP-CARS))
 (192 32 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (168 24 (:DEFINITION LEN))
 (128 16 (:REWRITE ADE::LEN-STRIP-CARS))
 (104 104 (:REWRITE DEFAULT-CDR))
 (104 24 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (96 96 (:REWRITE DEFAULT-CAR))
 (74 66 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (74 66 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (74 66 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (66 66 (:REWRITE |(equal (- x) (- y))|))
 (64 32 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (64 32 (:DEFINITION NTHCDR))
 (64 16 (:REWRITE ADE::BOOLEANP-OF-F-BUF))
 (62 62 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE))
 (56 24 (:REWRITE ADE::F-BUF-OF-3VP))
 (53 29 (:REWRITE DEFAULT-+-2))
 (32 32 (:TYPE-PRESCRIPTION ADE::3VP))
 (32 32 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (29 29 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (29 29 (:REWRITE NORMALIZE-ADDENDS))
 (29 29 (:REWRITE DEFAULT-+-1))
 (16 16 (:REWRITE SIMPLIFY-SUMS-<))
 (16 16 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (16 16 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (16 16 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (16 16 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (16 16 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE DEFAULT-<-1))
 (16 16 (:REWRITE |(< (- x) (- y))|))
 (13 2 (:REWRITE |(expt 2^i n)|))
 (6 6 (:META META-INTEGERP-CORRECT))
 (6 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (3 3 (:REWRITE |(+ 0 x)|))
 (2 2 (:REWRITE |(expt x (- n))|))
 (2 2 (:REWRITE |(expt 1/c n)|))
 (2 2 (:REWRITE |(expt (- x) n)|))
 (1 1 (:REWRITE DEFAULT-EXPT-1))
 )
(ADE::SIPO-SREG$OUTPUTS
 (1 1 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$CNT-OUT=1-2))
 (1 1 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$CNT-OUT=1-1))
 )
(ADE::SIPO-SREG$VALUE
 (2530 363 (:DEFINITION BINARY-APPEND))
 (1078 77 (:REWRITE CONSP-OF-REPEAT))
 (1014 78 (:REWRITE ZP-OPEN))
 (726 218 (:REWRITE ADE::CAR-V-THREEFIX))
 (720 80 (:REWRITE |(< d (+ c x))|))
 (498 498 (:TYPE-PRESCRIPTION PAIRLIS$))
 (436 218 (:DEFINITION ADE::3V-FIX))
 (418 63 (:REWRITE ADE::DISJOINT-ATOM))
 (377 15 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (370 370 (:DEFINITION STRIP-CARS))
 (366 33 (:REWRITE CAR-OF-APPEND))
 (322 247 (:REWRITE DEFAULT-+-2))
 (283 255 (:REWRITE NORMALIZE-ADDENDS))
 (247 247 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (247 247 (:REWRITE DEFAULT-+-1))
 (236 236 (:TYPE-PRESCRIPTION ADE::3VP))
 (231 104 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (209 102 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (190 168 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (187 104 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (170 170 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (170 170 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (140 119 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (137 119 (:REWRITE ADE::F-BUF-OF-3VP))
 (120 10 (:REWRITE ADE::TV-IF$VALUE))
 (104 104 (:REWRITE |(equal (- x) (- y))|))
 (92 8 (:DEFINITION ATOM))
 (91 77 (:REWRITE REPEAT-WHEN-ZP))
 (90 90 (:REWRITE NTH-WHEN-PREFIXP))
 (89 89 (:REWRITE SIMPLIFY-SUMS-<))
 (89 89 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (89 89 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (89 89 (:REWRITE DEFAULT-<-2))
 (89 89 (:REWRITE DEFAULT-<-1))
 (89 89 (:REWRITE |(< (- x) (- y))|))
 (80 1 (:DEFINITION SUBSETP-EQUAL))
 (77 77 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (77 50 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (69 69 (:TYPE-PRESCRIPTION POSP))
 (68 50 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (52 13 (:REWRITE TAKE-WHEN-ATOM))
 (49 2 (:REWRITE ADE::NTHCDR-APPEND))
 (34 34 (:TYPE-PRESCRIPTION ADE::NATP-TREE-NUMBER))
 (34 26 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (29 25 (:REWRITE ADE::FV-NOT=V-NOT))
 (28 8 (:REWRITE BUBBLE-DOWN-+-MATCH-1))
 (28 3 (:REWRITE ADE::DISJOINT-CONS))
 (27 1 (:DEFINITION MEMBER-EQUAL))
 (21 21 (:REWRITE ADE::T-OR-NOR$VALUE))
 (16 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (16 4 (:REWRITE |(+ x x)|))
 (15 5 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (14 6 (:REWRITE |(equal (+ c x) d)|))
 (12 4 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (12 4 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM-NAMES))
 (12 1 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (10 2 (:REWRITE |(+ y (+ x z))|))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 5 (:TYPE-PRESCRIPTION ATOM))
 (5 1 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (4 4 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (4 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 4 (:REWRITE DEFAULT-*-2))
 (4 4 (:REWRITE DEFAULT-*-1))
 (4 4 (:REWRITE |(+ x (- x))|))
 (4 1 (:DEFINITION TRUE-LISTP))
 (2 2 (:TYPE-PRESCRIPTION ADE::TREE-SIZE))
 (2 2 (:REWRITE ADE::TREE-SIZE-MAKE-TREE))
 (2 2 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (2 2 (:META META-INTEGERP-CORRECT))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (1 1 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::SIPO-SREG$STEP
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (6 6 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (6 6 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::SIPO-SREG$STATE
 (7471 1012 (:DEFINITION BINARY-APPEND))
 (3472 248 (:REWRITE CONSP-OF-REPEAT))
 (3237 249 (:REWRITE ZP-OPEN))
 (2277 253 (:REWRITE |(< d (+ c x))|))
 (2031 613 (:REWRITE ADE::CAR-V-THREEFIX))
 (1842 1842 (:DEFINITION STRIP-CARS))
 (1291 1291 (:TYPE-PRESCRIPTION PAIRLIS$))
 (1226 613 (:DEFINITION ADE::3V-FIX))
 (1171 47 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (1088 95 (:REWRITE CAR-OF-APPEND))
 (990 966 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (814 121 (:REWRITE ADE::DISJOINT-ATOM))
 (763 615 (:REWRITE DEFAULT-+-2))
 (663 623 (:REWRITE NORMALIZE-ADDENDS))
 (641 641 (:TYPE-PRESCRIPTION ADE::3VP))
 (615 615 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (615 615 (:REWRITE DEFAULT-+-1))
 (521 521 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (521 521 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (456 422 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (450 422 (:REWRITE ADE::F-BUF-OF-3VP))
 (407 238 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (407 238 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (407 238 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (384 260 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (307 293 (:REWRITE REPEAT-WHEN-ZP))
 (267 267 (:REWRITE SIMPLIFY-SUMS-<))
 (267 267 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (267 267 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (267 267 (:REWRITE DEFAULT-<-2))
 (267 267 (:REWRITE DEFAULT-<-1))
 (267 267 (:REWRITE |(< (- x) (- y))|))
 (238 238 (:REWRITE |(equal (- x) (- y))|))
 (230 230 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
 (171 171 (:REWRITE NTH-WHEN-PREFIXP))
 (162 108 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (152 14 (:DEFINITION ATOM))
 (146 146 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (144 108 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (133 133 (:TYPE-PRESCRIPTION POSP))
 (132 36 (:REWRITE TAKE-WHEN-ATOM))
 (125 113 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (120 112 (:REWRITE ADE::FV-NOT=V-NOT))
 (98 4 (:REWRITE ADE::NTHCDR-APPEND))
 (80 1 (:DEFINITION SUBSETP-EQUAL))
 (40 8 (:REWRITE BUBBLE-DOWN-+-MATCH-1))
 (32 16 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (32 8 (:REWRITE |(+ x x)|))
 (28 3 (:REWRITE ADE::DISJOINT-CONS))
 (27 1 (:DEFINITION MEMBER-EQUAL))
 (20 4 (:REWRITE |(equal (+ c x) d)|))
 (18 6 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (12 1 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (9 9 (:TYPE-PRESCRIPTION ATOM))
 (8 8 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (8 8 (:REWRITE DEFAULT-*-2))
 (8 8 (:REWRITE DEFAULT-*-1))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (4 1 (:DEFINITION TRUE-LISTP))
 (2 2 (:REWRITE ADE::T-OR-NOR$VALUE))
 (2 2 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (2 2 (:META META-INTEGERP-CORRECT))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (1 1 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::SIPO-SREG$INPUT-FORMAT)
(ADE::BOOLEANP-SIPO-SREG$IN-ACT
 (512 512 (:REWRITE NTH-WHEN-PREFIXP))
 (216 54 (:DEFINITION STRIP-CARS))
 (167 167 (:REWRITE DEFAULT-CDR))
 (162 6 (:REWRITE ADE::LEN-NTHCDR))
 (146 78 (:REWRITE DEFAULT-+-2))
 (130 94 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (130 94 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (130 94 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (108 108 (:REWRITE DEFAULT-CAR))
 (99 99 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (94 94 (:REWRITE |(equal (- x) (- y))|))
 (84 42 (:DEFINITION NTHCDR))
 (78 78 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (78 78 (:REWRITE NORMALIZE-ADDENDS))
 (78 78 (:REWRITE DEFAULT-+-1))
 (78 12 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (54 6 (:DEFINITION TRUE-LISTP))
 (45 20 (:REWRITE |(expt 2^i n)|))
 (42 42 (:LINEAR LEN-WHEN-PREFIXP))
 (30 23 (:REWRITE SIMPLIFY-SUMS-<))
 (30 23 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (30 23 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (30 23 (:REWRITE DEFAULT-<-1))
 (24 12 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (23 23 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (23 23 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (23 23 (:REWRITE DEFAULT-<-2))
 (23 23 (:REWRITE |(< (- x) (- y))|))
 (21 21 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (20 20 (:REWRITE |(expt x (- n))|))
 (20 20 (:REWRITE |(expt 1/c n)|))
 (20 20 (:REWRITE |(expt (- x) n)|))
 (18 18 (:REWRITE DEFAULT-EXPT-1))
 (18 6 (:REWRITE ADE::BVP-NTHCDR))
 (10 10 (:META META-INTEGERP-CORRECT))
 (8 6 (:REWRITE REDUCE-INTEGERP-+))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (6 6 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (6 6 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (6 6 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (6 6 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (3 3 (:LINEAR EXPT->-1-TWO))
 (3 3 (:LINEAR EXPT-<-1-TWO))
 (3 3 (:LINEAR EXPT-<-1-ONE))
 (1 1 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 )
(ADE::BOOLEANP-SIPO-SREG$OUT-ACT
 (1087 1087 (:REWRITE NTH-WHEN-PREFIXP))
 (368 92 (:DEFINITION STRIP-CARS))
 (288 288 (:REWRITE DEFAULT-CDR))
 (235 123 (:REWRITE DEFAULT-+-2))
 (216 8 (:REWRITE ADE::LEN-NTHCDR))
 (208 48 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (192 64 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (184 184 (:REWRITE DEFAULT-CAR))
 (164 112 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (164 112 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (164 112 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (164 82 (:DEFINITION NTHCDR))
 (128 64 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (128 32 (:REWRITE ADE::BOOLEANP-OF-F-BUF))
 (123 123 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (123 123 (:REWRITE NORMALIZE-ADDENDS))
 (123 123 (:REWRITE DEFAULT-+-1))
 (112 112 (:REWRITE |(equal (- x) (- y))|))
 (112 48 (:REWRITE ADE::F-BUF-OF-3VP))
 (104 16 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (76 76 (:LINEAR LEN-WHEN-PREFIXP))
 (72 8 (:DEFINITION TRUE-LISTP))
 (64 64 (:TYPE-PRESCRIPTION ADE::3VP))
 (64 64 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (64 36 (:REWRITE |(expt 2^i n)|))
 (52 42 (:REWRITE SIMPLIFY-SUMS-<))
 (52 42 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (52 42 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (52 42 (:REWRITE DEFAULT-<-1))
 (42 42 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (42 42 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (42 42 (:REWRITE DEFAULT-<-2))
 (42 42 (:REWRITE |(< (- x) (- y))|))
 (38 38 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (36 36 (:REWRITE |(expt x (- n))|))
 (36 36 (:REWRITE |(expt 1/c n)|))
 (36 36 (:REWRITE |(expt (- x) n)|))
 (34 34 (:REWRITE DEFAULT-EXPT-1))
 (32 16 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (24 8 (:REWRITE ADE::BVP-NTHCDR))
 (12 12 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (12 12 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (12 12 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (12 12 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (10 10 (:META META-INTEGERP-CORRECT))
 (8 6 (:REWRITE REDUCE-INTEGERP-+))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (6 6 (:LINEAR EXPT->-1-TWO))
 (6 6 (:LINEAR EXPT-<-1-TWO))
 (6 6 (:LINEAR EXPT-<-1-ONE))
 (2 2 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 )
(ADE::SIPO-SREG$ST-FORMAT-PRESERVED
 (132 4 (:DEFINITION BINARY-APPEND))
 (130 10 (:REWRITE ZP-OPEN))
 (112 8 (:REWRITE CONSP-OF-REPEAT))
 (107 69 (:REWRITE DEFAULT-CAR))
 (103 103 (:REWRITE NTH-WHEN-PREFIXP))
 (94 12 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (90 10 (:REWRITE |(< d (+ c x))|))
 (88 50 (:REWRITE DEFAULT-CDR))
 (84 21 (:DEFINITION STRIP-CARS))
 (52 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (45 9 (:REWRITE ADE::F-GATES=B-GATES))
 (42 9 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (37 37 (:TYPE-PRESCRIPTION BOOLEANP))
 (33 20 (:REWRITE DEFAULT-+-2))
 (32 4 (:REWRITE REPEAT-WHEN-ZP))
 (30 3 (:DEFINITION ADE::V-THREEFIX))
 (24 24 (:TYPE-PRESCRIPTION ADE::BVP))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (20 20 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (20 20 (:REWRITE DEFAULT-+-1))
 (20 4 (:DEFINITION PAIRLIS$))
 (18 18 (:TYPE-PRESCRIPTION ADE::F-OR))
 (18 6 (:REWRITE ADE::V-THREEFIX-BVP))
 (15 15 (:TYPE-PRESCRIPTION ADE::F-AND))
 (14 14 (:REWRITE SIMPLIFY-SUMS-<))
 (14 14 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (14 14 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (14 14 (:REWRITE DEFAULT-<-2))
 (14 14 (:REWRITE DEFAULT-<-1))
 (14 14 (:REWRITE |(< (- x) (- y))|))
 (14 2 (:REWRITE ADE::CAR-V-THREEFIX))
 (13 3 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$IN-ACT))
 (10 10 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (10 10 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 (10 6 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (10 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (10 6 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (10 5 (:DEFINITION ADE::3V-FIX))
 (9 9 (:TYPE-PRESCRIPTION ADE::JOINT-ACT))
 (7 3 (:REWRITE ADE::F$FAST-ZERO=V-ZP))
 (6 6 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (6 6 (:REWRITE |(equal (- x) (- y))|))
 (6 2 (:REWRITE ADE::FV-NOT=V-NOT))
 (6 2 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (6 2 (:REWRITE ADE::BOOLEANP-SIPO-SREG$IN-ACT))
 (5 5 (:TYPE-PRESCRIPTION ADE::3VP))
 (5 3 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (4 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 )
(ADE::SIPO-SREG$VALUE-ALT
 (243 9 (:REWRITE ADE::LEN-NTHCDR))
 (126 18 (:DEFINITION LEN))
 (117 18 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (81 9 (:DEFINITION TRUE-LISTP))
 (72 72 (:TYPE-PRESCRIPTION ADE::BVP))
 (65 65 (:REWRITE NTH-WHEN-PREFIXP))
 (64 32 (:DEFINITION NTHCDR))
 (59 59 (:REWRITE DEFAULT-CDR))
 (45 11 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (39 23 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (39 23 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (39 23 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (36 18 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (36 18 (:REWRITE DEFAULT-+-2))
 (32 32 (:LINEAR LEN-WHEN-PREFIXP))
 (27 9 (:REWRITE ADE::BVP-NTHCDR))
 (23 23 (:REWRITE |(equal (- x) (- y))|))
 (18 18 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (18 18 (:REWRITE NORMALIZE-ADDENDS))
 (18 18 (:REWRITE DEFAULT-+-1))
 (18 9 (:REWRITE SIMPLIFY-SUMS-<))
 (18 9 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (18 9 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (18 9 (:REWRITE DEFAULT-<-1))
 (16 16 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (11 11 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE |(< (- x) (- y))|))
 )
(ADE::SIPO-SREG$STATE-ALT
 (243 9 (:REWRITE ADE::LEN-NTHCDR))
 (126 18 (:DEFINITION LEN))
 (117 18 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (81 9 (:DEFINITION TRUE-LISTP))
 (72 72 (:TYPE-PRESCRIPTION ADE::BVP))
 (62 31 (:DEFINITION NTHCDR))
 (58 58 (:REWRITE DEFAULT-CDR))
 (39 23 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (39 23 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (39 23 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (36 18 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (36 18 (:REWRITE DEFAULT-+-2))
 (35 35 (:REWRITE NTH-WHEN-PREFIXP))
 (32 32 (:LINEAR LEN-WHEN-PREFIXP))
 (27 9 (:REWRITE ADE::BVP-NTHCDR))
 (23 23 (:REWRITE |(equal (- x) (- y))|))
 (18 18 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (18 18 (:REWRITE NORMALIZE-ADDENDS))
 (18 18 (:REWRITE DEFAULT-+-1))
 (18 9 (:REWRITE SIMPLIFY-SUMS-<))
 (18 9 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (18 9 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (18 9 (:REWRITE DEFAULT-<-1))
 (16 16 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 9 (:REWRITE DEFAULT-<-2))
 (9 9 (:REWRITE |(< (- x) (- y))|))
 )
(ADE::SIPO-SREG$RUN)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-SIPO-SREG$RUN-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-SIPO-SREG$RUN)
(ADE::SIPO-SREG$RUN-PLUS
 (349 25 (:REWRITE ZP-OPEN))
 (122 34 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (76 28 (:REWRITE |(< d (+ c x))|))
 (50 24 (:REWRITE |(+ c (+ d x))|))
 (41 41 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (34 34 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (34 34 (:REWRITE |(< (- x) (- y))|))
 (32 15 (:REWRITE DEFAULT-CDR))
 (27 10 (:REWRITE DEFAULT-CAR))
 (26 26 (:REWRITE SIMPLIFY-SUMS-<))
 (26 26 (:REWRITE DEFAULT-<-2))
 (26 26 (:REWRITE DEFAULT-<-1))
 (24 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (18 18 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (18 18 (:REWRITE NORMALIZE-ADDENDS))
 (18 18 (:REWRITE DEFAULT-+-2))
 (18 18 (:REWRITE DEFAULT-+-1))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:REWRITE |(< d (+ c x y))|))
 (8 8 (:REWRITE |(< 0 (- x))|))
 (4 4 (:REWRITE FOLD-CONSTS-IN-+))
 (3 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (3 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (3 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::SIPO-SREG$INPUT-FORMAT-N
 (333 18 (:DEFINITION INTEGER-ABS))
 (210 68 (:REWRITE DEFAULT-+-2))
 (180 9 (:DEFINITION LENGTH))
 (171 9 (:REWRITE |(+ (if a b c) x)|))
 (153 9 (:DEFINITION LEN))
 (99 9 (:REWRITE NUMERATOR-NEGATIVE))
 (88 68 (:REWRITE DEFAULT-+-1))
 (68 68 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (63 18 (:REWRITE STR::CONSP-OF-EXPLODE))
 (58 20 (:REWRITE DEFAULT-UNARY-MINUS))
 (51 24 (:REWRITE DEFAULT-CDR))
 (43 35 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (36 36 (:TYPE-PRESCRIPTION NUMERATOR-POSITIVE . 2))
 (36 36 (:TYPE-PRESCRIPTION NUMERATOR-POSITIVE . 1))
 (36 36 (:TYPE-PRESCRIPTION NUMERATOR-NEGATIVE . 2))
 (36 36 (:TYPE-PRESCRIPTION NUMERATOR-NEGATIVE . 1))
 (35 35 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (35 25 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (35 25 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (34 34 (:REWRITE |(< (- x) (- y))|))
 (29 29 (:REWRITE |(< (- x) 0)|))
 (28 24 (:REWRITE DEFAULT-<-2))
 (27 27 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (27 24 (:REWRITE DEFAULT-<-1))
 (22 22 (:REWRITE |(+ c (+ d x))|))
 (20 20 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (20 20 (:REWRITE FOLD-CONSTS-IN-+))
 (18 9 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (9 9 (:TYPE-PRESCRIPTION LEN))
 (9 9 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (9 9 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (9 9 (:REWRITE REDUCE-INTEGERP-+))
 (9 9 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (9 9 (:REWRITE INTEGERP==>NUMERATOR-=-X))
 (9 9 (:REWRITE INTEGERP==>DENOMINATOR-=-1))
 (9 9 (:REWRITE INTEGERP-MINUS-X))
 (9 9 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (9 9 (:REWRITE DEFAULT-REALPART))
 (9 9 (:REWRITE DEFAULT-NUMERATOR))
 (9 9 (:REWRITE DEFAULT-IMAGPART))
 (9 9 (:REWRITE DEFAULT-DENOMINATOR))
 (9 9 (:REWRITE |(equal (- x) (- y))|))
 (9 9 (:META META-INTEGERP-CORRECT))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 5 (:REWRITE ZP-OPEN))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (3 3 (:LINEAR ACL2-COUNT-CAR-CDR-LINEAR))
 (2 1 (:REWRITE |(< d (+ c x y))|))
 )
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-SIPO-SREG$INPUT-FORMAT-N-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-SIPO-SREG$INPUT-FORMAT-N)
(ADE::SIPO-SREG$INPUT-FORMAT-PLUS
 (199 87 (:REWRITE |(< d (+ c x))|))
 (130 130 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (113 113 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (113 113 (:REWRITE |(< (- x) (- y))|))
 (96 96 (:REWRITE SIMPLIFY-SUMS-<))
 (96 96 (:REWRITE DEFAULT-<-2))
 (96 96 (:REWRITE DEFAULT-<-1))
 (61 31 (:REWRITE DEFAULT-CDR))
 (60 30 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (58 28 (:REWRITE DEFAULT-CAR))
 (43 43 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (43 43 (:REWRITE NORMALIZE-ADDENDS))
 (43 43 (:REWRITE DEFAULT-+-2))
 (43 43 (:REWRITE DEFAULT-+-1))
 (42 42 (:REWRITE |(< 0 (- x))|))
 (30 30 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (25 25 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (17 17 (:REWRITE |(< d (+ c x y))|))
 (14 14 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (14 14 (:REWRITE REDUCE-INTEGERP-+))
 (14 14 (:REWRITE INTEGERP-MINUS-X))
 (14 14 (:REWRITE |(< (- x) 0)|))
 (14 14 (:META META-INTEGERP-CORRECT))
 (11 11 (:REWRITE FOLD-CONSTS-IN-+))
 (8 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (8 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (8 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::SIPO-SREG$DE-N
 (265 30 (:REWRITE ZP-OPEN))
 (108 12 (:REWRITE |(< d (+ c x))|))
 (62 2 (:DEFINITION ADE::SIPO-SREG$RUN))
 (36 36 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (31 31 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (24 24 (:REWRITE SIMPLIFY-SUMS-<))
 (24 24 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (24 24 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (24 24 (:REWRITE DEFAULT-<-2))
 (24 24 (:REWRITE DEFAULT-<-1))
 (24 24 (:REWRITE |(< (- x) (- y))|))
 (11 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (11 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (11 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (7 7 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE NORMALIZE-ADDENDS))
 (7 7 (:REWRITE DEFAULT-CDR))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE ADE::SIPO-SREG$INPUT-FORMAT-PLUS))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE ADE::DE-PLUS))
 )
(ADE::SIPO-SREG$EXTRACT)
(ADE::V-TO-NAT-OF-V-ZP
 (88 44 (:TYPE-PRESCRIPTION ADE::BOOLEANP-V-NZP))
 (44 44 (:TYPE-PRESCRIPTION ADE::BVP))
 (34 34 (:REWRITE ADE::V-NZP-AS-OR-CROCK))
 (22 12 (:REWRITE DEFAULT-*-2))
 (19 19 (:REWRITE DEFAULT-CDR))
 (17 17 (:REWRITE ADE::NOT-V-NZP-TAKE-NTHCDR))
 (15 15 (:REWRITE DEFAULT-CAR))
 (12 12 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (12 12 (:REWRITE DEFAULT-*-1))
 (12 6 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (12 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (12 6 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (11 6 (:REWRITE DEFAULT-+-2))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (6 6 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (6 6 (:REWRITE NORMALIZE-ADDENDS))
 (6 6 (:REWRITE DEFAULT-+-1))
 (6 6 (:REWRITE |(equal (- x) 0)|))
 (6 6 (:REWRITE |(equal (- x) (- y))|))
 (5 5 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 )
(ADE::SIPO-SREG$EXTRACT-NOT-EMPTY
 (722 722 (:REWRITE NTH-WHEN-PREFIXP))
 (586 436 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (586 436 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (586 436 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (536 134 (:DEFINITION STRIP-CARS))
 (449 255 (:REWRITE DEFAULT-+-2))
 (436 436 (:REWRITE |(equal (- x) (- y))|))
 (400 20 (:DEFINITION NTHCDR))
 (372 336 (:REWRITE DEFAULT-CDR))
 (282 282 (:REWRITE DEFAULT-CAR))
 (255 255 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (255 255 (:REWRITE NORMALIZE-ADDENDS))
 (255 255 (:REWRITE DEFAULT-+-1))
 (244 100 (:REWRITE |(expt 2^i n)|))
 (228 12 (:REWRITE ZP-OPEN))
 (216 8 (:REWRITE ADE::LEN-NTHCDR))
 (166 166 (:LINEAR LEN-WHEN-PREFIXP))
 (112 16 (:LINEAR EXPT-X->=-X))
 (112 16 (:LINEAR EXPT-X->-X))
 (112 16 (:LINEAR EXPT->-1-ONE))
 (100 100 (:REWRITE |(expt x (- n))|))
 (100 100 (:REWRITE |(expt 1/c n)|))
 (100 100 (:REWRITE |(expt (- x) n)|))
 (88 88 (:REWRITE DEFAULT-EXPT-1))
 (83 83 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (74 22 (:REWRITE ADE::F-GATES=B-GATES))
 (72 24 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (62 31 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$OUT-ACT))
 (60 60 (:TYPE-PRESCRIPTION STRIP-CARS))
 (60 12 (:REWRITE |(+ y x)|))
 (50 50 (:META META-INTEGERP-CORRECT))
 (40 20 (:REWRITE SIMPLIFY-SUMS-<))
 (40 20 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (40 20 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (40 20 (:REWRITE DEFAULT-<-2))
 (39 39 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 (32 32 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (32 32 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (32 32 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (32 32 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (28 26 (:REWRITE REDUCE-INTEGERP-+))
 (28 4 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (26 26 (:REWRITE INTEGERP-MINUS-X))
 (24 4 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (22 22 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (22 22 (:REWRITE |(equal (- x) 0)|))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (20 20 (:REWRITE DEFAULT-<-1))
 (20 20 (:REWRITE |(< (- x) (- y))|))
 (16 16 (:LINEAR EXPT->-1-TWO))
 (16 16 (:LINEAR EXPT-<-1-TWO))
 (16 16 (:LINEAR EXPT-<-1-ONE))
 (16 8 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$IN-ACT))
 (12 12 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (12 12 (:REWRITE |(< 0 (- x))|))
 (12 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (8 8 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$IN-ACT))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 )
(ADE::LEN-OF-SIPO-SREG$EXTRACT-LEMMA
 (518 19 (:DEFINITION NTHCDR))
 (304 16 (:REWRITE ZP-OPEN))
 (214 214 (:REWRITE NTH-WHEN-PREFIXP))
 (208 8 (:REWRITE ADE::LEN-NTHCDR))
 (184 46 (:DEFINITION STRIP-CARS))
 (155 107 (:REWRITE DEFAULT-CDR))
 (113 67 (:REWRITE DEFAULT-+-2))
 (100 100 (:REWRITE DEFAULT-CAR))
 (96 32 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (94 68 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (94 68 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (94 68 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (80 80 (:TYPE-PRESCRIPTION STRIP-CARS))
 (80 16 (:REWRITE |(+ y x)|))
 (73 19 (:REWRITE ADE::F-GATES=B-GATES))
 (68 68 (:REWRITE |(equal (- x) (- y))|))
 (67 67 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (67 67 (:REWRITE NORMALIZE-ADDENDS))
 (67 67 (:REWRITE DEFAULT-+-1))
 (48 24 (:REWRITE SIMPLIFY-SUMS-<))
 (48 24 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (48 24 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (48 24 (:REWRITE DEFAULT-<-2))
 (44 22 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$OUT-ACT))
 (40 40 (:LINEAR LEN-WHEN-PREFIXP))
 (30 30 (:TYPE-PRESCRIPTION BOOLEANP))
 (29 14 (:REWRITE |(expt 2^i n)|))
 (26 26 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (24 24 (:REWRITE DEFAULT-<-1))
 (24 24 (:REWRITE |(< (- x) (- y))|))
 (20 20 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (16 16 (:REWRITE |(< 0 (- x))|))
 (14 14 (:REWRITE |(expt x (- n))|))
 (14 14 (:REWRITE |(expt 1/c n)|))
 (14 14 (:REWRITE |(expt (- x) n)|))
 (14 2 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (14 2 (:LINEAR EXPT-X->=-X))
 (14 2 (:LINEAR EXPT-X->-X))
 (14 2 (:LINEAR EXPT->-1-ONE))
 (13 13 (:REWRITE DEFAULT-EXPT-1))
 (12 2 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (8 4 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::F-OR))
 (6 6 (:META META-INTEGERP-CORRECT))
 (6 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$IN-ACT))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (4 4 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (4 4 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (4 4 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (2 2 (:LINEAR EXPT->-1-TWO))
 (2 2 (:LINEAR EXPT-<-1-TWO))
 (2 2 (:LINEAR EXPT-<-1-ONE))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 )
(ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1
 (390 15 (:DEFINITION NTHCDR))
 (228 12 (:REWRITE ZP-OPEN))
 (168 42 (:DEFINITION STRIP-CARS))
 (158 158 (:REWRITE NTH-WHEN-PREFIXP))
 (121 85 (:REWRITE DEFAULT-CDR))
 (103 84 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (103 84 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (103 84 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (92 92 (:REWRITE DEFAULT-CAR))
 (84 84 (:REWRITE |(equal (- x) (- y))|))
 (78 50 (:REWRITE DEFAULT-+-2))
 (73 19 (:REWRITE ADE::F-GATES=B-GATES))
 (72 24 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (60 60 (:TYPE-PRESCRIPTION STRIP-CARS))
 (60 12 (:REWRITE |(+ y x)|))
 (50 50 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (50 50 (:REWRITE NORMALIZE-ADDENDS))
 (50 50 (:REWRITE DEFAULT-+-1))
 (44 22 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$OUT-ACT))
 (40 40 (:LINEAR LEN-WHEN-PREFIXP))
 (35 13 (:REWRITE |(expt 2^i n)|))
 (30 30 (:TYPE-PRESCRIPTION BOOLEANP))
 (26 26 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 (24 12 (:REWRITE SIMPLIFY-SUMS-<))
 (24 12 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (24 12 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (24 12 (:REWRITE DEFAULT-<-2))
 (20 20 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (14 2 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (14 2 (:LINEAR EXPT-X->=-X))
 (14 2 (:LINEAR EXPT-X->-X))
 (14 2 (:LINEAR EXPT->-1-ONE))
 (13 13 (:REWRITE |(expt x (- n))|))
 (13 13 (:REWRITE |(expt 1/c n)|))
 (13 13 (:REWRITE |(expt (- x) n)|))
 (12 12 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (12 12 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (12 12 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (12 12 (:REWRITE DEFAULT-<-1))
 (12 12 (:REWRITE |(< 0 (- x))|))
 (12 12 (:REWRITE |(< (- x) (- y))|))
 (12 2 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (11 11 (:REWRITE DEFAULT-EXPT-1))
 (10 10 (:META META-INTEGERP-CORRECT))
 (8 6 (:REWRITE REDUCE-INTEGERP-+))
 (8 4 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::F-OR))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$IN-ACT))
 (4 4 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (4 4 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (4 4 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (4 4 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (2 2 (:LINEAR EXPT->-1-TWO))
 (2 2 (:LINEAR EXPT-<-1-TWO))
 (2 2 (:LINEAR EXPT-<-1-ONE))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 )
(ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2
 (128 4 (:DEFINITION NTHCDR))
 (76 4 (:REWRITE ZP-OPEN))
 (48 48 (:TYPE-PRESCRIPTION ADE::NATP-V-TO-NAT))
 (38 2 (:DEFINITION LEN))
 (32 8 (:DEFINITION STRIP-CARS))
 (30 15 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$OUT-ACT))
 (26 14 (:REWRITE DEFAULT-CDR))
 (24 8 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (20 20 (:TYPE-PRESCRIPTION STRIP-CARS))
 (20 4 (:REWRITE |(+ y x)|))
 (18 18 (:REWRITE NTH-WHEN-PREFIXP))
 (16 16 (:REWRITE DEFAULT-CAR))
 (15 15 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (8 6 (:REWRITE DEFAULT-+-2))
 (8 4 (:REWRITE SIMPLIFY-SUMS-<))
 (8 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (8 4 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (8 4 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (6 6 (:REWRITE NORMALIZE-ADDENDS))
 (6 6 (:REWRITE DEFAULT-+-1))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (4 4 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (4 4 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE |(< 0 (- x))|))
 (4 4 (:REWRITE |(< (- x) (- y))|))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::SIPO-SREG$INV)
(ADE::LEN-OF-SIPO-SREG$EXTRACT-UPPER-BOUND
 (452 452 (:REWRITE NTH-WHEN-PREFIXP))
 (128 4 (:DEFINITION NTHCDR))
 (80 20 (:DEFINITION STRIP-CARS))
 (76 4 (:REWRITE ZP-OPEN))
 (65 37 (:REWRITE DEFAULT-+-2))
 (58 58 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE))
 (56 44 (:REWRITE DEFAULT-CDR))
 (42 34 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (42 34 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (42 34 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (40 40 (:REWRITE DEFAULT-CAR))
 (40 20 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (37 37 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (37 37 (:REWRITE DEFAULT-+-1))
 (34 34 (:REWRITE |(equal (- x) (- y))|))
 (28 16 (:REWRITE DEFAULT-<-2))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (22 22 (:REWRITE |(< (- x) (- y))|))
 (20 16 (:REWRITE DEFAULT-<-1))
 (13 2 (:REWRITE |(expt 2^i n)|))
 (12 12 (:TYPE-PRESCRIPTION STRIP-CARS))
 (12 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 6 (:REWRITE |(+ c (+ d x))|))
 (6 6 (:META META-INTEGERP-CORRECT))
 (6 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:REWRITE |(< (- x) 0)|))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (2 2 (:REWRITE |(expt x (- n))|))
 (2 2 (:REWRITE |(expt 1/c n)|))
 (2 2 (:REWRITE |(expt (- x) n)|))
 (2 2 (:REWRITE |(< (+ c x) d)|))
 (2 2 (:LINEAR ADE::SIPO-SREG$EXTRACT-NOT-EMPTY))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1 1 (:REWRITE DEFAULT-EXPT-1))
 )
(ADE::LEN-OF-SIPO-SREG$EXTRACT-UPPER-BOUND-WHEN-IN-ACT
 (261 261 (:REWRITE NTH-WHEN-PREFIXP))
 (132 6 (:DEFINITION NTHCDR))
 (76 4 (:REWRITE ZP-OPEN))
 (68 17 (:DEFINITION STRIP-CARS))
 (51 39 (:REWRITE DEFAULT-CDR))
 (49 27 (:REWRITE DEFAULT-+-2))
 (38 38 (:REWRITE DEFAULT-CAR))
 (31 17 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (28 14 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$IN-ACT))
 (27 27 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (27 27 (:REWRITE DEFAULT-+-1))
 (27 19 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (27 19 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (25 7 (:REWRITE ADE::F-GATES=B-GATES))
 (23 13 (:REWRITE DEFAULT-<-2))
 (20 20 (:LINEAR LEN-WHEN-PREFIXP))
 (19 19 (:REWRITE |(equal (- x) (- y))|))
 (17 17 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (17 17 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (17 17 (:REWRITE |(< (- x) (- y))|))
 (16 16 (:TYPE-PRESCRIPTION STRIP-CARS))
 (14 14 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 (14 2 (:LINEAR EXPT-X->=-X))
 (14 2 (:LINEAR EXPT-X->-X))
 (14 2 (:LINEAR EXPT->-1-ONE))
 (13 13 (:REWRITE DEFAULT-<-1))
 (12 4 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (10 10 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (9 9 (:REWRITE DEFAULT-EXPT-2))
 (9 9 (:REWRITE DEFAULT-EXPT-1))
 (9 9 (:REWRITE |(expt x (- n))|))
 (9 9 (:REWRITE |(expt 2^i n)|))
 (9 9 (:REWRITE |(expt 1/c n)|))
 (9 9 (:REWRITE |(expt (- x) n)|))
 (8 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (7 7 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (7 7 (:REWRITE |(< 0 (- x))|))
 (6 6 (:REWRITE |(+ c (+ d x))|))
 (4 4 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (4 4 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (4 4 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (4 4 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (3 3 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (3 3 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE |(< d (+ c x))|))
 (2 2 (:REWRITE |(< (+ c x) d)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (2 2 (:LINEAR EXPT->-1-TWO))
 (2 2 (:LINEAR EXPT-<-1-TWO))
 (2 2 (:LINEAR EXPT-<-1-ONE))
 (2 1 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:LINEAR ADE::SIPO-SREG$EXTRACT-NOT-EMPTY))
 )
(ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-1
 (2 2 (:REWRITE NTH-WHEN-PREFIXP))
 (2 1 (:DEFINITION NTHCDR))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-2
 (4 2 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-1))
 (4 1 (:REWRITE ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-1))
 (2 2 (:REWRITE NTH-WHEN-PREFIXP))
 (2 1 (:DEFINITION NTHCDR))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-3
 (4 2 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-2))
 (4 1 (:REWRITE ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-2))
 (4 1 (:REWRITE ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-1))
 (2 2 (:REWRITE NTH-WHEN-PREFIXP))
 (2 1 (:DEFINITION NTHCDR))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::V-TO-NAT-OF-REPEAT-LEMMA
 (291 40 (:REWRITE CONSP-OF-REPEAT))
 (250 41 (:REWRITE ZP-OPEN))
 (197 9 (:DEFINITION BINARY-APPEND))
 (168 19 (:REWRITE |(< d (+ c x))|))
 (145 8 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (116 18 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (96 18 (:REWRITE DEFAULT-CDR))
 (80 14 (:REWRITE DEFAULT-CAR))
 (70 70 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (68 4 (:REWRITE CAR-OF-APPEND))
 (57 6 (:LINEAR ADE::EXPT-LINEAR-LOWER-<=-INSTANCE))
 (53 49 (:REWRITE SIMPLIFY-SUMS-<))
 (53 49 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (53 49 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (52 49 (:REWRITE DEFAULT-<-2))
 (51 6 (:LINEAR EXPT-X->=-X))
 (51 6 (:LINEAR EXPT-X->-X))
 (50 49 (:REWRITE DEFAULT-<-1))
 (49 49 (:REWRITE |(< (- x) (- y))|))
 (24 6 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (24 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (24 6 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (16 8 (:REWRITE DEFAULT-*-2))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (14 1 (:DEFINITION NATP))
 (13 9 (:REWRITE DEFAULT-+-2))
 (12 12 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (12 12 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (12 12 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE NORMALIZE-ADDENDS))
 (9 9 (:REWRITE DEFAULT-EXPT-2))
 (9 9 (:REWRITE DEFAULT-EXPT-1))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 9 (:REWRITE |(expt x (- n))|))
 (9 9 (:REWRITE |(expt 2^i n)|))
 (9 9 (:REWRITE |(expt 1/c n)|))
 (9 9 (:REWRITE |(expt (- x) n)|))
 (9 1 (:REWRITE |(< (+ c x) d)|))
 (8 8 (:REWRITE DEFAULT-*-1))
 (7 6 (:LINEAR EXPT-<-1-TWO))
 (6 6 (:REWRITE |(equal (- x) (- y))|))
 (6 6 (:LINEAR EXPT->-1-TWO))
 (6 6 (:LINEAR EXPT-<-1-ONE))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (5 5 (:REWRITE REDUCE-INTEGERP-+))
 (5 5 (:REWRITE INTEGERP-MINUS-X))
 (5 5 (:REWRITE |(< (- x) 0)|))
 (5 5 (:META META-INTEGERP-CORRECT))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (3 3 (:REWRITE |(< 0 (- x))|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::SIPO-SREG$INV-PRESERVED
 (976 93 (:DEFINITION STRIP-CARS))
 (962 962 (:REWRITE NTH-WHEN-PREFIXP))
 (643 451 (:REWRITE DEFAULT-CDR))
 (556 337 (:REWRITE DEFAULT-CAR))
 (540 20 (:DEFINITION ADE::V-THREEFIX))
 (486 37 (:REWRITE ZP-OPEN))
 (482 74 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (482 74 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (482 74 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (468 15 (:DEFINITION BINARY-APPEND))
 (434 31 (:REWRITE CONSP-OF-REPEAT))
 (418 209 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (407 227 (:REWRITE DEFAULT-+-2))
 (364 41 (:REWRITE |(< d (+ c x))|))
 (227 227 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (227 227 (:REWRITE DEFAULT-+-1))
 (225 17 (:REWRITE CAR-OF-APPEND))
 (211 30 (:REWRITE ADE::CAR-V-THREEFIX))
 (209 209 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (191 13 (:DEFINITION PAIRLIS$))
 (184 184 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (162 30 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (122 122 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (122 3 (:REWRITE ADE::NTHCDR-APPEND))
 (104 16 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (100 50 (:DEFINITION ADE::3V-FIX))
 (99 10 (:REWRITE REPEAT-WHEN-ZP))
 (83 72 (:REWRITE SIMPLIFY-SUMS-<))
 (81 81 (:TYPE-PRESCRIPTION BOOLEANP))
 (79 72 (:REWRITE DEFAULT-<-1))
 (76 72 (:REWRITE DEFAULT-<-2))
 (74 74 (:REWRITE |(equal (- x) (- y))|))
 (74 74 (:REWRITE |(< (- x) (- y))|))
 (71 71 (:TYPE-PRESCRIPTION ADE::3VP))
 (56 56 (:LINEAR LEN-WHEN-PREFIXP))
 (49 7 (:LINEAR EXPT-X->=-X))
 (49 7 (:LINEAR EXPT-X->-X))
 (49 7 (:LINEAR EXPT->-1-ONE))
 (42 21 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-3))
 (37 37 (:REWRITE DEFAULT-EXPT-2))
 (37 37 (:REWRITE DEFAULT-EXPT-1))
 (37 37 (:REWRITE |(expt x (- n))|))
 (37 37 (:REWRITE |(expt 2^i n)|))
 (37 37 (:REWRITE |(expt 1/c n)|))
 (37 37 (:REWRITE |(expt (- x) n)|))
 (36 3 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (28 28 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (16 16 (:REWRITE DEFAULT-UNARY-MINUS))
 (14 14 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (14 14 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (14 14 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (14 14 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (12 2 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (9 9 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (9 9 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (9 9 (:REWRITE |(< 0 (- x))|))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (8 8 (:REWRITE |(equal (- x) 0)|))
 (8 2 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (7 7 (:LINEAR EXPT->-1-TWO))
 (7 7 (:LINEAR EXPT-<-1-TWO))
 (7 7 (:LINEAR EXPT-<-1-ONE))
 (6 6 (:TYPE-PRESCRIPTION ZP))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (5 5 (:REWRITE |(< (- x) 0)|))
 (3 3 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (2 2 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (1 1 (:REWRITE |(< (+ c x) d)|))
 )
(ADE::SIPO-SREG$EXTRACTED-STEP
 (18 18 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-3))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$OUT-ACT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$IN-ACT))
 )
(ADE::NTHCDR-APPEND-2
 (1440 565 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (565 565 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (260 5 (:REWRITE ADE::NTHCDR-APPEND))
 (125 5 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (125 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (125 5 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (79 44 (:REWRITE DEFAULT-CDR))
 (78 49 (:REWRITE DEFAULT-+-2))
 (49 49 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (49 49 (:REWRITE NORMALIZE-ADDENDS))
 (49 49 (:REWRITE DEFAULT-+-1))
 (42 25 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (36 30 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (34 21 (:REWRITE SIMPLIFY-SUMS-<))
 (33 33 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (28 21 (:REWRITE DEFAULT-<-1))
 (27 21 (:REWRITE DEFAULT-<-2))
 (25 25 (:REWRITE |(< (- x) (- y))|))
 (24 24 (:LINEAR LEN-WHEN-PREFIXP))
 (15 15 (:REWRITE DEFAULT-CAR))
 (13 8 (:REWRITE |(< (+ c x) d)|))
 (12 12 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (6 6 (:REWRITE |(< 0 (- x))|))
 (5 5 (:REWRITE CONSP-OF-APPEND))
 (5 5 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (5 5 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:META META-INTEGERP-CORRECT))
 )
(ADE::NTHCDR-OF-LEN-OF-LIST
 (76 4 (:REWRITE ZP-OPEN))
 (24 8 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (16 16 (:TYPE-PRESCRIPTION ADE::BVP))
 (14 9 (:REWRITE DEFAULT-+-2))
 (12 12 (:REWRITE DEFAULT-CDR))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE NORMALIZE-ADDENDS))
 (9 9 (:REWRITE DEFAULT-+-1))
 (8 4 (:REWRITE SIMPLIFY-SUMS-<))
 (8 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (8 4 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (8 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (4 4 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (4 4 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE |(< 0 (- x))|))
 (4 4 (:REWRITE |(< (- x) (- y))|))
 )
(ADE::SIPO-SREG$EXTRACTED-STEP-CORRECT
 (41858 581 (:DEFINITION STRIP-CARS))
 (37335 1622 (:REWRITE DEFAULT-CAR))
 (29641 4478 (:REWRITE DEFAULT-CDR))
 (9725 84 (:DEFINITION BINARY-APPEND))
 (9167 54 (:DEFINITION ADE::V-THREEFIX))
 (7410 4073 (:REWRITE DEFAULT-+-2))
 (4073 4073 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (4073 4073 (:REWRITE DEFAULT-+-1))
 (3918 2150 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (3682 2134 (:REWRITE DEFAULT-<-2))
 (3311 47 (:DEFINITION PAIRLIS$))
 (3300 3300 (:REWRITE NTH-WHEN-PREFIXP))
 (3263 370 (:REWRITE |(< d (+ c x))|))
 (3232 3232 (:LINEAR LEN-WHEN-PREFIXP))
 (3229 2134 (:REWRITE SIMPLIFY-SUMS-<))
 (3117 2150 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2672 151 (:REWRITE CONSP-OF-REPEAT))
 (2506 600 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2354 50 (:REWRITE ADE::CAR-V-THREEFIX))
 (2224 2134 (:REWRITE DEFAULT-<-1))
 (2179 2152 (:REWRITE |(< (- x) (- y))|))
 (2101 600 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2058 559 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1616 1616 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1591 1591 (:REWRITE |(< 0 (- x))|))
 (1575 1575 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1561 5 (:REWRITE TAKE-WHEN-PREFIXP))
 (1527 18 (:REWRITE ADE::LEN-NTHCDR))
 (1211 10 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (954 76 (:REWRITE |(< (+ c x) d)|))
 (945 55 (:DEFINITION NFIX))
 (881 10 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (682 666 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (600 600 (:REWRITE |(equal (- x) (- y))|))
 (585 55 (:REWRITE |(+ (if a b c) x)|))
 (569 84 (:REWRITE REPEAT-WHEN-ZP))
 (447 21 (:DEFINITION NATP))
 (284 86 (:REWRITE |(equal (+ c x) d)|))
 (265 7 (:REWRITE TAKE-WHEN-ATOM))
 (238 5 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (210 30 (:LINEAR EXPT-X->=-X))
 (210 30 (:LINEAR EXPT-X->-X))
 (210 30 (:LINEAR EXPT->-1-ONE))
 (208 172 (:REWRITE |(expt 2^i n)|))
 (208 104 (:DEFINITION ADE::3V-FIX))
 (205 5 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (205 5 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (193 12 (:REWRITE |(< x (if a b c))|))
 (183 9 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (172 172 (:REWRITE |(expt x (- n))|))
 (172 172 (:REWRITE |(expt 1/c n)|))
 (172 172 (:REWRITE |(expt (- x) n)|))
 (171 171 (:REWRITE DEFAULT-EXPT-1))
 (142 21 (:REWRITE |(+ x (if a b c))|))
 (105 105 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (104 104 (:TYPE-PRESCRIPTION ADE::3VP))
 (70 5 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (65 65 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (65 65 (:REWRITE |(equal (- x) 0)|))
 (60 60 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (60 60 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (60 60 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (60 60 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (57 44 (:REWRITE DEFAULT-UNARY-MINUS))
 (48 34 (:REWRITE |(- (- x))|))
 (48 8 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (43 22 (:REWRITE ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-3))
 (42 42 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (37 37 (:REWRITE |(equal (+ d x) (+ c y))|))
 (37 37 (:REWRITE |(equal (+ c x) (+ d y))|))
 (32 8 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (30 30 (:TYPE-PRESCRIPTION ADE::F-AND4))
 (30 30 (:LINEAR EXPT->-1-TWO))
 (30 30 (:LINEAR EXPT-<-1-TWO))
 (30 30 (:LINEAR EXPT-<-1-ONE))
 (24 24 (:TYPE-PRESCRIPTION ADE::F-AND3))
 (21 21 (:TYPE-PRESCRIPTION NATP))
 (20 20 (:TYPE-PRESCRIPTION PREFIXP))
 (15 5 (:REWRITE |(< (if a b c) x)|))
 (10 10 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (10 10 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (10 10 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (10 10 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (8 8 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (8 8 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (6 6 (:REWRITE FOLD-CONSTS-IN-+))
 (6 6 (:META META-INTEGERP-CORRECT))
 (6 4 (:REWRITE REDUCE-INTEGERP-+))
 (5 5 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (3 3 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 )
(ADE::SIPO-SREG$VALID-ST-PRESERVED
 (110332 194 (:DEFINITION ADE::V-THREEFIX))
 (102488 10178 (:REWRITE DEFAULT-CDR))
 (100306 451 (:REWRITE ADE::NTHCDR-OF-LEN-OF-LIST))
 (81061 2533 (:REWRITE DEFAULT-CAR))
 (68784 218 (:DEFINITION BINARY-APPEND))
 (65469 59 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (53770 770 (:DEFINITION STRIP-CARS))
 (38605 436 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (20130 12010 (:REWRITE DEFAULT-+-2))
 (12920 76 (:REWRITE ADE::CADR-V-THREEFIX))
 (12010 12010 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (12010 12010 (:REWRITE DEFAULT-+-1))
 (9952 60 (:REWRITE CAR-OF-APPEND))
 (7182 21 (:REWRITE ADE::CADDR-V-THREEFIX))
 (6548 128 (:REWRITE ADE::CAR-V-THREEFIX))
 (6333 756 (:REWRITE |(< d (+ c x))|))
 (3712 285 (:REWRITE ZP-OPEN))
 (3682 263 (:REWRITE CONSP-OF-REPEAT))
 (3653 3653 (:REWRITE NTH-WHEN-PREFIXP))
 (3601 45 (:DEFINITION PAIRLIS$))
 (3123 1971 (:REWRITE DEFAULT-<-2))
 (3057 1971 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2981 1971 (:REWRITE SIMPLIFY-SUMS-<))
 (2981 1971 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2744 2744 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2740 2740 (:LINEAR LEN-WHEN-PREFIXP))
 (1981 1971 (:REWRITE DEFAULT-<-1))
 (1971 1971 (:REWRITE |(< (- x) (- y))|))
 (1370 1370 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1163 1163 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1163 1163 (:REWRITE |(< 0 (- x))|))
 (966 321 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (966 321 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (966 321 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (838 419 (:DEFINITION ADE::3V-FIX))
 (582 582 (:TYPE-PRESCRIPTION ADE::3VP))
 (555 555 (:TYPE-PRESCRIPTION BOOLEANP))
 (468 153 (:REWRITE REPEAT-WHEN-ZP))
 (321 321 (:REWRITE |(equal (- x) (- y))|))
 (233 108 (:REWRITE |(equal (+ c x) d)|))
 (96 96 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (96 16 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (80 80 (:REWRITE DEFAULT-UNARY-MINUS))
 (74 74 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (74 74 (:REWRITE |(equal (- x) 0)|))
 (73 73 (:REWRITE DEFAULT-EXPT-2))
 (73 73 (:REWRITE DEFAULT-EXPT-1))
 (73 73 (:REWRITE |(expt x (- n))|))
 (73 73 (:REWRITE |(expt 2^i n)|))
 (73 73 (:REWRITE |(expt 1/c n)|))
 (73 73 (:REWRITE |(expt (- x) n)|))
 (70 10 (:LINEAR EXPT-X->=-X))
 (70 10 (:LINEAR EXPT-X->-X))
 (70 10 (:LINEAR EXPT->-1-ONE))
 (64 16 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (49 49 (:TYPE-PRESCRIPTION ADE::BOOLEANP-IF*))
 (48 48 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (26 26 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (24 24 (:TYPE-PRESCRIPTION ADE::F-AND))
 (22 22 (:TYPE-PRESCRIPTION ZP))
 (20 20 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (20 20 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (20 20 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (20 20 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (20 20 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (16 16 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (16 16 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (10 10 (:LINEAR EXPT->-1-TWO))
 (10 10 (:LINEAR EXPT-<-1-TWO))
 (10 10 (:LINEAR EXPT-<-1-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE |(< (- x) 0)|))
 )
(ADE::SIPO-SREG$EXTRACT-LEMMA
 (3561 83 (:REWRITE ADE::NTHCDR-OF-LEN-OF-LIST))
 (3212 1358 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-1))
 (2984 1422 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-2))
 (2904 2904 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 (2667 41 (:DEFINITION NTHCDR))
 (1838 248 (:REWRITE ADE::F-GATES=B-GATES))
 (1194 41 (:REWRITE ADE::LEN-CDR))
 (1024 32 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (922 182 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (920 2 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (801 182 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (791 176 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (748 65 (:DEFINITION STRIP-CARS))
 (552 552 (:REWRITE NTH-WHEN-PREFIXP))
 (456 456 (:TYPE-PRESCRIPTION BOOLEANP))
 (416 416 (:LINEAR LEN-WHEN-PREFIXP))
 (371 193 (:REWRITE DEFAULT-+-2))
 (298 277 (:REWRITE DEFAULT-CDR))
 (272 48 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (208 208 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (193 193 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (193 193 (:REWRITE NORMALIZE-ADDENDS))
 (193 193 (:REWRITE DEFAULT-+-1))
 (182 182 (:REWRITE |(equal (- x) (- y))|))
 (182 114 (:REWRITE ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-2))
 (176 32 (:REWRITE ADE::BOOLEANP-OF-F-BUF))
 (160 64 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (133 7 (:REWRITE ZP-OPEN))
 (130 130 (:REWRITE DEFAULT-CAR))
 (112 56 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$OUT-ACT))
 (112 48 (:REWRITE ADE::F-BUF-OF-3VP))
 (108 62 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (107 62 (:REWRITE DEFAULT-<-2))
 (104 62 (:REWRITE SIMPLIFY-SUMS-<))
 (104 62 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (64 64 (:TYPE-PRESCRIPTION ADE::3VP))
 (63 62 (:REWRITE DEFAULT-<-1))
 (62 62 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (62 62 (:REWRITE |(< (- x) (- y))|))
 (45 45 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (45 45 (:REWRITE |(< 0 (- x))|))
 (35 7 (:REWRITE |(+ y x)|))
 (32 32 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (32 32 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (32 18 (:REWRITE |(expt 2^i n)|))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (21 3 (:LINEAR EXPT-X->=-X))
 (21 3 (:LINEAR EXPT-X->-X))
 (21 3 (:LINEAR EXPT->-1-ONE))
 (20 11 (:REWRITE |(equal (+ c x) d)|))
 (18 18 (:REWRITE |(expt x (- n))|))
 (18 18 (:REWRITE |(expt 1/c n)|))
 (18 18 (:REWRITE |(expt (- x) n)|))
 (17 17 (:REWRITE DEFAULT-EXPT-1))
 (16 8 (:REWRITE |(+ c (+ d x))|))
 (6 6 (:META META-INTEGERP-CORRECT))
 (6 6 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (6 6 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (6 6 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (6 6 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (6 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (3 3 (:LINEAR EXPT->-1-TWO))
 (3 3 (:LINEAR EXPT-<-1-TWO))
 (3 3 (:LINEAR EXPT-<-1-ONE))
 (2 2 (:REWRITE |(equal (+ d x) (+ c y))|))
 (2 2 (:REWRITE |(equal (+ c x) (+ d y))|))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 )
(ADE::SIPO-SREG$IN-SEQ
 (12 12 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-3))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$IN-ACT))
 )
(ADE::SIPO-SREG$IN-SEQ-NETLIST
 (12 12 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-3))
 (12 6 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-1))
 )
(ADE::SIPO-SREG$IN-SEQ-LEMMA
 (725 65 (:REWRITE ZP-OPEN))
 (434 296 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$IN-ACT))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (276 58 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (276 58 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (276 58 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (213 35 (:DEFINITION BINARY-APPEND))
 (188 40 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (160 32 (:REWRITE |(+ c (+ d x))|))
 (120 120 (:REWRITE DEFAULT-CAR))
 (115 115 (:REWRITE DEFAULT-CDR))
 (104 104 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (94 94 (:REWRITE NTH-WHEN-PREFIXP))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (84 14 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (80 80 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (80 80 (:REWRITE NORMALIZE-ADDENDS))
 (80 80 (:REWRITE DEFAULT-+-2))
 (80 80 (:REWRITE DEFAULT-+-1))
 (64 64 (:REWRITE SIMPLIFY-SUMS-<))
 (64 64 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (64 64 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (64 64 (:REWRITE DEFAULT-<-2))
 (64 64 (:REWRITE DEFAULT-<-1))
 (64 64 (:REWRITE |(< (- x) (- y))|))
 (58 58 (:REWRITE |(equal (- x) (- y))|))
 (50 50 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$STEP))
 (42 42 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-2))
 (14 14 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (14 14 (:REWRITE ADE::SIPO-SREG$EXTRACT-LEMMA))
 (14 14 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (12 12 (:REWRITE ADE::SIPO-SREG$INPUT-FORMAT-PLUS))
 (10 10 (:TYPE-PRESCRIPTION ADE::DE))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::SIPO-SREG$OUT-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 )
(ADE::SIPO-SREG$OUT-SEQ-NETLIST
 (12 6 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-2))
 (6 6 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 )
(ADE::SIPO-SREG$OUT-SEQ-LEMMA
 (1140 36 (:REWRITE ADE::NTHCDR-OF-LEN-OF-LIST))
 (954 78 (:DEFINITION LEN))
 (725 65 (:REWRITE ZP-OPEN))
 (684 6 (:DEFINITION TAKE))
 (640 46 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (434 296 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$OUT-ACT))
 (398 84 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (398 84 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (398 84 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (384 6 (:DEFINITION NTHCDR))
 (378 12 (:REWRITE ADE::LEN-CDR))
 (372 46 (:REWRITE |(< d (+ c x))|))
 (286 100 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (271 181 (:REWRITE DEFAULT-CDR))
 (230 164 (:REWRITE DEFAULT-+-2))
 (216 108 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (213 35 (:DEFINITION BINARY-APPEND))
 (182 40 (:REWRITE |(+ c (+ d x))|))
 (180 12 (:REWRITE ADE::LEN-NTHCDR))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (165 129 (:REWRITE DEFAULT-CAR))
 (164 164 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (164 164 (:REWRITE DEFAULT-+-1))
 (140 140 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (136 100 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (132 132 (:REWRITE NTH-WHEN-PREFIXP))
 (124 94 (:REWRITE SIMPLIFY-SUMS-<))
 (120 120 (:LINEAR LEN-WHEN-PREFIXP))
 (118 94 (:REWRITE DEFAULT-<-2))
 (116 116 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (100 100 (:REWRITE |(< (- x) (- y))|))
 (100 94 (:REWRITE DEFAULT-<-1))
 (84 84 (:REWRITE |(equal (- x) (- y))|))
 (84 12 (:REWRITE TAKE-WHEN-ATOM))
 (60 60 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (57 57 (:REWRITE ADE::SIPO-SREG$EXTRACT-LEMMA))
 (56 14 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (50 50 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$STEP))
 (46 46 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (46 46 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (36 36 (:REWRITE ADE::LEN-SIPO-SREG$DATA-OUT-2))
 (36 36 (:REWRITE CDR-CONS))
 (28 28 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-1))
 (12 12 (:REWRITE ADE::SIPO-SREG$INPUT-FORMAT-PLUS))
 (12 12 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (12 12 (:REWRITE |(equal (+ c x) d)|))
 (12 12 (:REWRITE |(< 0 (- x))|))
 (10 10 (:TYPE-PRESCRIPTION ADE::DE))
 (6 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (6 6 (:REWRITE |(< (+ c x) d)|))
 (6 6 (:REWRITE |(+ 0 x)|))
 )
(ADE::APPEND1)
(ADE::PACK-REV
 (1193 9 (:LINEAR ACL2-COUNT-CAR-CDR-LINEAR))
 (1073 58 (:DEFINITION INTEGER-ABS))
 (878 334 (:REWRITE DEFAULT-+-2))
 (580 29 (:DEFINITION LENGTH))
 (551 29 (:REWRITE |(+ (if a b c) x)|))
 (413 17 (:REWRITE ADE::NTHCDR-OF-LEN-OF-LIST))
 (405 334 (:REWRITE DEFAULT-+-1))
 (334 334 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (334 334 (:REWRITE NORMALIZE-ADDENDS))
 (319 29 (:REWRITE NUMERATOR-NEGATIVE))
 (203 58 (:REWRITE STR::CONSP-OF-EXPLODE))
 (190 103 (:REWRITE DEFAULT-CDR))
 (187 114 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (181 111 (:REWRITE SIMPLIFY-SUMS-<))
 (176 146 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (174 58 (:REWRITE DEFAULT-UNARY-MINUS))
 (161 111 (:REWRITE DEFAULT-<-2))
 (160 142 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (143 143 (:REWRITE |(< (- x) (- y))|))
 (131 111 (:REWRITE DEFAULT-<-1))
 (116 116 (:TYPE-PRESCRIPTION NUMERATOR-POSITIVE . 2))
 (116 116 (:TYPE-PRESCRIPTION NUMERATOR-POSITIVE . 1))
 (116 116 (:TYPE-PRESCRIPTION NUMERATOR-NEGATIVE . 2))
 (116 116 (:TYPE-PRESCRIPTION NUMERATOR-NEGATIVE . 1))
 (104 104 (:LINEAR LEN-WHEN-PREFIXP))
 (99 47 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (92 92 (:REWRITE FOLD-CONSTS-IN-+))
 (87 87 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (87 87 (:REWRITE |(< (- x) 0)|))
 (58 58 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (58 29 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (52 52 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (50 47 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (47 47 (:REWRITE |(equal (- x) (- y))|))
 (45 43 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (44 44 (:REWRITE DEFAULT-CAR))
 (29 29 (:REWRITE REDUCE-INTEGERP-+))
 (29 29 (:REWRITE INTEGERP==>NUMERATOR-=-X))
 (29 29 (:REWRITE INTEGERP==>DENOMINATOR-=-1))
 (29 29 (:REWRITE INTEGERP-MINUS-X))
 (29 29 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (29 29 (:REWRITE DEFAULT-REALPART))
 (29 29 (:REWRITE DEFAULT-NUMERATOR))
 (29 29 (:REWRITE DEFAULT-IMAGPART))
 (29 29 (:REWRITE DEFAULT-DENOMINATOR))
 (29 29 (:META META-INTEGERP-CORRECT))
 (18 11 (:REWRITE |(equal (+ c x) d)|))
 (15 9 (:REWRITE |(< d (+ c x y))|))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (4 4 (:REWRITE |(< 0 (- x))|))
 (3 3 (:REWRITE |(equal (+ d x) (+ c y))|))
 (3 3 (:REWRITE |(equal (+ c x) (+ d y))|))
 (3 3 (:REWRITE |(< (+ c x) d)|))
 )
(ADE::SIPO-SREG$DATAFLOW-CORRECT-AUX
 (14 2 (:DEFINITION LEN))
 (4 2 (:REWRITE SIMPLIFY-SUMS-<))
 (4 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (4 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (4 2 (:REWRITE DEFAULT-<-2))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2 2 (:REWRITE NORMALIZE-ADDENDS))
 (2 2 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 )
(ADE::SIPO-SREG$DATAFLOW-CORRECT
 (13069 103 (:REWRITE TAKE-OF-TOO-MANY))
 (8983 16 (:REWRITE ADE::NTHCDR-APPEND))
 (8167 30 (:DEFINITION TAKE))
 (7673 1164 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (6098 629 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (5508 29 (:DEFINITION NTHCDR))
 (5247 8 (:REWRITE TAKE-OF-CONS))
 (4475 8 (:REWRITE ADE::NTHCDR-CONS))
 (3617 2062 (:REWRITE DEFAULT-+-2))
 (3148 155 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (3104 314 (:LINEAR ADE::LEN-OF-SIPO-SREG$EXTRACT-UPPER-BOUND))
 (2578 40 (:DEFINITION NATP))
 (2442 1311 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-2))
 (2190 2062 (:REWRITE DEFAULT-+-1))
 (2138 629 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2062 2062 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1999 556 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1976 16 (:REWRITE |(< (if a b c) x)|))
 (1746 1746 (:LINEAR LEN-WHEN-PREFIXP))
 (1663 271 (:DEFINITION BINARY-APPEND))
 (1641 59 (:REWRITE ADE::LEN-CDR))
 (1580 1580 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (1166 1166 (:REWRITE |(< (- x) (- y))|))
 (1124 947 (:REWRITE DEFAULT-<-2))
 (1066 51 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (1001 947 (:REWRITE DEFAULT-<-1))
 (936 16 (:DEFINITION NFIX))
 (903 15 (:REWRITE REPEAT-WHEN-ZP))
 (873 873 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (629 629 (:REWRITE |(equal (- x) (- y))|))
 (622 326 (:REWRITE |(- (- x))|))
 (510 88 (:REWRITE TAKE-WHEN-ATOM))
 (459 153 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (366 22 (:REWRITE |(+ (+ x y) z)|))
 (363 363 (:REWRITE NTH-WHEN-PREFIXP))
 (324 120 (:REWRITE REV-WHEN-NOT-CONSP))
 (306 306 (:TYPE-PRESCRIPTION ADE::BVP))
 (292 292 (:LINEAR ADE::SIPO-SREG$EXTRACT-NOT-EMPTY))
 (232 160 (:REWRITE |(< (+ c x) d)|))
 (179 129 (:REWRITE |(equal (+ c x) d)|))
 (163 155 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (146 146 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (142 142 (:REWRITE FOLD-CONSTS-IN-+))
 (128 8 (:DEFINITION POSP))
 (110 110 (:REWRITE |(< 0 (- x))|))
 (103 103 (:TYPE-PRESCRIPTION NFIX))
 (89 59 (:REWRITE DEFAULT-UNARY-MINUS))
 (80 64 (:REWRITE |(< d (+ c x y))|))
 (78 62 (:REWRITE |(equal (+ c x y) d)|))
 (76 76 (:REWRITE ADE::SIPO-SREG$RUN-PLUS))
 (62 46 (:REWRITE |(< (+ d x) (+ c y))|))
 (59 45 (:REWRITE |(equal (+ d x) (+ c y))|))
 (57 57 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (56 56 (:REWRITE |(< (+ c x y) d)|))
 (47 47 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (47 47 (:REWRITE |(equal (- x) 0)|))
 (47 47 (:REWRITE |(< (- x) 0)|))
 (46 46 (:REWRITE |(< (+ c x) (+ d y))|))
 (45 45 (:REWRITE ADE::SIPO-SREG$INPUT-FORMAT-PLUS))
 (45 45 (:REWRITE |(equal (+ c x) (+ d y))|))
 (40 40 (:TYPE-PRESCRIPTION NATP))
 (13 13 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (11 11 (:REWRITE REDUCE-INTEGERP-+))
 (11 11 (:REWRITE INTEGERP-MINUS-X))
 (11 11 (:META META-INTEGERP-CORRECT))
 (8 8 (:TYPE-PRESCRIPTION POSP))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (4 4 (:REWRITE DEFAULT-UNARY-/))
 )
(ADE::SIPO-SREG$FUNCTIONALLY-CORRECT
 (417 4 (:DEFINITION ADE::SIPO-SREG$OUT-SEQ))
 (192 4 (:DEFINITION ADE::SIPO-SREG$IN-SEQ))
 (128 4 (:REWRITE ADE::SIPO-SREG$OUT-ACT-INACTIVE))
 (115 4 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-2))
 (106 106 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT))
 (104 52 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-2))
 (75 18 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (75 18 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (75 18 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (72 12 (:DEFINITION BINARY-APPEND))
 (60 24 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (54 6 (:DEFINITION LEN))
 (52 52 (:TYPE-PRESCRIPTION ZP))
 (52 26 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$IN-ACT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-SIPO-SREG$OUT-ACT))
 (34 34 (:REWRITE ZP-OPEN))
 (33 33 (:TYPE-PRESCRIPTION LEN))
 (33 3 (:LINEAR ADE::LEN-OF-SIPO-SREG$EXTRACT-UPPER-BOUND))
 (32 32 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$IN-SEQ))
 (30 30 (:REWRITE DEFAULT-CDR))
 (26 26 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$IN-ACT))
 (24 18 (:REWRITE DEFAULT-+-2))
 (24 6 (:REWRITE ADE::OPEN-SIPO-SREG$INPUT-FORMAT-N-ZP))
 (24 6 (:REWRITE ADE::OPEN-SIPO-SREG$INPUT-FORMAT-N))
 (24 4 (:REWRITE ADE::SIPO-SREG$IN-ACT-INACTIVE))
 (22 4 (:REWRITE ADE::SIPO-SREG$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (20 20 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$OUT-ACT))
 (20 20 (:REWRITE DEFAULT-CAR))
 (18 18 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (18 18 (:REWRITE NORMALIZE-ADDENDS))
 (18 18 (:REWRITE DEFAULT-+-1))
 (18 18 (:REWRITE |(equal (- x) (- y))|))
 (16 8 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$INPUT-FORMAT-LEMMA-1))
 (16 4 (:REWRITE REV-WHEN-NOT-CONSP))
 (16 4 (:REWRITE ADE::OPEN-DE-N-ZP))
 (16 4 (:REWRITE ADE::OPEN-DE-N))
 (12 3 (:REWRITE ADE::OPEN-SIPO-SREG$RUN-ZP))
 (12 3 (:REWRITE ADE::OPEN-SIPO-SREG$RUN))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (5 5 (:REWRITE ADE::LEN-OF-SIPO-SREG$EXTRACT-CONTRAPOSITIVE-LEMMA-1))
 (4 4 (:REWRITE ADE::SIPO-SREG$EXTRACT-LEMMA))
 (3 3 (:TYPE-PRESCRIPTION ADE::SIPO-SREG$RUN))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-N))
 (3 3 (:LINEAR ADE::SIPO-SREG$EXTRACT-NOT-EMPTY))
 (3 3 (:LINEAR ADE::LEN-OF-SIPO-SREG$EXTRACT-UPPER-BOUND-WHEN-IN-ACT))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )