(ADE::Q10-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::Q10-COMP-GCD$INS-LEN)
(ADE::Q10-COMP-GCD*)
(ADE::Q10-COMP-GCD*$DESTRUCTURE
 (180 18 (:DEFINITION BINARY-APPEND))
 (153 36 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (48 48 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (48 48 (:REWRITE DEFAULT-*-2))
 (48 48 (:REWRITE DEFAULT-*-1))
 (28 28 (:REWRITE DEFAULT-CDR))
 (23 23 (:REWRITE DEFAULT-CAR))
 )
(ADE::NOT-PRIMP-Q10-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::Q10-COMP-GCD$NETLIST)
(ADE::Q10-COMP-GCD&
 (162 9 (:DEFINITION ASSOC-EQUAL))
 (40 10 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
 (31 31 (:REWRITE DEFAULT-CAR))
 (29 19 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (29 19 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (29 19 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (20 20 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
 (19 19 (:REWRITE |(equal (- x) (- y))|))
 (18 1 (:DEFINITION ADE::DELETE-TO-EQ))
 (13 13 (:REWRITE DEFAULT-CDR))
 (11 11 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (11 11 (:REWRITE DEFAULT-*-2))
 (11 11 (:REWRITE DEFAULT-*-1))
 (10 10 (:REWRITE DEFAULT-SYMBOL-NAME))
 (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-Q10-COMP-GCD$NETLIST-64)
(ADE::Q10-COMP-GCD$ST-FORMAT)
(ADE::Q10-COMP-GCD$ST-FORMAT=>CONSTRAINT
 (7 1 (:DEFINITION LEN))
 (4 4 (:REWRITE NTH-WHEN-PREFIXP))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1 1 (:REWRITE NORMALIZE-ADDENDS))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::Q10-COMP-GCD$VALID-ST)
(ADE::Q10-COMP-GCD$VALID-ST=>CONSTRAINT
 (7 1 (:DEFINITION LEN))
 (6 6 (:REWRITE NTH-WHEN-PREFIXP))
 (5 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (5 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (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 |(equal (- x) (- y))|))
 (4 4 (:REWRITE |(< (- x) (- y))|))
 (4 1 (:DEFINITION STRIP-CARS))
 (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-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (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::Q10-COMP-GCD$VALID-ST=>ST-FORMAT
 (11 11 (:REWRITE NTH-WHEN-PREFIXP))
 (6 6 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (6 6 (:REWRITE DEFAULT-*-2))
 (6 6 (:REWRITE DEFAULT-*-1))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (3 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (3 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::Q10-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-Q10-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::Q10-COMP-GCD$Q10-INPUTS
 (1 1 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::Q10-COMP-GCD$COMP-GCD-INPUTS
 (1 1 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::Q10-COMP-GCD$IN-ACT)
(ADE::Q10-COMP-GCD$IN-ACT-INACTIVE
 (136 2 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (54 1 (:DEFINITION TAKE))
 (43 43 (:TYPE-PRESCRIPTION LEN))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (29 3 (:DEFINITION LEN))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 6 (:REWRITE DEFAULT-CDR))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 7 (:REWRITE DEFAULT-<-2))
 (9 6 (:REWRITE DEFAULT-+-2))
 (9 3 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (6 6 (:REWRITE NTH-WHEN-PREFIXP))
 (6 6 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (6 6 (:REWRITE NORMALIZE-ADDENDS))
 (6 6 (:REWRITE DEFAULT-+-1))
 (6 1 (:DEFINITION BINARY-APPEND))
 (5 5 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$DATA-IN))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (: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 NATP))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::Q10-COMP-GCD$OUT-ACT)
(ADE::Q10-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)|))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (15 9 (:REWRITE DEFAULT-CDR))
 (15 6 (:REWRITE DEFAULT-CAR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (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 8 (:REWRITE NTH-WHEN-PREFIXP))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (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 BOOLEANP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::Q10-COMP-GCD$DATA-OUT)
(ADE::LEN-Q10-COMP-GCD$DATA-OUT-1
 (7 1 (:DEFINITION LEN))
 (5 5 (:REWRITE NTH-WHEN-PREFIXP))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (3 1 (:REWRITE ADE::LEN-COMP-GCD$DATA-OUT-2))
 (2 2 (:TYPE-PRESCRIPTION ADE::COMP-GCD$VALID-ST))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (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-CDR))
 (1 1 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::LEN-Q10-COMP-GCD$DATA-OUT-2
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (7 1 (:DEFINITION LEN))
 (5 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (5 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE |(equal (- x) (- y))|))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 1 (:DEFINITION STRIP-CARS))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (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::BVP-Q10-COMP-GCD$DATA-OUT
 (14 14 (:REWRITE NTH-WHEN-PREFIXP))
 (12 2 (:REWRITE ADE::Q10-COMP-GCD$OUT-ACT-INACTIVE))
 (12 2 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (9 8 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (9 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (9 8 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (8 8 (:REWRITE |(equal (- x) (- y))|))
 (7 1 (:DEFINITION LEN))
 (4 1 (:DEFINITION STRIP-CARS))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (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::Q10-COMP-GCD$OUTPUTS)
(ADE::Q10-COMP-GCD$VALUE
 (680 41 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (537 272 (:REWRITE DEFAULT-+-2))
 (407 63 (:DEFINITION BINARY-APPEND))
 (272 272 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (272 272 (:REWRITE DEFAULT-+-1))
 (216 126 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (180 60 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (170 12 (:REWRITE ADE::DISJOINT-ATOM))
 (134 134 (:TYPE-PRESCRIPTION ADE::BVP))
 (123 9 (:REWRITE LEN-OF-APPEND))
 (119 49 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (118 12 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (112 12 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (112 12 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
 (105 49 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (105 49 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (90 9 (:REWRITE |(equal (if a b c) x)|))
 (87 20 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (80 6 (:DEFINITION ATOM))
 (79 32 (:REWRITE TAKE-WHEN-ATOM))
 (76 1 (:REWRITE ADE::LEN-NTHCDR))
 (74 5 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (65 12 (:REWRITE |(+ y x)|))
 (63 63 (:REWRITE NTH-WHEN-PREFIXP))
 (63 21 (:REWRITE ADE::CAR-V-THREEFIX))
 (62 7 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (52 13 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (50 50 (:TYPE-PRESCRIPTION PAIRLIS$))
 (49 49 (:REWRITE |(equal (- x) (- y))|))
 (48 32 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (48 32 (:REWRITE ADE::F-BUF-OF-3VP))
 (45 45 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (42 21 (:DEFINITION ADE::3V-FIX))
 (42 18 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (41 41 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (41 27 (:REWRITE DEFAULT-<-2))
 (38 38 (:LINEAR LEN-WHEN-PREFIXP))
 (37 37 (:TYPE-PRESCRIPTION ADE::3VP))
 (35 5 (:DEFINITION NATP))
 (33 21 (:REWRITE ADE::V-THREEFIX-BVP))
 (32 27 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (29 27 (:REWRITE SIMPLIFY-SUMS-<))
 (29 1 (:REWRITE ADE::ASSOC-EQ-VALUES-ARGS-PAIRLIS$-ARGS))
 (28 28 (:REWRITE |(< (- x) (- y))|))
 (27 27 (:REWRITE DEFAULT-<-1))
 (27 7 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (24 3 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (22 22 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (22 22 (:REWRITE DEFAULT-*-2))
 (22 22 (:REWRITE DEFAULT-*-1))
 (20 5 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
 (19 19 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (19 19 (:REWRITE REDUCE-INTEGERP-+))
 (19 19 (:REWRITE INTEGERP-MINUS-X))
 (19 19 (:REWRITE |(< 0 (- x))|))
 (19 19 (:META META-INTEGERP-CORRECT))
 (19 19 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (19 19 (:DEFINITION STRIP-CARS))
 (16 16 (:TYPE-PRESCRIPTION BOOLEANP))
 (16 3 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (13 2 (:REWRITE |(+ (+ x y) z)|))
 (12 1 (:REWRITE ADE::Q10-COMP-GCD$OUT-ACT-INACTIVE))
 (11 7 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 2 (:REWRITE |(< x (if a b c))|))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (8 8 (:REWRITE |(< (- x) 0)|))
 (7 3 (:REWRITE ADE::LEN-COMP-GCD$DATA-OUT-2))
 (5 5 (:TYPE-PRESCRIPTION NATP))
 (5 5 (:REWRITE DEFAULT-SYMBOL-NAME))
 (5 2 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (5 2 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (5 1 (:REWRITE ADE::Q10-COMP-GCD$IN-ACT-INACTIVE))
 (5 1 (:REWRITE |(+ y (+ x z))|))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (4 4 (:REWRITE |(equal (- x) 0)|))
 (4 4 (:REWRITE |(< d (+ c x))|))
 (4 2 (:REWRITE |(- (if a b c))|))
 (3 3 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (3 3 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (3 3 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (3 3 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (3 1 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (1 1 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (1 1 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (1 1 (:REWRITE ADE::NO-DUPLICATESP-SIS))
 (1 1 (:REWRITE CONSP-OF-APPEND))
 )
(ADE::Q10-COMP-GCD$STEP
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-COMP-GCD$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::COMP-GCD$INPUT-FORMAT))
 )
(ADE::Q10-COMP-GCD$STATE
 (712 115 (:DEFINITION BINARY-APPEND))
 (526 263 (:REWRITE DEFAULT-+-2))
 (332 230 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (320 20 (:REWRITE ADE::DISJOINT-ATOM))
 (263 263 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (263 263 (:REWRITE DEFAULT-+-1))
 (211 15 (:REWRITE ADE::UPDATE-ALIST-OF-NOT-A-KEY))
 (205 20 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (205 20 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
 (190 20 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (189 15 (:REWRITE LEN-OF-APPEND))
 (175 47 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (150 10 (:DEFINITION ATOM))
 (132 17 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (126 26 (:DEFINITION ALISTP))
 (117 39 (:REWRITE ADE::CAR-V-THREEFIX))
 (107 66 (:REWRITE TAKE-WHEN-ATOM))
 (101 18 (:REWRITE |(+ y x)|))
 (98 42 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (90 30 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (86 86 (:TYPE-PRESCRIPTION PAIRLIS$))
 (84 42 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (84 42 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (84 7 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (80 66 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (80 66 (:REWRITE ADE::F-BUF-OF-3VP))
 (78 78 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (78 39 (:DEFINITION ADE::3V-FIX))
 (76 28 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (76 1 (:REWRITE ADE::LEN-NTHCDR))
 (74 74 (:TYPE-PRESCRIPTION ADE::BVP))
 (70 70 (:REWRITE NTH-WHEN-PREFIXP))
 (67 5 (:REWRITE |(equal (if a b c) x)|))
 (60 10 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (54 29 (:REWRITE DEFAULT-<-2))
 (54 12 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (53 53 (:TYPE-PRESCRIPTION ADE::3VP))
 (51 7 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (50 38 (:REWRITE ADE::V-THREEFIX-BVP))
 (42 42 (:REWRITE |(equal (- x) (- y))|))
 (40 40 (:DEFINITION STRIP-CARS))
 (39 39 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (36 29 (:REWRITE SIMPLIFY-SUMS-<))
 (36 29 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (32 8 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (30 30 (:REWRITE |(< (- x) (- y))|))
 (30 30 (:LINEAR LEN-WHEN-PREFIXP))
 (29 29 (:REWRITE DEFAULT-<-1))
 (26 26 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
 (26 26 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (26 26 (:REWRITE |(< 0 (- x))|))
 (23 7 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (22 22 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (22 22 (:REWRITE DEFAULT-*-2))
 (22 22 (:REWRITE DEFAULT-*-1))
 (20 20 (:TYPE-PRESCRIPTION BOOLEANP))
 (20 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (20 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (15 15 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (14 2 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (+ x y) z)|))
 (12 12 (:TYPE-PRESCRIPTION ADE::FV-IF))
 (12 3 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
 (10 10 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (10 10 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (10 10 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (10 10 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (10 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 2 (:REWRITE |(< x (if a b c))|))
 (9 3 (:REWRITE ADE::BOOLEANP-QUEUE10$OUT-ACT))
 (7 7 (:REWRITE REDUCE-INTEGERP-+))
 (7 7 (:REWRITE INTEGERP-MINUS-X))
 (7 7 (:META META-INTEGERP-CORRECT))
 (5 5 (:REWRITE ADE::LEN-QUEUE10$DATA-OUT-2))
 (5 1 (:REWRITE |(+ y (+ x z))|))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (4 4 (:REWRITE |(equal (- x) 0)|))
 (4 2 (:REWRITE |(- (if a b c))|))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (3 3 (:REWRITE DEFAULT-SYMBOL-NAME))
 (3 3 (:REWRITE |(< (- x) 0)|))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (1 1 (:REWRITE CONSP-OF-APPEND))
 )
(ADE::Q10-COMP-GCD$INPUT-FORMAT)
(ADE::Q10-COMP-GCD$INPUT-FORMAT=>Q10$INPUT-FORMAT
 (1018 24 (:REWRITE TAKE-OF-TOO-MANY))
 (512 8 (:DEFINITION TAKE))
 (462 16 (:REWRITE ADE::LEN-NTHCDR))
 (361 39 (:DEFINITION LEN))
 (354 106 (:REWRITE DEFAULT-CDR))
 (308 60 (:REWRITE DEFAULT-CAR))
 (156 20 (:REWRITE TAKE-WHEN-ATOM))
 (156 16 (:DEFINITION BINARY-APPEND))
 (146 60 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (134 32 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (132 58 (:REWRITE SIMPLIFY-SUMS-<))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (107 66 (:REWRITE DEFAULT-+-2))
 (91 7 (:DEFINITION NTHCDR))
 (86 30 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (86 30 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (86 30 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (76 6 (:REWRITE ZP-OPEN))
 (74 56 (:REWRITE DEFAULT-<-2))
 (72 72 (:LINEAR LEN-WHEN-PREFIXP))
 (72 56 (:REWRITE DEFAULT-<-1))
 (68 68 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (68 68 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (66 66 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (66 66 (:REWRITE DEFAULT-+-1))
 (62 62 (:REWRITE |(< (- x) (- y))|))
 (44 44 (:REWRITE NTH-WHEN-PREFIXP))
 (36 36 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (33 3 (:REWRITE |(+ (+ x y) z)|))
 (32 32 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (32 32 (:REWRITE DEFAULT-*-2))
 (32 32 (:REWRITE DEFAULT-*-1))
 (30 30 (:REWRITE |(equal (- x) (- y))|))
 (30 12 (:REWRITE |(< d (+ c x))|))
 (28 2 (:REWRITE REPEAT-WHEN-ZP))
 (26 26 (:TYPE-PRESCRIPTION NFIX))
 (26 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (24 2 (:REWRITE LEN-OF-APPEND))
 (18 2 (:REWRITE CAR-OF-TAKE))
 (18 2 (:DEFINITION TRUE-LISTP))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 2 (:REWRITE CONSP-OF-APPEND))
 (12 2 (:REWRITE |(+ y (+ x z))|))
 (10 10 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (10 10 (:REWRITE CONSP-OF-TAKE))
 (10 10 (:REWRITE |(< 0 (- x))|))
 (8 8 (:REWRITE |(* (- x) y)|))
 (8 4 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (8 2 (:DEFINITION STRIP-CARS))
 (6 6 (:REWRITE |(< 0 (* x y))|))
 (6 2 (:REWRITE ADE::BVP-NTHCDR))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (4 4 (:REWRITE DEFAULT-UNARY-/))
 (4 4 (:REWRITE |(< (- x) 0)|))
 (4 4 (:REWRITE |(* c (* d x))|))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE |(equal (- x) 0)|))
 (2 2 (:REWRITE |(< (+ c x) d)|))
 (2 2 (:REWRITE |(< (* x y) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::Q10-COMP-GCD$INPUT-FORMAT=>COMP-GCD$INPUT-FORMAT
 (650 16 (:REWRITE TAKE-OF-TOO-MANY))
 (310 8 (:REWRITE ADE::LEN-NTHCDR))
 (216 4 (:DEFINITION TAKE))
 (130 14 (:REWRITE TAKE-WHEN-ATOM))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (107 66 (:REWRITE DEFAULT-+-2))
 (98 34 (:REWRITE SIMPLIFY-SUMS-<))
 (96 72 (:REWRITE DEFAULT-CDR))
 (75 9 (:DEFINITION NTHCDR))
 (66 66 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (66 66 (:REWRITE DEFAULT-+-1))
 (66 8 (:DEFINITION BINARY-APPEND))
 (59 26 (:REWRITE DEFAULT-CAR))
 (56 34 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (55 5 (:REWRITE |(+ (+ x y) z)|))
 (48 48 (:REWRITE NTH-WHEN-PREFIXP))
 (44 44 (:LINEAR LEN-WHEN-PREFIXP))
 (44 32 (:REWRITE DEFAULT-<-1))
 (42 42 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (42 42 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (42 32 (:REWRITE DEFAULT-<-2))
 (36 36 (:REWRITE |(< (- x) (- y))|))
 (26 10 (:REWRITE |(< d (+ c x))|))
 (26 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (24 6 (:DEFINITION STRIP-CARS))
 (24 4 (:REWRITE CONSP-OF-APPEND))
 (22 22 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (22 18 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (22 18 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (22 18 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (21 3 (:REWRITE ADE::CAR-V-THREEFIX))
 (20 20 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (20 20 (:REWRITE DEFAULT-*-2))
 (20 20 (:REWRITE DEFAULT-*-1))
 (20 2 (:DEFINITION ADE::V-THREEFIX))
 (18 18 (:REWRITE |(equal (- x) (- y))|))
 (18 2 (:DEFINITION TRUE-LISTP))
 (16 16 (:TYPE-PRESCRIPTION NFIX))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 2 (:REWRITE |(+ y (+ x z))|))
 (10 5 (:DEFINITION ADE::3V-FIX))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (8 8 (:REWRITE |(< 0 (- x))|))
 (8 8 (:REWRITE |(* (- x) y)|))
 (8 4 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (6 6 (:REWRITE |(equal (- x) 0)|))
 (6 2 (:REWRITE ADE::BVP-NTHCDR))
 (5 5 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 4 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (4 4 (:REWRITE DEFAULT-UNARY-/))
 (4 4 (:REWRITE CONSP-OF-TAKE))
 (4 4 (:REWRITE |(equal (* x y) 0)|))
 (4 4 (:REWRITE |(< 0 (* x y))|))
 (4 4 (:REWRITE |(* c (* d x))|))
 (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-Q10-COMP-GCD$IN-ACT
 (24 24 (:REWRITE NTH-WHEN-PREFIXP))
 (8 8 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (8 8 (:REWRITE DEFAULT-*-2))
 (8 8 (:REWRITE DEFAULT-*-1))
 (8 2 (:DEFINITION STRIP-CARS))
 (6 3 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CDR))
 (5 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (5 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE |(equal (- x) (- y))|))
 (4 2 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (4 2 (:REWRITE ADE::Q10-COMP-GCD$IN-ACT-INACTIVE))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-1))
 )
(ADE::BOOLEANP-Q10-COMP-GCD$OUT-ACT
 (24 24 (:REWRITE NTH-WHEN-PREFIXP))
 (12 2 (:REWRITE ADE::Q10-COMP-GCD$OUT-ACT-INACTIVE))
 (12 2 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (9 8 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (9 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (9 8 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (8 8 (:REWRITE |(equal (- x) (- y))|))
 (8 2 (:DEFINITION STRIP-CARS))
 (6 6 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (6 6 (:REWRITE DEFAULT-*-2))
 (6 6 (:REWRITE DEFAULT-*-1))
 (6 3 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-1))
 )
(ADE::Q10-COMP-GCD$ST-FORMAT-PRESERVED
 (42 2 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (27 27 (:REWRITE NTH-WHEN-PREFIXP))
 (18 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE10$OUT-ACT))
 (12 2 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (12 2 (:REWRITE ADE::BOOLEANP-QUEUE10$OUT-ACT))
 (10 10 (:TYPE-PRESCRIPTION ADE::QUEUE10$INPUT-FORMAT))
 (9 9 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (9 9 (:REWRITE DEFAULT-*-2))
 (9 9 (:REWRITE DEFAULT-*-1))
 (8 2 (:DEFINITION STRIP-CARS))
 (7 1 (:DEFINITION LEN))
 (6 6 (:TYPE-PRESCRIPTION ADE::QUEUE10$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$Q10-INPUTS))
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::Q10-COMP-GCD$INPUT-FORMAT=>Q10$INPUT-FORMAT))
 (5 1 (:DEFINITION PAIRLIS$))
 (4 4 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$INPUT-FORMAT))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (4 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (4 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3 3 (:REWRITE ADE::LEN-QUEUE10$DATA-OUT-2))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 1 (:REWRITE DEFAULT-+-2))
 (2 1 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (1 1 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1 1 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE |(* (- x) y)|))
 )
(ADE::Q10-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::Q10-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::Q10-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::Q10-COMP-GCD$RUN)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-Q10-COMP-GCD$RUN-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-Q10-COMP-GCD$RUN)
(ADE::Q10-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::Q10-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-Q10-COMP-GCD$INPUT-FORMAT-N-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-Q10-COMP-GCD$INPUT-FORMAT-N)
(ADE::Q10-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::Q10-COMP-GCD$DE-N
 (265 30 (:REWRITE ZP-OPEN))
 (108 12 (:REWRITE |(< d (+ c x))|))
 (62 2 (:DEFINITION ADE::Q10-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::Q10-COMP-GCD$INPUT-FORMAT-PLUS))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE ADE::DE-PLUS))
 )
(ADE::Q10-COMP-GCD$EXTRACT)
(ADE::Q10-COMP-GCD$EXTRACT-NOT-EMPTY
 (57 7 (:DEFINITION LEN))
 (47 4 (:DEFINITION BINARY-APPEND))
 (46 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (44 22 (:TYPE-PRESCRIPTION ADE::BOOLEANP-Q10-COMP-GCD$OUT-ACT))
 (28 28 (:TYPE-PRESCRIPTION ADE::GCD$OP-MAP))
 (23 23 (:REWRITE NTH-WHEN-PREFIXP))
 (20 20 (:TYPE-PRESCRIPTION ADE::COMP-GCD$EXTRACT))
 (19 9 (:REWRITE DEFAULT-+-2))
 (17 17 (:REWRITE DEFAULT-CDR))
 (17 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (15 10 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (15 10 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (15 10 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (12 4 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (12 2 (:REWRITE ADE::Q10-COMP-GCD$OUT-ACT-INACTIVE))
 (12 2 (:REWRITE CONSP-OF-APPEND))
 (12 2 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (11 11 (:REWRITE DEFAULT-CAR))
 (11 9 (:REWRITE DEFAULT-+-1))
 (10 10 (:REWRITE |(equal (- x) (- y))|))
 (9 9 (:TYPE-PRESCRIPTION ADE::QUEUE10$EXTRACT))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE NORMALIZE-ADDENDS))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (8 2 (:DEFINITION STRIP-CARS))
 (8 2 (:DEFINITION ADE::GCD$OP-MAP))
 (4 4 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (4 4 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (4 4 (:REWRITE DEFAULT-*-2))
 (4 4 (:REWRITE DEFAULT-*-1))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 2 (:LINEAR ADE::QUEUE10$EXTRACT-NOT-EMPTY))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 (1 1 (:REWRITE |(equal (+ c x) d)|))
 (1 1 (:REWRITE |(equal (+ c x y) d)|))
 (1 1 (:REWRITE |(+ c (+ d x))|))
 )
(ADE::Q10-COMP-GCD$INV)
(ADE::Q10-COMP-GCD$INV-PRESERVED
 (89 2 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (63 2 (:REWRITE ADE::BOOLEANP-QUEUE10$OUT-ACT))
 (59 2 (:REWRITE ADE::Q10-COMP-GCD$INPUT-FORMAT=>Q10$INPUT-FORMAT))
 (58 58 (:REWRITE NTH-WHEN-PREFIXP))
 (20 5 (:DEFINITION STRIP-CARS))
 (18 18 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (18 18 (:REWRITE DEFAULT-*-2))
 (18 18 (:REWRITE DEFAULT-*-1))
 (12 12 (:REWRITE DEFAULT-CDR))
 (12 12 (:REWRITE DEFAULT-CAR))
 (12 4 (:TYPE-PRESCRIPTION ADE::BOOLEANP-QUEUE10$OUT-ACT))
 (12 2 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (10 5 (:REWRITE DEFAULT-+-2))
 (10 2 (:DEFINITION PAIRLIS$))
 (7 6 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (7 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (7 6 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (6 6 (:TYPE-PRESCRIPTION ADE::QUEUE10$INPUT-FORMAT))
 (6 6 (:REWRITE |(equal (- x) (- y))|))
 (5 5 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (5 5 (:REWRITE DEFAULT-+-1))
 (4 4 (:TYPE-PRESCRIPTION ADE::QUEUE10$OUT-ACT))
 (4 4 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$Q10-INPUTS))
 (4 4 (:TYPE-PRESCRIPTION ADE::FV-IF))
 (4 2 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (2 2 (:TYPE-PRESCRIPTION BOOLEANP))
 (2 2 (:REWRITE ADE::BVP-QUEUE10$DATA-OUT))
 (2 2 (:REWRITE |(* (- x) y)|))
 )
(ADE::Q10-COMP-GCD$EXTRACTED-STEP
 (24 12 (:TYPE-PRESCRIPTION ADE::BOOLEANP-Q10-COMP-GCD$IN-ACT))
 (18 18 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-Q10-COMP-GCD$OUT-ACT))
 )
(ADE::Q10-COMP-GCD$Q10-OUT-ACT-INACTIVE
 (136 2 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (54 1 (:DEFINITION TAKE))
 (43 43 (:TYPE-PRESCRIPTION LEN))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (29 3 (:DEFINITION LEN))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (15 1 (:DEFINITION NTHCDR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 6 (:REWRITE DEFAULT-CDR))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 7 (:REWRITE DEFAULT-<-2))
 (9 6 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (8 2 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (6 6 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (6 6 (:REWRITE NORMALIZE-ADDENDS))
 (6 6 (:REWRITE DEFAULT-+-1))
 (6 1 (:DEFINITION BINARY-APPEND))
 (5 5 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$DATA-IN))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 1 (:REWRITE |(+ y x)|))
 (5 1 (:REWRITE |(+ c (+ d x))|))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (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 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 |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::Q10-COMP-GCD$COMP-GCD-IN-ACT-INACTIVE
 (136 2 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (54 1 (:DEFINITION TAKE))
 (43 43 (:TYPE-PRESCRIPTION LEN))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (30 2 (:DEFINITION NTHCDR))
 (29 3 (:DEFINITION LEN))
 (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 5 (:REWRITE DEFAULT-CAR))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 1 (:DEFINITION NATP))
 (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 8 (:REWRITE NTH-WHEN-PREFIXP))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (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 2 (:DEFINITION ADE::3V-FIX))
 (4 1 (:DEFINITION STRIP-CARS))
 (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 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::Q10-COMP-GCD-AUX-1
 (427 9 (:REWRITE TAKE-OF-TOO-MANY))
 (257 3 (:DEFINITION TAKE))
 (112 56 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (111 111 (:TYPE-PRESCRIPTION LEN))
 (110 4 (:REWRITE ADE::LEN-NTHCDR))
 (105 11 (:DEFINITION LEN))
 (89 5 (:REWRITE ZP-OPEN))
 (88 8 (:REWRITE TAKE-WHEN-ATOM))
 (86 24 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (78 6 (:REWRITE CONSP-OF-TAKE))
 (56 56 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (56 8 (:REWRITE |(< 0 (* x y))|))
 (54 22 (:REWRITE SIMPLIFY-SUMS-<))
 (44 1 (:DEFINITION BINARY-APPEND))
 (39 18 (:REWRITE DEFAULT-CDR))
 (33 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (32 19 (:REWRITE DEFAULT-+-2))
 (30 1 (:REWRITE CONSP-OF-APPEND))
 (29 5 (:REWRITE DEFAULT-CAR))
 (28 28 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (28 28 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (28 21 (:REWRITE DEFAULT-<-2))
 (26 26 (:LINEAR LEN-WHEN-PREFIXP))
 (25 25 (:REWRITE |(< (- x) (- y))|))
 (25 21 (:REWRITE DEFAULT-<-1))
 (20 4 (:REWRITE |(+ y x)|))
 (19 19 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (19 19 (:REWRITE DEFAULT-+-1))
 (17 3 (:DEFINITION NTHCDR))
 (15 1 (:REWRITE ADE::NTHCDR-APPEND))
 (13 13 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (10 10 (:TYPE-PRESCRIPTION NFIX))
 (10 10 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (10 10 (:REWRITE |(< 0 (- x))|))
 (10 4 (:REWRITE |(+ c (+ d x))|))
 (10 1 (:REWRITE CAR-OF-TAKE))
 (9 1 (:REWRITE LEN-OF-APPEND))
 (7 7 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (7 7 (:REWRITE DEFAULT-*-2))
 (7 7 (:REWRITE DEFAULT-*-1))
 (6 5 (:REWRITE |(< d (+ c x))|))
 (6 2 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (6 1 (:REWRITE |(+ y (+ x z))|))
 (5 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (4 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (4 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (4 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4 4 (:REWRITE |(equal (- x) 0)|))
 (4 4 (:REWRITE |(equal (- x) (- y))|))
 (3 3 (:REWRITE NTH-WHEN-PREFIXP))
 (3 3 (:REWRITE |(* (- x) y)|))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE |(< (+ c x) d)|))
 (2 2 (:REWRITE |(+ 0 x)|))
 (2 2 (:REWRITE |(* c (* d x))|))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::Q10-COMP-GCD-AUX-2
 (204 5 (:REWRITE TAKE-OF-TOO-MANY))
 (56 2 (:REWRITE ADE::LEN-NTHCDR))
 (54 1 (:DEFINITION TAKE))
 (42 21 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (36 4 (:REWRITE TAKE-WHEN-ATOM))
 (35 9 (:REWRITE SIMPLIFY-SUMS-<))
 (27 17 (:REWRITE DEFAULT-+-2))
 (26 2 (:DEFINITION NTHCDR))
 (25 5 (:REWRITE |(+ y x)|))
 (23 17 (:REWRITE DEFAULT-CDR))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (21 21 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (21 1 (:REWRITE ADE::NTHCDR-APPEND))
 (17 17 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (17 17 (:REWRITE DEFAULT-+-1))
 (15 9 (:REWRITE DEFAULT-CAR))
 (15 1 (:REWRITE LEN-OF-APPEND))
 (14 9 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 12 (:LINEAR LEN-WHEN-PREFIXP))
 (12 3 (:DEFINITION STRIP-CARS))
 (11 8 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (10 10 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (10 10 (:REWRITE NTH-WHEN-PREFIXP))
 (10 10 (:REWRITE |(< (- x) (- y))|))
 (10 8 (:REWRITE DEFAULT-<-1))
 (7 1 (:DEFINITION BINARY-APPEND))
 (6 6 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (6 6 (:REWRITE DEFAULT-*-2))
 (6 6 (:REWRITE DEFAULT-*-1))
 (6 6 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (6 2 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (6 1 (:REWRITE CONSP-OF-APPEND))
 (6 1 (:REWRITE |(+ y (+ x z))|))
 (5 5 (:TYPE-PRESCRIPTION NFIX))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (3 3 (:REWRITE |(< d (+ c x))|))
 (3 3 (:REWRITE |(< 0 (- x))|))
 (3 3 (:REWRITE |(* (- x) y)|))
 (3 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (3 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (3 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE LEN-OF-TAKE))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE CONSP-OF-TAKE))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE |(* c (* d x))|))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 (1 1 (:REWRITE |(< 0 (* x y))|))
 (1 1 (:REWRITE |(< (- x) 0)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(ADE::GCD$OP-MAP-OF-APPEND-INSTANCE)
(ADE::Q10-COMP-GCD$EXTRACTED-STEP-CORRECT
 (4893 57 (:DEFINITION TAKE))
 (933 513 (:REWRITE DEFAULT-+-2))
 (905 548 (:REWRITE DEFAULT-CDR))
 (800 400 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (768 768 (:REWRITE NTH-WHEN-PREFIXP))
 (570 2 (:REWRITE TAKE-WHEN-PREFIXP))
 (560 281 (:REWRITE DEFAULT-CAR))
 (560 120 (:REWRITE TAKE-WHEN-ATOM))
 (535 513 (:REWRITE DEFAULT-+-1))
 (531 127 (:REWRITE |(< d (+ c x))|))
 (530 263 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (513 513 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (484 14 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (400 400 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (378 14 (:REWRITE ADE::LEN-NTHCDR))
 (368 368 (:LINEAR LEN-WHEN-PREFIXP))
 (335 52 (:DEFINITION BINARY-APPEND))
 (322 2 (:REWRITE PREFIXP-OF-CONS-RIGHT))
 (308 300 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (308 300 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (266 14 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (263 263 (:REWRITE |(< (- x) (- y))|))
 (248 148 (:REWRITE DEFAULT-<-2))
 (220 34 (:DEFINITION NTHCDR))
 (216 54 (:DEFINITION STRIP-CARS))
 (212 4 (:REWRITE CONSP-OF-TAKE))
 (197 117 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (197 117 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (197 117 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (184 184 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (180 178 (:REWRITE DEFAULT-*-2))
 (178 178 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (178 178 (:REWRITE DEFAULT-*-1))
 (176 148 (:REWRITE DEFAULT-<-1))
 (175 30 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (128 76 (:REWRITE DEFAULT-UNARY-MINUS))
 (118 18 (:LINEAR ADE::QUEUE10$EXTRACT-NOT-EMPTY))
 (117 117 (:REWRITE |(equal (- x) (- y))|))
 (103 88 (:REWRITE |(< (+ c x) d)|))
 (93 18 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (74 4 (:REWRITE LEN-WHEN-PREFIXP))
 (70 36 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (70 4 (:REWRITE CONSP-OF-APPEND))
 (46 2 (:REWRITE |(< 0 (* x y))|))
 (34 17 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (31 1 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (30 6 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (29 1 (:REWRITE CAR-OF-APPEND))
 (28 28 (:TYPE-PRESCRIPTION PREFIXP))
 (14 14 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (14 14 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (14 14 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (14 14 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (12 8 (:REWRITE |(< (+ d x) (+ c y))|))
 (12 8 (:REWRITE |(< (+ c x) (+ d y))|))
 (12 2 (:REWRITE ADE::Q10-COMP-GCD$OUT-ACT-INACTIVE))
 (10 10 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (10 10 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (10 10 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (8 8 (:REWRITE |(< 0 (- x))|))
 (8 4 (:REWRITE ADE::Q10-COMP-GCD$IN-ACT-INACTIVE))
 (8 4 (:REWRITE |(< d (+ c x y))|))
 (8 4 (:REWRITE |(< (+ c x y) d)|))
 (8 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (6 6 (:REWRITE FOLD-CONSTS-IN-+))
 (6 6 (:REWRITE |(< (- x) 0)|))
 (5 1 (:DEFINITION PAIRLIS$))
 (4 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:META META-INTEGERP-CORRECT))
 (4 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (2 2 (:TYPE-PRESCRIPTION LIST-EQUIV))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (2 2 (:REWRITE |(equal (- x) 0)|))
 (2 2 (:REWRITE |(* (- x) y)|))
 )
(ADE::Q10-COMP-GCD$VALID-ST-PRESERVED
 (283 283 (:REWRITE NTH-WHEN-PREFIXP))
 (76 76 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (76 76 (:REWRITE DEFAULT-*-2))
 (76 76 (:REWRITE DEFAULT-*-1))
 (76 19 (:DEFINITION STRIP-CARS))
 (64 32 (:REWRITE DEFAULT-+-2))
 (62 37 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (62 37 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (62 37 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (55 55 (:REWRITE DEFAULT-CDR))
 (42 42 (:REWRITE DEFAULT-CAR))
 (37 37 (:REWRITE |(equal (- x) (- y))|))
 (32 32 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (32 32 (:REWRITE DEFAULT-+-1))
 (27 7 (:REWRITE ADE::QUEUE10$OUT-ACT-INACTIVE))
 (21 4 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (6 3 (:REWRITE ADE::COMP-GCD$IN-ACT-INACTIVE))
 (5 1 (:DEFINITION PAIRLIS$))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 2 (:REWRITE |(* (- x) y)|))
 )
(ADE::Q10-COMP-GCD$EXTRACT-LEMMA
 (160 4 (:DEFINITION NTHCDR))
 (84 4 (:REWRITE ZP-OPEN))
 (60 33 (:REWRITE DEFAULT-+-2))
 (56 8 (:DEFINITION BINARY-APPEND))
 (56 4 (:REWRITE |(< d (+ c x))|))
 (54 41 (:REWRITE DEFAULT-CDR))
 (42 21 (:TYPE-PRESCRIPTION ADE::BOOLEANP-Q10-COMP-GCD$OUT-ACT))
 (37 33 (:REWRITE DEFAULT-+-1))
 (35 35 (:REWRITE NTH-WHEN-PREFIXP))
 (33 33 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (28 28 (:REWRITE DEFAULT-CAR))
 (24 24 (:TYPE-PRESCRIPTION ADE::GCD$OP-MAP))
 (20 5 (:DEFINITION STRIP-CARS))
 (16 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (12 2 (:REWRITE ADE::Q10-COMP-GCD$OUT-ACT-INACTIVE))
 (12 2 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (9 8 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (9 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (9 8 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (8 8 (:REWRITE |(equal (- x) (- y))|))
 (8 4 (:REWRITE SIMPLIFY-SUMS-<))
 (8 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (8 4 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (8 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE |(< (- x) (- y))|))
 (4 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE FOLD-CONSTS-IN-+))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 )
(ADE::Q10-COMP-GCD$IN-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-Q10-COMP-GCD$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$INPUT-FORMAT))
 )
(ADE::Q10-COMP-GCD$IN-SEQ-NETLIST)
(ADE::Q10-COMP-GCD$IN-SEQ-LEMMA
 (725 65 (:REWRITE ZP-OPEN))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (213 35 (:DEFINITION BINARY-APPEND))
 (212 72 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (212 72 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (212 72 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (156 156 (:REWRITE NTH-WHEN-PREFIXP))
 (120 120 (:REWRITE DEFAULT-CAR))
 (104 104 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (91 91 (:REWRITE DEFAULT-CDR))
 (84 14 (:REWRITE ADE::Q10-COMP-GCD$OUT-ACT-INACTIVE))
 (80 40 (:REWRITE ADE::QUEUE10$IN-ACT-INACTIVE))
 (80 16 (:REWRITE |(+ c (+ d x))|))
 (72 72 (:REWRITE |(equal (- x) (- y))|))
 (72 36 (:REWRITE ADE::Q10-COMP-GCD$IN-ACT-INACTIVE))
 (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))
 (40 40 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (40 40 (:REWRITE DEFAULT-*-2))
 (40 40 (:REWRITE DEFAULT-*-1))
 (12 12 (:REWRITE ADE::Q10-COMP-GCD$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::Q10-COMP-GCD$OUT-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-Q10-COMP-GCD$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$INPUT-FORMAT))
 )
(ADE::Q10-COMP-GCD$OUT-SEQ-NETLIST)
(ADE::Q10-COMP-GCD$OUT-SEQ-LEMMA
 (725 65 (:REWRITE ZP-OPEN))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (274 134 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (274 134 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (274 134 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (240 40 (:REWRITE ADE::COMP-GCD$OUT-ACT-INACTIVE))
 (216 36 (:REWRITE ADE::Q10-COMP-GCD$OUT-ACT-INACTIVE))
 (213 35 (:DEFINITION BINARY-APPEND))
 (170 170 (:REWRITE NTH-WHEN-PREFIXP))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (134 134 (:REWRITE |(equal (- x) (- y))|))
 (120 120 (:REWRITE DEFAULT-CAR))
 (115 97 (:REWRITE DEFAULT-CDR))
 (111 29 (:REWRITE ADE::Q10-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))
 (30 10 (:REWRITE ADE::Q10-COMP-GCD$VALID-ST-PRESERVED))
 (30 6 (:DEFINITION NTHCDR))
 (28 14 (:REWRITE ADE::Q10-COMP-GCD$IN-ACT-INACTIVE))
 (18 18 (:TYPE-PRESCRIPTION ADE::SE))
 (12 12 (:REWRITE ADE::Q10-COMP-GCD$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::Q10-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::Q10-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-<))
 (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-<))
 (260 76 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (260 76 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (260 76 (: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))
 (232 47 (:REWRITE ADE::Q10-COMP-GCD$OUT-ACT-INACTIVE))
 (220 20 (:REWRITE |(+ (+ x y) z)|))
 (214 166 (:REWRITE DEFAULT-<-2))
 (207 21 (:LINEAR ADE::Q10-COMP-GCD$EXTRACT-NOT-EMPTY))
 (202 24 (:DEFINITION NATP))
 (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))
 (110 59 (:REWRITE ADE::Q10-COMP-GCD$IN-ACT-INACTIVE))
 (108 108 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$IN-SEQ))
 (88 88 (:REWRITE NTH-WHEN-PREFIXP))
 (80 20 (:REWRITE TAKE-WHEN-ATOM))
 (76 76 (:REWRITE |(equal (- x) (- y))|))
 (62 4 (:REWRITE LEN-OF-TAKE))
 (60 60 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$STEP))
 (54 54 (:LINEAR LEN-WHEN-PREFIXP))
 (50 10 (:REWRITE |(+ y (+ x z))|))
 (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::Q10-COMP-GCD$RUN-PLUS))
 (12 12 (:REWRITE ADE::Q10-COMP-GCD$INPUT-FORMAT-PLUS))
 (12 8 (:REWRITE ADE::Q10-COMP-GCD$INV-PRESERVED))
 (3 3 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$RUN))
 (3 3 (:TYPE-PRESCRIPTION POSP))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (2 2 (:REWRITE |(< 0 (- x))|))
 )
(ADE::Q10-COMP-GCD$FUNCTIONALLY-CORRECT
 (340 4 (:DEFINITION ADE::Q10-COMP-GCD$OUT-SEQ))
 (168 4 (:REWRITE ADE::Q10-COMP-GCD$EXTRACT-LEMMA))
 (156 4 (:DEFINITION ADE::Q10-COMP-GCD$IN-SEQ))
 (120 3 (:DEFINITION NTHCDR))
 (97 37 (:REWRITE ZP-OPEN))
 (80 32 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (52 52 (:TYPE-PRESCRIPTION ZP))
 (51 15 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (51 15 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (51 15 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (43 34 (:REWRITE DEFAULT-CDR))
 (42 3 (:REWRITE |(< d (+ c x))|))
 (40 40 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$INPUT-FORMAT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-Q10-COMP-GCD$OUT-ACT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-Q10-COMP-GCD$IN-ACT))
 (39 39 (:TYPE-PRESCRIPTION LEN))
 (33 3 (:REWRITE |(+ (+ x y) z)|))
 (28 28 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$IN-SEQ))
 (28 28 (:REWRITE DEFAULT-CAR))
 (27 3 (:DEFINITION LEN))
 (26 20 (:REWRITE DEFAULT-+-2))
 (24 6 (:REWRITE ADE::OPEN-Q10-COMP-GCD$INPUT-FORMAT-N-ZP))
 (24 6 (:REWRITE ADE::OPEN-Q10-COMP-GCD$INPUT-FORMAT-N))
 (24 4 (:REWRITE ADE::Q10-COMP-GCD$OUT-ACT-INACTIVE))
 (20 20 (:TYPE-PRESCRIPTION ADE::Q10-COMP-GCD$OUT-ACT))
 (20 20 (:TYPE-PRESCRIPTION ADE::Q10-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))
 (15 15 (:REWRITE |(equal (- x) (- y))|))
 (15 3 (:REWRITE |(+ y x)|))
 (15 3 (:REWRITE |(+ c (+ d x))|))
 (12 3 (:REWRITE ADE::OPEN-Q10-COMP-GCD$RUN-ZP))
 (12 3 (:REWRITE ADE::OPEN-Q10-COMP-GCD$RUN))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (8 4 (:REWRITE ADE::Q10-COMP-GCD$IN-ACT-INACTIVE))
 (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::Q10-COMP-GCD$RUN))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-N))
 (3 3 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 )