(ADE::COMP-GCD-COND$DATA-INS-LEN
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-SUMS-<))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (1 1 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (1 1 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:REWRITE |(< (- x) (- y))|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::COMP-GCD-COND$INS-LEN)
(ADE::COMP-GCD-COND*)
(ADE::COMP-GCD-COND*$DESTRUCTURE
 (520 47 (:DEFINITION BINARY-APPEND))
 (427 94 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (100 10 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (57 57 (:REWRITE DEFAULT-CDR))
 (52 52 (:REWRITE DEFAULT-CAR))
 (18 18 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (18 18 (:REWRITE DEFAULT-*-2))
 (18 18 (:REWRITE DEFAULT-*-1))
 )
(ADE::NOT-PRIMP-COMP-GCD-COND
 (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::COMP-GCD-COND$NETLIST)
(ADE::COMP-GCD-COND&)
(ADE::CHECK-COMP-GCD-COND$NETLIST-64)
(ADE::COMP-GCD-COND$ST-FORMAT)
(ADE::COMP-GCD-COND$ST-FORMAT=>CONSTRAINT
 (28 4 (:DEFINITION LEN))
 (10 10 (: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))|))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::COMP-GCD-COND$VALID-ST)
(ADE::COMP-GCD-COND$VALID-ST=>CONSTRAINT
 (28 4 (:DEFINITION LEN))
 (20 16 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (20 16 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (20 16 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (18 18 (:REWRITE NTH-WHEN-PREFIXP))
 (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 |(equal (- x) (- y))|))
 (16 16 (:REWRITE |(< (- x) (- y))|))
 (16 4 (:DEFINITION STRIP-CARS))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-CAR))
 (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-+-1))
 )
(ADE::COMP-GCD-COND$VALID-ST=>ST-FORMAT
 (6 6 (:REWRITE NTH-WHEN-PREFIXP))
 )
(ADE::COMP-GCD-COND$DATA-IN
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE SIMPLIFY-SUMS-<))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (1 1 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (1 1 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:REWRITE |(< (- x) (- y))|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::LEN-COMP-GCD-COND$DATA-IN
 (14 1 (:DEFINITION NATP))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (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 REDUCE-INTEGERP-+))
 (3 3 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (3 3 (:REWRITE INTEGERP-MINUS-X))
 (3 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE |(< (- x) 0)|))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 (3 3 (:META META-INTEGERP-CORRECT))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::COMP-GCD-COND$Q2-INPUTS
 (2 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::COMP-GCD-COND$Q3-INPUTS
 (2 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::COMP-GCD-COND$BR-INPUTS)
(ADE::COMP-GCD-COND$IN-ACT)
(ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (7 7 (:REWRITE NTH-WHEN-PREFIXP))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (2 2 (:TYPE-PRESCRIPTION BOOLEANP))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(ADE::COMP-GCD-COND$OUT-ACT0)
(ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA
 (104 1 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (63 3 (:DEFINITION ADE::V-THREEFIX))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (38 38 (:TYPE-PRESCRIPTION STRIP-CARS))
 (34 34 (:TYPE-PRESCRIPTION LEN))
 (30 2 (:DEFINITION NTHCDR))
 (26 14 (:REWRITE DEFAULT-CAR))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (25 11 (:REWRITE DEFAULT-CDR))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (22 2 (:DEFINITION BINARY-APPEND))
 (21 6 (:REWRITE ADE::V-THREEFIX-BVP))
 (18 2 (:DEFINITION LEN))
 (16 8 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (16 2 (:REWRITE CAR-OF-APPEND))
 (14 14 (:TYPE-PRESCRIPTION ADE::BVP))
 (14 1 (:DEFINITION NATP))
 (13 13 (:REWRITE NTH-WHEN-PREFIXP))
 (11 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (10 8 (:REWRITE DEFAULT-+-2))
 (10 6 (:REWRITE SIMPLIFY-SUMS-<))
 (10 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (10 6 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (10 2 (:REWRITE CONSP-OF-APPEND))
 (10 2 (:REWRITE |(+ y x)|))
 (9 6 (:REWRITE DEFAULT-<-1))
 (9 3 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (8 8 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (8 8 (:REWRITE NORMALIZE-ADDENDS))
 (8 8 (:REWRITE DEFAULT-+-1))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (8 4 (:DEFINITION ADE::3V-FIX))
 (8 2 (:DEFINITION STRIP-CARS))
 (7 6 (:REWRITE DEFAULT-<-2))
 (7 1 (:REWRITE TAKE-WHEN-ATOM))
 (6 6 (:REWRITE |(< (- x) (- y))|))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (5 5 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 1 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (3 3 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (3 1 (:REWRITE ADE::BVP-APPEND))
 (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 (:TYPE-PRESCRIPTION NFIX))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::COMP-GCD-COND$OUT-ACT1)
(ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA
 (104 1 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (63 3 (:DEFINITION ADE::V-THREEFIX))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (38 38 (:TYPE-PRESCRIPTION STRIP-CARS))
 (34 34 (:TYPE-PRESCRIPTION LEN))
 (30 2 (:DEFINITION NTHCDR))
 (26 14 (:REWRITE DEFAULT-CAR))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (25 11 (:REWRITE DEFAULT-CDR))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (22 2 (:DEFINITION BINARY-APPEND))
 (21 6 (:REWRITE ADE::V-THREEFIX-BVP))
 (18 2 (:DEFINITION LEN))
 (16 8 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (16 2 (:REWRITE CAR-OF-APPEND))
 (14 14 (:TYPE-PRESCRIPTION ADE::BVP))
 (14 14 (:REWRITE NTH-WHEN-PREFIXP))
 (14 1 (:DEFINITION NATP))
 (11 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (10 8 (:REWRITE DEFAULT-+-2))
 (10 6 (:REWRITE SIMPLIFY-SUMS-<))
 (10 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (10 6 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (10 2 (:REWRITE CONSP-OF-APPEND))
 (10 2 (:REWRITE |(+ y x)|))
 (9 6 (:REWRITE DEFAULT-<-1))
 (9 3 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (8 8 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (8 8 (:REWRITE NORMALIZE-ADDENDS))
 (8 8 (:REWRITE DEFAULT-+-1))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (8 4 (:DEFINITION ADE::3V-FIX))
 (8 2 (:DEFINITION STRIP-CARS))
 (7 6 (:REWRITE DEFAULT-<-2))
 (7 1 (:REWRITE TAKE-WHEN-ATOM))
 (6 6 (:REWRITE |(< (- x) (- y))|))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (5 5 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 1 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (3 3 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (3 1 (:REWRITE ADE::BVP-APPEND))
 (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 (:TYPE-PRESCRIPTION NFIX))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE
 (3720 100 (:REWRITE TAKE-OF-TOO-MANY))
 (1204 732 (:REWRITE DEFAULT-+-2))
 (1064 56 (:REWRITE LEN-OF-APPEND))
 (852 796 (:REWRITE DEFAULT-CDR))
 (850 850 (:REWRITE NTH-WHEN-PREFIXP))
 (760 176 (:REWRITE SIMPLIFY-SUMS-<))
 (732 732 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (732 732 (:REWRITE DEFAULT-+-1))
 (704 88 (:DEFINITION BINARY-APPEND))
 (676 52 (:DEFINITION NTHCDR))
 (632 380 (:REWRITE DEFAULT-CAR))
 (572 52 (:REWRITE |(+ (+ x y) z)|))
 (560 20 (:REWRITE ADE::LEN-NTHCDR))
 (500 100 (:REWRITE TAKE-WHEN-ATOM))
 (464 116 (:DEFINITION STRIP-CARS))
 (368 176 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (352 48 (:REWRITE |(+ y (+ x z))|))
 (332 20 (:DEFINITION ADE::V-THREEFIX))
 (232 232 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (232 232 (:REWRITE |(< (- x) (- y))|))
 (224 224 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (216 176 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (216 176 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (216 176 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (216 176 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (196 76 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (176 176 (:REWRITE |(equal (- x) (- y))|))
 (164 144 (:REWRITE DEFAULT-<-2))
 (164 144 (:REWRITE DEFAULT-<-1))
 (160 32 (:REWRITE |(- (* c x))|))
 (144 144 (:LINEAR LEN-WHEN-PREFIXP))
 (128 128 (:REWRITE DEFAULT-UNARY-MINUS))
 (128 32 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (128 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (120 120 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (120 120 (:REWRITE DEFAULT-*-2))
 (120 120 (:REWRITE DEFAULT-*-1))
 (112 112 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (112 112 (:REWRITE DEFAULT-UNARY-/))
 (96 24 (:REWRITE |(+ x x)|))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (92 92 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (88 88 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (88 88 (:REWRITE |(< 0 (- x))|))
 (88 16 (:REWRITE CONSP-OF-APPEND))
 (84 84 (:TYPE-PRESCRIPTION NFIX))
 (76 76 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (72 72 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (72 36 (:DEFINITION ADE::3V-FIX))
 (64 32 (:REWRITE |(+ (* c x) (* d x))|))
 (64 8 (:REWRITE CAR-OF-APPEND))
 (56 56 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (56 56 (:REWRITE |(equal (- x) 0)|))
 (52 52 (:REWRITE |(< d (+ c x))|))
 (52 4 (:REWRITE ADE::GCD-COND$ACT1-INACTIVE))
 (52 4 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (48 48 (:REWRITE CDR-CONS))
 (44 4 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (36 36 (:TYPE-PRESCRIPTION ADE::3VP))
 (32 32 (:REWRITE |(* 0 x)|))
 (32 32 (:REWRITE |(* (- x) y)|))
 (24 24 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (24 24 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (24 24 (:REWRITE |(* c (* d x))|))
 (24 4 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (16 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (12 12 (:TYPE-PRESCRIPTION ADE::F-NOR3))
 (12 4 (:REWRITE ADE::BVP-APPEND))
 )
(ADE::COMP-GCD-COND$OUT-ACT)
(ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA
 (3 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (2 2 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$VALID-ST))
 (2 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2 2 (:REWRITE NTH-WHEN-PREFIXP))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::COMP-GCD-COND$FLAG)
(ADE::COMP-GCD-COND$DATA0-OUT)
(ADE::LEN-COMP-GCD-COND$DATA0-OUT-1
 (28 4 (:DEFINITION LEN))
 (10 10 (: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))|))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::LEN-COMP-GCD-COND$DATA0-OUT-2
 (28 4 (:DEFINITION LEN))
 (20 16 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (20 16 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (20 16 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (18 18 (:REWRITE NTH-WHEN-PREFIXP))
 (16 16 (:REWRITE |(equal (- x) (- y))|))
 (16 4 (:DEFINITION STRIP-CARS))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-CAR))
 (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-+-1))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::BVP-COMP-GCD-COND$DATA0-OUT
 (2136 44 (:REWRITE TAKE-OF-TOO-MANY))
 (608 72 (:DEFINITION BINARY-APPEND))
 (560 20 (:REWRITE ADE::LEN-NTHCDR))
 (520 40 (:DEFINITION NTHCDR))
 (460 316 (:REWRITE DEFAULT-+-2))
 (440 40 (:REWRITE |(+ (+ x y) z)|))
 (440 24 (:REWRITE LEN-OF-APPEND))
 (400 344 (:REWRITE DEFAULT-CDR))
 (394 82 (:REWRITE SIMPLIFY-SUMS-<))
 (388 208 (:REWRITE DEFAULT-CAR))
 (332 20 (:DEFINITION ADE::V-THREEFIX))
 (316 316 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (316 316 (:REWRITE DEFAULT-+-1))
 (300 144 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (296 296 (:REWRITE NTH-WHEN-PREFIXP))
 (236 44 (:REWRITE TAKE-WHEN-ATOM))
 (176 44 (:DEFINITION STRIP-CARS))
 (176 24 (:REWRITE |(+ y (+ x z))|))
 (128 32 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (128 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (122 82 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (98 98 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (98 98 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (98 98 (:REWRITE |(< (- x) (- y))|))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (92 92 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (92 36 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (86 66 (:REWRITE DEFAULT-<-2))
 (86 66 (:REWRITE DEFAULT-<-1))
 (80 80 (:LINEAR LEN-WHEN-PREFIXP))
 (80 16 (:REWRITE |(- (* c x))|))
 (72 36 (:DEFINITION ADE::3V-FIX))
 (64 8 (:REWRITE CAR-OF-APPEND))
 (60 60 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (60 60 (:REWRITE DEFAULT-*-2))
 (60 60 (:REWRITE DEFAULT-*-1))
 (48 48 (:REWRITE DEFAULT-UNARY-MINUS))
 (44 44 (:TYPE-PRESCRIPTION NFIX))
 (44 40 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (44 40 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (44 40 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (44 4 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (40 40 (:REWRITE |(equal (- x) (- y))|))
 (40 40 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (40 8 (:REWRITE CONSP-OF-APPEND))
 (36 36 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (36 36 (:TYPE-PRESCRIPTION ADE::3VP))
 (36 36 (:REWRITE |(< d (+ c x))|))
 (32 32 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (32 32 (:REWRITE DEFAULT-UNARY-/))
 (32 16 (:REWRITE |(+ (* c x) (* d x))|))
 (32 8 (:REWRITE |(+ x x)|))
 (24 24 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (24 24 (:REWRITE CDR-CONS))
 (24 24 (:REWRITE |(< 0 (- x))|))
 (16 16 (:REWRITE |(* 0 x)|))
 (16 16 (:REWRITE |(* (- x) y)|))
 (16 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (12 4 (:REWRITE ADE::F-GATES=B-GATES))
 (8 8 (:REWRITE |(* c (* d x))|))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::COMP-GCD-COND$DATA1-OUT)
(ADE::LEN-COMP-GCD-COND$DATA1-OUT-1
 (28 4 (:DEFINITION LEN))
 (10 10 (: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))|))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::LEN-COMP-GCD-COND$DATA1-OUT-2
 (32 32 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (32 32 (:REWRITE DEFAULT-*-2))
 (32 32 (:REWRITE DEFAULT-*-1))
 (28 4 (:DEFINITION LEN))
 (20 16 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (20 16 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (20 16 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (18 18 (:REWRITE NTH-WHEN-PREFIXP))
 (16 16 (:REWRITE |(equal (- x) (- y))|))
 (16 4 (:DEFINITION STRIP-CARS))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-CAR))
 (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-+-1))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::BVP-COMP-GCD-COND$DATA1-OUT
 (2136 44 (:REWRITE TAKE-OF-TOO-MANY))
 (2112 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (756 756 (:REWRITE NTH-WHEN-PREFIXP))
 (716 444 (:REWRITE DEFAULT-+-2))
 (608 72 (:DEFINITION BINARY-APPEND))
 (560 504 (:REWRITE DEFAULT-CDR))
 (560 20 (:REWRITE ADE::LEN-NTHCDR))
 (520 40 (:DEFINITION NTHCDR))
 (452 272 (:REWRITE DEFAULT-CAR))
 (444 444 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (444 444 (:REWRITE DEFAULT-+-1))
 (440 40 (:REWRITE |(+ (+ x y) z)|))
 (440 24 (:REWRITE LEN-OF-APPEND))
 (410 98 (:REWRITE SIMPLIFY-SUMS-<))
 (332 20 (:DEFINITION ADE::V-THREEFIX))
 (304 76 (:DEFINITION STRIP-CARS))
 (300 144 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (236 44 (:REWRITE TAKE-WHEN-ATOM))
 (176 24 (:REWRITE |(+ y (+ x z))|))
 (138 98 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (128 32 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (128 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (114 114 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (114 114 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (114 114 (:REWRITE |(< (- x) (- y))|))
 (102 82 (:REWRITE DEFAULT-<-2))
 (102 82 (:REWRITE DEFAULT-<-1))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (92 92 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (92 36 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (80 80 (:LINEAR LEN-WHEN-PREFIXP))
 (80 16 (:REWRITE |(- (* c x))|))
 (72 36 (:DEFINITION ADE::3V-FIX))
 (64 8 (:REWRITE CAR-OF-APPEND))
 (60 60 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (60 60 (:REWRITE DEFAULT-*-2))
 (60 60 (:REWRITE DEFAULT-*-1))
 (52 4 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (48 48 (:REWRITE DEFAULT-UNARY-MINUS))
 (44 44 (:TYPE-PRESCRIPTION NFIX))
 (44 40 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (44 40 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (44 40 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (40 40 (:REWRITE |(equal (- x) (- y))|))
 (40 40 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (40 8 (:REWRITE CONSP-OF-APPEND))
 (36 36 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (36 36 (:TYPE-PRESCRIPTION ADE::3VP))
 (36 36 (:REWRITE |(< d (+ c x))|))
 (36 8 (:REWRITE ADE::F-GATES=B-GATES))
 (32 32 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT0))
 (32 32 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (32 32 (:REWRITE DEFAULT-UNARY-/))
 (32 16 (:REWRITE |(+ (* c x) (* d x))|))
 (32 8 (:REWRITE |(+ x x)|))
 (24 24 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (24 24 (:REWRITE CDR-CONS))
 (24 24 (:REWRITE |(< 0 (- x))|))
 (16 16 (:REWRITE |(* 0 x)|))
 (16 16 (:REWRITE |(* (- x) y)|))
 (16 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (12 12 (:TYPE-PRESCRIPTION ADE::GCD-COND$FLAG))
 (8 8 (:REWRITE |(* c (* d x))|))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::COMP-GCD-COND$DATA-OUTS)
(ADE::COMP-GCD-COND$OUTPUTS)
(ADE::GCD-COND$VALUE-ALT
 (41 41 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (24 1 (:REWRITE ADE::GCD-COND$ACT-INACTIVE))
 (23 1 (:REWRITE ADE::GCD-COND$VALUE))
 (18 4 (:DEFINITION BINARY-APPEND))
 (16 16 (:REWRITE NTH-WHEN-PREFIXP))
 (16 6 (:REWRITE NTH-ADD1))
 (16 1 (:REWRITE ADE::GCD-COND$ACT1-INACTIVE))
 (15 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (14 1 (:REWRITE ADE::GCD-COND$ACT0-INACTIVE))
 (11 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (10 10 (:REWRITE NTH-0-CONS))
 (10 5 (:REWRITE DEFAULT-+-2))
 (9 9 (:REWRITE DEFAULT-CDR))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (5 5 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (5 5 (:REWRITE DEFAULT-+-1))
 (5 5 (:REWRITE |(equal (- x) (- y))|))
 (4 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (4 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 2 (:REWRITE |(* y x)|))
 (3 3 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (3 1 (:REWRITE |(* y (* x z))|))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE |(* a (/ a))|))
 (1 1 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (1 1 (:REWRITE |(* c (* d x))|))
 )
(ADE::COMP-GCD-COND$VALUE
 (370 227 (:REWRITE DEFAULT-+-2))
 (345 115 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (268 268 (:REWRITE NTH-WHEN-PREFIXP))
 (227 227 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (227 227 (:REWRITE DEFAULT-+-1))
 (218 21 (:REWRITE LEN-OF-APPEND))
 (211 159 (:REWRITE ADE::V-THREEFIX-BVP))
 (171 57 (:REWRITE ADE::CAR-V-THREEFIX))
 (147 83 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (147 83 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (147 83 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (144 144 (:DEFINITION STRIP-CARS))
 (140 10 (:REWRITE ADE::GCD-COND$ACT1-INACTIVE))
 (138 138 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (130 41 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (128 112 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (128 112 (:REWRITE ADE::F-BUF-OF-3VP))
 (124 9 (:REWRITE ADE::GCD-COND$ACT0-INACTIVE))
 (114 57 (:DEFINITION ADE::3V-FIX))
 (83 83 (:REWRITE |(equal (- x) (- y))|))
 (78 9 (:REWRITE ADE::QUEUE2$OUT-ACT-INACTIVE))
 (77 8 (:REWRITE ADE::QUEUE3$OUT-ACT-INACTIVE))
 (73 73 (:TYPE-PRESCRIPTION ADE::3VP))
 (72 72 (:TYPE-PRESCRIPTION ADE::BVP))
 (69 69 (:TYPE-PRESCRIPTION PAIRLIS$))
 (61 43 (:REWRITE TAKE-WHEN-ATOM))
 (55 11 (:REWRITE |(+ y x)|))
 (50 30 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (48 48 (:LINEAR LEN-WHEN-PREFIXP))
 (44 4 (:REWRITE |(+ y (+ x z))|))
 (40 30 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (38 1 (:REWRITE ADE::GCD-COND$ACT-INACTIVE))
 (30 2 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (29 8 (:REWRITE ADE::QUEUE2$IN-ACT-INACTIVE))
 (28 7 (:REWRITE ADE::QUEUE3$IN-ACT-INACTIVE))
 (26 1 (:REWRITE TAKE-WHEN-PREFIXP))
 (24 24 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (24 2 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (19 19 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (19 19 (:REWRITE DEFAULT-*-2))
 (19 19 (:REWRITE DEFAULT-*-1))
 (18 6 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (18 3 (:DEFINITION TRUE-LISTP))
 (15 15 (:REWRITE FOLD-CONSTS-IN-+))
 (14 2 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (12 4 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (12 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (8 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (5 5 (:TYPE-PRESCRIPTION PREFIXP))
 (5 5 (:REWRITE SIMPLIFY-SUMS-<))
 (5 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (5 5 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (5 5 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (5 5 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (5 5 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-<-1))
 (5 5 (:REWRITE |(< (- x) (- y))|))
 (5 2 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (5 2 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (5 1 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (4 4 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$VALID-ST))
 (2 2 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (2 2 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (2 2 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (2 2 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::COMP-GCD-COND$STEP
 (12 12 (:TYPE-PRESCRIPTION ADE::QUEUE3$INPUT-FORMAT))
 (12 12 (:TYPE-PRESCRIPTION ADE::QUEUE2$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE3$OUT-ACT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE3$IN-ACT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE2$OUT-ACT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE2$IN-ACT))
 )
(ADE::COMP-GCD-COND$STATE
 (750 250 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (718 617 (:REWRITE ADE::V-THREEFIX-BVP))
 (608 608 (:DEFINITION STRIP-CARS))
 (530 322 (:REWRITE DEFAULT-+-2))
 (456 135 (:REWRITE ADE::CAR-V-THREEFIX))
 (449 413 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (449 413 (:REWRITE ADE::F-BUF-OF-3VP))
 (328 30 (:REWRITE LEN-OF-APPEND))
 (322 322 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (322 322 (:REWRITE DEFAULT-+-1))
 (284 284 (:REWRITE NTH-WHEN-PREFIXP))
 (275 216 (:REWRITE TAKE-WHEN-ATOM))
 (274 54 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (271 159 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (271 159 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (271 159 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (270 135 (:DEFINITION ADE::3V-FIX))
 (239 239 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (184 54 (:REWRITE ADE::GCD-COND$ACT1-INACTIVE))
 (171 171 (:TYPE-PRESCRIPTION ADE::3VP))
 (168 53 (:REWRITE ADE::GCD-COND$ACT0-INACTIVE))
 (159 159 (:REWRITE |(equal (- x) (- y))|))
 (157 42 (:REWRITE ADE::QUEUE2$OUT-ACT-INACTIVE))
 (154 39 (:REWRITE ADE::QUEUE3$OUT-ACT-INACTIVE))
 (130 130 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
 (119 39 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (102 102 (:TYPE-PRESCRIPTION PAIRLIS$))
 (100 100 (:TYPE-PRESCRIPTION ADE::FV-IF))
 (100 60 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (96 96 (:TYPE-PRESCRIPTION ADE::BVP))
 (93 9 (:REWRITE |(+ y (+ x z))|))
 (80 60 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (76 34 (:REWRITE ADE::QUEUE2$IN-ACT-INACTIVE))
 (67 32 (:REWRITE ADE::QUEUE3$IN-ACT-INACTIVE))
 (53 3 (:REWRITE TAKE-MORE-OF-TAKE-FEWER))
 (51 17 (:REWRITE CAR-OF-TAKE))
 (48 48 (:LINEAR LEN-WHEN-PREFIXP))
 (47 13 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (43 1 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (38 1 (:REWRITE ADE::GCD-COND$ACT-INACTIVE))
 (24 24 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (23 11 (:REWRITE SIMPLIFY-SUMS-<))
 (21 21 (:TYPE-PRESCRIPTION NFIX))
 (21 21 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (21 21 (:REWRITE DEFAULT-*-2))
 (21 21 (:REWRITE DEFAULT-*-1))
 (16 8 (:TYPE-PRESCRIPTION ADE::BVP-TAKE))
 (15 15 (:REWRITE DEFAULT-UNARY-MINUS))
 (15 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (13 13 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (13 13 (:REWRITE |(< (- x) (- y))|))
 (12 6 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (12 4 (:REWRITE ADE::BVP-TAKE))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (12 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (11 11 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (11 11 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (10 10 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE DEFAULT-<-1))
 (9 3 (:REWRITE ADE::BVP-NTHCDR))
 (9 3 (:REWRITE ADE::BOOLEANP-QUEUE3$OUT-ACT))
 (9 3 (:REWRITE ADE::BOOLEANP-QUEUE2$OUT-ACT))
 (8 4 (:REWRITE |(* y x)|))
 (8 2 (:DEFINITION TRUE-LISTP))
 (5 5 (:REWRITE ADE::LEN-QUEUE3$DATA-OUT-2))
 (5 5 (:REWRITE ADE::LEN-QUEUE2$DATA-OUT-2))
 (5 1 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (4 4 (:REWRITE DEFAULT-UNARY-/))
 (4 4 (:REWRITE |(* a (/ a))|))
 (3 3 (:TYPE-PRESCRIPTION ADE::GCD-COND$DATA0-OUT))
 (3 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (2 2 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$VALID-ST))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (2 2 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (2 2 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (2 2 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (2 2 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (2 2 (:REWRITE CONSP-OF-TAKE))
 (2 2 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE CONSP-OF-APPEND))
 (1 1 (:REWRITE |(< d (+ c x))|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::COMP-GCD-COND$INPUT-FORMAT)
(ADE::COMP-GCD-COND$INPUT-FORMAT=>Q2$INPUT-FORMAT
 (2680 80 (:REWRITE TAKE-OF-TOO-MANY))
 (864 16 (:DEFINITION TAKE))
 (608 34 (:REWRITE ADE::LEN-NTHCDR))
 (480 64 (:REWRITE TAKE-WHEN-ATOM))
 (455 285 (:REWRITE DEFAULT-+-2))
 (366 120 (:REWRITE SIMPLIFY-SUMS-<))
 (363 267 (:REWRITE DEFAULT-CDR))
 (300 34 (:DEFINITION BINARY-APPEND))
 (293 65 (:REWRITE |(+ y x)|))
 (285 285 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (285 285 (:REWRITE DEFAULT-+-1))
 (248 16 (:REWRITE LEN-OF-APPEND))
 (242 98 (:REWRITE DEFAULT-CAR))
 (223 17 (:DEFINITION NTHCDR))
 (190 120 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (187 17 (:REWRITE |(+ (+ x y) z)|))
 (167 167 (:REWRITE NTH-WHEN-PREFIXP))
 (152 104 (:REWRITE DEFAULT-<-2))
 (140 140 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (140 140 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (140 140 (:LINEAR LEN-WHEN-PREFIXP))
 (136 136 (:REWRITE |(< (- x) (- y))|))
 (126 104 (:REWRITE DEFAULT-<-1))
 (122 68 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (112 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (96 16 (:REWRITE CONSP-OF-APPEND))
 (80 80 (:TYPE-PRESCRIPTION NFIX))
 (80 20 (:DEFINITION STRIP-CARS))
 (80 16 (:REWRITE |(+ y (+ x z))|))
 (80 8 (:DEFINITION ADE::V-THREEFIX))
 (70 70 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (64 64 (:REWRITE DEFAULT-UNARY-MINUS))
 (48 48 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (48 48 (:REWRITE |(< 0 (- x))|))
 (48 24 (:DEFINITION ADE::3V-FIX))
 (42 36 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (42 36 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (42 36 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (36 36 (:REWRITE |(equal (- x) (- y))|))
 (34 34 (:REWRITE |(< d (+ c x))|))
 (32 32 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (32 32 (:REWRITE DEFAULT-UNARY-/))
 (26 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (24 24 (:TYPE-PRESCRIPTION ADE::3VP))
 (18 2 (:DEFINITION TRUE-LISTP))
 (17 17 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (17 17 (:REWRITE DEFAULT-*-2))
 (17 17 (:REWRITE DEFAULT-*-1))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (16 16 (:REWRITE CONSP-OF-TAKE))
 (16 16 (:REWRITE |(equal (- x) 0)|))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (8 4 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (6 2 (:REWRITE ADE::BVP-NTHCDR))
 (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 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::COMP-GCD-COND$INPUT-FORMAT=>Q3$INPUT-FORMAT
 (2680 80 (:REWRITE TAKE-OF-TOO-MANY))
 (864 16 (:DEFINITION TAKE))
 (608 34 (:REWRITE ADE::LEN-NTHCDR))
 (480 64 (:REWRITE TAKE-WHEN-ATOM))
 (455 285 (:REWRITE DEFAULT-+-2))
 (366 120 (:REWRITE SIMPLIFY-SUMS-<))
 (363 267 (:REWRITE DEFAULT-CDR))
 (300 34 (:DEFINITION BINARY-APPEND))
 (293 65 (:REWRITE |(+ y x)|))
 (285 285 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (285 285 (:REWRITE DEFAULT-+-1))
 (248 16 (:REWRITE LEN-OF-APPEND))
 (242 98 (:REWRITE DEFAULT-CAR))
 (223 17 (:DEFINITION NTHCDR))
 (190 120 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (187 17 (:REWRITE |(+ (+ x y) z)|))
 (167 167 (:REWRITE NTH-WHEN-PREFIXP))
 (152 104 (:REWRITE DEFAULT-<-2))
 (140 140 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (140 140 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (140 140 (:LINEAR LEN-WHEN-PREFIXP))
 (136 136 (:REWRITE |(< (- x) (- y))|))
 (126 104 (:REWRITE DEFAULT-<-1))
 (122 68 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (112 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (96 16 (:REWRITE CONSP-OF-APPEND))
 (80 80 (:TYPE-PRESCRIPTION NFIX))
 (80 20 (:DEFINITION STRIP-CARS))
 (80 16 (:REWRITE |(+ y (+ x z))|))
 (80 8 (:DEFINITION ADE::V-THREEFIX))
 (70 70 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (64 64 (:REWRITE DEFAULT-UNARY-MINUS))
 (48 48 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (48 48 (:REWRITE |(< 0 (- x))|))
 (48 24 (:DEFINITION ADE::3V-FIX))
 (42 36 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (42 36 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (42 36 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (36 36 (:REWRITE |(equal (- x) (- y))|))
 (34 34 (:REWRITE |(< d (+ c x))|))
 (32 32 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (32 32 (:REWRITE DEFAULT-UNARY-/))
 (26 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (24 24 (:TYPE-PRESCRIPTION ADE::3VP))
 (18 2 (:DEFINITION TRUE-LISTP))
 (17 17 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (17 17 (:REWRITE DEFAULT-*-2))
 (17 17 (:REWRITE DEFAULT-*-1))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (16 16 (:REWRITE CONSP-OF-TAKE))
 (16 16 (:REWRITE |(equal (- x) 0)|))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (8 4 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (6 2 (:REWRITE ADE::BVP-NTHCDR))
 (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 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::BOOLEANP-COMP-GCD-COND$IN-ACT
 (223 17 (:DEFINITION NTHCDR))
 (187 17 (:REWRITE |(+ (+ x y) z)|))
 (151 151 (:REWRITE NTH-WHEN-PREFIXP))
 (144 2 (:REWRITE ADE::LEN-NTHCDR))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (85 17 (:REWRITE |(+ y x)|))
 (85 17 (:REWRITE |(+ c (+ d x))|))
 (71 61 (:REWRITE DEFAULT-+-2))
 (70 10 (:DEFINITION LEN))
 (61 61 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (61 61 (:REWRITE NORMALIZE-ADDENDS))
 (61 61 (:REWRITE DEFAULT-+-1))
 (35 35 (:REWRITE DEFAULT-CDR))
 (32 16 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (26 20 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (26 20 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (26 20 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (26 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (20 20 (:REWRITE |(equal (- x) (- y))|))
 (18 2 (:DEFINITION TRUE-LISTP))
 (17 17 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (17 17 (:REWRITE DEFAULT-*-2))
 (17 17 (:REWRITE DEFAULT-*-1))
 (16 4 (:DEFINITION STRIP-CARS))
 (14 8 (:REWRITE SIMPLIFY-SUMS-<))
 (14 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (14 8 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (14 8 (:REWRITE DEFAULT-<-1))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (12 12 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (12 12 (:LINEAR LEN-WHEN-PREFIXP))
 (12 2 (:DEFINITION BINARY-APPEND))
 (10 10 (:REWRITE DEFAULT-CAR))
 (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (8 8 (:REWRITE DEFAULT-<-2))
 (8 8 (:REWRITE |(< (- x) (- y))|))
 (8 4 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (6 6 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (6 2 (:REWRITE ADE::BVP-NTHCDR))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE |(< d (+ c x))|))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0
 (2220 56 (:REWRITE TAKE-OF-TOO-MANY))
 (995 621 (:REWRITE DEFAULT-+-2))
 (847 65 (:DEFINITION NTHCDR))
 (819 819 (:REWRITE NTH-WHEN-PREFIXP))
 (792 26 (:REWRITE ADE::LEN-NTHCDR))
 (715 65 (:REWRITE |(+ (+ x y) z)|))
 (711 655 (:REWRITE DEFAULT-CDR))
 (621 621 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (621 621 (:REWRITE DEFAULT-+-1))
 (580 70 (:DEFINITION BINARY-APPEND))
 (532 28 (:REWRITE LEN-OF-APPEND))
 (486 306 (:REWRITE DEFAULT-CAR))
 (434 116 (:REWRITE SIMPLIFY-SUMS-<))
 (368 92 (:DEFINITION STRIP-CARS))
 (332 20 (:DEFINITION ADE::V-THREEFIX))
 (302 140 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (292 56 (:REWRITE TAKE-WHEN-ATOM))
 (198 152 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (198 152 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (198 152 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (176 24 (:REWRITE |(+ y (+ x z))|))
 (162 116 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (152 152 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (152 152 (:REWRITE |(equal (- x) (- y))|))
 (144 144 (:REWRITE |(< (- x) (- y))|))
 (130 100 (:REWRITE DEFAULT-<-1))
 (130 20 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (128 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (116 100 (:REWRITE DEFAULT-<-2))
 (108 108 (:LINEAR LEN-WHEN-PREFIXP))
 (96 24 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (93 93 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (93 93 (:REWRITE DEFAULT-*-2))
 (93 93 (:REWRITE DEFAULT-*-1))
 (92 92 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (90 10 (:DEFINITION TRUE-LISTP))
 (80 16 (:REWRITE |(- (* c x))|))
 (72 36 (:DEFINITION ADE::3V-FIX))
 (64 64 (:REWRITE DEFAULT-UNARY-MINUS))
 (64 12 (:REWRITE CONSP-OF-APPEND))
 (64 8 (:REWRITE CAR-OF-APPEND))
 (56 56 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (56 56 (:REWRITE DEFAULT-UNARY-/))
 (54 54 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (48 48 (:TYPE-PRESCRIPTION NFIX))
 (48 12 (:REWRITE |(+ x x)|))
 (44 44 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (44 44 (:REWRITE |(< 0 (- x))|))
 (44 4 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (42 42 (:REWRITE |(< d (+ c x))|))
 (40 20 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (36 36 (:TYPE-PRESCRIPTION ADE::3VP))
 (32 16 (:REWRITE |(+ (* c x) (* d x))|))
 (30 10 (:REWRITE ADE::BVP-NTHCDR))
 (28 28 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (28 28 (:REWRITE |(equal (- x) 0)|))
 (24 24 (:REWRITE CDR-CONS))
 (16 16 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (16 16 (:REWRITE |(* 0 x)|))
 (16 16 (:REWRITE |(* (- x) y)|))
 (16 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (12 12 (:REWRITE |(* c (* d x))|))
 (12 4 (:REWRITE ADE::BVP-APPEND))
 (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 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT1
 (2220 56 (:REWRITE TAKE-OF-TOO-MANY))
 (1280 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (1123 685 (:REWRITE DEFAULT-+-2))
 (1119 1119 (:REWRITE NTH-WHEN-PREFIXP))
 (847 65 (:DEFINITION NTHCDR))
 (807 751 (:REWRITE DEFAULT-CDR))
 (792 26 (:REWRITE ADE::LEN-NTHCDR))
 (715 65 (:REWRITE |(+ (+ x y) z)|))
 (685 685 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (685 685 (:REWRITE DEFAULT-+-1))
 (580 70 (:DEFINITION BINARY-APPEND))
 (550 370 (:REWRITE DEFAULT-CAR))
 (532 28 (:REWRITE LEN-OF-APPEND))
 (496 124 (:DEFINITION STRIP-CARS))
 (434 116 (:REWRITE SIMPLIFY-SUMS-<))
 (332 20 (:DEFINITION ADE::V-THREEFIX))
 (302 140 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (292 56 (:REWRITE TAKE-WHEN-ATOM))
 (198 152 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (198 152 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (198 152 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (176 24 (:REWRITE |(+ y (+ x z))|))
 (162 116 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (152 152 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (152 152 (:REWRITE |(equal (- x) (- y))|))
 (144 144 (:REWRITE |(< (- x) (- y))|))
 (130 100 (:REWRITE DEFAULT-<-1))
 (130 20 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (128 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (116 100 (:REWRITE DEFAULT-<-2))
 (108 108 (:LINEAR LEN-WHEN-PREFIXP))
 (96 24 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (93 93 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (93 93 (:REWRITE DEFAULT-*-2))
 (93 93 (:REWRITE DEFAULT-*-1))
 (92 92 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (90 10 (:DEFINITION TRUE-LISTP))
 (80 16 (:REWRITE |(- (* c x))|))
 (72 36 (:DEFINITION ADE::3V-FIX))
 (64 64 (:REWRITE DEFAULT-UNARY-MINUS))
 (64 32 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (64 12 (:REWRITE CONSP-OF-APPEND))
 (64 8 (:REWRITE CAR-OF-APPEND))
 (56 56 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (56 56 (:REWRITE DEFAULT-UNARY-/))
 (54 54 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (52 4 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (48 48 (:TYPE-PRESCRIPTION NFIX))
 (48 12 (:REWRITE |(+ x x)|))
 (44 44 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (44 44 (:REWRITE |(< 0 (- x))|))
 (42 42 (:REWRITE |(< d (+ c x))|))
 (40 20 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (36 36 (:TYPE-PRESCRIPTION ADE::3VP))
 (32 32 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT0))
 (32 16 (:REWRITE |(+ (* c x) (* d x))|))
 (30 10 (:REWRITE ADE::BVP-NTHCDR))
 (28 28 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (28 28 (:REWRITE |(equal (- x) 0)|))
 (24 24 (:REWRITE CDR-CONS))
 (16 16 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (16 16 (:REWRITE |(* 0 x)|))
 (16 16 (:REWRITE |(* (- x) y)|))
 (16 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (:TYPE-PRESCRIPTION ADE::F-NOR3))
 (12 12 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (12 12 (:REWRITE |(* c (* d x))|))
 (12 4 (:REWRITE ADE::BVP-APPEND))
 (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 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT
 (6 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (6 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (6 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (3 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (3 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (3 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3 3 (:REWRITE NTH-WHEN-PREFIXP))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (3 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 )
(ADE::COMP-GCD-COND$ST-FORMAT-PRESERVED
 (140 2 (:DEFINITION TAKE))
 (130 8 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (86 86 (:REWRITE NTH-WHEN-PREFIXP))
 (63 9 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (53 11 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (46 6 (:DEFINITION LEN))
 (38 23 (:REWRITE DEFAULT-CDR))
 (32 26 (:REWRITE DEFAULT-CAR))
 (32 8 (:DEFINITION STRIP-CARS))
 (30 3 (:DEFINITION NTHCDR))
 (23 23 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT))
 (21 13 (:REWRITE DEFAULT-+-2))
 (20 4 (:DEFINITION PAIRLIS$))
 (18 9 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$IN-ACT))
 (18 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE3$OUT-ACT))
 (18 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE2$OUT-ACT))
 (16 4 (:REWRITE TAKE-WHEN-ATOM))
 (14 14 (:TYPE-PRESCRIPTION BOOLEANP))
 (13 13 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (13 13 (:REWRITE DEFAULT-+-1))
 (13 9 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (13 9 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (13 9 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (12 2 (:REWRITE ADE::QUEUE3$OUT-ACT-INACTIVE))
 (12 2 (:REWRITE ADE::QUEUE2$OUT-ACT-INACTIVE))
 (12 2 (:REWRITE ADE::BOOLEANP-QUEUE3$OUT-ACT))
 (12 2 (:REWRITE ADE::BOOLEANP-QUEUE2$OUT-ACT))
 (11 11 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (11 11 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (11 11 (:REWRITE |(< (- x) (- y))|))
 (10 10 (:TYPE-PRESCRIPTION ADE::QUEUE3$INPUT-FORMAT))
 (10 10 (:TYPE-PRESCRIPTION ADE::QUEUE2$INPUT-FORMAT))
 (9 9 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$IN-ACT))
 (9 9 (:REWRITE |(equal (- x) (- y))|))
 (9 7 (:REWRITE SIMPLIFY-SUMS-<))
 (9 7 (:REWRITE DEFAULT-<-2))
 (9 3 (:REWRITE ADE::BOOLEANP-COMP-GCD-COND$IN-ACT))
 (8 8 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (8 8 (:REWRITE DEFAULT-*-2))
 (8 8 (:REWRITE DEFAULT-*-1))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (8 4 (:REWRITE |(* y x)|))
 (7 7 (:REWRITE DEFAULT-UNARY-MINUS))
 (7 7 (:REWRITE DEFAULT-<-1))
 (6 6 (:TYPE-PRESCRIPTION ADE::QUEUE3$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::QUEUE2$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$Q3-INPUTS))
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$Q2-INPUTS))
 (6 2 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT=>Q3$INPUT-FORMAT))
 (6 2 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT=>Q2$INPUT-FORMAT))
 (6 2 (:REWRITE |(* y (* x z))|))
 (6 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (5 3 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (4 4 (:REWRITE DEFAULT-UNARY-/))
 (4 4 (:REWRITE |(* a (/ a))|))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 2 (:REWRITE |(< d (+ c x))|))
 (4 2 (:REWRITE |(+ c (+ d x))|))
 (3 3 (:REWRITE ADE::LEN-QUEUE3$DATA-OUT-2))
 (3 3 (:REWRITE ADE::LEN-QUEUE2$DATA-OUT-2))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (2 2 (:REWRITE |(< 0 (- x))|))
 (2 2 (:REWRITE |(< (+ c x) d)|))
 (2 2 (:REWRITE |(* c (* d x))|))
 (2 1 (:REWRITE ADE::QUEUE3$IN-ACT-INACTIVE))
 (2 1 (:REWRITE ADE::QUEUE2$IN-ACT-INACTIVE))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::COMP-GCD-COND$VALUE-ALT
 (572 44 (:DEFINITION NTHCDR))
 (484 44 (:REWRITE |(+ (+ x y) z)|))
 (302 44 (:DEFINITION BINARY-APPEND))
 (252 9 (:REWRITE ADE::LEN-NTHCDR))
 (220 44 (:REWRITE |(+ y x)|))
 (180 162 (:REWRITE DEFAULT-+-2))
 (175 88 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (174 174 (:REWRITE NTH-WHEN-PREFIXP))
 (162 162 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (162 162 (:REWRITE DEFAULT-+-1))
 (126 18 (:DEFINITION LEN))
 (117 18 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (115 115 (:REWRITE DEFAULT-CDR))
 (81 9 (:DEFINITION TRUE-LISTP))
 (76 12 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (60 60 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (60 60 (:REWRITE DEFAULT-*-2))
 (60 60 (:REWRITE DEFAULT-*-1))
 (53 11 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (45 11 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (45 11 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (44 44 (:REWRITE DEFAULT-CAR))
 (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))
 (33 11 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (32 32 (:LINEAR LEN-WHEN-PREFIXP))
 (27 9 (:REWRITE ADE::BVP-NTHCDR))
 (23 23 (:REWRITE |(equal (- x) (- y))|))
 (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 |(< d (+ c x))|))
 (9 9 (:REWRITE |(< (- x) (- y))|))
 (4 4 (:REWRITE |(* (- x) y)|))
 )
(ADE::COMP-GCD-COND$STATE-ALT
 (429 33 (:DEFINITION NTHCDR))
 (363 33 (:REWRITE |(+ (+ x y) z)|))
 (252 9 (:REWRITE ADE::LEN-NTHCDR))
 (170 22 (:DEFINITION BINARY-APPEND))
 (165 33 (:REWRITE |(+ y x)|))
 (147 129 (:REWRITE DEFAULT-+-2))
 (129 129 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (129 129 (:REWRITE DEFAULT-+-1))
 (126 18 (:DEFINITION LEN))
 (117 18 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (98 44 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (82 82 (:REWRITE DEFAULT-CDR))
 (81 9 (:DEFINITION TRUE-LISTP))
 (76 12 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (67 67 (:REWRITE NTH-WHEN-PREFIXP))
 (49 49 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (49 49 (:REWRITE DEFAULT-*-2))
 (49 49 (:REWRITE DEFAULT-*-1))
 (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))
 (32 32 (:LINEAR LEN-WHEN-PREFIXP))
 (27 9 (:REWRITE ADE::BVP-NTHCDR))
 (23 23 (:REWRITE |(equal (- x) (- y))|))
 (22 22 (:REWRITE DEFAULT-CAR))
 (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 |(< d (+ c x))|))
 (9 9 (:REWRITE |(< (- x) (- y))|))
 (4 4 (:REWRITE |(* (- x) y)|))
 )
(ADE::COMP-GCD-COND$RUN)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-COMP-GCD-COND$RUN-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-COMP-GCD-COND$RUN)
(ADE::COMP-GCD-COND$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::COMP-GCD-COND$INPUT-FORMAT-N
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (4 4 (:REWRITE SIMPLIFY-SUMS-<))
 (4 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (4 4 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (4 4 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (4 4 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE |(< (- x) 0)|))
 (4 4 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 2 (:META META-INTEGERP-CORRECT))
 )
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-COMP-GCD-COND$INPUT-FORMAT-N-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-COMP-GCD-COND$INPUT-FORMAT-N)
(ADE::COMP-GCD-COND$INPUT-FORMAT-PLUS
 (87 39 (:REWRITE |(< d (+ c x))|))
 (56 56 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (47 47 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (47 47 (:REWRITE |(< (- x) (- y))|))
 (35 35 (:REWRITE SIMPLIFY-SUMS-<))
 (35 35 (:REWRITE DEFAULT-<-2))
 (35 35 (:REWRITE DEFAULT-<-1))
 (27 15 (:REWRITE DEFAULT-CDR))
 (27 15 (:REWRITE DEFAULT-CAR))
 (24 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (22 22 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (22 22 (:REWRITE NORMALIZE-ADDENDS))
 (22 22 (:REWRITE DEFAULT-+-2))
 (22 22 (:REWRITE DEFAULT-+-1))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (12 12 (:REWRITE |(< d (+ c x y))|))
 (12 12 (:REWRITE |(< 0 (- x))|))
 (6 6 (:REWRITE FOLD-CONSTS-IN-+))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (4 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:REWRITE |(< (- x) 0)|))
 (4 4 (:META META-INTEGERP-CORRECT))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::COMP-GCD-COND$DE-N
 (265 30 (:REWRITE ZP-OPEN))
 (108 12 (:REWRITE |(< d (+ c x))|))
 (62 2 (:DEFINITION ADE::COMP-GCD-COND$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::COMP-GCD-COND$INPUT-FORMAT-PLUS))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE ADE::DE-PLUS))
 )
(ADE::COMP-GCD-COND$OP
 (10 5 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (5 5 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (5 5 (:TYPE-PRESCRIPTION BINARY-APPEND))
 )
(ADE::COMP-GCD-COND$OP-MAP)
(ADE::LEN-OF-COMP-GCD-COND$OP-MAP
 (28 28 (:LINEAR LEN-WHEN-PREFIXP))
 (14 14 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (14 7 (:REWRITE DEFAULT-+-2))
 (9 8 (:REWRITE DEFAULT-CDR))
 (9 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (9 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (9 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-+-1))
 (3 3 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::COMP-GCD-COND$OP-MAP-OF-APPEND
 (50 19 (:REWRITE DEFAULT-CDR))
 (29 26 (:REWRITE DEFAULT-CAR))
 (15 15 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (12 4 (:REWRITE CAR-OF-APPEND))
 (8 8 (:REWRITE CONSP-OF-APPEND))
 (6 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::COMP-GCD-COND$EXTRACT)
(ADE::COMP-GCD-COND$EXTRACT-NOT-EMPTY-1
 (442 442 (:LINEAR LEN-WHEN-PREFIXP))
 (424 16 (:DEFINITION ADE::V-THREEFIX))
 (416 4 (:REWRITE TAKE-OF-TOO-MANY))
 (379 379 (:REWRITE NTH-WHEN-PREFIXP))
 (356 208 (:REWRITE DEFAULT-CDR))
 (288 288 (:TYPE-PRESCRIPTION STRIP-CARS))
 (288 4 (:REWRITE ADE::LEN-NTHCDR))
 (271 175 (:REWRITE DEFAULT-CAR))
 (242 26 (:DEFINITION BINARY-APPEND))
 (240 8 (:REWRITE |(< x (if a b c))|))
 (225 136 (:REWRITE DEFAULT-+-2))
 (221 221 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (184 46 (:DEFINITION STRIP-CARS))
 (172 12 (:DEFINITION NTHCDR))
 (142 20 (:REWRITE CAR-OF-APPEND))
 (139 136 (:REWRITE DEFAULT-+-1))
 (136 136 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (132 12 (:REWRITE |(+ (+ x y) z)|))
 (121 88 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (121 88 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (121 88 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (121 52 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (120 32 (:REWRITE ADE::V-THREEFIX-BVP))
 (111 24 (:REWRITE CONSP-OF-APPEND))
 (106 41 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (104 16 (:REWRITE |(+ (if a b c) x)|))
 (92 4 (:REWRITE ADE::GCD-COND$ACT0-INACTIVE))
 (88 88 (:REWRITE |(equal (- x) (- y))|))
 (88 44 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (88 8 (:REWRITE ADE::CAR-V-THREEFIX))
 (68 1 (:DEFINITION PAIRLIS$))
 (59 59 (:TYPE-PRESCRIPTION ADE::QUEUE2$EXTRACT))
 (56 4 (:DEFINITION NATP))
 (48 24 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (48 24 (:DEFINITION ADE::3V-FIX))
 (45 1 (:REWRITE ADE::PAIRLIS$-APPEND))
 (44 44 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (41 41 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (40 40 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (40 24 (:REWRITE SIMPLIFY-SUMS-<))
 (40 24 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (40 24 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (36 36 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (36 24 (:REWRITE DEFAULT-<-1))
 (34 10 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (32 32 (:TYPE-PRESCRIPTION ADE::3VP))
 (32 32 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (32 32 (:REWRITE DEFAULT-*-2))
 (32 32 (:REWRITE DEFAULT-*-1))
 (32 32 (:LINEAR ADE::QUEUE2$EXTRACT-NOT-EMPTY))
 (30 10 (:REWRITE ADE::F-GATES=B-GATES))
 (28 28 (:TYPE-PRESCRIPTION BOOLEANP))
 (28 24 (:REWRITE DEFAULT-<-2))
 (28 4 (:REWRITE TAKE-WHEN-ATOM))
 (24 24 (:REWRITE |(< (- x) (- y))|))
 (24 8 (:REWRITE ADE::BVP-APPEND))
 (24 4 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (24 4 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (20 20 (:TYPE-PRESCRIPTION ADE::GCD-COND$DATA-IN))
 (13 13 (:TYPE-PRESCRIPTION ADE::QUEUE3$EXTRACT))
 (13 13 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (13 13 (:REWRITE |(equal (- x) 0)|))
 (12 4 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (12 4 (:REWRITE ADE::F-BUF-OF-3VP))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (8 8 (:REWRITE REDUCE-INTEGERP-+))
 (8 8 (:REWRITE INTEGERP-MINUS-X))
 (8 8 (:REWRITE |(< (- x) 0)|))
 (8 8 (:META META-INTEGERP-CORRECT))
 (6 6 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (6 6 (:TYPE-PRESCRIPTION ADE::F-AND))
 (5 1 (:DEFINITION ADE::COMP-GCD-COND$OP-MAP))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE |(< d (+ c x))|))
 (4 4 (:REWRITE |(* (- x) y)|))
 (4 4 (:DEFINITION ADE::BRANCH$ACT0))
 (2 2 (:TYPE-PRESCRIPTION PAIRLIS$))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE |(equal (+ c x) d)|))
 (1 1 (:REWRITE |(equal (+ c x y) d)|))
 )
(ADE::COMP-GCD-COND$EXTRACT-NOT-EMPTY-2
 (442 442 (:LINEAR LEN-WHEN-PREFIXP))
 (424 16 (:DEFINITION ADE::V-THREEFIX))
 (416 4 (:REWRITE TAKE-OF-TOO-MANY))
 (383 383 (:REWRITE NTH-WHEN-PREFIXP))
 (356 208 (:REWRITE DEFAULT-CDR))
 (288 288 (:TYPE-PRESCRIPTION STRIP-CARS))
 (288 4 (:REWRITE ADE::LEN-NTHCDR))
 (271 175 (:REWRITE DEFAULT-CAR))
 (242 26 (:DEFINITION BINARY-APPEND))
 (240 8 (:REWRITE |(< x (if a b c))|))
 (225 136 (:REWRITE DEFAULT-+-2))
 (221 221 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (184 46 (:DEFINITION STRIP-CARS))
 (172 12 (:DEFINITION NTHCDR))
 (142 20 (:REWRITE CAR-OF-APPEND))
 (139 136 (:REWRITE DEFAULT-+-1))
 (136 136 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (132 12 (:REWRITE |(+ (+ x y) z)|))
 (121 88 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (121 88 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (121 88 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (121 52 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (120 32 (:REWRITE ADE::V-THREEFIX-BVP))
 (111 24 (:REWRITE CONSP-OF-APPEND))
 (106 41 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (104 16 (:REWRITE |(+ (if a b c) x)|))
 (100 4 (:REWRITE ADE::GCD-COND$ACT1-INACTIVE))
 (88 88 (:REWRITE |(equal (- x) (- y))|))
 (88 44 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (88 8 (:REWRITE ADE::CAR-V-THREEFIX))
 (68 1 (:DEFINITION PAIRLIS$))
 (59 59 (:TYPE-PRESCRIPTION ADE::QUEUE2$EXTRACT))
 (56 4 (:DEFINITION NATP))
 (48 24 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT1))
 (48 24 (:DEFINITION ADE::3V-FIX))
 (45 1 (:REWRITE ADE::PAIRLIS$-APPEND))
 (44 44 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (41 41 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (40 40 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (40 24 (:REWRITE SIMPLIFY-SUMS-<))
 (40 24 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (40 24 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (36 36 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (36 24 (:REWRITE DEFAULT-<-1))
 (34 10 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (32 32 (:TYPE-PRESCRIPTION ADE::3VP))
 (32 32 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (32 32 (:REWRITE DEFAULT-*-2))
 (32 32 (:REWRITE DEFAULT-*-1))
 (32 32 (:LINEAR ADE::QUEUE2$EXTRACT-NOT-EMPTY))
 (30 10 (:REWRITE ADE::F-GATES=B-GATES))
 (28 28 (:TYPE-PRESCRIPTION BOOLEANP))
 (28 24 (:REWRITE DEFAULT-<-2))
 (28 4 (:REWRITE TAKE-WHEN-ATOM))
 (28 4 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (24 24 (:REWRITE |(< (- x) (- y))|))
 (24 8 (:REWRITE ADE::BVP-APPEND))
 (24 4 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (24 4 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (20 20 (:TYPE-PRESCRIPTION ADE::GCD-COND$DATA-IN))
 (16 8 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (13 13 (:TYPE-PRESCRIPTION ADE::QUEUE3$EXTRACT))
 (13 13 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (13 13 (:REWRITE |(equal (- x) 0)|))
 (12 4 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (12 4 (:REWRITE ADE::F-BUF-OF-3VP))
 (8 8 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT0))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (8 8 (:REWRITE REDUCE-INTEGERP-+))
 (8 8 (:REWRITE INTEGERP-MINUS-X))
 (8 8 (:REWRITE |(< (- x) 0)|))
 (8 8 (:META META-INTEGERP-CORRECT))
 (6 6 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (6 6 (:TYPE-PRESCRIPTION ADE::F-AND))
 (5 1 (:DEFINITION ADE::COMP-GCD-COND$OP-MAP))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE |(< d (+ c x))|))
 (4 4 (:REWRITE |(* (- x) y)|))
 (4 4 (:DEFINITION ADE::BRANCH$ACT1))
 (2 2 (:TYPE-PRESCRIPTION PAIRLIS$))
 (2 2 (:LINEAR ADE::COMP-GCD-COND$EXTRACT-NOT-EMPTY-1))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE |(equal (+ c x) d)|))
 (1 1 (:REWRITE |(equal (+ c x y) d)|))
 )
(ADE::COMP-GCD-COND$INV)
(ADE::COMP-GCD-COND$Q2-IN-ACT-INACTIVE
 (136 2 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (54 1 (:DEFINITION TAKE))
 (43 43 (:TYPE-PRESCRIPTION LEN))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (29 3 (:DEFINITION LEN))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 6 (:REWRITE DEFAULT-CAR))
 (15 1 (:DEFINITION NTHCDR))
 (14 8 (:REWRITE DEFAULT-CDR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 1 (:DEFINITION BINARY-APPEND))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (10 7 (:REWRITE DEFAULT-+-2))
 (10 1 (:DEFINITION ADE::V-THREEFIX))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 9 (:REWRITE NTH-WHEN-PREFIXP))
 (9 7 (:REWRITE DEFAULT-<-2))
 (7 7 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE NORMALIZE-ADDENDS))
 (7 7 (:REWRITE DEFAULT-+-1))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (5 5 (:TYPE-PRESCRIPTION STRIP-CARS))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 1 (:REWRITE |(+ y x)|))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (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 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::COMP-GCD-COND$Q3-IN-ACT-INACTIVE
 (136 2 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (54 1 (:DEFINITION TAKE))
 (43 43 (:TYPE-PRESCRIPTION LEN))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (29 3 (:DEFINITION LEN))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 6 (:REWRITE DEFAULT-CAR))
 (15 1 (:DEFINITION NTHCDR))
 (14 8 (:REWRITE DEFAULT-CDR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 1 (:DEFINITION BINARY-APPEND))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (10 7 (:REWRITE DEFAULT-+-2))
 (10 1 (:DEFINITION ADE::V-THREEFIX))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 9 (:REWRITE NTH-WHEN-PREFIXP))
 (9 7 (:REWRITE DEFAULT-<-2))
 (7 7 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE NORMALIZE-ADDENDS))
 (7 7 (:REWRITE DEFAULT-+-1))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (5 5 (:TYPE-PRESCRIPTION STRIP-CARS))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 1 (:REWRITE |(+ y x)|))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (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 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::COMP-GCD-COND$Q2-OUT-ACT-INACTIVE
 (136 2 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (54 1 (:DEFINITION TAKE))
 (43 43 (:TYPE-PRESCRIPTION LEN))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (29 3 (:DEFINITION LEN))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 6 (:REWRITE DEFAULT-CAR))
 (15 1 (:DEFINITION NTHCDR))
 (14 8 (:REWRITE DEFAULT-CDR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 1 (:DEFINITION BINARY-APPEND))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (10 10 (:REWRITE NTH-WHEN-PREFIXP))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (10 7 (:REWRITE DEFAULT-+-2))
 (10 1 (:DEFINITION ADE::V-THREEFIX))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 7 (:REWRITE DEFAULT-<-2))
 (7 7 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE NORMALIZE-ADDENDS))
 (7 7 (:REWRITE DEFAULT-+-1))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (5 5 (:TYPE-PRESCRIPTION STRIP-CARS))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 1 (:REWRITE |(+ y x)|))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (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 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::COMP-GCD-COND$Q3-OUT-ACT-INACTIVE
 (136 2 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (54 1 (:DEFINITION TAKE))
 (43 43 (:TYPE-PRESCRIPTION LEN))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (29 3 (:DEFINITION LEN))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 6 (:REWRITE DEFAULT-CAR))
 (15 1 (:DEFINITION NTHCDR))
 (14 8 (:REWRITE DEFAULT-CDR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 1 (:DEFINITION BINARY-APPEND))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (10 10 (:REWRITE NTH-WHEN-PREFIXP))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (10 7 (:REWRITE DEFAULT-+-2))
 (10 1 (:DEFINITION ADE::V-THREEFIX))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 7 (:REWRITE DEFAULT-<-2))
 (7 7 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE NORMALIZE-ADDENDS))
 (7 7 (:REWRITE DEFAULT-+-1))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (5 5 (:TYPE-PRESCRIPTION STRIP-CARS))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 1 (:REWRITE |(+ y x)|))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (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 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::COMP-GCD-COND$INV-PRESERVED
 (25072 25072 (:REWRITE NTH-WHEN-PREFIXP))
 (21908 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (18854 10269 (:REWRITE DEFAULT-+-2))
 (12612 11296 (:REWRITE DEFAULT-CDR))
 (10313 10269 (:REWRITE DEFAULT-+-1))
 (10269 10269 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (10118 118 (:DEFINITION TAKE))
 (7427 1158 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (7140 1785 (:DEFINITION STRIP-CARS))
 (7004 406 (:DEFINITION NTHCDR))
 (6200 4832 (:REWRITE DEFAULT-CAR))
 (5366 3291 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5366 3291 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (5366 3291 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (5166 2313 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (3563 962 (:REWRITE SIMPLIFY-SUMS-<))
 (3291 3291 (:REWRITE |(equal (- x) (- y))|))
 (2896 208 (:REWRITE ZP-OPEN))
 (2864 2864 (:LINEAR LEN-WHEN-PREFIXP))
 (2705 2705 (:TYPE-PRESCRIPTION BOOLEANP))
 (2684 276 (:DEFINITION BINARY-APPEND))
 (2448 192 (:REWRITE ADE::LEN-V-THREEFIX))
 (2337 482 (:REWRITE |(< d (+ c x))|))
 (2286 516 (:REWRITE TAKE-WHEN-ATOM))
 (2048 152 (:DEFINITION ADE::V-THREEFIX))
 (1822 56 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (1626 1626 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (1594 1594 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (1572 24 (:REWRITE TAKE-WHEN-PREFIXP))
 (1517 32 (:REWRITE |(< (if a b c) x)|))
 (1432 1432 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1370 1370 (:REWRITE |(< (- x) (- y))|))
 (1298 234 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (1272 180 (:DEFINITION PAIRLIS$))
 (1211 260 (:REWRITE |(< (+ c x) d)|))
 (1096 820 (:REWRITE DEFAULT-<-2))
 (1068 16 (:REWRITE ADE::TAKE-V-THREEFIX))
 (1002 56 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (968 124 (:REWRITE ADE::CAR-V-THREEFIX))
 (945 820 (:REWRITE DEFAULT-<-1))
 (846 20 (:REWRITE LEN-WHEN-PREFIXP))
 (844 289 (:REWRITE ADE::QUEUE3$OUT-ACT-INACTIVE))
 (844 289 (:REWRITE ADE::QUEUE2$OUT-ACT-INACTIVE))
 (710 710 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (710 710 (:REWRITE DEFAULT-*-2))
 (710 710 (:REWRITE DEFAULT-*-1))
 (704 104 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (674 624 (:REWRITE DEFAULT-UNARY-MINUS))
 (664 664 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (640 32 (:DEFINITION NFIX))
 (560 112 (:REWRITE |(- (* c x))|))
 (552 276 (:DEFINITION ADE::3V-FIX))
 (448 112 (:REWRITE |(+ x x)|))
 (424 424 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (424 424 (:REWRITE DEFAULT-UNARY-/))
 (400 16 (:REWRITE ADE::NTHCDR-V-THREEFIX))
 (337 176 (:REWRITE |(equal (+ c x) d)|))
 (316 316 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (316 316 (:REWRITE |(< 0 (- x))|))
 (276 276 (:TYPE-PRESCRIPTION ADE::3VP))
 (264 48 (:REWRITE CONSP-OF-APPEND))
 (262 131 (:REWRITE ADE::QUEUE3$IN-ACT-INACTIVE))
 (262 131 (:REWRITE ADE::QUEUE2$IN-ACT-INACTIVE))
 (224 112 (:REWRITE |(+ (* c x) (* d x))|))
 (224 28 (:REWRITE CAR-OF-APPEND))
 (176 176 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (176 176 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (176 176 (:REWRITE |(equal (- x) 0)|))
 (176 16 (:REWRITE ADE::F$V-EQUAL-OF-V-THREEFIX-CANCELED))
 (144 48 (:TYPE-PRESCRIPTION ADE::BVP-TAKE))
 (144 48 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (132 132 (:REWRITE |(* c (* d x))|))
 (126 18 (:REWRITE CAR-OF-TAKE))
 (122 122 (:TYPE-PRESCRIPTION PREFIXP))
 (112 112 (:REWRITE |(* 0 x)|))
 (112 112 (:REWRITE |(* (- x) y)|))
 (112 28 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (112 28 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (72 72 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (72 24 (:REWRITE ADE::BVP-TAKE))
 (72 24 (:REWRITE ADE::BVP-NTHCDR))
 (64 16 (:REWRITE ADE::F$FAST-ZERO-OF-V-THREEFIX-CANCELED))
 (58 28 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (58 28 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (56 56 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (56 56 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (56 56 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (56 56 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (52 4 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (48 16 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (48 12 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (44 4 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (36 12 (:REWRITE ADE::BVP-APPEND))
 (32 16 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (32 16 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (28 28 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (28 14 (:REWRITE |(equal (+ c x y) d)|))
 (24 24 (:REWRITE CONSP-OF-TAKE))
 (16 16 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT0))
 (16 16 (:REWRITE FOLD-CONSTS-IN-+))
 (12 12 (:TYPE-PRESCRIPTION ADE::F-NOR3))
 (8 8 (:REWRITE |(< 0 (* x y))|))
 )
(ADE::COMP-GCD-COND$EXTRACTED-STEP
 (24 12 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$IN-ACT))
 (18 18 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT))
 )
(ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (3 3 (:REWRITE NTH-WHEN-PREFIXP))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (3 3 (:REWRITE NTH-WHEN-PREFIXP))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 2 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 )
(ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-3
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (3 3 (:REWRITE NTH-WHEN-PREFIXP))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 2 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (2 2 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (1 1 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 )
(ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-4
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (3 3 (:REWRITE NTH-WHEN-PREFIXP))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 2 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-3))
 (2 2 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-3))
 (1 1 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (1 1 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 )
(ADE::COMP-GCD-COND$Q2-DATA-IN-REWRITE
 (468 1 (:REWRITE TAKE-WHEN-PREFIXP))
 (341 1 (:REWRITE PREFIXP-OF-APPEND-ARG2))
 (302 6 (:REWRITE TAKE-OF-TOO-MANY))
 (290 26 (:DEFINITION LEN))
 (179 4 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (155 79 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (115 106 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 (110 5 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (75 21 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (71 3 (:REWRITE ADE::LEN-NTHCDR))
 (67 34 (:REWRITE DEFAULT-+-2))
 (65 1 (:DEFINITION TAKE))
 (63 10 (:REWRITE SIMPLIFY-SUMS-<))
 (56 1 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (53 11 (:REWRITE |(+ y x)|))
 (49 34 (:REWRITE DEFAULT-CDR))
 (48 2 (:DEFINITION NTHCDR))
 (40 2 (:REWRITE LEN-OF-APPEND))
 (36 4 (:REWRITE TAKE-WHEN-ATOM))
 (34 34 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (34 34 (:REWRITE DEFAULT-+-1))
 (34 1 (:REWRITE ADE::NTHCDR-APPEND))
 (31 10 (:REWRITE DEFAULT-CAR))
 (30 1 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (26 26 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (24 3 (:DEFINITION STRIP-CARS))
 (22 1 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (18 10 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (18 9 (:REWRITE DEFAULT-UNARY-MINUS))
 (18 2 (:REWRITE ADE::F-GATES=B-GATES))
 (18 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (18 1 (:DEFINITION TRUE-LISTP))
 (16 1 (:REWRITE ZP-OPEN))
 (15 15 (:REWRITE NTH-WHEN-PREFIXP))
 (15 3 (:REWRITE |(+ y (+ x z))|))
 (13 7 (:REWRITE DEFAULT-<-2))
 (13 1 (:REWRITE |(+ (+ x y) z)|))
 (12 12 (:LINEAR LEN-WHEN-PREFIXP))
 (11 11 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (11 11 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (11 11 (:REWRITE |(< (- x) (- y))|))
 (11 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (11 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (9 9 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-3))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (8 7 (:REWRITE DEFAULT-<-1))
 (7 7 (:TYPE-PRESCRIPTION PREFIXP))
 (7 1 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (7 1 (:DEFINITION BINARY-APPEND))
 (6 6 (:TYPE-PRESCRIPTION NFIX))
 (6 6 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (6 4 (:REWRITE |(< d (+ c x))|))
 (6 2 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (6 1 (:REWRITE CONSP-OF-APPEND))
 (5 5 (:REWRITE LEN-OF-TAKE))
 (5 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (5 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (4 4 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (4 4 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (4 4 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (4 4 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (4 4 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (4 4 (:REWRITE |(< 0 (- x))|))
 (4 1 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (3 3 (:REWRITE CONSP-OF-TAKE))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (2 2 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (2 2 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE |(equal (- x) 0)|))
 (2 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(ADE::COMP-GCD-COND$Q3-DATA-IN-REWRITE
 (468 1 (:REWRITE TAKE-WHEN-PREFIXP))
 (341 1 (:REWRITE PREFIXP-OF-APPEND-ARG2))
 (302 6 (:REWRITE TAKE-OF-TOO-MANY))
 (290 26 (:DEFINITION LEN))
 (179 4 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (167 167 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (110 5 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (75 21 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (71 3 (:REWRITE ADE::LEN-NTHCDR))
 (67 34 (:REWRITE DEFAULT-+-2))
 (65 1 (:DEFINITION TAKE))
 (63 10 (:REWRITE SIMPLIFY-SUMS-<))
 (56 1 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (53 11 (:REWRITE |(+ y x)|))
 (49 34 (:REWRITE DEFAULT-CDR))
 (48 2 (:DEFINITION NTHCDR))
 (40 2 (:REWRITE LEN-OF-APPEND))
 (36 4 (:REWRITE TAKE-WHEN-ATOM))
 (34 34 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (34 34 (:REWRITE DEFAULT-+-1))
 (34 1 (:REWRITE ADE::NTHCDR-APPEND))
 (30 1 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (28 10 (:REWRITE DEFAULT-CAR))
 (27 18 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 (26 26 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (24 3 (:DEFINITION STRIP-CARS))
 (22 1 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (18 10 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (18 9 (:REWRITE DEFAULT-UNARY-MINUS))
 (18 1 (:DEFINITION TRUE-LISTP))
 (16 1 (:REWRITE ZP-OPEN))
 (15 15 (:REWRITE NTH-WHEN-PREFIXP))
 (15 3 (:REWRITE |(+ y (+ x z))|))
 (15 2 (:REWRITE ADE::F-GATES=B-GATES))
 (15 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (13 7 (:REWRITE DEFAULT-<-2))
 (13 1 (:REWRITE |(+ (+ x y) z)|))
 (12 12 (:LINEAR LEN-WHEN-PREFIXP))
 (11 11 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (11 11 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (11 11 (:REWRITE |(< (- x) (- y))|))
 (11 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (11 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (8 7 (:REWRITE DEFAULT-<-1))
 (7 7 (:TYPE-PRESCRIPTION PREFIXP))
 (7 1 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (7 1 (:DEFINITION BINARY-APPEND))
 (6 6 (:TYPE-PRESCRIPTION NFIX))
 (6 6 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (6 4 (:REWRITE |(< d (+ c x))|))
 (6 2 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (6 1 (:REWRITE CONSP-OF-APPEND))
 (5 5 (:REWRITE LEN-OF-TAKE))
 (5 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (5 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (4 4 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (4 4 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (4 4 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (4 4 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (4 4 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (4 4 (:REWRITE |(< 0 (- x))|))
 (4 1 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (3 3 (:REWRITE CONSP-OF-TAKE))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (2 2 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (2 2 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE |(equal (- x) 0)|))
 (2 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(ADE::COMP-GCD-COND$EXTRACTED-STEP-CORRECT-AUX
 (4 4 (:TYPE-PRESCRIPTION BINARY-APPEND))
 )
(ADE::COMP-GCD-COND$EXTRACTED-STEP-CORRECT
 (88007 335 (:REWRITE TAKE-WHEN-PREFIXP))
 (53318 148 (:REWRITE PREFIXP-OF-APPEND-ARG2))
 (48930 1132 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (42077 42077 (:REWRITE NTH-WHEN-PREFIXP))
 (37616 20735 (:REWRITE DEFAULT-+-2))
 (35686 1392 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (31863 24172 (:REWRITE DEFAULT-CDR))
 (20735 20735 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (20735 20735 (:REWRITE DEFAULT-+-1))
 (17797 3294 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (14956 4353 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (14956 4353 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (14956 4353 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (14419 2805 (:REWRITE SIMPLIFY-SUMS-<))
 (11955 6797 (:REWRITE DEFAULT-CAR))
 (9716 118 (:REWRITE PREFIXP-OF-CONS-RIGHT))
 (8498 148 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (7205 655 (:REWRITE |(+ (+ x y) z)|))
 (5481 1357 (:REWRITE TAKE-WHEN-ATOM))
 (5141 1495 (:REWRITE |(< d (+ c x))|))
 (4960 852 (:REWRITE |(+ y (+ x z))|))
 (4624 315 (:REWRITE ADE::QUEUE3$OUT-ACT-INACTIVE))
 (4540 4540 (:LINEAR LEN-WHEN-PREFIXP))
 (4422 299 (:REWRITE ADE::QUEUE2$OUT-ACT-INACTIVE))
 (4353 4353 (:REWRITE |(equal (- x) (- y))|))
 (4349 4345 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (4331 4331 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (3898 3898 (:REWRITE |(< (- x) (- y))|))
 (3863 566 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (3174 2692 (:REWRITE DEFAULT-UNARY-MINUS))
 (2896 2053 (:REWRITE DEFAULT-<-2))
 (2755 2755 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (2388 186 (:DEFINITION ADE::V-THREEFIX))
 (2271 2053 (:REWRITE DEFAULT-<-1))
 (2270 2270 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2037 277 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (1944 108 (:DEFINITION TRUE-LISTP))
 (1913 566 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (1874 1874 (:TYPE-PRESCRIPTION PREFIXP))
 (1838 573 (:REWRITE |(< (+ c x) d)|))
 (1720 1720 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$IN-ACT))
 (1562 42 (:REWRITE |(< (if a b c) x)|))
 (1516 1516 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1516 1516 (:REWRITE DEFAULT-*-2))
 (1516 1516 (:REWRITE DEFAULT-*-1))
 (1428 238 (:REWRITE ADE::QUEUE2$IN-ACT-INACTIVE))
 (1413 300 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (1401 236 (:DEFINITION NATP))
 (1380 230 (:REWRITE ADE::QUEUE3$IN-ACT-INACTIVE))
 (1296 176 (:REWRITE ADE::CAR-V-THREEFIX))
 (1296 108 (:REWRITE LEN-OF-LIST-FIX))
 (1208 1208 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (1208 1208 (:REWRITE DEFAULT-UNARY-/))
 (1198 36 (:REWRITE LEN-WHEN-PREFIXP))
 (1132 1132 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (1132 1132 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (1132 1132 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (1132 1132 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (1016 488 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (1001 1001 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1001 1001 (:REWRITE |(< 0 (- x))|))
 (1000 200 (:REWRITE |(- (* c x))|))
 (888 222 (:REWRITE |(+ x x)|))
 (860 860 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT))
 (840 42 (:DEFINITION NFIX))
 (756 108 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (724 362 (:DEFINITION ADE::3V-FIX))
 (663 300 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (650 25 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (648 216 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (600 25 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (584 584 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (566 566 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (432 432 (:TYPE-PRESCRIPTION TRUE-LIST-FIX))
 (400 200 (:REWRITE |(+ (* c x) (* d x))|))
 (364 364 (:REWRITE |(* c (* d x))|))
 (362 362 (:TYPE-PRESCRIPTION ADE::3VP))
 (312 52 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (312 52 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (312 52 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (236 236 (:TYPE-PRESCRIPTION NATP))
 (224 112 (:REWRITE LIST-EQUIV-OF-NIL-RIGHT))
 (220 55 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (200 200 (:REWRITE |(* 0 x)|))
 (200 200 (:REWRITE |(* (- x) y)|))
 (176 176 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (176 176 (:REWRITE |(equal (- x) 0)|))
 (168 168 (:TYPE-PRESCRIPTION BOOLEANP))
 (108 108 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (105 105 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (48 16 (:REWRITE ADE::BVP-APPEND))
 (42 42 (:TYPE-PRESCRIPTION ADE::F-NOR3))
 (42 42 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (38 1 (:REWRITE |(< (+ c x) (+ d y))|))
 (21 21 (:TYPE-PRESCRIPTION ADE::F-AND))
 (3 1 (:REWRITE |(< (+ d x) (+ c y))|))
 )
(ADE::COMP-GCD-COND$VALID-ST-PRESERVED
 (38583 38583 (:REWRITE NTH-WHEN-PREFIXP))
 (20346 11025 (:REWRITE DEFAULT-+-2))
 (19866 354 (:REWRITE TAKE-WHEN-PREFIXP))
 (18932 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (18316 2501 (:DEFINITION STRIP-CARS))
 (15810 492 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (15456 13518 (:REWRITE DEFAULT-CDR))
 (11961 3356 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (11961 3356 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (11961 3356 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (11025 11025 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (11025 11025 (:REWRITE DEFAULT-+-1))
 (9159 6438 (:REWRITE DEFAULT-CAR))
 (9066 492 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (7541 406 (:DEFINITION TAKE))
 (5537 452 (:DEFINITION NTHCDR))
 (4665 1092 (:REWRITE TAKE-WHEN-ATOM))
 (4655 364 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (3729 339 (:REWRITE |(+ (+ x y) z)|))
 (3356 3356 (:REWRITE |(equal (- x) (- y))|))
 (3236 284 (:DEFINITION ADE::V-THREEFIX))
 (2623 174 (:REWRITE ADE::QUEUE3$OUT-ACT-INACTIVE))
 (2502 450 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (2344 174 (:REWRITE ADE::QUEUE2$OUT-ACT-INACTIVE))
 (2128 112 (:REWRITE ADE::LEN-NTHCDR))
 (2064 450 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (1912 216 (:DEFINITION BINARY-APPEND))
 (1540 308 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA-IN))
 (1539 1539 (:REWRITE |(< (- x) (- y))|))
 (1504 1326 (:REWRITE SIMPLIFY-SUMS-<))
 (1504 1326 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (1504 1326 (:REWRITE DEFAULT-<-1))
 (1456 1456 (:LINEAR LEN-WHEN-PREFIXP))
 (1326 1326 (:REWRITE DEFAULT-<-2))
 (1270 158 (:DEFINITION PAIRLIS$))
 (1160 40 (:REWRITE LEN-OF-APPEND))
 (1100 148 (:REWRITE ADE::CAR-V-THREEFIX))
 (912 432 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (864 432 (:DEFINITION ADE::3V-FIX))
 (780 780 (:TYPE-PRESCRIPTION PREFIXP))
 (751 751 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (751 751 (:REWRITE DEFAULT-*-2))
 (751 751 (:REWRITE DEFAULT-*-1))
 (728 728 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (672 16 (:REWRITE ADE::TAKE-V-THREEFIX))
 (600 100 (:REWRITE ADE::QUEUE3$IN-ACT-INACTIVE))
 (600 100 (:REWRITE ADE::QUEUE2$IN-ACT-INACTIVE))
 (549 549 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (492 492 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (492 492 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (492 492 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (492 492 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (464 16 (:REWRITE ADE::NTHCDR-V-THREEFIX))
 (450 450 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (440 440 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (432 432 (:TYPE-PRESCRIPTION ADE::3VP))
 (426 426 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (426 426 (:REWRITE DEFAULT-UNARY-/))
 (421 421 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (421 421 (:REWRITE REDUCE-INTEGERP-+))
 (421 421 (:REWRITE INTEGERP-MINUS-X))
 (421 421 (:REWRITE |(< (- x) 0)|))
 (421 421 (:META META-INTEGERP-CORRECT))
 (368 368 (:REWRITE DEFAULT-UNARY-MINUS))
 (294 42 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (288 72 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (264 48 (:REWRITE CONSP-OF-APPEND))
 (261 261 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (261 261 (:REWRITE |(< 0 (- x))|))
 (224 28 (:REWRITE CAR-OF-APPEND))
 (212 16 (:REWRITE ADE::F$V-EQUAL-OF-V-THREEFIX-CANCELED))
 (168 42 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (160 40 (:REWRITE |(+ x x)|))
 (156 156 (:REWRITE ADE::LEN-QUEUE3$DATA-OUT-2))
 (140 140 (:REWRITE ADE::LEN-QUEUE2$DATA-OUT-2))
 (104 4 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (98 98 (:REWRITE |(* c (* d x))|))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (96 4 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (84 28 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (80 16 (:REWRITE |(- (* c x))|))
 (64 16 (:REWRITE ADE::F$FAST-ZERO-OF-V-THREEFIX-CANCELED))
 (64 16 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (48 48 (:TYPE-PRESCRIPTION BOOLEANP))
 (48 12 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (36 36 (:TYPE-PRESCRIPTION ADE::F-NOR3))
 (36 36 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (36 12 (:REWRITE ADE::BVP-APPEND))
 (32 16 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (32 16 (:REWRITE |(+ (* c x) (* d x))|))
 (16 16 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT0))
 (16 16 (:REWRITE |(* 0 x)|))
 (16 16 (:REWRITE |(* (- x) y)|))
 (8 8 (:REWRITE |(< 0 (* x y))|))
 (8 4 (:REWRITE BOOL-FIX-UNDER-IFF))
 )
(ADE::COMP-GCD-COND$DATA-OUTS-REWRITE
 (2259 1625 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 (1221 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (1021 774 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (552 12 (:REWRITE TAKE-OF-TOO-MANY))
 (525 519 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-3))
 (442 62 (:DEFINITION STRIP-CARS))
 (440 440 (:REWRITE NTH-WHEN-PREFIXP))
 (361 229 (:REWRITE DEFAULT-+-2))
 (355 284 (:REWRITE DEFAULT-CDR))
 (343 222 (:REWRITE DEFAULT-CAR))
 (334 44 (:DEFINITION BINARY-APPEND))
 (313 68 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (313 68 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (313 68 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (312 24 (:DEFINITION NTHCDR))
 (295 29 (:REWRITE ADE::F-GATES=B-GATES))
 (295 13 (:DEFINITION ADE::V-THREEFIX))
 (264 24 (:REWRITE |(+ (+ x y) z)|))
 (229 229 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (229 229 (:REWRITE DEFAULT-+-1))
 (180 36 (:REWRITE |(+ y x)|))
 (160 88 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (120 60 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (116 20 (:REWRITE SIMPLIFY-SUMS-<))
 (112 4 (:REWRITE ADE::LEN-NTHCDR))
 (96 12 (:REWRITE CAR-OF-APPEND))
 (92 16 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (77 7 (:REWRITE ADE::CAR-V-THREEFIX))
 (76 76 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (76 76 (:REWRITE DEFAULT-*-2))
 (76 76 (:REWRITE DEFAULT-*-1))
 (74 74 (:TYPE-PRESCRIPTION BOOLEANP))
 (68 68 (:REWRITE |(equal (- x) (- y))|))
 (60 60 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (50 10 (:REWRITE CONSP-OF-APPEND))
 (48 48 (:LINEAR LEN-WHEN-PREFIXP))
 (48 12 (:REWRITE TAKE-WHEN-ATOM))
 (48 1 (:REWRITE ADE::GCD-COND$ACT1-INACTIVE))
 (48 1 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (46 1 (:REWRITE ADE::GCD-COND$ACT0-INACTIVE))
 (46 1 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (40 20 (:DEFINITION ADE::3V-FIX))
 (28 20 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (24 24 (:REWRITE |(< (- x) (- y))|))
 (24 24 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (24 4 (:REWRITE |(+ y (+ x z))|))
 (20 20 (:TYPE-PRESCRIPTION ADE::3VP))
 (20 16 (:REWRITE DEFAULT-<-2))
 (20 16 (:REWRITE DEFAULT-<-1))
 (20 5 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (19 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (19 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (18 18 (:REWRITE |(* (- x) y)|))
 (16 16 (:TYPE-PRESCRIPTION ADE::JOINT-ACT))
 (16 16 (:TYPE-PRESCRIPTION ADE::F-AND))
 (15 15 (:TYPE-PRESCRIPTION ADE::GCD-COND$FLAG))
 (14 14 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT))
 (12 12 (:TYPE-PRESCRIPTION NFIX))
 (10 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (8 8 (:REWRITE DEFAULT-UNARY-/))
 (8 8 (:REWRITE |(< d (+ c x))|))
 (8 8 (:REWRITE |(< 0 (- x))|))
 (8 8 (:REWRITE |(* c (* d x))|))
 (6 6 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (5 5 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-3))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (4 4 (:REWRITE |(equal (- x) 0)|))
 (4 4 (:REWRITE |(< 0 (* x y))|))
 (2 1 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (1 1 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT0))
 )
(ADE::COMP-GCD-COND$EXTRACT-LEMMA
 (9528 20 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (3600 60 (:REWRITE TAKE-OF-TOO-MANY))
 (2280 314 (:DEFINITION STRIP-CARS))
 (2276 2276 (:REWRITE NTH-WHEN-PREFIXP))
 (1728 130 (:DEFINITION NTHCDR))
 (1706 1173 (:REWRITE DEFAULT-+-2))
 (1680 60 (:REWRITE ADE::LEN-NTHCDR))
 (1487 1209 (:REWRITE DEFAULT-CDR))
 (1419 962 (:REWRITE DEFAULT-CAR))
 (1408 128 (:REWRITE |(+ (+ x y) z)|))
 (1173 1173 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1173 1173 (:REWRITE DEFAULT-+-1))
 (996 60 (:DEFINITION ADE::V-THREEFIX))
 (570 60 (:REWRITE ADE::F-GATES=B-GATES))
 (524 524 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (436 147 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (436 147 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (436 147 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (432 24 (:REWRITE ADE::LEN-V-THREEFIX))
 (420 60 (:REWRITE TAKE-WHEN-ATOM))
 (380 20 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (356 356 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (356 356 (:REWRITE DEFAULT-*-2))
 (356 356 (:REWRITE DEFAULT-*-1))
 (318 318 (:LINEAR LEN-WHEN-PREFIXP))
 (304 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (244 122 (:REWRITE SIMPLIFY-SUMS-<))
 (244 122 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (244 122 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (238 64 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (236 20 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (210 38 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
 (192 8 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (184 122 (:REWRITE DEFAULT-<-2))
 (182 122 (:REWRITE DEFAULT-<-1))
 (176 8 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (159 159 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (158 158 (:TYPE-PRESCRIPTION BOOLEANP))
 (147 147 (:REWRITE |(equal (- x) (- y))|))
 (140 140 (:TYPE-PRESCRIPTION ADE::GCD-COND$DATA-IN))
 (134 67 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT))
 (122 122 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (122 122 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (122 122 (:REWRITE |(< (- x) (- y))|))
 (120 60 (:DEFINITION ADE::3V-FIX))
 (72 72 (:REWRITE |(* (- x) y)|))
 (60 60 (:TYPE-PRESCRIPTION NFIX))
 (60 60 (:TYPE-PRESCRIPTION ADE::3VP))
 (60 60 (:REWRITE |(< d (+ c x))|))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (38 38 (:TYPE-PRESCRIPTION ADE::JOINT-ACT))
 (38 19 (:REWRITE |(equal (+ c x) d)|))
 (38 2 (:REWRITE ZP-OPEN))
 (36 12 (:REWRITE ADE::BVP-APPEND))
 (30 30 (:TYPE-PRESCRIPTION ADE::GCD-COND$FLAG))
 (30 30 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (20 20 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT0))
 (20 20 (:LINEAR ADE::QUEUE3$EXTRACT-NOT-EMPTY))
 (12 12 (:REWRITE ADE::JOINT-ACT-REWRITE))
 (11 11 (:LINEAR ADE::QUEUE2$EXTRACT-NOT-EMPTY))
 (10 10 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-3))
 (6 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 2 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT1))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (2 2 (:REWRITE |(< 0 (- x))|))
 )
(ADE::COMP-GCD-COND$IN-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT))
 )
(ADE::COMP-GCD-COND$IN-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 )
(ADE::COMP-GCD-COND$IN-SEQ-LEMMA
 (3022 74 (:REWRITE TAKE-OF-TOO-MANY))
 (2590 37 (:DEFINITION TAKE))
 (1169 170 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (921 258 (:REWRITE DEFAULT-CAR))
 (890 77 (:DEFINITION NTHCDR))
 (884 202 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (725 65 (:REWRITE ZP-OPEN))
 (614 614 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$DATA-IN))
 (592 296 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (587 587 (:TYPE-PRESCRIPTION LEN))
 (478 256 (:REWRITE DEFAULT-CDR))
 (440 40 (:REWRITE |(+ (+ x y) z)|))
 (434 77 (:REWRITE |(< d (+ c x))|))
 (410 58 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (410 58 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (410 58 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (398 324 (:REWRITE DEFAULT-+-2))
 (396 40 (:REWRITE ADE::F-GATES=B-GATES))
 (386 386 (:REWRITE NTH-WHEN-PREFIXP))
 (385 77 (:REWRITE |(+ y x)|))
 (354 93 (:REWRITE |(+ c (+ d x))|))
 (333 37 (:DEFINITION LEN))
 (329 49 (:DEFINITION BINARY-APPEND))
 (324 324 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (324 324 (:REWRITE NORMALIZE-ADDENDS))
 (324 324 (:REWRITE DEFAULT-+-1))
 (296 296 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (281 74 (:REWRITE TAKE-WHEN-ATOM))
 (242 242 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (240 204 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (236 98 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (230 230 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (202 202 (:REWRITE |(< (- x) (- y))|))
 (170 133 (:REWRITE SIMPLIFY-SUMS-<))
 (170 133 (:REWRITE DEFAULT-<-2))
 (160 32 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA-IN))
 (148 148 (:LINEAR LEN-WHEN-PREFIXP))
 (144 36 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (133 133 (:REWRITE DEFAULT-<-1))
 (128 64 (:REWRITE |(* y x)|))
 (96 32 (:REWRITE |(* y (* x z))|))
 (90 90 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$STEP))
 (84 14 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (84 14 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (84 14 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (74 74 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (72 72 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (72 72 (:REWRITE DEFAULT-*-2))
 (72 72 (:REWRITE DEFAULT-*-1))
 (70 70 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$DATA0-OUT))
 (70 22 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (69 69 (:TYPE-PRESCRIPTION NFIX))
 (64 64 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (64 64 (:REWRITE DEFAULT-UNARY-/))
 (64 64 (:REWRITE |(* a (/ a))|))
 (58 58 (:REWRITE |(equal (- x) (- y))|))
 (48 48 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$DATA1-OUT))
 (42 42 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-3))
 (42 14 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (37 37 (:REWRITE |(< (+ c x) d)|))
 (37 37 (:REWRITE |(+ 0 x)|))
 (32 32 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (32 32 (:REWRITE |(< 0 (- x))|))
 (32 32 (:REWRITE |(* c (* d x))|))
 (28 28 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$VALID-ST))
 (18 18 (:TYPE-PRESCRIPTION ADE::DE))
 (12 12 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-PLUS))
 )
(ADE::COMP-GCD-COND$OUT-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT))
 )
(ADE::COMP-GCD-COND$OUT-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 )
(ADE::COMP-GCD-COND$OUT-SEQ-LEMMA
 (725 65 (:REWRITE ZP-OPEN))
 (636 40 (:REWRITE ADE::F-GATES=B-GATES))
 (506 54 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (398 36 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (380 54 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (329 49 (:DEFINITION BINARY-APPEND))
 (312 100 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (312 100 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (312 100 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (302 302 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-3))
 (300 300 (:REWRITE NTH-WHEN-PREFIXP))
 (276 120 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (236 98 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (192 54 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (138 138 (:REWRITE DEFAULT-CAR))
 (129 111 (:REWRITE DEFAULT-CDR))
 (120 120 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT0))
 (120 40 (:REWRITE ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (111 29 (:REWRITE ADE::COMP-GCD-COND$EXTRACT-LEMMA))
 (104 104 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (104 104 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (104 104 (:REWRITE DEFAULT-+-2))
 (104 104 (:REWRITE DEFAULT-+-1))
 (100 100 (:REWRITE |(equal (- x) (- y))|))
 (96 6 (:DEFINITION NTHCDR))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (80 80 (:TYPE-PRESCRIPTION BOOLEANP))
 (70 70 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$DATA0-OUT))
 (70 22 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (66 6 (:REWRITE |(+ (+ x y) z)|))
 (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))|))
 (60 20 (:REWRITE ADE::COMP-GCD-COND$VALID-ST-PRESERVED))
 (56 14 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (48 48 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$DATA1-OUT))
 (30 30 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$STEP))
 (30 6 (:REWRITE |(+ y x)|))
 (28 28 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 (24 12 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA0-OUT-2))
 (12 12 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-PLUS))
 (6 6 (:TYPE-PRESCRIPTION ADE::DE))
 (6 6 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(ADE::COMP-GCD-COND$DATAFLOW-CORRECT-AUX
 (184 172 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (43 12 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (22 8 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-CAR))
 (10 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (10 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (10 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (6 2 (:REWRITE CAR-OF-APPEND))
 (6 2 (:DEFINITION ADE::COMP-GCD-COND$OP-MAP))
 (5 5 (:REWRITE CONSP-OF-APPEND))
 (4 4 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (2 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::COMP-GCD-COND$DATAFLOW-CORRECT
 (7064 92 (:REWRITE TAKE-OF-TOO-MANY))
 (3516 46 (:DEFINITION TAKE))
 (2000 206 (:REWRITE ZP-OPEN))
 (1990 440 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (1816 82 (:REWRITE |(< (if a b c) x)|))
 (1537 476 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (1362 78 (:REWRITE |(< x (if a b c))|))
 (1288 86 (:DEFINITION NFIX))
 (1237 57 (:DEFINITION NTHCDR))
 (1148 132 (:REWRITE ADE::NFIX-OF-NAT))
 (1102 156 (:REWRITE |(< d (+ c x))|))
 (1038 98 (:DEFINITION LEN))
 (934 58 (:DEFINITION NATP))
 (762 762 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (756 36 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA-IN))
 (729 729 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (683 351 (:REWRITE DEFAULT-CDR))
 (612 612 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$DATA-IN))
 (583 384 (:REWRITE SIMPLIFY-SUMS-<))
 (543 368 (:REWRITE DEFAULT-+-2))
 (516 82 (:REWRITE |(< (+ c x) d)|))
 (476 476 (:REWRITE |(< (- x) (- y))|))
 (461 72 (:DEFINITION BINARY-APPEND))
 (452 374 (:REWRITE DEFAULT-<-2))
 (428 388 (:REWRITE NORMALIZE-ADDENDS))
 (402 374 (:REWRITE DEFAULT-<-1))
 (386 248 (:REWRITE DEFAULT-CAR))
 (368 368 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (368 368 (:REWRITE DEFAULT-+-1))
 (368 92 (:REWRITE TAKE-WHEN-ATOM))
 (365 77 (:REWRITE |(+ y x)|))
 (349 113 (:REWRITE |(+ c (+ d x))|))
 (349 47 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (295 84 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (295 84 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (295 84 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (266 266 (:LINEAR LEN-WHEN-PREFIXP))
 (240 4 (:REWRITE LEN-OF-TAKE))
 (220 20 (:REWRITE |(+ (+ x y) z)|))
 (212 59 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (201 201 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (180 72 (:REWRITE |(* x (if a b c))|))
 (144 72 (:REWRITE |(* y x)|))
 (133 133 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (116 116 (:REWRITE NTH-WHEN-PREFIXP))
 (112 4 (:REWRITE CONSP-OF-TAKE))
 (108 108 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$IN-SEQ))
 (108 108 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (108 108 (:REWRITE REDUCE-INTEGERP-+))
 (108 108 (:REWRITE INTEGERP-MINUS-X))
 (108 108 (:REWRITE |(< (- x) 0)|))
 (108 108 (:META META-INTEGERP-CORRECT))
 (108 36 (:REWRITE |(* y (* x z))|))
 (102 102 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 (101 3 (:REWRITE ADE::NTHCDR-CONS))
 (92 92 (:TYPE-PRESCRIPTION NFIX))
 (85 3 (:DEFINITION POSP))
 (84 84 (:REWRITE |(equal (- x) (- y))|))
 (72 72 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (72 72 (:REWRITE DEFAULT-UNARY-/))
 (72 72 (:REWRITE |(* a (/ a))|))
 (60 60 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$STEP))
 (60 59 (:REWRITE |(+ 0 x)|))
 (58 58 (:TYPE-PRESCRIPTION NATP))
 (58 10 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (50 10 (:REWRITE |(+ y (+ x z))|))
 (48 4 (:REWRITE |(+ (if a b c) x)|))
 (41 41 (:LINEAR ADE::COMP-GCD-COND$EXTRACT-NOT-EMPTY-2))
 (41 41 (:LINEAR ADE::COMP-GCD-COND$EXTRACT-NOT-EMPTY-1))
 (40 20 (:REWRITE BUBBLE-DOWN-+-MATCH-1))
 (40 6 (:REWRITE |(+ x (if a b c))|))
 (38 38 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (38 38 (:REWRITE |(< 0 (- x))|))
 (36 36 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (36 36 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (36 36 (:REWRITE INSERT-0-*))
 (36 36 (:REWRITE DEFAULT-*-2))
 (36 36 (:REWRITE DEFAULT-*-1))
 (36 36 (:REWRITE |(equal (- x) 0)|))
 (36 36 (:REWRITE |(* c (* d x))|))
 (20 20 (:REWRITE DEFAULT-UNARY-MINUS))
 (20 20 (:REWRITE |(+ x (- x))|))
 (14 14 (:REWRITE ADE::COMP-GCD-COND$RUN-PLUS))
 (12 12 (:REWRITE ADE::COMP-GCD-COND$INPUT-FORMAT-PLUS))
 (12 8 (:REWRITE ADE::COMP-GCD-COND$INV-PRESERVED))
 (3 3 (:TYPE-PRESCRIPTION POSP))
 (3 3 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$RUN))
 )
(ADE::COMP-GCD-COND$FUNCTIONALLY-CORRECT
 (896 4 (:DEFINITION ADE::COMP-GCD-COND$IN-SEQ))
 (600 8 (:REWRITE TAKE-OF-TOO-MANY))
 (392 4 (:DEFINITION ADE::COMP-GCD-COND$OUT-SEQ))
 (284 4 (:DEFINITION TAKE))
 (168 4 (:REWRITE ADE::COMP-GCD-COND$EXTRACT-LEMMA))
 (164 8 (:REWRITE |(< (if a b c) x)|))
 (164 7 (:DEFINITION NTHCDR))
 (146 31 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (140 8 (:REWRITE |(< x (if a b c))|))
 (138 27 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (112 8 (:DEFINITION NFIX))
 (105 45 (:REWRITE ZP-OPEN))
 (103 103 (:TYPE-PRESCRIPTION LEN))
 (84 4 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA-IN))
 (80 32 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (79 46 (:REWRITE DEFAULT-CDR))
 (76 4 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (72 12 (:REWRITE ADE::NFIX-OF-NAT))
 (68 68 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$DATA-IN))
 (67 19 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (67 19 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (67 19 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (63 7 (:DEFINITION LEN))
 (56 4 (:DEFINITION NATP))
 (52 52 (:TYPE-PRESCRIPTION ZP))
 (52 52 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-2))
 (50 50 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (50 50 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (50 36 (:REWRITE DEFAULT-+-2))
 (50 7 (:REWRITE |(< d (+ c x))|))
 (44 32 (:REWRITE DEFAULT-CAR))
 (40 40 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$IN-ACT))
 (36 36 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (36 36 (:REWRITE NORMALIZE-ADDENDS))
 (36 36 (:REWRITE DEFAULT-+-1))
 (35 7 (:REWRITE |(+ y x)|))
 (33 3 (:REWRITE |(+ (+ x y) z)|))
 (32 8 (:REWRITE TAKE-WHEN-ATOM))
 (31 31 (:REWRITE |(< (- x) (- y))|))
 (30 23 (:REWRITE SIMPLIFY-SUMS-<))
 (30 23 (:REWRITE DEFAULT-<-2))
 (28 28 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$IN-SEQ))
 (24 6 (:REWRITE ADE::OPEN-COMP-GCD-COND$INPUT-FORMAT-N-ZP))
 (24 6 (:REWRITE ADE::OPEN-COMP-GCD-COND$INPUT-FORMAT-N))
 (23 23 (:REWRITE DEFAULT-<-1))
 (23 7 (:REWRITE |(+ c (+ d x))|))
 (20 20 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT))
 (20 20 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$IN-ACT))
 (20 8 (:REWRITE |(* x (if a b c))|))
 (20 4 (:DEFINITION ADE::COMP-GCD-COND$OP-MAP))
 (19 19 (:REWRITE |(equal (- x) (- y))|))
 (16 16 (:LINEAR LEN-WHEN-PREFIXP))
 (16 8 (:REWRITE |(* y x)|))
 (16 4 (:REWRITE ADE::OPEN-DE-N-ZP))
 (16 4 (:REWRITE ADE::OPEN-DE-N))
 (16 4 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (12 12 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (12 12 (:REWRITE REDUCE-INTEGERP-+))
 (12 12 (:REWRITE INTEGERP-MINUS-X))
 (12 12 (:REWRITE |(< (- x) 0)|))
 (12 12 (:META META-INTEGERP-CORRECT))
 (12 4 (:REWRITE |(* y (* x z))|))
 (12 3 (:REWRITE ADE::OPEN-COMP-GCD-COND$RUN-ZP))
 (12 3 (:REWRITE ADE::OPEN-COMP-GCD-COND$RUN))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (8 8 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT-LEMMA-1))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (8 8 (:REWRITE DEFAULT-UNARY-/))
 (8 8 (:REWRITE |(* a (/ a))|))
 (8 8 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (4 4 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (4 4 (:REWRITE INSERT-0-*))
 (4 4 (:REWRITE DEFAULT-*-2))
 (4 4 (:REWRITE DEFAULT-*-1))
 (4 4 (:REWRITE |(equal (- x) 0)|))
 (4 4 (:REWRITE |(< 0 (- x))|))
 (4 4 (:REWRITE |(< (+ c x) d)|))
 (4 4 (:REWRITE |(+ 0 x)|))
 (4 4 (:REWRITE |(* c (* d x))|))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-N))
 (3 3 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$RUN))
 )