(ADE::COMP-GCD$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$INS-LEN)
(ADE::COMP-GCD*)
(ADE::COMP-GCD*$DESTRUCTURE
 (360 36 (:DEFINITION BINARY-APPEND))
 (351 72 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (108 108 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (108 108 (:REWRITE DEFAULT-*-2))
 (108 108 (:REWRITE DEFAULT-*-1))
 (46 46 (:REWRITE DEFAULT-CDR))
 (41 41 (:REWRITE DEFAULT-CAR))
 )
(ADE::NOT-PRIMP-COMP-GCD
 (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$NETLIST)
(ADE::COMP-GCD&
 (216 12 (:DEFINITION ASSOC-EQUAL))
 (52 13 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
 (40 40 (:REWRITE DEFAULT-CAR))
 (38 25 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (38 25 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (38 25 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (26 26 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
 (25 25 (:REWRITE |(equal (- x) (- y))|))
 (18 1 (:DEFINITION ADE::DELETE-TO-EQ))
 (16 16 (:REWRITE DEFAULT-CDR))
 (13 13 (:REWRITE DEFAULT-SYMBOL-NAME))
 (10 10 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (10 10 (:REWRITE DEFAULT-*-2))
 (10 10 (:REWRITE DEFAULT-*-1))
 (3 3 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (1 1 (:REWRITE SIMPLIFY-SUMS-<))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (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) (- y))|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::CHECK-COMP-GCD$NETLIST-64)
(ADE::COMP-GCD$ST-FORMAT)
(ADE::COMP-GCD$ST-FORMAT=>CONSTRAINT
 (21 3 (:DEFINITION LEN))
 (7 7 (:REWRITE NTH-WHEN-PREFIXP))
 (6 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (6 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 (3 3 (: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$VALID-ST)
(ADE::COMP-GCD$VALID-ST=>CONSTRAINT
 (32 32 (:REWRITE SIMPLIFY-SUMS-<))
 (32 32 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (32 32 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (32 32 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (32 32 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (32 32 (:REWRITE DEFAULT-<-2))
 (32 32 (:REWRITE DEFAULT-<-1))
 (32 32 (:REWRITE |(< (- x) (- y))|))
 (28 4 (:DEFINITION LEN))
 (20 16 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (20 16 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (20 16 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (16 16 (:REWRITE REDUCE-INTEGERP-+))
 (16 16 (:REWRITE NTH-WHEN-PREFIXP))
 (16 16 (:REWRITE INTEGERP-MINUS-X))
 (16 16 (:REWRITE |(equal (- x) (- y))|))
 (16 16 (:REWRITE |(< (- x) 0)|))
 (16 16 (:META META-INTEGERP-CORRECT))
 (12 3 (:DEFINITION STRIP-CARS))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 4 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (4 4 (:REWRITE NORMALIZE-ADDENDS))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 )
(ADE::COMP-GCD$VALID-ST=>ST-FORMAT
 (77 77 (:REWRITE NTH-WHEN-PREFIXP))
 (51 51 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (51 51 (:REWRITE DEFAULT-*-2))
 (51 51 (:REWRITE DEFAULT-*-1))
 (14 13 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (14 13 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (14 13 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (13 13 (:REWRITE |(equal (- x) (- y))|))
 (12 3 (:DEFINITION STRIP-CARS))
 (7 7 (:REWRITE DEFAULT-CAR))
 (7 1 (:DEFINITION LEN))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 5 (:REWRITE DEFAULT-CDR))
 (5 1 (:DEFINITION TRUE-LISTP))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1 1 (:REWRITE NORMALIZE-ADDENDS))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::COMP-GCD$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$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$ME-INPUTS)
(ADE::COMP-GCD$BR-INPUTS
 (1 1 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::COMP-GCD$BODY-INPUTS
 (2 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::COMP-GCD$IN-ACT)
(ADE::COMP-GCD$IN-ACT-INACTIVE
 (104 1 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (34 34 (:TYPE-PRESCRIPTION LEN))
 (20 11 (:REWRITE DEFAULT-CAR))
 (18 2 (:DEFINITION LEN))
 (18 2 (:DEFINITION BINARY-APPEND))
 (16 8 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (11 11 (:REWRITE NTH-WHEN-PREFIXP))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (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 1 (:DEFINITION ADE::V-THREEFIX))
 (9 6 (:REWRITE DEFAULT-<-1))
 (8 8 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (7 7 (:REWRITE DEFAULT-CDR))
 (7 6 (:REWRITE DEFAULT-<-2))
 (7 5 (:REWRITE DEFAULT-+-2))
 (7 1 (:REWRITE TAKE-WHEN-ATOM))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 6 (:REWRITE |(< (- x) (- y))|))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (5 5 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (5 5 (:TYPE-PRESCRIPTION STRIP-CARS))
 (5 5 (:TYPE-PRESCRIPTION ADE::COMP-GCD$DATA-IN))
 (5 5 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (5 5 (:REWRITE NORMALIZE-ADDENDS))
 (5 5 (:REWRITE DEFAULT-+-1))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (4 1 (:DEFINITION STRIP-CARS))
 (2 2 (:TYPE-PRESCRIPTION BOOLEANP))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NFIX))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::COMP-GCD$OUT-ACT)
(ADE::COMP-GCD$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))
 (30 2 (:DEFINITION NTHCDR))
 (29 3 (:DEFINITION LEN))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (18 9 (:REWRITE DEFAULT-CAR))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 9 (:REWRITE DEFAULT-CDR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (12 12 (:REWRITE NTH-WHEN-PREFIXP))
 (12 9 (:REWRITE DEFAULT-+-2))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 1 (:DEFINITION BINARY-APPEND))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (10 2 (:REWRITE |(+ y x)|))
 (10 1 (:DEFINITION ADE::V-THREEFIX))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE NORMALIZE-ADDENDS))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 7 (:REWRITE DEFAULT-<-2))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 3 (:REWRITE ADE::F-GATES=B-GATES))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 6 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (5 5 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (5 5 (:TYPE-PRESCRIPTION STRIP-CARS))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (4 1 (:DEFINITION STRIP-CARS))
 (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$DATA-OUT)
(ADE::LEN-COMP-GCD$DATA-OUT-1
 (21 3 (:DEFINITION LEN))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (6 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (6 3 (:REWRITE DEFAULT-+-2))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (3 1 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA0-OUT-2))
 (2 2 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$VALID-ST))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::LEN-COMP-GCD$DATA-OUT-2
 (32 32 (:REWRITE NTH-WHEN-PREFIXP))
 (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))
 (16 16 (:REWRITE |(equal (- x) (- y))|))
 (12 3 (:DEFINITION STRIP-CARS))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 4 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (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))
 (3 3 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::BVP-COMP-GCD$DATA-OUT
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (96 16 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (80 80 (:REWRITE NTH-WHEN-PREFIXP))
 (52 48 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (52 48 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (52 48 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (48 48 (:REWRITE |(equal (- x) (- y))|))
 (28 4 (:DEFINITION LEN))
 (12 3 (:DEFINITION STRIP-CARS))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 4 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (4 4 (:REWRITE NORMALIZE-ADDENDS))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 )
(ADE::COMP-GCD$OUTPUTS)
(ADE::COMP-GCD$VALUE
 (2190 314 (:DEFINITION BINARY-APPEND))
 (861 447 (:REWRITE DEFAULT-+-2))
 (447 447 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (447 447 (:REWRITE DEFAULT-+-1))
 (414 138 (:REWRITE ADE::CAR-V-THREEFIX))
 (346 33 (:REWRITE ADE::DISJOINT-ATOM))
 (299 21 (:REWRITE LEN-OF-APPEND))
 (276 138 (:DEFINITION ADE::3V-FIX))
 (237 106 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (236 66 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (223 183 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (223 183 (:REWRITE ADE::F-BUF-OF-3VP))
 (223 106 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (223 106 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (210 75 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (209 33 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (200 33 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (191 191 (:TYPE-PRESCRIPTION PAIRLIS$))
 (178 178 (:TYPE-PRESCRIPTION ADE::3VP))
 (153 125 (:REWRITE ADE::V-THREEFIX-BVP))
 (150 11 (:DEFINITION ATOM))
 (126 126 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (119 119 (:DEFINITION STRIP-CARS))
 (119 1 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-WHEN-DISJOINT))
 (115 7 (:REWRITE ADE::MERGE$ACT0-INACTIVE))
 (109 56 (:REWRITE TAKE-WHEN-ATOM))
 (106 106 (:REWRITE |(equal (- x) (- y))|))
 (88 9 (:REWRITE |(equal (if a b c) x)|))
 (85 5 (:REWRITE ADE::MERGE$ACT-INACTIVE))
 (84 9 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (79 5 (:REWRITE ADE::MERGE$ACT1-INACTIVE))
 (76 1 (:REWRITE ADE::LEN-NTHCDR))
 (74 74 (:TYPE-PRESCRIPTION ADE::BVP))
 (70 6 (:REWRITE |(+ y (+ x z))|))
 (66 66 (:TYPE-PRESCRIPTION ADE::F-OR))
 (62 40 (:REWRITE DEFAULT-<-2))
 (60 20 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (59 4 (:DEFINITION POSP))
 (58 7 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (54 54 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (52 13 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (50 50 (:LINEAR LEN-WHEN-PREFIXP))
 (50 5 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (49 44 (:REWRITE DEFAULT-*-2))
 (47 40 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (44 44 (:TYPE-PRESCRIPTION BOOLEANP))
 (44 44 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (44 44 (:REWRITE DEFAULT-*-1))
 (44 40 (:REWRITE SIMPLIFY-SUMS-<))
 (42 6 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (41 41 (:REWRITE |(< (- x) (- y))|))
 (40 40 (:REWRITE DEFAULT-<-1))
 (37 4 (:REWRITE CONSP-OF-APPEND))
 (35 5 (:DEFINITION NATP))
 (33 5 (:REWRITE ADE::GCD-BODY1$VALUE))
 (31 31 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (31 31 (:REWRITE |(< 0 (- x))|))
 (30 6 (:REWRITE CAR-OF-APPEND))
 (25 25 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (25 5 (:REWRITE |(+ x x)|))
 (23 23 (:REWRITE REDUCE-INTEGERP-+))
 (23 23 (:REWRITE INTEGERP-MINUS-X))
 (23 23 (:META META-INTEGERP-CORRECT))
 (23 19 (:REWRITE DEFAULT-UNARY-MINUS))
 (22 4 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (22 2 (:REWRITE ADE::STRIP-CARS-PAIRLIS$))
 (21 1 (:DEFINITION SUBSETP-EQUAL))
 (18 8 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (18 3 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM-NAMES))
 (15 1 (:REWRITE |(equal (* x y) 0)|))
 (13 7 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (13 2 (:REWRITE |(+ (+ x y) z)|))
 (11 5 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA0-OUT-2))
 (10 2 (:REWRITE |(< x (if a b c))|))
 (10 1 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (9 9 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (9 9 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (9 9 (:REWRITE |(equal (- x) 0)|))
 (9 9 (:REWRITE |(< (- x) 0)|))
 (7 1 (:REWRITE ADE::MEMBER-APPEND))
 (6 6 (:REWRITE |(< d (+ c x))|))
 (5 5 (:TYPE-PRESCRIPTION NATP))
 (5 5 (:REWRITE DEFAULT-SYMBOL-NAME))
 (4 2 (:REWRITE |(- (if a b c))|))
 (4 1 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (4 1 (:DEFINITION MEMBER-EQUAL))
 (2 2 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 )
(ADE::COMP-GCD$STEP
 (18 18 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT1))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$IN-ACT))
 )
(ADE::COMP-GCD$STATE
 (7031 1125 (:DEFINITION BINARY-APPEND))
 (2571 1367 (:REWRITE DEFAULT-+-2))
 (1818 606 (:REWRITE ADE::CAR-V-THREEFIX))
 (1367 1367 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1367 1367 (:REWRITE DEFAULT-+-1))
 (1212 606 (:DEFINITION ADE::3V-FIX))
 (925 879 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (925 879 (:REWRITE ADE::F-BUF-OF-3VP))
 (860 64 (:REWRITE ADE::DISJOINT-ATOM))
 (652 652 (:TYPE-PRESCRIPTION ADE::3VP))
 (608 40 (:REWRITE LEN-OF-APPEND))
 (602 572 (:REWRITE ADE::V-THREEFIX-BVP))
 (597 597 (:DEFINITION STRIP-CARS))
 (513 207 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (498 498 (:TYPE-PRESCRIPTION PAIRLIS$))
 (452 118 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (422 64 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (404 64 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (390 26 (:DEFINITION ATOM))
 (352 173 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (350 243 (:REWRITE TAKE-WHEN-ATOM))
 (350 50 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (326 173 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (326 173 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (301 26 (:REWRITE CONSP-OF-APPEND))
 (293 29 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM-NAMES))
 (262 12 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-WHEN-DISJOINT))
 (250 50 (:REWRITE CAR-OF-APPEND))
 (202 202 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$DATA0-OUT))
 (184 24 (:REWRITE ADE::ASSOC-EQ-VALUES-ARGS-PAIRLIS$-ARGS))
 (176 176 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (173 173 (:REWRITE |(equal (- x) (- y))|))
 (167 122 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT1))
 (165 49 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (140 12 (:REWRITE |(+ y (+ x z))|))
 (124 69 (:REWRITE DEFAULT-<-2))
 (124 39 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (119 20 (:REWRITE ADE::MERGE$ACT1-INACTIVE))
 (116 41 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (113 113 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT))
 (113 113 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$IN-ACT))
 (110 100 (:REWRITE DEFAULT-*-2))
 (106 19 (:REWRITE ADE::MERGE$ACT0-INACTIVE))
 (104 4 (:REWRITE LEN-WHEN-PREFIXP))
 (100 100 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (100 100 (:REWRITE DEFAULT-*-1))
 (98 2 (:DEFINITION SUBSETP-EQUAL))
 (95 9 (:REWRITE |(equal (if a b c) x)|))
 (94 89 (:REWRITE DEFAULT-UNARY-MINUS))
 (90 6 (:DEFINITION POSP))
 (88 88 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
 (87 87 (:TYPE-PRESCRIPTION ADE::F-OR))
 (86 69 (:REWRITE SIMPLIFY-SUMS-<))
 (86 69 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (85 85 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (84 28 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (78 10 (:REWRITE ADE::MERGE$ACT-INACTIVE))
 (77 17 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (76 1 (:REWRITE ADE::LEN-NTHCDR))
 (73 69 (:REWRITE DEFAULT-<-1))
 (72 72 (:REWRITE |(< (- x) (- y))|))
 (66 66 (:TYPE-PRESCRIPTION BOOLEANP))
 (60 2 (:REWRITE ADE::MEMBER-APPEND))
 (58 58 (:LINEAR LEN-WHEN-PREFIXP))
 (58 28 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (57 57 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (57 57 (:REWRITE |(< 0 (- x))|))
 (56 8 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (52 13 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (50 10 (:REWRITE |(+ x x)|))
 (50 4 (:DEFINITION MEMBER-EQUAL))
 (49 39 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (44 4 (:REWRITE ADE::STRIP-CARS-PAIRLIS$))
 (38 5 (:REWRITE ADE::GCD-BODY1$ACT-INACTIVE))
 (30 3 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (30 2 (:REWRITE |(equal (* x y) 0)|))
 (29 29 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (28 4 (:DEFINITION NATP))
 (22 22 (:REWRITE REDUCE-INTEGERP-+))
 (22 22 (:REWRITE INTEGERP-MINUS-X))
 (22 22 (:META META-INTEGERP-CORRECT))
 (20 20 (:TYPE-PRESCRIPTION PREFIXP))
 (20 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (20 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (16 16 (:REWRITE |(equal (- x) 0)|))
 (13 2 (:REWRITE |(+ (+ x y) z)|))
 (12 4 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA0-OUT-2))
 (10 2 (:REWRITE |(< x (if a b c))|))
 (9 3 (:REWRITE ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT1))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (8 8 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (8 8 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (8 8 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (8 8 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (8 8 (:REWRITE |(< (- x) 0)|))
 (6 6 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (6 6 (:REWRITE DEFAULT-UNARY-/))
 (5 3 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA1-OUT-2))
 (4 4 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (4 4 (:REWRITE ADE::NO-DUPLICATESP-SIS))
 (4 2 (:REWRITE |(- (if a b c))|))
 (3 3 (:REWRITE DEFAULT-SYMBOL-NAME))
 )
(ADE::COMP-GCD$INPUT-FORMAT)
(ADE::COMP-GCD$INPUT-FORMAT=>BR$INPUT-FORMAT
 (5200 128 (:REWRITE TAKE-OF-TOO-MANY))
 (1728 32 (:DEFINITION TAKE))
 (1472 50 (:REWRITE ADE::LEN-NTHCDR))
 (1040 112 (:REWRITE TAKE-WHEN-ATOM))
 (767 481 (:REWRITE DEFAULT-+-2))
 (686 216 (:REWRITE SIMPLIFY-SUMS-<))
 (684 492 (:REWRITE DEFAULT-CDR))
 (495 65 (:DEFINITION NTHCDR))
 (492 492 (:REWRITE NTH-WHEN-PREFIXP))
 (481 481 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (481 481 (:REWRITE DEFAULT-+-1))
 (444 50 (:DEFINITION BINARY-APPEND))
 (441 177 (:REWRITE DEFAULT-CAR))
 (363 33 (:REWRITE |(+ (+ x y) z)|))
 (350 216 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (280 200 (:REWRITE DEFAULT-<-2))
 (268 268 (:LINEAR LEN-WHEN-PREFIXP))
 (254 200 (:REWRITE DEFAULT-<-1))
 (252 252 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (252 252 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (232 232 (:REWRITE |(< (- x) (- y))|))
 (194 66 (:REWRITE |(< d (+ c x))|))
 (192 32 (:REWRITE CONSP-OF-APPEND))
 (168 24 (:REWRITE ADE::CAR-V-THREEFIX))
 (160 16 (:DEFINITION ADE::V-THREEFIX))
 (152 38 (:DEFINITION STRIP-CARS))
 (134 134 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (128 128 (:TYPE-PRESCRIPTION NFIX))
 (120 120 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (120 120 (:REWRITE DEFAULT-*-2))
 (120 120 (:REWRITE DEFAULT-*-1))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (112 48 (:REWRITE ADE::F-GATES=B-GATES))
 (99 88 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (99 88 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (99 88 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (96 16 (:REWRITE |(+ y (+ x z))|))
 (88 88 (:REWRITE |(equal (- x) (- y))|))
 (80 40 (:DEFINITION ADE::3V-FIX))
 (72 72 (:TYPE-PRESCRIPTION ADE::3VP))
 (64 64 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (64 64 (:REWRITE |(< 0 (- x))|))
 (64 64 (:REWRITE |(* (- x) y)|))
 (48 48 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (48 48 (:REWRITE |(equal (- x) 0)|))
 (48 16 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (48 16 (:REWRITE ADE::F-BUF-OF-3VP))
 (44 10 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (33 5 (:DEFINITION TRUE-LISTP))
 (32 32 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (32 32 (:REWRITE DEFAULT-UNARY-/))
 (32 32 (:REWRITE CONSP-OF-TAKE))
 (32 32 (:REWRITE |(equal (* x y) 0)|))
 (32 32 (:REWRITE |(< 0 (* x y))|))
 (32 32 (:REWRITE |(* c (* d x))|))
 (16 16 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (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$IN-ACT
 (1904 32 (:REWRITE TAKE-OF-TOO-MANY))
 (1024 34 (:REWRITE ADE::LEN-NTHCDR))
 (532 532 (:REWRITE NTH-WHEN-PREFIXP))
 (492 66 (:DEFINITION BINARY-APPEND))
 (465 225 (:REWRITE DEFAULT-CAR))
 (415 37 (:DEFINITION NTHCDR))
 (330 132 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (272 248 (:REWRITE DEFAULT-CDR))
 (251 165 (:REWRITE DEFAULT-+-2))
 (231 21 (:REWRITE |(+ (+ x y) z)|))
 (224 32 (:REWRITE TAKE-WHEN-ATOM))
 (165 165 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (165 165 (:REWRITE DEFAULT-+-1))
 (162 162 (:TYPE-PRESCRIPTION STRIP-CARS))
 (160 16 (:DEFINITION ADE::V-THREEFIX))
 (152 38 (:DEFINITION STRIP-CARS))
 (150 80 (:REWRITE SIMPLIFY-SUMS-<))
 (150 80 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (150 80 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (140 140 (:LINEAR LEN-WHEN-PREFIXP))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (118 80 (:REWRITE DEFAULT-<-1))
 (112 80 (:REWRITE DEFAULT-<-2))
 (112 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (96 96 (:TYPE-PRESCRIPTION ADE::3VP))
 (96 32 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (96 32 (:REWRITE ADE::F-BUF-OF-3VP))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (86 26 (:REWRITE |(< d (+ c x))|))
 (84 84 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (84 84 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (84 84 (:REWRITE DEFAULT-*-2))
 (84 84 (:REWRITE DEFAULT-*-1))
 (82 82 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (80 80 (:REWRITE |(< (- x) (- y))|))
 (80 4 (:REWRITE ZP-OPEN))
 (70 70 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (68 4 (:DEFINITION POSP))
 (64 64 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (64 32 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (64 32 (:DEFINITION ADE::3V-FIX))
 (51 40 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (51 40 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (51 40 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (48 8 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (44 10 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (40 40 (:REWRITE |(equal (- x) (- y))|))
 (33 5 (:DEFINITION TRUE-LISTP))
 (32 32 (:TYPE-PRESCRIPTION NFIX))
 (18 18 (:META META-INTEGERP-CORRECT))
 (16 8 (:REWRITE ADE::BOOLEANP-OF-F-BUF))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (10 10 (:REWRITE REDUCE-INTEGERP-+))
 (10 10 (:REWRITE INTEGERP-MINUS-X))
 (8 8 (:REWRITE |(integerp (* c x))|))
 (8 8 (:REWRITE |(* (- x) y)|))
 (8 4 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (6 2 (:REWRITE ADE::BVP-NTHCDR))
 (4 4 (:TYPE-PRESCRIPTION POSP))
 (4 4 (:REWRITE CDR-CONS))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::BOOLEANP-COMP-GCD$OUT-ACT
 (2191 313 (:DEFINITION LEN))
 (1418 1418 (:REWRITE NTH-WHEN-PREFIXP))
 (682 385 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (682 385 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (682 385 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (626 313 (:REWRITE DEFAULT-+-2))
 (552 184 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (510 510 (:REWRITE DEFAULT-CDR))
 (460 92 (:DEFINITION TRUE-LISTP))
 (420 105 (:DEFINITION STRIP-CARS))
 (385 385 (:REWRITE |(equal (- x) (- y))|))
 (313 313 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (313 313 (:REWRITE NORMALIZE-ADDENDS))
 (313 313 (:REWRITE DEFAULT-+-1))
 (256 256 (:REWRITE DEFAULT-CAR))
 (235 235 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (235 235 (:REWRITE DEFAULT-*-2))
 (235 235 (:REWRITE DEFAULT-*-1))
 (96 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (96 16 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 )
(ADE::COMP-GCD$ST-FORMAT-PRESERVED
 (166 2 (:DEFINITION TAKE))
 (95 95 (:REWRITE NTH-WHEN-PREFIXP))
 (72 8 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (72 2 (:REWRITE ADE::LEN-GCD-BODY1$DATA-OUT))
 (68 14 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (52 4 (:REWRITE |(< x (if a b c))|))
 (34 28 (:REWRITE DEFAULT-CAR))
 (32 8 (:DEFINITION STRIP-CARS))
 (28 28 (:TYPE-PRESCRIPTION ADE::GCD-BODY1$DATA-OUT))
 (28 2 (:DEFINITION NFIX))
 (28 2 (:DEFINITION NATP))
 (27 21 (:REWRITE DEFAULT-CDR))
 (26 2 (:REWRITE ZP-OPEN))
 (24 2 (:REWRITE ADE::MERGE$ACT-INACTIVE))
 (22 12 (:REWRITE DEFAULT-+-2))
 (21 1 (:REWRITE ADE::F-GATES=B-GATES))
 (20 20 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (20 20 (:REWRITE DEFAULT-*-2))
 (20 20 (:REWRITE DEFAULT-*-1))
 (20 2 (:REWRITE ADE::GCD-BODY1$ACT-INACTIVE))
 (18 18 (:TYPE-PRESCRIPTION BOOLEANP))
 (18 18 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (18 18 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (18 14 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (18 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT1))
 (16 4 (:REWRITE TAKE-WHEN-ATOM))
 (15 15 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$INPUT-FORMAT))
 (15 3 (:DEFINITION PAIRLIS$))
 (14 14 (:REWRITE |(< (- x) (- y))|))
 (14 12 (:REWRITE SIMPLIFY-SUMS-<))
 (14 12 (:REWRITE DEFAULT-<-2))
 (14 11 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (14 11 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (14 11 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (12 12 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (12 12 (:REWRITE DEFAULT-<-1))
 (12 12 (:REWRITE DEFAULT-+-1))
 (12 2 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (12 2 (:REWRITE ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT1))
 (11 11 (:REWRITE |(equal (- x) (- y))|))
 (10 4 (:REWRITE |(* x (if a b c))|))
 (10 1 (:REWRITE ADE::MERGE$ACT1-INACTIVE))
 (9 9 (:TYPE-PRESCRIPTION ADE::COMP-GCD$BR-INPUTS))
 (9 3 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT))
 (9 3 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT=>BR$INPUT-FORMAT))
 (8 8 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$VALID-ST))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (8 8 (:REWRITE |(< (- x) 0)|))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (7 3 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA1-OUT-2))
 (6 6 (:TYPE-PRESCRIPTION ADE::MERGE$ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::GCD-BODY1$ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT1))
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT))
 (6 2 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (6 1 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (6 1 (:REWRITE ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT))
 (4 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:REWRITE |(< (* x y) 0)|))
 (4 4 (:META META-INTEGERP-CORRECT))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 2 (:REWRITE |(< d (+ c x))|))
 (4 2 (:REWRITE |(+ c (+ d x))|))
 (3 3 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (2 2 (:REWRITE |(< 0 (- x))|))
 (2 2 (:REWRITE |(< 0 (* x y))|))
 (2 2 (:REWRITE |(< (+ c x) d)|))
 (2 2 (:REWRITE |(+ 0 x)|))
 (2 2 (:REWRITE |(* (- x) y)|))
 (2 1 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 )
(ADE::COMP-GCD$VALUE-ALT
 (442 34 (:DEFINITION NTHCDR))
 (374 34 (:REWRITE |(+ (+ x y) z)|))
 (252 9 (:REWRITE ADE::LEN-NTHCDR))
 (170 34 (:REWRITE |(+ y x)|))
 (162 23 (:DEFINITION BINARY-APPEND))
 (146 128 (:REWRITE DEFAULT-+-2))
 (128 128 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (128 128 (:REWRITE DEFAULT-+-1))
 (126 18 (:DEFINITION LEN))
 (117 18 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (94 46 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (84 84 (:REWRITE DEFAULT-CDR))
 (81 9 (:DEFINITION TRUE-LISTP))
 (67 67 (:REWRITE NTH-WHEN-PREFIXP))
 (50 50 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (50 50 (:REWRITE DEFAULT-*-2))
 (50 50 (:REWRITE DEFAULT-*-1))
 (48 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (45 11 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (39 23 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (39 23 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (39 23 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (36 18 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (32 32 (:LINEAR LEN-WHEN-PREFIXP))
 (27 9 (:REWRITE ADE::BVP-NTHCDR))
 (23 23 (:REWRITE DEFAULT-CAR))
 (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$STATE-ALT
 (403 31 (:DEFINITION NTHCDR))
 (341 31 (:REWRITE |(+ (+ x y) z)|))
 (252 9 (:REWRITE ADE::LEN-NTHCDR))
 (155 31 (:REWRITE |(+ y x)|))
 (144 20 (:DEFINITION BINARY-APPEND))
 (137 119 (:REWRITE DEFAULT-+-2))
 (126 18 (:DEFINITION LEN))
 (119 119 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (119 119 (:REWRITE DEFAULT-+-1))
 (117 18 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (88 40 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (81 9 (:DEFINITION TRUE-LISTP))
 (78 78 (:REWRITE DEFAULT-CDR))
 (48 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (47 47 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (47 47 (:REWRITE DEFAULT-*-2))
 (47 47 (: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))
 (35 35 (:REWRITE NTH-WHEN-PREFIXP))
 (32 32 (:LINEAR LEN-WHEN-PREFIXP))
 (27 9 (:REWRITE ADE::BVP-NTHCDR))
 (23 23 (:REWRITE |(equal (- x) (- y))|))
 (20 20 (: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$RUN)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-COMP-GCD$RUN-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-COMP-GCD$RUN)
(ADE::COMP-GCD$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$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$INPUT-FORMAT-N-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-COMP-GCD$INPUT-FORMAT-N)
(ADE::COMP-GCD$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$DE-N
 (265 30 (:REWRITE ZP-OPEN))
 (108 12 (:REWRITE |(< d (+ c x))|))
 (62 2 (:DEFINITION ADE::COMP-GCD$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$INPUT-FORMAT-PLUS))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE ADE::DE-PLUS))
 )
(ADE::COMP-GCD$EXTRACT)
(ADE::COMP-GCD$EXTRACT-NOT-EMPTY
 (384 50 (:DEFINITION LEN))
 (190 190 (:REWRITE NTH-WHEN-PREFIXP))
 (141 107 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (141 107 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (141 107 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (107 107 (:REWRITE |(equal (- x) (- y))|))
 (102 51 (:REWRITE DEFAULT-+-2))
 (98 98 (:REWRITE DEFAULT-CDR))
 (88 22 (:DEFINITION STRIP-CARS))
 (68 68 (:LINEAR LEN-WHEN-PREFIXP))
 (63 63 (:REWRITE DEFAULT-CAR))
 (56 28 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD$OUT-ACT))
 (52 51 (:REWRITE DEFAULT-+-1))
 (51 51 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (51 51 (:REWRITE NORMALIZE-ADDENDS))
 (48 16 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (48 8 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (48 8 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (40 8 (:DEFINITION TRUE-LISTP))
 (36 36 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$EXTRACT))
 (34 34 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (24 24 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (24 24 (:REWRITE DEFAULT-*-2))
 (24 24 (:REWRITE DEFAULT-*-1))
 (16 16 (:LINEAR ADE::COMP-GCD-COND$EXTRACT-NOT-EMPTY-2))
 (14 2 (:DEFINITION BINARY-APPEND))
 (11 11 (:TYPE-PRESCRIPTION ADE::GCD$OP-MAP))
 (8 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (8 2 (:DEFINITION ADE::GCD$OP-MAP))
 (7 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 (1 1 (:REWRITE |(equal (+ c x) d)|))
 )
(ADE::COMP-GCD$INV)
(ADE::COMP-GCD$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 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 NTH-WHEN-PREFIXP))
 (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$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 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$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 NTH-WHEN-PREFIXP))
 (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$INPUT-FORMAT-LEMMA-1))
 )
(ADE::COMP-GCD$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 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$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 NTH-WHEN-PREFIXP))
 (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$INPUT-FORMAT-LEMMA-2))
 (1 1 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-LEMMA-1))
 )
(ADE::COMP-GCD-COND$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))
 (33 33 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (30 2 (:DEFINITION NTHCDR))
 (29 3 (:DEFINITION LEN))
 (26 8 (:REWRITE DEFAULT-CAR))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 9 (:REWRITE DEFAULT-CDR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE ADE::F-GATES=B-GATES))
 (12 12 (:REWRITE NTH-WHEN-PREFIXP))
 (12 9 (:REWRITE DEFAULT-+-2))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 1 (:DEFINITION BINARY-APPEND))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (10 2 (:REWRITE |(+ y x)|))
 (10 1 (:DEFINITION ADE::V-THREEFIX))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE NORMALIZE-ADDENDS))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 7 (:REWRITE DEFAULT-<-2))
 (8 1 (:DEFINITION STRIP-CARS))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (7 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (7 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (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))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 (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 NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE
 (136 2 (:REWRITE TAKE-OF-TOO-MANY))
 (76 67 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-1))
 (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))
 (30 2 (:DEFINITION NTHCDR))
 (29 3 (:DEFINITION LEN))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (25 7 (:REWRITE DEFAULT-CAR))
 (22 3 (:REWRITE ADE::F-GATES=B-GATES))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 9 (:REWRITE DEFAULT-CDR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (13 13 (:REWRITE NTH-WHEN-PREFIXP))
 (12 9 (:REWRITE DEFAULT-+-2))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 1 (:DEFINITION BINARY-APPEND))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (10 2 (:REWRITE |(+ y x)|))
 (10 1 (:DEFINITION ADE::V-THREEFIX))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE NORMALIZE-ADDENDS))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 7 (:REWRITE DEFAULT-<-2))
 (9 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (8 1 (:DEFINITION STRIP-CARS))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (7 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (7 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (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))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (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 NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE
 (272 4 (:REWRITE TAKE-OF-TOO-MANY))
 (144 2 (:REWRITE ADE::LEN-NTHCDR))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (110 92 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-1))
 (108 2 (:DEFINITION TAKE))
 (86 86 (:TYPE-PRESCRIPTION LEN))
 (64 32 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (60 4 (:DEFINITION NTHCDR))
 (58 6 (:DEFINITION LEN))
 (54 15 (:REWRITE DEFAULT-CAR))
 (52 8 (:REWRITE |(+ (if a b c) x)|))
 (47 6 (:REWRITE ADE::F-GATES=B-GATES))
 (44 4 (:REWRITE |(+ (+ x y) z)|))
 (32 32 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (32 32 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (30 18 (:REWRITE DEFAULT-CDR))
 (28 28 (:REWRITE NTH-WHEN-PREFIXP))
 (28 4 (:REWRITE TAKE-WHEN-ATOM))
 (28 2 (:DEFINITION NATP))
 (24 18 (:REWRITE DEFAULT-+-2))
 (24 14 (:REWRITE SIMPLIFY-SUMS-<))
 (24 14 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (24 14 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (24 2 (:DEFINITION BINARY-APPEND))
 (20 20 (:LINEAR LEN-WHEN-PREFIXP))
 (20 14 (:REWRITE DEFAULT-<-1))
 (20 4 (:REWRITE |(+ y x)|))
 (20 2 (:DEFINITION ADE::V-THREEFIX))
 (18 18 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (18 18 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (18 18 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (18 18 (:REWRITE NORMALIZE-ADDENDS))
 (18 18 (:REWRITE DEFAULT-+-1))
 (18 14 (:REWRITE DEFAULT-<-2))
 (18 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (16 16 (:TYPE-PRESCRIPTION BOOLEANP))
 (16 2 (:DEFINITION STRIP-CARS))
 (14 14 (:REWRITE |(< (- x) (- y))|))
 (14 2 (:REWRITE ADE::CAR-V-THREEFIX))
 (12 4 (:REWRITE ADE::V-THREEFIX-BVP))
 (11 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (11 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (11 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (10 10 (:TYPE-PRESCRIPTION STRIP-CARS))
 (10 10 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 8 (:TYPE-PRESCRIPTION ADE::3VP))
 (8 4 (:DEFINITION ADE::3V-FIX))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (6 2 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$VALID-ST))
 (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 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE |(< d (+ c x))|))
 )
(ADE::COMP-GCD-COND$FLAG-INACTIVE
 (6776 152 (:REWRITE TAKE-OF-TOO-MANY))
 (2112 1040 (:REWRITE DEFAULT-CDR))
 (1920 48 (:REWRITE ADE::LEN-NTHCDR))
 (1728 612 (:REWRITE DEFAULT-CAR))
 (1728 32 (:DEFINITION TAKE))
 (1540 948 (:REWRITE DEFAULT-+-2))
 (1368 64 (:REWRITE LEN-OF-APPEND))
 (1327 1327 (:REWRITE NTH-WHEN-PREFIXP))
 (1056 152 (:REWRITE TAKE-WHEN-ATOM))
 (1028 108 (:DEFINITION BINARY-APPEND))
 (972 148 (:DEFINITION STRIP-CARS))
 (948 948 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (948 948 (:REWRITE DEFAULT-+-1))
 (888 308 (:REWRITE SIMPLIFY-SUMS-<))
 (832 64 (:REWRITE ADE::LEN-V-THREEFIX))
 (652 52 (:DEFINITION ADE::V-THREEFIX))
 (540 20 (:REWRITE |(< (+ d x) (+ c y))|))
 (492 492 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (480 308 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (468 216 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (438 176 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (438 176 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (438 176 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (432 432 (:LINEAR LEN-WHEN-PREFIXP))
 (420 20 (:REWRITE ZP-OPEN))
 (408 284 (:REWRITE DEFAULT-<-2))
 (400 68 (:REWRITE CONSP-OF-APPEND))
 (396 396 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (388 388 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (356 356 (:REWRITE |(< (- x) (- y))|))
 (352 48 (:REWRITE ADE::CAR-V-THREEFIX))
 (340 20 (:REWRITE |(< 0 (* x y))|))
 (332 284 (:REWRITE DEFAULT-<-1))
 (320 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (264 36 (:REWRITE |(+ y (+ x z))|))
 (224 56 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (216 216 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (200 100 (:DEFINITION ADE::3V-FIX))
 (180 20 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (176 176 (:REWRITE |(equal (- x) (- y))|))
 (176 56 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (140 140 (:TYPE-PRESCRIPTION ADE::3VP))
 (132 132 (:TYPE-PRESCRIPTION NFIX))
 (128 128 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (128 128 (:REWRITE DEFAULT-*-2))
 (128 128 (:REWRITE DEFAULT-*-1))
 (124 4 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (120 24 (:REWRITE |(- (* c x))|))
 (96 96 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (96 96 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (96 96 (:REWRITE DEFAULT-UNARY-MINUS))
 (96 96 (:REWRITE DEFAULT-UNARY-/))
 (96 96 (:REWRITE |(< 0 (- x))|))
 (80 20 (:REWRITE |(+ x x)|))
 (72 72 (:REWRITE |(< d (+ c x))|))
 (68 68 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (68 68 (:REWRITE |(equal (- x) 0)|))
 (64 44 (:REWRITE |(< (+ c x) d)|))
 (64 8 (:REWRITE CAR-OF-APPEND))
 (60 60 (:REWRITE CONSP-OF-TAKE))
 (60 20 (:REWRITE ADE::F-BUF-OF-3VP))
 (48 24 (:REWRITE |(+ (* c x) (* d x))|))
 (36 36 (:REWRITE CDR-CONS))
 (28 28 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (24 24 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (24 24 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (24 24 (:REWRITE |(* 0 x)|))
 (24 24 (:REWRITE |(* (- x) y)|))
 (20 20 (:REWRITE LEN-OF-TAKE))
 (20 20 (:REWRITE |(* c (* d x))|))
 (12 4 (:REWRITE ADE::BVP-APPEND))
 )
(ADE::COMP-GCD-COND$FLAG-ACTIVE
 (6420 144 (:REWRITE TAKE-OF-TOO-MANY))
 (2217 2081 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (2004 1060 (:REWRITE DEFAULT-CDR))
 (1820 44 (:REWRITE ADE::LEN-NTHCDR))
 (1696 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-MUTUALLY-EXCLUSIVE))
 (1636 628 (:REWRITE DEFAULT-CAR))
 (1580 960 (:REWRITE DEFAULT-+-2))
 (1512 28 (:DEFINITION TAKE))
 (1368 64 (:REWRITE LEN-OF-APPEND))
 (1343 1343 (:REWRITE NTH-WHEN-PREFIXP))
 (1084 164 (:DEFINITION STRIP-CARS))
 (1000 144 (:REWRITE TAKE-WHEN-ATOM))
 (976 104 (:DEFINITION BINARY-APPEND))
 (960 960 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (960 960 (:REWRITE DEFAULT-+-1))
 (864 296 (:REWRITE SIMPLIFY-SUMS-<))
 (832 64 (:REWRITE ADE::LEN-V-THREEFIX))
 (612 48 (:DEFINITION ADE::V-THREEFIX))
 (540 20 (:REWRITE |(< (+ d x) (+ c y))|))
 (456 296 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (448 208 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (428 428 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (420 20 (:REWRITE ZP-OPEN))
 (388 272 (:REWRITE DEFAULT-<-2))
 (384 384 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (384 384 (:LINEAR LEN-WHEN-PREFIXP))
 (376 376 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (376 64 (:REWRITE CONSP-OF-APPEND))
 (344 344 (:REWRITE |(< (- x) (- y))|))
 (340 20 (:REWRITE |(< 0 (* x y))|))
 (334 152 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (334 152 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (334 152 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (324 44 (:REWRITE ADE::CAR-V-THREEFIX))
 (316 272 (:REWRITE DEFAULT-<-1))
 (272 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (264 36 (:REWRITE |(+ y (+ x z))|))
 (208 52 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (192 192 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (192 32 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (184 92 (:DEFINITION ADE::3V-FIX))
 (180 20 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (156 48 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (152 152 (:REWRITE |(equal (- x) (- y))|))
 (132 132 (:TYPE-PRESCRIPTION ADE::3VP))
 (124 124 (:TYPE-PRESCRIPTION NFIX))
 (120 120 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (120 120 (:REWRITE DEFAULT-*-2))
 (120 120 (:REWRITE DEFAULT-*-1))
 (120 24 (:REWRITE |(- (* c x))|))
 (104 4 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (96 96 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (96 96 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (96 96 (:REWRITE DEFAULT-UNARY-MINUS))
 (96 96 (:REWRITE DEFAULT-UNARY-/))
 (96 96 (:REWRITE |(< 0 (- x))|))
 (80 20 (:REWRITE |(+ x x)|))
 (68 68 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (68 68 (:REWRITE |(equal (- x) 0)|))
 (68 68 (:REWRITE |(< d (+ c x))|))
 (64 44 (:REWRITE |(< (+ c x) d)|))
 (64 8 (:REWRITE CAR-OF-APPEND))
 (60 20 (:REWRITE ADE::F-BUF-OF-3VP))
 (52 52 (:REWRITE CONSP-OF-TAKE))
 (48 24 (:REWRITE |(+ (* c x) (* d x))|))
 (36 36 (:REWRITE CDR-CONS))
 (32 32 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$OUT-ACT0))
 (24 24 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (24 24 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (24 24 (:REWRITE |(* 0 x)|))
 (24 24 (:REWRITE |(* (- x) y)|))
 (20 20 (:REWRITE LEN-OF-TAKE))
 (20 20 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (20 20 (:REWRITE |(* c (* d x))|))
 (12 4 (:REWRITE ADE::BVP-APPEND))
 )
(ADE::BOOLEANP-COMP-GCD$BODY-ACT
 (179 10 (:DEFINITION NTHCDR))
 (161 2 (:DEFINITION TAKE))
 (148 148 (:REWRITE NTH-WHEN-PREFIXP))
 (132 17 (:DEFINITION BINARY-APPEND))
 (131 3 (:DEFINITION NATP))
 (128 53 (:REWRITE DEFAULT-CAR))
 (112 73 (:REWRITE DEFAULT-+-2))
 (107 74 (:REWRITE DEFAULT-CDR))
 (101 5 (:REWRITE LEN-OF-APPEND))
 (82 17 (:REWRITE |(< d (+ c x))|))
 (81 5 (:DEFINITION ADE::V-THREEFIX))
 (81 1 (:REWRITE REPEAT-WHEN-ZP))
 (73 73 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (73 73 (:REWRITE DEFAULT-+-1))
 (69 36 (:REWRITE SIMPLIFY-SUMS-<))
 (67 1 (:REWRITE ADE::GCD-BODY1$ACT-INACTIVE))
 (63 63 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (59 20 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (59 20 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (59 20 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (57 1 (:REWRITE |(< x (if a b c))|))
 (54 9 (:DEFINITION STRIP-CARS))
 (53 53 (:REWRITE |(< (- x) (- y))|))
 (53 5 (:REWRITE |(< 0 (* x y))|))
 (52 52 (:LINEAR LEN-WHEN-PREFIXP))
 (51 35 (:REWRITE DEFAULT-<-2))
 (39 2 (:REWRITE ADE::MERGE$ACT1-INACTIVE))
 (38 38 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (38 38 (:REWRITE DEFAULT-*-2))
 (38 38 (:REWRITE DEFAULT-*-1))
 (38 11 (:REWRITE TAKE-WHEN-ATOM))
 (37 35 (:REWRITE DEFAULT-<-1))
 (36 6 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (35 5 (:REWRITE ADE::CAR-V-THREEFIX))
 (35 2 (:REWRITE ADE::MERGE$ACT0-INACTIVE))
 (30 15 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (29 3 (:REWRITE CONSP-OF-TAKE))
 (26 26 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (24 4 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (24 2 (:DEFINITION POSP))
 (22 22 (:TYPE-PRESCRIPTION ADE::3VP))
 (20 20 (:REWRITE |(equal (- x) (- y))|))
 (20 20 (:META META-INTEGERP-CORRECT))
 (20 10 (:DEFINITION ADE::3V-FIX))
 (18 6 (:REWRITE ADE::F-BUF-OF-3VP))
 (17 13 (:REWRITE |(< (+ c x) d)|))
 (16 16 (:REWRITE REDUCE-INTEGERP-+))
 (16 16 (:REWRITE INTEGERP-MINUS-X))
 (15 2 (:REWRITE REV-WHEN-NOT-CONSP))
 (12 12 (:REWRITE |(< 0 (- x))|))
 (11 11 (:REWRITE |(< (- x) 0)|))
 (10 10 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (9 9 (:TYPE-PRESCRIPTION ADE::GCD-BODY1$ME-INPUTS))
 (9 9 (:REWRITE CDR-CONS))
 (8 8 (:REWRITE |(* (- x) y)|))
 (7 1 (:REWRITE CAR-OF-TAKE))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (6 6 (:REWRITE |(integerp (* c x))|))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (5 5 (:REWRITE |(equal (- x) 0)|))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (4 4 (:REWRITE DEFAULT-UNARY-/))
 (4 4 (:REWRITE |(< (+ c x y) d)|))
 (4 1 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 1 (:REWRITE ADE::BVP-TAKE))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 (2 2 (:TYPE-PRESCRIPTION POSP))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 1 (:REWRITE DEFAULT-UNARY-MINUS))
 (1 1 (:REWRITE |(< d (+ c x y))|))
 )
(ADE::COMP-GCD$BODY-ACT-INACTIVE
 (36 12 (:REWRITE DEFAULT-CAR))
 (30 2 (:DEFINITION NTHCDR))
 (28 2 (:DEFINITION NATP))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (24 2 (:DEFINITION BINARY-APPEND))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (20 2 (:DEFINITION ADE::V-THREEFIX))
 (19 19 (:REWRITE NTH-WHEN-PREFIXP))
 (14 2 (:REWRITE ADE::CAR-V-THREEFIX))
 (13 3 (:REWRITE ADE::F-GATES=B-GATES))
 (13 3 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (12 6 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (12 4 (:REWRITE ADE::V-THREEFIX-BVP))
 (12 2 (:DEFINITION STRIP-CARS))
 (10 10 (:TYPE-PRESCRIPTION STRIP-CARS))
 (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (10 2 (:REWRITE |(+ y x)|))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (8 8 (:TYPE-PRESCRIPTION ADE::3VP))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (8 8 (:REWRITE NORMALIZE-ADDENDS))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE DEFAULT-+-1))
 (8 4 (:DEFINITION ADE::3V-FIX))
 (8 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (8 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (8 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (7 3 (:REWRITE ADE::F-BUF-OF-3VP))
 (6 6 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (6 3 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (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 REDUCE-INTEGERP-+))
 (4 4 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE |(< (- x) 0)|))
 (4 4 (:REWRITE |(< (- x) (- y))|))
 (4 4 (:META META-INTEGERP-CORRECT))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::BVP-COMP-GCD$BODY-DATA-OUT
 (265 6 (:REWRITE TAKE-OF-TOO-MANY))
 (153 5 (:REWRITE |(< (if a b c) x)|))
 (69 3 (:REWRITE ADE::NTHCDR-APPEND))
 (63 18 (:REWRITE SIMPLIFY-SUMS-<))
 (60 24 (:REWRITE DEFAULT-CAR))
 (57 3 (:REWRITE LEN-OF-APPEND))
 (54 54 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-1))
 (45 9 (:REWRITE |(+ y x)|))
 (43 43 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (38 24 (:REWRITE DEFAULT-+-2))
 (37 2 (:DEFINITION NATP))
 (36 6 (:REWRITE ADE::F-GATES=B-GATES))
 (36 6 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (36 6 (:REWRITE |(< (- x) 0)|))
 (36 6 (:DEFINITION STRIP-CARS))
 (31 31 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (31 31 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (31 31 (:REWRITE DEFAULT-CDR))
 (30 3 (:DEFINITION NTHCDR))
 (29 29 (:REWRITE NTH-WHEN-PREFIXP))
 (29 1 (:REWRITE TAKE-OF-CONS))
 (28 1 (:REWRITE ZP-OPEN))
 (25 10 (:REWRITE |(< 0 (- x))|))
 (24 24 (:TYPE-PRESCRIPTION BOOLEANP))
 (24 24 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (24 24 (:REWRITE DEFAULT-+-1))
 (23 23 (:REWRITE |(< (- x) (- y))|))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (21 1 (:REWRITE |(< x (if a b c))|))
 (20 4 (:REWRITE |(< d (+ c x))|))
 (19 18 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (19 3 (:REWRITE |(+ (if a b c) x)|))
 (18 9 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (18 6 (:REWRITE TAKE-WHEN-ATOM))
 (18 6 (:REWRITE ADE::F-BUF-OF-3VP))
 (18 3 (:DEFINITION BINARY-APPEND))
 (17 16 (:REWRITE DEFAULT-<-1))
 (16 16 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (16 16 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE DEFAULT-*-2))
 (16 16 (:REWRITE DEFAULT-*-1))
 (15 6 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (13 13 (:TYPE-PRESCRIPTION NFIX))
 (12 12 (:TYPE-PRESCRIPTION ADE::3VP))
 (12 2 (:REWRITE |(+ y (+ x z))|))
 (10 10 (:REWRITE REDUCE-INTEGERP-+))
 (10 10 (:REWRITE INTEGERP-MINUS-X))
 (10 10 (:META META-INTEGERP-CORRECT))
 (9 9 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (9 9 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (8 8 (:REWRITE |(< 0 (* x y))|))
 (8 5 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (8 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (8 5 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (6 6 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (6 6 (:REWRITE DEFAULT-UNARY-/))
 (6 6 (:REWRITE |(* c (* d x))|))
 (6 6 (:REWRITE |(* (- x) y)|))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (6 3 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (5 5 (:REWRITE CDR-CONS))
 (5 5 (:REWRITE |(equal (- x) (- y))|))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (3 3 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (3 3 (:REWRITE |(< (* x y) 0)|))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (2 2 (:REWRITE |(equal (- x) 0)|))
 (1 1 (:REWRITE |(+ 0 x)|))
 (1 1 (:DEFINITION TAKE))
 )
(ADE::COMP-GCD$INV-PRESERVED
 (4362 4362 (:REWRITE NTH-WHEN-PREFIXP))
 (4347 57 (:DEFINITION TAKE))
 (3074 458 (:DEFINITION STRIP-CARS))
 (2659 1731 (:REWRITE DEFAULT-CAR))
 (2529 2012 (:REWRITE DEFAULT-CDR))
 (1876 302 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (1849 270 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (1841 992 (:REWRITE DEFAULT-+-2))
 (1776 659 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1776 659 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1776 659 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1397 115 (:DEFINITION PAIRLIS$))
 (1184 37 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (1170 117 (:DEFINITION ADE::V-THREEFIX))
 (992 992 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (992 992 (:REWRITE DEFAULT-+-1))
 (948 108 (:DEFINITION TRUE-LISTP))
 (827 113 (:REWRITE ZP-OPEN))
 (798 94 (:DEFINITION NATP))
 (756 108 (:REWRITE ADE::CAR-V-THREEFIX))
 (727 43 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (659 659 (:REWRITE |(equal (- x) (- y))|))
 (648 216 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (555 480 (:REWRITE DEFAULT-*-2))
 (544 544 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$DATA-IN))
 (540 126 (:REWRITE TAKE-WHEN-ATOM))
 (503 63 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (480 480 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (480 480 (:REWRITE DEFAULT-*-1))
 (471 39 (:REWRITE |(+ (+ x y) z)|))
 (450 225 (:DEFINITION ADE::3V-FIX))
 (446 16 (:REWRITE ADE::GCD-BODY1$ACT-INACTIVE))
 (438 438 (:LINEAR LEN-WHEN-PREFIXP))
 (416 46 (:DEFINITION BINARY-APPEND))
 (376 71 (:REWRITE |(+ y x)|))
 (342 90 (:REWRITE |(< d (+ c x))|))
 (326 326 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (314 314 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (314 19 (:REWRITE ADE::LEN-GCD-BODY1$DATA-OUT))
 (310 213 (:REWRITE SIMPLIFY-SUMS-<))
 (307 213 (:REWRITE DEFAULT-<-2))
 (302 302 (:REWRITE |(< (- x) (- y))|))
 (297 9 (:REWRITE ADE::LEN-NTHCDR))
 (240 240 (:META META-INTEGERP-CORRECT))
 (225 225 (:TYPE-PRESCRIPTION ADE::3VP))
 (222 213 (:REWRITE DEFAULT-<-1))
 (219 219 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (208 208 (:REWRITE REDUCE-INTEGERP-+))
 (208 208 (:REWRITE INTEGERP-MINUS-X))
 (204 59 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (198 14 (:DEFINITION POSP))
 (192 32 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA-IN))
 (192 32 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (170 170 (:TYPE-PRESCRIPTION ADE::COMP-GCD$BODY-INPUTS))
 (162 12 (:REWRITE CONSP-OF-TAKE))
 (128 64 (:REWRITE |(* y x)|))
 (126 61 (:TYPE-PRESCRIPTION ADE::F-IF))
 (126 52 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (97 97 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$FLAG))
 (96 32 (:REWRITE |(* y (* x z))|))
 (94 94 (:TYPE-PRESCRIPTION NATP))
 (92 4 (:REWRITE ADE::MERGE$ACT0-INACTIVE))
 (90 6 (:REWRITE CAR-OF-TAKE))
 (89 89 (:REWRITE |(+ 0 x)|))
 (84 14 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (69 69 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (69 69 (:REWRITE |(< 0 (- x))|))
 (64 64 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (64 64 (:REWRITE DEFAULT-UNARY-/))
 (64 64 (:REWRITE |(* a (/ a))|))
 (57 57 (:REWRITE |(< (+ c x) d)|))
 (52 52 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (52 52 (:REWRITE |(equal (- x) 0)|))
 (40 40 (:REWRITE |(integerp (* c x))|))
 (37 37 (:REWRITE |(< 0 (* x y))|))
 (33 3 (:REWRITE ADE::LEN-COMP-GCD$DATA-IN))
 (32 32 (:REWRITE INSERT-0-*))
 (21 7 (:REWRITE ADE::BVP-GCD-BODY1$DATA-OUT))
 (20 20 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (20 20 (:REWRITE |(< (- x) 0)|))
 (18 18 (:REWRITE |(* (- x) y)|))
 (14 14 (:TYPE-PRESCRIPTION POSP))
 (4 1 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-LEMMA-3))
 )
(ADE::COMP-GCD$EXTRACTED-STEP
 (24 12 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD$IN-ACT))
 (18 18 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD$OUT-ACT))
 )
(ADE::FV-IF=V-IF
 (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 (:LINEAR LEN-WHEN-PREFIXP))
 (3 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (3 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (3 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::COMP-GCD$EXTRACTED-STEP-CORRECT-AUX-1
 (522 14 (:REWRITE TAKE-OF-TOO-MANY))
 (284 4 (:DEFINITION TAKE))
 (129 21 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (87 17 (:REWRITE SIMPLIFY-SUMS-<))
 (73 44 (:REWRITE DEFAULT-+-2))
 (70 46 (:REWRITE DEFAULT-CDR))
 (69 3 (:REWRITE ADE::NTHCDR-APPEND))
 (57 5 (:DEFINITION NTHCDR))
 (51 51 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (44 44 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (44 44 (:REWRITE DEFAULT-+-1))
 (44 14 (:REWRITE TAKE-WHEN-ATOM))
 (40 16 (:REWRITE DEFAULT-CAR))
 (27 27 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (27 27 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (27 27 (:REWRITE |(< (- x) (- y))|))
 (18 18 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-1))
 (18 18 (:LINEAR LEN-WHEN-PREFIXP))
 (18 14 (:REWRITE DEFAULT-<-2))
 (18 3 (:REWRITE |(+ y (+ x z))|))
 (18 3 (:DEFINITION STRIP-CARS))
 (18 3 (:DEFINITION BINARY-APPEND))
 (17 17 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (17 17 (:REWRITE DEFAULT-*-2))
 (17 17 (:REWRITE DEFAULT-*-1))
 (15 6 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (15 2 (:REWRITE REV-WHEN-NOT-CONSP))
 (14 14 (:REWRITE DEFAULT-<-1))
 (13 13 (:TYPE-PRESCRIPTION NFIX))
 (12 12 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (12 12 (:REWRITE DEFAULT-UNARY-/))
 (12 2 (:REWRITE ADE::F-GATES=B-GATES))
 (12 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (11 11 (:REWRITE NTH-WHEN-PREFIXP))
 (11 7 (:REWRITE |(< d (+ c x))|))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (10 10 (:TYPE-PRESCRIPTION ADE::V-ADDER-OUTPUT))
 (10 10 (:REWRITE ZP-OPEN))
 (9 9 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (9 9 (:REWRITE |(< 0 (- x))|))
 (9 9 (:REWRITE |(* (- x) y)|))
 (9 9 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (8 7 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (8 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (8 7 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (7 7 (:REWRITE |(equal (- x) (- y))|))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (6 6 (:REWRITE CDR-CONS))
 (6 6 (:REWRITE |(equal (- x) 0)|))
 (6 3 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (5 1 (:REWRITE CONSP-OF-TAKE))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 4 (:REWRITE |(< (+ c x) d)|))
 (4 4 (:REWRITE |(+ 0 x)|))
 (3 3 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (3 3 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (3 3 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (3 3 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (3 3 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (3 3 (:REWRITE |(< 0 (* x y))|))
 (2 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (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$EXTRACTED-STEP-CORRECT-AUX-2
 (376 12 (:REWRITE TAKE-OF-TOO-MANY))
 (179 3 (:DEFINITION TAKE))
 (82 82 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (72 36 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (69 22 (:REWRITE DEFAULT-CAR))
 (63 5 (:DEFINITION NTHCDR))
 (60 42 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-1))
 (57 3 (:REWRITE ADE::LEN-NTHCDR))
 (54 10 (:REWRITE TAKE-WHEN-ATOM))
 (52 32 (:REWRITE DEFAULT-CDR))
 (51 33 (:REWRITE DEFAULT-+-2))
 (49 15 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (44 6 (:REWRITE ADE::F-GATES=B-GATES))
 (44 4 (:REWRITE |(+ (+ x y) z)|))
 (43 14 (:REWRITE SIMPLIFY-SUMS-<))
 (40 8 (:REWRITE |(+ y x)|))
 (34 34 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (33 33 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (33 33 (:REWRITE DEFAULT-+-1))
 (32 4 (:DEFINITION STRIP-CARS))
 (26 2 (:REWRITE ADE::NTHCDR-APPEND))
 (22 22 (:REWRITE NTH-WHEN-PREFIXP))
 (20 20 (:LINEAR LEN-WHEN-PREFIXP))
 (19 13 (:REWRITE DEFAULT-<-2))
 (19 1 (:REWRITE LEN-OF-APPEND))
 (18 18 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (18 18 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (18 18 (:REWRITE |(< (- x) (- y))|))
 (18 5 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (18 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (16 16 (:TYPE-PRESCRIPTION BOOLEANP))
 (15 13 (:REWRITE DEFAULT-<-1))
 (14 2 (:DEFINITION BINARY-APPEND))
 (10 10 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (10 4 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (9 9 (:TYPE-PRESCRIPTION TRUE-LISTP-TAKE))
 (9 9 (:TYPE-PRESCRIPTION NFIX))
 (9 9 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (9 9 (:REWRITE DEFAULT-*-2))
 (9 9 (:REWRITE DEFAULT-*-1))
 (8 4 (:REWRITE CONSP-OF-TAKE))
 (6 6 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (6 6 (:REWRITE DEFAULT-UNARY-/))
 (6 2 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (6 1 (:REWRITE CONSP-OF-APPEND))
 (6 1 (:REWRITE |(+ y (+ x z))|))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (5 5 (:REWRITE |(< 0 (- x))|))
 (5 5 (:REWRITE |(* c (* d x))|))
 (5 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (5 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (5 4 (:REWRITE |(< d (+ c x))|))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 4 (:REWRITE ZP-OPEN))
 (4 4 (:REWRITE |(equal (- x) (- y))|))
 (4 4 (:REWRITE |(* (- x) y)|))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (3 3 (:REWRITE |(equal (- x) 0)|))
 (2 2 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (2 2 (:REWRITE LEN-OF-TAKE))
 (2 2 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(< 0 (* x y))|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:REWRITE |(< (+ c x) d)|))
 (1 1 (:REWRITE |(+ 0 x)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::COMP-GCD$EXTRACTED-STEP-CORRECT
 (4534 4534 (:REWRITE NTH-WHEN-PREFIXP))
 (3264 485 (:DEFINITION STRIP-CARS))
 (2697 1773 (:REWRITE DEFAULT-CAR))
 (2280 1984 (:REWRITE DEFAULT-CDR))
 (1855 25 (:DEFINITION TAKE))
 (1820 644 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1820 644 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1820 644 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1744 943 (:REWRITE DEFAULT-+-2))
 (1150 115 (:DEFINITION ADE::V-THREEFIX))
 (987 99 (:DEFINITION PAIRLIS$))
 (984 112 (:DEFINITION TRUE-LISTP))
 (943 943 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (943 943 (:REWRITE DEFAULT-+-1))
 (929 180 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (881 38 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (796 26 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (726 22 (:REWRITE ADE::LEN-NTHCDR))
 (721 103 (:REWRITE ADE::CAR-V-THREEFIX))
 (675 197 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (672 224 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (644 644 (:REWRITE |(equal (- x) (- y))|))
 (636 72 (:DEFINITION BINARY-APPEND))
 (611 580 (:REWRITE DEFAULT-*-2))
 (580 580 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (580 580 (:REWRITE DEFAULT-*-1))
 (576 200 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (516 63 (:REWRITE ADE::FV-IF=V-IF))
 (506 42 (:REWRITE |(+ (+ x y) z)|))
 (462 33 (:DEFINITION NATP))
 (446 16 (:REWRITE ADE::GCD-BODY1$ACT-INACTIVE))
 (438 78 (:REWRITE TAKE-WHEN-ATOM))
 (436 218 (:DEFINITION ADE::3V-FIX))
 (376 376 (:LINEAR LEN-WHEN-PREFIXP))
 (306 20 (:REWRITE ZP-OPEN))
 (296 59 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (289 289 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$DATA-IN))
 (264 67 (:REWRITE |(< d (+ c x))|))
 (254 155 (:REWRITE SIMPLIFY-SUMS-<))
 (232 155 (:REWRITE DEFAULT-<-2))
 (222 222 (:TYPE-PRESCRIPTION ADE::3VP))
 (217 217 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (197 197 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (197 197 (:REWRITE |(< (- x) (- y))|))
 (188 188 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (177 155 (:REWRITE DEFAULT-<-1))
 (170 170 (:TYPE-PRESCRIPTION ADE::COMP-GCD$BODY-INPUTS))
 (170 10 (:DEFINITION POSP))
 (130 55 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (120 20 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (120 16 (:REWRITE ADE::BVP-TAKE))
 (114 19 (:REWRITE ADE::COMP-GCD-COND$FLAG-ACTIVE))
 (100 40 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (86 17 (:REWRITE ADE::LEN-COMP-GCD-COND$DATA-IN))
 (84 28 (:TYPE-PRESCRIPTION ADE::BVP-TAKE))
 (84 14 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (73 73 (:META META-INTEGERP-CORRECT))
 (68 34 (:REWRITE |(* y x)|))
 (54 9 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (53 53 (:REWRITE REDUCE-INTEGERP-+))
 (53 53 (:REWRITE INTEGERP-MINUS-X))
 (52 13 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (51 17 (:REWRITE |(* y (* x z))|))
 (49 49 (:REWRITE |(* (- x) y)|))
 (42 42 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$FLAG))
 (34 34 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (34 34 (:REWRITE DEFAULT-UNARY-/))
 (34 34 (:REWRITE |(* a (/ a))|))
 (33 33 (:TYPE-PRESCRIPTION NATP))
 (33 33 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (33 33 (:REWRITE |(< (- x) 0)|))
 (30 12 (:REWRITE ADE::BVP-GCD-BODY1$DATA-OUT))
 (25 25 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (25 25 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (25 25 (:REWRITE |(equal (- x) 0)|))
 (25 25 (:REWRITE |(< 0 (- x))|))
 (25 25 (:REWRITE |(< (+ c x) d)|))
 (20 20 (:REWRITE |(integerp (* c x))|))
 (14 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (13 4 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (10 10 (:TYPE-PRESCRIPTION POSP))
 (8 8 (:REWRITE |(< 0 (* x y))|))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (4 1 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (1 1 (:REWRITE INSERT-0-*))
 )
(ADE::COMP-GCD$VALID-ST-PRESERVED
 (8198 8198 (:REWRITE NTH-WHEN-PREFIXP))
 (4128 1231 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (4128 1231 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (4128 1231 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3686 560 (:DEFINITION STRIP-CARS))
 (3060 1838 (:REWRITE DEFAULT-CAR))
 (2340 1290 (:REWRITE DEFAULT-+-2))
 (2308 2224 (:REWRITE DEFAULT-CDR))
 (2180 73 (:REWRITE ADE::GCD-BODY1$ACT-INACTIVE))
 (2010 960 (:TYPE-PRESCRIPTION ADE::F-IF))
 (1829 92 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (1600 160 (:DEFINITION ADE::V-THREEFIX))
 (1535 175 (:DEFINITION TRUE-LISTP))
 (1290 1290 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1290 1290 (:REWRITE DEFAULT-+-1))
 (1252 76 (:DEFINITION NTHCDR))
 (1231 1231 (:REWRITE |(equal (- x) (- y))|))
 (1200 1172 (:REWRITE DEFAULT-*-2))
 (1172 1172 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1172 1172 (:REWRITE DEFAULT-*-1))
 (1062 1062 (:TYPE-PRESCRIPTION ADE::COMP-GCD-COND$FLAG))
 (1050 350 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (1016 112 (:DEFINITION PAIRLIS$))
 (996 12 (:DEFINITION TAKE))
 (868 76 (:REWRITE |(+ (+ x y) z)|))
 (833 833 (:TYPE-PRESCRIPTION ADE::COMP-GCD$BODY-INPUTS))
 (744 744 (:LINEAR LEN-WHEN-PREFIXP))
 (640 20 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT-INACTIVE-LEMMA))
 (602 86 (:REWRITE ADE::CAR-V-THREEFIX))
 (600 236 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (528 16 (:REWRITE ADE::LEN-NTHCDR))
 (508 124 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (492 246 (:DEFINITION ADE::3V-FIX))
 (392 28 (:DEFINITION NATP))
 (372 372 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (368 48 (:DEFINITION BINARY-APPEND))
 (316 20 (:REWRITE ZP-OPEN))
 (290 90 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT1-INACTIVE-LEMMA))
 (276 46 (:REWRITE ADE::COMP-GCD-COND$IN-ACT-INACTIVE-LEMMA))
 (256 40 (:REWRITE TAKE-WHEN-ATOM))
 (246 246 (:TYPE-PRESCRIPTION ADE::3VP))
 (228 96 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (208 124 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (192 44 (:REWRITE |(< d (+ c x))|))
 (184 112 (:REWRITE SIMPLIFY-SUMS-<))
 (184 8 (:REWRITE ADE::MERGE$ACT0-INACTIVE))
 (168 112 (:REWRITE DEFAULT-<-2))
 (140 140 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (136 8 (:DEFINITION POSP))
 (128 112 (:REWRITE DEFAULT-<-1))
 (124 124 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (124 124 (:REWRITE |(< (- x) (- y))|))
 (96 16 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (94 94 (:REWRITE |(* (- x) y)|))
 (60 60 (:META META-INTEGERP-CORRECT))
 (44 44 (:REWRITE REDUCE-INTEGERP-+))
 (44 44 (:REWRITE INTEGERP-MINUS-X))
 (40 16 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (36 12 (:REWRITE ADE::BVP-GCD-BODY1$DATA-OUT))
 (28 28 (:TYPE-PRESCRIPTION NATP))
 (28 28 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (28 28 (:REWRITE |(< (- x) 0)|))
 (16 16 (:REWRITE |(integerp (* c x))|))
 (12 12 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (12 12 (:REWRITE |(< 0 (- x))|))
 (12 12 (:REWRITE |(< 0 (* x y))|))
 (12 12 (:REWRITE |(< (+ c x) d)|))
 (12 4 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
 (8 8 (:TYPE-PRESCRIPTION POSP))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP-LEN))
 )
(ADE::COMP-GCD$EXTRACT-LEMMA-AUX-1
 (2184 44 (:REWRITE TAKE-OF-TOO-MANY))
 (1154 173 (:DEFINITION STRIP-CARS))
 (1139 649 (:REWRITE DEFAULT-CAR))
 (1098 800 (:REWRITE DEFAULT-CDR))
 (968 121 (:DEFINITION BINARY-APPEND))
 (952 952 (:REWRITE NTH-WHEN-PREFIXP))
 (808 495 (:REWRITE DEFAULT-+-2))
 (582 151 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (582 151 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (582 151 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (572 44 (:DEFINITION NTHCDR))
 (560 20 (:REWRITE ADE::LEN-NTHCDR))
 (501 495 (:REWRITE DEFAULT-+-1))
 (495 495 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (484 44 (:REWRITE |(+ (+ x y) z)|))
 (406 86 (:REWRITE SIMPLIFY-SUMS-<))
 (360 20 (:DEFINITION ADE::V-THREEFIX))
 (304 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (274 40 (:REWRITE CONSP-OF-APPEND))
 (262 5 (:REWRITE ADE::PAIRLIS$-APPEND))
 (238 238 (:LINEAR LEN-WHEN-PREFIXP))
 (236 44 (:REWRITE TAKE-WHEN-ATOM))
 (208 44 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (156 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (151 151 (:REWRITE |(equal (- x) (- y))|))
 (142 71 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (134 86 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (119 119 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (112 4 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (107 107 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (107 107 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (102 102 (:REWRITE |(< (- x) (- y))|))
 (98 70 (:REWRITE DEFAULT-<-2))
 (96 21 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (90 70 (:REWRITE DEFAULT-<-1))
 (80 16 (:REWRITE |(- (* c x))|))
 (72 36 (:DEFINITION ADE::3V-FIX))
 (64 64 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (64 64 (:REWRITE DEFAULT-*-2))
 (64 64 (:REWRITE DEFAULT-*-1))
 (48 48 (:REWRITE DEFAULT-UNARY-MINUS))
 (44 44 (:TYPE-PRESCRIPTION NFIX))
 (42 6 (:REWRITE ADE::F-GATES=B-GATES))
 (36 36 (:TYPE-PRESCRIPTION ADE::3VP))
 (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)|))
 (25 25 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (25 25 (:REWRITE |(< 0 (- x))|))
 (17 17 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (17 17 (:REWRITE |(equal (- x) 0)|))
 (16 16 (:REWRITE |(* 0 x)|))
 (16 16 (:REWRITE |(* (- x) y)|))
 (13 13 (:LINEAR ADE::QUEUE3$EXTRACT-NOT-EMPTY))
 (11 11 (:LINEAR ADE::QUEUE2$EXTRACT-NOT-EMPTY))
 (8 8 (:REWRITE |(* c (* d x))|))
 (6 6 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (4 2 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT1))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE |(< d (+ c x y))|))
 (1 1 (:LINEAR ADE::COMP-GCD-COND$EXTRACT-NOT-EMPTY-2))
 )
(ADE::COMP-GCD$EXTRACT-LEMMA-AUX-2
 (5916 144 (:REWRITE TAKE-OF-TOO-MANY))
 (1812 1040 (:REWRITE DEFAULT-+-2))
 (1414 1414 (:REWRITE NTH-WHEN-PREFIXP))
 (1348 1292 (:REWRITE DEFAULT-CDR))
 (1040 1040 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1040 1040 (:REWRITE DEFAULT-+-1))
 (1020 720 (:REWRITE DEFAULT-CAR))
 (936 124 (:DEFINITION BINARY-APPEND))
 (900 144 (:REWRITE TAKE-WHEN-ATOM))
 (832 64 (:DEFINITION NTHCDR))
 (828 236 (:REWRITE SIMPLIFY-SUMS-<))
 (704 64 (:REWRITE |(+ (+ x y) z)|))
 (682 232 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (682 232 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (682 232 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (672 24 (:REWRITE ADE::LEN-NTHCDR))
 (548 248 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (544 8 (:REWRITE ADE::V-IF-WORKS))
 (520 8 (:DEFINITION ADE::BV2P))
 (352 48 (:REWRITE |(+ y (+ x z))|))
 (332 332 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (332 332 (:REWRITE |(< (- x) (- y))|))
 (332 20 (:DEFINITION ADE::V-THREEFIX))
 (328 328 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (304 16 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (284 236 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (232 232 (:REWRITE |(equal (- x) (- y))|))
 (228 204 (:REWRITE DEFAULT-<-2))
 (228 204 (:REWRITE DEFAULT-<-1))
 (224 224 (:LINEAR LEN-WHEN-PREFIXP))
 (196 196 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (196 196 (:REWRITE DEFAULT-*-2))
 (196 196 (:REWRITE DEFAULT-*-1))
 (192 192 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (192 192 (:REWRITE DEFAULT-UNARY-/))
 (176 16 (:REWRITE ADE::LEN-V-ADDER-OUTPUT))
 (160 40 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (160 32 (:REWRITE |(- (* c x))|))
 (148 148 (:REWRITE DEFAULT-UNARY-MINUS))
 (148 40 (:REWRITE REV-WHEN-NOT-CONSP))
 (144 144 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (144 144 (:REWRITE |(< 0 (- x))|))
 (128 128 (:TYPE-PRESCRIPTION NFIX))
 (128 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (112 112 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (112 4 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (80 80 (:TYPE-PRESCRIPTION ADE::V-ADDER-OUTPUT))
 (72 36 (:DEFINITION ADE::3V-FIX))
 (64 64 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (64 64 (:REWRITE |(equal (- x) 0)|))
 (64 32 (:REWRITE |(+ (* c x) (* d x))|))
 (64 8 (:REWRITE CAR-OF-APPEND))
 (62 31 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT0))
 (60 60 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (56 56 (:REWRITE |(< d (+ c x))|))
 (48 48 (:REWRITE CDR-CONS))
 (36 36 (:TYPE-PRESCRIPTION ADE::3VP))
 (32 32 (:REWRITE |(* 0 x)|))
 (32 32 (:REWRITE |(* (- x) y)|))
 (24 24 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (16 16 (:TYPE-PRESCRIPTION ADE::BVP-V-ADDER-OUTPUT))
 (16 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (8 8 (:TYPE-PRESCRIPTION ADE::BV2P))
 (8 8 (:TYPE-PRESCRIPTION ADE::BOOLEANP-V-<))
 (8 8 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (4 4 (:REWRITE ZP-OPEN))
 (4 2 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD-COND$OUT-ACT1))
 )
(ADE::COMP-GCD$EXTRACT-LEMMA
 (3603 70 (:REWRITE TAKE-OF-TOO-MANY))
 (1890 35 (:DEFINITION TAKE))
 (1396 202 (:DEFINITION STRIP-CARS))
 (1363 35 (:REWRITE ADE::LEN-NTHCDR))
 (1109 752 (:REWRITE DEFAULT-CAR))
 (1104 822 (:REWRITE DEFAULT-CDR))
 (1084 1084 (:REWRITE NTH-WHEN-PREFIXP))
 (755 644 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-1))
 (617 361 (:REWRITE DEFAULT-+-2))
 (560 560 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (540 18 (:REWRITE |(< x (if a b c))|))
 (525 52 (:DEFINITION NTHCDR))
 (490 70 (:REWRITE TAKE-WHEN-ATOM))
 (385 35 (:REWRITE |(+ (+ x y) z)|))
 (361 361 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (361 361 (:REWRITE NORMALIZE-ADDENDS))
 (361 361 (:REWRITE DEFAULT-+-1))
 (360 35 (:DEFINITION BINARY-APPEND))
 (354 186 (:REWRITE SIMPLIFY-SUMS-<))
 (354 186 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (354 186 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (336 336 (:LINEAR LEN-WHEN-PREFIXP))
 (301 186 (:REWRITE DEFAULT-<-2))
 (257 47 (:REWRITE ADE::F-GATES=B-GATES))
 (250 25 (:DEFINITION ADE::V-THREEFIX))
 (239 186 (:REWRITE DEFAULT-<-1))
 (234 36 (:REWRITE |(+ (if a b c) x)|))
 (210 30 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (204 204 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (204 204 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (186 186 (:REWRITE |(< (- x) (- y))|))
 (175 35 (:REWRITE |(+ y x)|))
 (175 25 (:REWRITE ADE::CAR-V-THREEFIX))
 (171 9 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (168 168 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (156 38 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (156 38 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (156 38 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (130 130 (:TYPE-PRESCRIPTION BOOLEANP))
 (126 9 (:DEFINITION NATP))
 (112 56 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD$OUT-ACT))
 (110 110 (:TYPE-PRESCRIPTION ADE::3VP))
 (100 50 (:DEFINITION ADE::3V-FIX))
 (96 48 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (90 30 (:REWRITE ADE::F-BUF-OF-3VP))
 (70 70 (:TYPE-PRESCRIPTION NFIX))
 (65 65 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (45 45 (:LINEAR ADE::COMP-GCD-COND$EXTRACT-NOT-EMPTY-2))
 (45 45 (:LINEAR ADE::COMP-GCD-COND$EXTRACT-NOT-EMPTY-1))
 (38 38 (:REWRITE |(equal (- x) (- y))|))
 (25 25 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (25 25 (:REWRITE DEFAULT-*-2))
 (25 25 (:REWRITE DEFAULT-*-1))
 (22 22 (:REWRITE |(< d (+ c x))|))
 (18 18 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (18 18 (:REWRITE REDUCE-INTEGERP-+))
 (18 18 (:REWRITE INTEGERP-MINUS-X))
 (18 18 (:REWRITE |(< (- x) 0)|))
 (18 18 (:META META-INTEGERP-CORRECT))
 (9 9 (:TYPE-PRESCRIPTION NATP))
 (9 1 (:DEFINITION TRUE-LISTP))
 (7 7 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (7 7 (:REWRITE |(equal (- x) 0)|))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 )
(ADE::COMP-GCD$IN-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT))
 )
(ADE::COMP-GCD$IN-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-1))
 )
(ADE::COMP-GCD$IN-SEQ-LEMMA
 (725 65 (:REWRITE ZP-OPEN))
 (720 40 (:REWRITE ADE::MERGE$ACT0-INACTIVE))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (250 250 (:REWRITE NTH-WHEN-PREFIXP))
 (226 98 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (226 98 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (226 98 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (213 35 (:DEFINITION BINARY-APPEND))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (160 160 (:TYPE-PRESCRIPTION ADE::COMP-GCD$ME-INPUTS))
 (144 36 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (120 120 (:REWRITE DEFAULT-CAR))
 (104 104 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (98 98 (:REWRITE |(equal (- x) (- y))|))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (91 91 (:REWRITE DEFAULT-CDR))
 (84 14 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (80 16 (:REWRITE |(+ c (+ d x))|))
 (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))|))
 (56 56 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (56 56 (:REWRITE NORMALIZE-ADDENDS))
 (56 56 (:REWRITE DEFAULT-+-2))
 (56 56 (:REWRITE DEFAULT-+-1))
 (42 42 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (40 40 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (40 40 (:REWRITE DEFAULT-*-2))
 (40 40 (:REWRITE DEFAULT-*-1))
 (12 12 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::COMP-GCD$OUT-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT))
 )
(ADE::COMP-GCD$OUT-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 )
(ADE::COMP-GCD$OUT-SEQ-LEMMA
 (1476 40 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE))
 (1280 40 (:REWRITE ADE::COMP-GCD-COND$OUT-ACT0-INACTIVE-LEMMA))
 (1224 1068 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-1))
 (922 152 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (922 152 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (922 152 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (725 65 (:REWRITE ZP-OPEN))
 (398 36 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (272 272 (:REWRITE NTH-WHEN-PREFIXP))
 (213 35 (:DEFINITION BINARY-APPEND))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (152 152 (:REWRITE |(equal (- x) (- y))|))
 (130 130 (:TYPE-PRESCRIPTION ADE::COMP-GCD$STEP))
 (120 120 (:REWRITE DEFAULT-CAR))
 (115 97 (:REWRITE DEFAULT-CDR))
 (111 29 (:REWRITE ADE::COMP-GCD$EXTRACT-LEMMA))
 (104 104 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (80 16 (:REWRITE |(+ c (+ d x))|))
 (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))|))
 (56 56 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (56 56 (:REWRITE NORMALIZE-ADDENDS))
 (56 56 (:REWRITE DEFAULT-+-2))
 (56 56 (:REWRITE DEFAULT-+-1))
 (56 14 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (30 10 (:REWRITE ADE::COMP-GCD$VALID-ST-PRESERVED))
 (30 6 (:DEFINITION NTHCDR))
 (26 26 (:TYPE-PRESCRIPTION ADE::DE))
 (12 12 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::COMP-GCD$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::GCD$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$DATAFLOW-CORRECT
 (1922 134 (:REWRITE ZP-OPEN))
 (1370 20 (:REWRITE TAKE-OF-TOO-MANY))
 (1076 120 (:REWRITE |(< d (+ c x))|))
 (950 10 (:DEFINITION TAKE))
 (892 196 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (829 21 (:DEFINITION NTHCDR))
 (728 78 (:DEFINITION LEN))
 (455 72 (:DEFINITION BINARY-APPEND))
 (375 259 (:REWRITE DEFAULT-CDR))
 (373 240 (:REWRITE DEFAULT-+-2))
 (353 176 (:REWRITE SIMPLIFY-SUMS-<))
 (349 47 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (300 260 (:REWRITE NORMALIZE-ADDENDS))
 (296 296 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (291 77 (:REWRITE |(+ c (+ d x))|))
 (278 24 (:REWRITE ADE::NFIX-OF-NAT))
 (265 265 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (263 196 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (259 48 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (259 48 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (259 48 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (241 211 (:REWRITE DEFAULT-CAR))
 (240 240 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (240 240 (:REWRITE DEFAULT-+-1))
 (220 20 (:REWRITE |(+ (+ x y) z)|))
 (214 166 (:REWRITE DEFAULT-<-2))
 (212 59 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (207 21 (:LINEAR ADE::COMP-GCD$EXTRACT-NOT-EMPTY))
 (202 24 (:DEFINITION NATP))
 (201 201 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (196 196 (:REWRITE |(< (- x) (- y))|))
 (185 41 (:REWRITE |(+ y x)|))
 (166 166 (:REWRITE DEFAULT-<-1))
 (132 3 (:REWRITE ADE::NTHCDR-CONS))
 (130 4 (:REWRITE CONSP-OF-TAKE))
 (120 3 (:DEFINITION POSP))
 (116 116 (:REWRITE NTH-WHEN-PREFIXP))
 (108 108 (:TYPE-PRESCRIPTION ADE::COMP-GCD$IN-SEQ))
 (80 20 (:REWRITE TAKE-WHEN-ATOM))
 (62 4 (:REWRITE LEN-OF-TAKE))
 (60 60 (:TYPE-PRESCRIPTION ADE::COMP-GCD$STEP))
 (54 54 (:LINEAR LEN-WHEN-PREFIXP))
 (50 10 (:REWRITE |(+ y (+ x z))|))
 (48 48 (:REWRITE |(equal (- x) (- y))|))
 (46 10 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (40 20 (:REWRITE DEFAULT-UNARY-MINUS))
 (40 20 (:REWRITE BUBBLE-DOWN-+-MATCH-1))
 (36 23 (:REWRITE |(+ 0 x)|))
 (30 20 (:REWRITE |(< (+ c x) d)|))
 (27 27 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (24 24 (:TYPE-PRESCRIPTION NATP))
 (20 20 (:TYPE-PRESCRIPTION NFIX))
 (20 20 (:REWRITE |(+ x (- x))|))
 (14 14 (:REWRITE ADE::COMP-GCD$RUN-PLUS))
 (12 12 (:REWRITE ADE::COMP-GCD$INPUT-FORMAT-PLUS))
 (12 8 (:REWRITE ADE::COMP-GCD$INV-PRESERVED))
 (3 3 (:TYPE-PRESCRIPTION POSP))
 (3 3 (:TYPE-PRESCRIPTION ADE::COMP-GCD$RUN))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (2 2 (:REWRITE |(< 0 (- x))|))
 )
(ADE::COMP-GCD$FUNCTIONALLY-CORRECT
 (392 4 (:DEFINITION ADE::COMP-GCD$OUT-SEQ))
 (168 4 (:REWRITE ADE::COMP-GCD$EXTRACT-LEMMA))
 (164 4 (:DEFINITION ADE::COMP-GCD$IN-SEQ))
 (120 3 (:DEFINITION NTHCDR))
 (97 37 (:REWRITE ZP-OPEN))
 (80 32 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (76 4 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (63 15 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (63 15 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (63 15 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (52 52 (:TYPE-PRESCRIPTION ZP))
 (52 52 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-2))
 (43 34 (:REWRITE DEFAULT-CDR))
 (42 3 (:REWRITE |(< d (+ c x))|))
 (40 40 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD$OUT-ACT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD$IN-ACT))
 (39 39 (:TYPE-PRESCRIPTION LEN))
 (33 3 (:REWRITE |(+ (+ x y) z)|))
 (28 28 (:TYPE-PRESCRIPTION ADE::COMP-GCD$IN-SEQ))
 (28 28 (:REWRITE DEFAULT-CAR))
 (27 3 (:DEFINITION LEN))
 (26 20 (:REWRITE DEFAULT-+-2))
 (24 6 (:REWRITE ADE::OPEN-COMP-GCD$INPUT-FORMAT-N-ZP))
 (24 6 (:REWRITE ADE::OPEN-COMP-GCD$INPUT-FORMAT-N))
 (20 20 (:TYPE-PRESCRIPTION ADE::COMP-GCD$OUT-ACT))
 (20 20 (:TYPE-PRESCRIPTION ADE::COMP-GCD$IN-ACT))
 (20 20 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (20 20 (:REWRITE NORMALIZE-ADDENDS))
 (20 20 (:REWRITE DEFAULT-+-1))
 (20 4 (:DEFINITION ADE::GCD$OP-MAP))
 (16 4 (:REWRITE ADE::OPEN-DE-N-ZP))
 (16 4 (:REWRITE ADE::OPEN-DE-N))
 (16 4 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (15 15 (:REWRITE |(equal (- x) (- y))|))
 (15 3 (:REWRITE |(+ y x)|))
 (15 3 (:REWRITE |(+ c (+ d x))|))
 (12 3 (:REWRITE ADE::OPEN-COMP-GCD$RUN-ZP))
 (12 3 (:REWRITE ADE::OPEN-COMP-GCD$RUN))
 (8 8 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT-LEMMA-1))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (6 6 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (6 6 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (6 3 (:REWRITE SIMPLIFY-SUMS-<))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (6 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-N))
 (3 3 (:TYPE-PRESCRIPTION ADE::COMP-GCD$RUN))
 (3 3 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 )