(ADE::GCD-BODY1$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::GCD-BODY1$INS-LEN)
(ADE::GCD-BODY1*)
(ADE::GCD-BODY1*$DESTRUCTURE
 (546 96 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (546 48 (:DEFINITION BINARY-APPEND))
 (120 12 (:REWRITE REV-WHEN-NOT-CONSP))
 (78 24 (:REWRITE CONSP-OF-REV))
 (76 58 (:REWRITE DEFAULT-CDR))
 (71 53 (:REWRITE DEFAULT-CAR))
 (60 60 (:TYPE-PRESCRIPTION REV))
 (60 60 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (60 60 (:REWRITE DEFAULT-*-2))
 (60 60 (:REWRITE DEFAULT-*-1))
 (12 12 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (12 12 (:REWRITE NORMALIZE-ADDENDS))
 (12 12 (:REWRITE DEFAULT-+-2))
 (12 12 (:REWRITE DEFAULT-+-1))
 )
(ADE::NOT-PRIMP-GCD-BODY1
 (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::GCD-BODY1$NETLIST)
(ADE::GCD-BODY1&
 (180 10 (:DEFINITION ASSOC-EQUAL))
 (44 11 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
 (34 34 (:REWRITE DEFAULT-CAR))
 (32 21 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (32 21 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (32 21 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (22 22 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
 (21 21 (:REWRITE |(equal (- x) (- y))|))
 (18 1 (:DEFINITION ADE::DELETE-TO-EQ))
 (14 14 (:REWRITE DEFAULT-CDR))
 (13 13 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (13 13 (:REWRITE DEFAULT-*-2))
 (13 13 (:REWRITE DEFAULT-*-1))
 (11 11 (:REWRITE DEFAULT-SYMBOL-NAME))
 (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::CHECK-GCD-BODY1$NETLIST-64)
(ADE::GCD-BODY1$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-GCD-BODY1$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::GCD-BODY1$A<B)
(ADE::GCD-BODY1$DATA0-OUT)
(ADE::LEN-GCD-BODY1$DATA0-OUT
 (150 2 (:REWRITE TAKE-OF-TOO-MANY))
 (71 1 (:DEFINITION TAKE))
 (55 4 (:REWRITE |(< (if a b c) x)|))
 (53 1 (:DEFINITION ADE::V-THREEFIX))
 (42 14 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (40 13 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (39 39 (:TYPE-PRESCRIPTION ADE::GCD-BODY1$DATA-IN))
 (38 8 (:REWRITE DEFAULT-CDR))
 (35 2 (:REWRITE |(< x (if a b c))|))
 (28 2 (:DEFINITION NATP))
 (24 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (20 2 (:DEFINITION LEN))
 (19 19 (:TYPE-PRESCRIPTION ADE::FV-ADDER-OUTPUT))
 (18 18 (:TYPE-PRESCRIPTION ADE::BVP))
 (16 16 (:LINEAR LEN-WHEN-PREFIXP))
 (14 14 (:REWRITE |(< (- x) (- y))|))
 (14 9 (:REWRITE DEFAULT-+-2))
 (13 12 (:REWRITE SIMPLIFY-SUMS-<))
 (13 12 (:REWRITE DEFAULT-<-2))
 (13 4 (:REWRITE DEFAULT-CAR))
 (13 2 (:REWRITE CONSP-OF-APPEND))
 (12 12 (:REWRITE DEFAULT-<-1))
 (12 3 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (12 1 (:REWRITE ADE::FV-NOT=V-NOT))
 (12 1 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (11 1 (:REWRITE CAR-OF-APPEND))
 (10 10 (:REWRITE REDUCE-INTEGERP-+))
 (10 10 (:REWRITE INTEGERP-MINUS-X))
 (10 10 (:META META-INTEGERP-CORRECT))
 (9 9 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 9 (:REWRITE |(< (- x) 0)|))
 (9 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (9 5 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (9 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (8 8 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (8 2 (:REWRITE TAKE-WHEN-ATOM))
 (6 2 (:TYPE-PRESCRIPTION ADE::BVP-TAKE))
 (6 2 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (6 1 (:DEFINITION BINARY-APPEND))
 (5 5 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (5 5 (:REWRITE DEFAULT-*-2))
 (5 5 (:REWRITE DEFAULT-*-1))
 (5 5 (:REWRITE |(equal (- x) (- y))|))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (4 4 (:REWRITE ZP-OPEN))
 (4 3 (:REWRITE |(+ c (+ d x))|))
 (4 2 (:REWRITE |(* y x)|))
 (4 1 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (3 3 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (3 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:REWRITE |(equal (- x) 0)|))
 (3 1 (:REWRITE ADE::BVP-TAKE))
 (3 1 (:REWRITE ADE::BVP-NTHCDR))
 (3 1 (:REWRITE ADE::BVP-APPEND))
 (3 1 (:REWRITE |(* y (* x z))|))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE |(< 0 (- x))|))
 (2 2 (:REWRITE |(* a (/ a))|))
 (2 1 (:REWRITE |(< d (+ c x))|))
 (2 1 (:DEFINITION ADE::3V-FIX))
 (1 1 (:TYPE-PRESCRIPTION ADE::3VP))
 (1 1 (:REWRITE INSERT-0-*))
 (1 1 (:REWRITE |(equal (+ c x) d)|))
 (1 1 (:REWRITE |(< (+ c x) d)|))
 (1 1 (:REWRITE |(* c (* d x))|))
 )
(ADE::BVP-GCD-BODY1$DATA0-OUT
 (150 2 (:REWRITE TAKE-OF-TOO-MANY))
 (71 1 (:DEFINITION TAKE))
 (41 2 (:REWRITE |(< (if a b c) x)|))
 (35 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (35 2 (:REWRITE |(< x (if a b c))|))
 (33 6 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (33 3 (:DEFINITION NTHCDR))
 (28 2 (:DEFINITION NFIX))
 (21 1 (:REWRITE ADE::LEN-GCD-BODY1$DATA-IN))
 (18 6 (:REWRITE DEFAULT-CDR))
 (18 3 (:REWRITE ADE::NFIX-OF-NAT))
 (16 16 (:TYPE-PRESCRIPTION LEN))
 (15 3 (:REWRITE |(+ y x)|))
 (14 1 (:DEFINITION NATP))
 (11 11 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (11 11 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 1 (:DEFINITION LEN))
 (8 6 (:REWRITE DEFAULT-+-2))
 (8 2 (:REWRITE TAKE-WHEN-ATOM))
 (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 5 (:REWRITE SIMPLIFY-SUMS-<))
 (6 5 (:REWRITE DEFAULT-<-2))
 (6 1 (:DEFINITION BINARY-APPEND))
 (5 5 (:TYPE-PRESCRIPTION ADE::V-ADDER-OUTPUT))
 (5 5 (:REWRITE DEFAULT-<-1))
 (5 2 (:REWRITE DEFAULT-CAR))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 2 (:REWRITE |(* x (if a b c))|))
 (4 4 (:REWRITE ZP-OPEN))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 2 (:REWRITE |(* y x)|))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (3 3 (:REWRITE REDUCE-INTEGERP-+))
 (3 3 (:REWRITE INTEGERP-MINUS-X))
 (3 3 (:REWRITE |(< (- x) 0)|))
 (3 3 (:META META-INTEGERP-CORRECT))
 (3 1 (:REWRITE |(* y (* x z))|))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE |(* a (/ a))|))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 1 (:REWRITE |(< d (+ c x))|))
 (2 1 (:REWRITE |(+ c (+ d x))|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (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 INSERT-0-*))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< (+ c x) d)|))
 (1 1 (:REWRITE |(+ 0 x)|))
 (1 1 (:REWRITE |(* c (* d x))|))
 )
(ADE::GCD-BODY1$DATA1-OUT)
(ADE::LEN-GCD-BODY1$DATA1-OUT
 (204 4 (:REWRITE TAKE-OF-TOO-MANY))
 (142 2 (:DEFINITION TAKE))
 (99 1 (:DEFINITION ADE::V-THREEFIX))
 (72 18 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (67 6 (:REWRITE |(< (if a b c) x)|))
 (58 1 (:REWRITE CAR-OF-APPEND))
 (49 19 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (46 1 (:REWRITE CAR-OF-TAKE))
 (42 3 (:DEFINITION NATP))
 (39 9 (:REWRITE DEFAULT-CDR))
 (37 37 (:TYPE-PRESCRIPTION ADE::GCD-BODY1$DATA-IN))
 (35 2 (:REWRITE |(< x (if a b c))|))
 (29 3 (:DEFINITION LEN))
 (27 27 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (20 20 (:LINEAR LEN-WHEN-PREFIXP))
 (19 19 (:TYPE-PRESCRIPTION ADE::FV-ADDER-OUTPUT))
 (19 19 (:REWRITE |(< (- x) (- y))|))
 (18 18 (:TYPE-PRESCRIPTION ADE::BVP))
 (18 16 (:REWRITE SIMPLIFY-SUMS-<))
 (18 16 (:REWRITE DEFAULT-<-2))
 (18 11 (:REWRITE DEFAULT-+-2))
 (18 5 (:REWRITE DEFAULT-CAR))
 (17 2 (:REWRITE CONSP-OF-APPEND))
 (16 16 (:REWRITE DEFAULT-<-1))
 (13 4 (:REWRITE TAKE-WHEN-ATOM))
 (13 3 (:REWRITE CONSP-OF-TAKE))
 (12 12 (:REWRITE REDUCE-INTEGERP-+))
 (12 12 (:REWRITE INTEGERP-MINUS-X))
 (12 12 (:META META-INTEGERP-CORRECT))
 (12 1 (:REWRITE ADE::FV-NOT=V-NOT))
 (12 1 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (11 11 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (11 11 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (11 11 (:REWRITE DEFAULT-+-1))
 (11 11 (:REWRITE |(< (- x) 0)|))
 (10 10 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (9 9 (:REWRITE ZP-OPEN))
 (9 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (9 5 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (9 3 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (9 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (7 7 (:TYPE-PRESCRIPTION TRUE-LISTP-TAKE))
 (6 4 (:REWRITE |(+ c (+ d x))|))
 (6 2 (:TYPE-PRESCRIPTION ADE::BVP-TAKE))
 (6 2 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (6 1 (:DEFINITION BINARY-APPEND))
 (5 5 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (5 5 (:REWRITE DEFAULT-*-2))
 (5 5 (:REWRITE DEFAULT-*-1))
 (5 5 (:REWRITE |(equal (- x) (- y))|))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (4 2 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (4 2 (:REWRITE |(< d (+ c x))|))
 (4 2 (:REWRITE |(* y x)|))
 (4 1 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 (3 3 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (3 3 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:REWRITE |(equal (- x) 0)|))
 (3 1 (:REWRITE ADE::BVP-TAKE))
 (3 1 (:REWRITE ADE::BVP-NTHCDR))
 (3 1 (:REWRITE ADE::BVP-APPEND))
 (3 1 (:REWRITE |(* y (* x z))|))
 (2 2 (:TYPE-PRESCRIPTION ZP))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE |(< 0 (- x))|))
 (2 2 (:REWRITE |(< (+ c x) d)|))
 (2 2 (:REWRITE |(* a (/ a))|))
 (2 1 (:DEFINITION ADE::3V-FIX))
 (1 1 (:TYPE-PRESCRIPTION ADE::3VP))
 (1 1 (:REWRITE INSERT-0-*))
 (1 1 (:REWRITE |(equal (+ c x) d)|))
 (1 1 (:REWRITE |(* c (* d x))|))
 )
(ADE::BVP-GCD-BODY1$DATA1-OUT
 (204 4 (:REWRITE TAKE-OF-TOO-MANY))
 (142 2 (:DEFINITION TAKE))
 (64 10 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (55 4 (:REWRITE |(< (if a b c) x)|))
 (42 3 (:DEFINITION NFIX))
 (42 2 (:REWRITE ADE::LEN-GCD-BODY1$DATA-IN))
 (41 11 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (39 1 (:REWRITE ADE::V-NOT-TAKE))
 (35 2 (:REWRITE |(< x (if a b c))|))
 (32 32 (:TYPE-PRESCRIPTION LEN))
 (20 5 (:REWRITE ADE::NFIX-OF-NAT))
 (18 2 (:DEFINITION LEN))
 (17 17 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (17 17 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (15 6 (:REWRITE DEFAULT-CDR))
 (14 1 (:DEFINITION NATP))
 (13 4 (:REWRITE TAKE-WHEN-ATOM))
 (11 11 (:REWRITE |(< (- x) (- y))|))
 (11 7 (:REWRITE DEFAULT-+-2))
 (11 1 (:DEFINITION NTHCDR))
 (10 8 (:REWRITE SIMPLIFY-SUMS-<))
 (10 8 (:REWRITE DEFAULT-<-2))
 (10 4 (:REWRITE |(* x (if a b c))|))
 (9 3 (:REWRITE DEFAULT-CAR))
 (8 8 (:REWRITE DEFAULT-<-1))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (7 7 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (7 7 (:REWRITE NORMALIZE-ADDENDS))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 1 (:DEFINITION BINARY-APPEND))
 (5 5 (:TYPE-PRESCRIPTION ADE::V-ADDER-OUTPUT))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (5 1 (:REWRITE |(+ y x)|))
 (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))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 2 (:REWRITE |(< d (+ c x))|))
 (4 2 (:REWRITE |(+ c (+ d x))|))
 (4 2 (:REWRITE |(* y x)|))
 (3 3 (:TYPE-PRESCRIPTION NFIX))
 (3 3 (:REWRITE ZP-OPEN))
 (3 1 (:REWRITE |(* y (* x z))|))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE |(< 0 (- x))|))
 (2 2 (:REWRITE |(< (+ c x) d)|))
 (2 2 (:REWRITE |(+ 0 x)|))
 (2 2 (:REWRITE |(* a (/ a))|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE INSERT-0-*))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(* c (* d x))|))
 )
(ADE::GCD-BODY1$ME-INPUTS
 (67 29 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (43 29 (:TYPE-PRESCRIPTION BINARY-APPEND))
 )
(ADE::GCD-BODY1$ACT)
(ADE::GCD-BODY1$ACT-INACTIVE
 (64 48 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (64 48 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (54 9 (:DEFINITION BINARY-APPEND))
 (52 52 (:REWRITE NTH-WHEN-PREFIXP))
 (48 3 (:REWRITE ADE::NFIX-OF-NAT))
 (45 18 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (43 21 (:REWRITE DEFAULT-CAR))
 (42 3 (:DEFINITION NATP))
 (41 41 (:TYPE-PRESCRIPTION ADE::GCD-BODY1$DATA0-OUT))
 (32 16 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (16 16 (:TYPE-PRESCRIPTION ADE::GCD-BODY1$A<B))
 (12 12 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (12 12 (:REWRITE NORMALIZE-ADDENDS))
 (12 12 (:REWRITE DEFAULT-+-2))
 (12 12 (:REWRITE DEFAULT-+-1))
 (10 10 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (10 10 (:REWRITE DEFAULT-*-2))
 (10 10 (:REWRITE DEFAULT-*-1))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (8 8 (:REWRITE SIMPLIFY-SUMS-<))
 (8 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (8 8 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (8 8 (:REWRITE REDUCE-INTEGERP-+))
 (8 8 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (8 8 (:REWRITE INTEGERP-MINUS-X))
 (8 8 (:REWRITE DEFAULT-<-2))
 (8 8 (:REWRITE DEFAULT-<-1))
 (8 8 (:REWRITE |(< (- x) 0)|))
 (8 8 (:REWRITE |(< (- x) (- y))|))
 (8 8 (:META META-INTEGERP-CORRECT))
 (5 5 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (5 5 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (5 5 (:REWRITE |(equal (- x) (- y))|))
 (3 3 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::GCD-BODY1$DATA-OUT)
(ADE::LEN-GCD-BODY1$DATA-OUT
 (17 2 (:REWRITE ADE::NFIX-OF-NAT))
 (14 1 (:DEFINITION NATP))
 (6 1 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (3 3 (:TYPE-PRESCRIPTION ADE::GCD-BODY1$A<B))
 (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 (:TYPE-PRESCRIPTION BOOLEANP))
 (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))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::BVP-GCD-BODY1$DATA-OUT
 (150 2 (:REWRITE TAKE-OF-TOO-MANY))
 (71 1 (:DEFINITION TAKE))
 (41 2 (:REWRITE |(< (if a b c) x)|))
 (38 10 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (36 9 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (35 5 (:REWRITE ADE::NFIX-OF-NAT))
 (35 2 (:REWRITE |(< x (if a b c))|))
 (28 2 (:DEFINITION NATP))
 (21 1 (:REWRITE ADE::LEN-GCD-BODY1$DATA-IN))
 (15 2 (:REWRITE REV-WHEN-NOT-CONSP))
 (14 14 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (14 14 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (11 1 (:DEFINITION NTHCDR))
 (10 10 (:REWRITE |(< (- x) (- y))|))
 (9 8 (:REWRITE SIMPLIFY-SUMS-<))
 (9 8 (:REWRITE DEFAULT-<-2))
 (9 3 (:REWRITE DEFAULT-CDR))
 (9 1 (:DEFINITION LEN))
 (8 8 (:REWRITE DEFAULT-<-1))
 (8 2 (:REWRITE TAKE-WHEN-ATOM))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (6 6 (:REWRITE REDUCE-INTEGERP-+))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (6 6 (:REWRITE |(< (- x) 0)|))
 (6 6 (:META META-INTEGERP-CORRECT))
 (6 4 (:REWRITE DEFAULT-+-2))
 (5 1 (:REWRITE CONSP-OF-TAKE))
 (5 1 (:REWRITE |(+ y x)|))
 (4 4 (:REWRITE ZP-OPEN))
 (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))
 (4 2 (:REWRITE |(* y x)|))
 (4 1 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 (3 1 (:REWRITE |(* y (* x z))|))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE |(* a (/ a))|))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 1 (:REWRITE |(< d (+ c x))|))
 (2 1 (:REWRITE |(+ c (+ d x))|))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE INSERT-0-*))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< (+ c x) d)|))
 (1 1 (:REWRITE |(+ 0 x)|))
 (1 1 (:REWRITE |(* c (* d x))|))
 )
(ADE::LIST-OF-SINGLETON
 (54 18 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (45 45 (:REWRITE DEFAULT-CDR))
 (38 24 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (38 24 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (38 24 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (36 36 (:TYPE-PRESCRIPTION ADE::BVP))
 (34 34 (:LINEAR LEN-WHEN-PREFIXP))
 (31 16 (:REWRITE DEFAULT-+-2))
 (24 24 (:REWRITE |(equal (- x) (- y))|))
 (21 21 (:REWRITE DEFAULT-CAR))
 (17 17 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (16 16 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (16 16 (:REWRITE NORMALIZE-ADDENDS))
 (16 16 (:REWRITE DEFAULT-+-1))
 (11 11 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (11 11 (:REWRITE |(equal (- x) 0)|))
 )
(ADE::GCD-BODY1$VALUE
 (2238 193 (:DEFINITION BINARY-APPEND))
 (625 154 (:REWRITE CONSP-OF-TAKE))
 (587 121 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (577 346 (:REWRITE DEFAULT-+-2))
 (570 50 (:REWRITE ADE::CAR-V-THREEFIX))
 (497 109 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (432 54 (:REWRITE CAR-OF-APPEND))
 (399 83 (:REWRITE ADE::DISJOINT-ATOM))
 (390 15 (:REWRITE ZP-OPEN))
 (372 118 (:REWRITE CAR-OF-TAKE))
 (346 346 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (346 346 (:REWRITE DEFAULT-+-1))
 (344 215 (:REWRITE TAKE-WHEN-ATOM))
 (315 45 (:REWRITE |(+ y (+ x z))|))
 (306 64 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (269 4 (:DEFINITION SUBSETP-EQUAL))
 (266 46 (:REWRITE ADE::V-THREEFIX-BVP))
 (264 116 (:TYPE-PRESCRIPTION ADE::BVP-TAKE))
 (254 34 (:REWRITE ADE::FV-<=V-<))
 (234 10 (:REWRITE ADE::MERGE$ACT-INACTIVE))
 (228 70 (:REWRITE ADE::FV-NOT=V-NOT))
 (216 70 (:REWRITE ADE::FV-ADDER=V-ADDER))
 (188 16 (:REWRITE ADE::BVP-APPEND))
 (173 121 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (152 152 (:REWRITE ADE::NTHCDR-OF-POS-CONST-IDX))
 (144 48 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (134 70 (:REWRITE REV-WHEN-NOT-CONSP))
 (121 121 (:REWRITE |(equal (- x) (- y))|))
 (119 4 (:DEFINITION MEMBER-EQUAL))
 (118 118 (:TYPE-PRESCRIPTION NFIX))
 (118 78 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (118 78 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (104 48 (:REWRITE ADE::BVP-TAKE))
 (100 50 (:DEFINITION ADE::3V-FIX))
 (100 20 (:TYPE-PRESCRIPTION ADE::BVP-REV))
 (100 10 (:REWRITE ADE::BVP-REV))
 (95 95 (:REWRITE DEFAULT-UNARY-MINUS))
 (90 90 (:TYPE-PRESCRIPTION PAIRLIS$))
 (88 44 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (88 4 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (84 28 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (75 25 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (70 70 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (70 70 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (70 70 (:REWRITE |(< (- x) (- y))|))
 (63 63 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (63 63 (:REWRITE DEFAULT-*-2))
 (63 63 (:REWRITE DEFAULT-*-1))
 (56 14 (:DEFINITION TRUE-LISTP))
 (54 54 (:REWRITE |(- (- x))|))
 (51 49 (:REWRITE SIMPLIFY-SUMS-<))
 (51 49 (:REWRITE DEFAULT-<-1))
 (50 50 (:TYPE-PRESCRIPTION ADE::3VP))
 (49 49 (:REWRITE DEFAULT-<-2))
 (49 5 (:REWRITE ADE::MERGE$ACT1-INACTIVE))
 (46 22 (:REWRITE ADE::BVP-NTHCDR))
 (44 44 (:LINEAR LEN-WHEN-PREFIXP))
 (43 42 (:REWRITE |(equal (+ c x) d)|))
 (42 12 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (40 4 (:REWRITE ADE::MERGE$ACT0-INACTIVE))
 (40 4 (:REWRITE ADE::FV-ADDER-OUTPUT=V-ADDER-OUTPUT))
 (39 5 (:REWRITE ADE::DISJOINT-CONS))
 (30 30 (:REWRITE |(< 0 (- x))|))
 (22 22 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (17 1 (:REWRITE ADE::GCD-BODY1$ACT-INACTIVE))
 (15 15 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (15 15 (:REWRITE |(< d (+ c x))|))
 (13 13 (:REWRITE FOLD-CONSTS-IN-+))
 (12 12 (:TYPE-PRESCRIPTION BOOLEANP))
 (12 12 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (12 12 (:REWRITE DEFAULT-UNARY-/))
 (12 12 (:REWRITE |(equal (+ c x y) d)|))
 (12 8 (:REWRITE CONSP-OF-APPEND))
 (12 4 (:REWRITE CONSP-OF-REV))
 (9 9 (:TYPE-PRESCRIPTION NATP))
 (9 9 (:DEFINITION NATP))
 (8 8 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (8 8 (:REWRITE DEFAULT-SYMBOL-NAME))
 (7 7 (:REWRITE REDUCE-INTEGERP-+))
 (7 7 (:REWRITE INTEGERP-MINUS-X))
 (7 7 (:META META-INTEGERP-CORRECT))
 (6 6 (:REWRITE |(equal (+ d x) (+ c y))|))
 (6 6 (:REWRITE |(equal (+ c x) (+ d y))|))
 )