(ADE::GCD3$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::GCD3$INS-LEN)
(ADE::GCD3*)
(ADE::GCD3*$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-GCD3
 (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::GCD3$NETLIST)
(ADE::GCD3&
 (252 14 (:DEFINITION ASSOC-EQUAL))
 (60 15 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
 (46 46 (:REWRITE DEFAULT-CAR))
 (44 29 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (44 29 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (44 29 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (30 30 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
 (29 29 (:REWRITE |(equal (- x) (- y))|))
 (18 18 (:REWRITE DEFAULT-CDR))
 (18 1 (:DEFINITION ADE::DELETE-TO-EQ))
 (15 15 (:REWRITE DEFAULT-SYMBOL-NAME))
 (12 12 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (12 12 (:REWRITE DEFAULT-*-2))
 (12 12 (:REWRITE DEFAULT-*-1))
 (6 6 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:META META-INTEGERP-CORRECT))
 )
(ADE::CHECK-GCD3$NETLIST-64-7)
(ADE::GCD3$ST-FORMAT)
(ADE::GCD3$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))
 (5 5 (:REWRITE SIMPLIFY-SUMS-<))
 (5 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (5 5 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (5 5 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (5 5 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (5 5 (:REWRITE DEFAULT-<-2))
 (5 5 (:REWRITE DEFAULT-<-1))
 (5 5 (:REWRITE |(< (- x) (- y))|))
 (3 3 (:REWRITE REDUCE-INTEGERP-+))
 (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 INTEGERP-MINUS-X))
 (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 3 (:META META-INTEGERP-CORRECT))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE |(< (- x) 0)|))
 )
(ADE::GCD3$VALID-ST)
(ADE::GCD3$VALID-ST=>CONSTRAINT
 (65 65 (:REWRITE SIMPLIFY-SUMS-<))
 (65 65 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (65 65 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (65 65 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (65 65 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (65 65 (:REWRITE DEFAULT-<-2))
 (65 65 (:REWRITE DEFAULT-<-1))
 (65 65 (:REWRITE |(< (- x) (- y))|))
 (48 48 (:REWRITE REDUCE-INTEGERP-+))
 (48 48 (:REWRITE INTEGERP-MINUS-X))
 (48 48 (:META META-INTEGERP-CORRECT))
 (32 32 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (32 32 (:REWRITE |(< (- x) 0)|))
 (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 NTH-WHEN-PREFIXP))
 (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))
 (3 3 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (3 3 (:REWRITE DEFAULT-*-2))
 (3 3 (:REWRITE DEFAULT-*-1))
 )
(ADE::GCD3$VALID-ST=>ST-FORMAT
 (128 128 (:REWRITE NTH-WHEN-PREFIXP))
 (104 52 (:REWRITE DEFAULT-+-2))
 (56 56 (:REWRITE DEFAULT-CDR))
 (52 52 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (52 52 (:REWRITE NORMALIZE-ADDENDS))
 (52 52 (:REWRITE DEFAULT-+-1))
 (51 51 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (51 51 (:REWRITE DEFAULT-*-2))
 (51 51 (:REWRITE DEFAULT-*-1))
 (20 16 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (20 16 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (20 16 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (17 17 (:REWRITE SIMPLIFY-SUMS-<))
 (17 17 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (17 17 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (17 17 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (17 17 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (17 17 (:REWRITE DEFAULT-<-2))
 (17 17 (:REWRITE DEFAULT-<-1))
 (17 17 (:REWRITE |(< (- x) (- y))|))
 (16 16 (:REWRITE |(equal (- x) (- y))|))
 (12 3 (:DEFINITION STRIP-CARS))
 (7 7 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 )
(ADE::GCD3$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-GCD3$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::GCD3$ME-INPUTS)
(ADE::GCD3$BR-INPUTS
 (1 1 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::GCD3$BODY-INPUTS
 (2 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::GCD3$IN-ACT)
(ADE::GCD3$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::GCD3$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::GCD3$OUT-ACT)
(ADE::GCD3$OUT-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))
 (30 2 (:DEFINITION NTHCDR))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (18 9 (:REWRITE DEFAULT-CAR))
 (18 2 (:DEFINITION LEN))
 (16 8 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (14 1 (:DEFINITION NATP))
 (13 13 (:REWRITE NTH-WHEN-PREFIXP))
 (12 1 (:DEFINITION BINARY-APPEND))
 (10 10 (:TYPE-PRESCRIPTION BOOLEANP))
 (10 8 (:REWRITE DEFAULT-+-2))
 (10 6 (:REWRITE SIMPLIFY-SUMS-<))
 (10 6 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (10 6 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (10 4 (:REWRITE ADE::F-GATES=B-GATES))
 (10 2 (:REWRITE |(+ y x)|))
 (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 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (8 8 (:REWRITE NORMALIZE-ADDENDS))
 (8 8 (:REWRITE DEFAULT-+-1))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (7 7 (:REWRITE DEFAULT-CDR))
 (7 6 (:REWRITE DEFAULT-<-2))
 (7 1 (:REWRITE TAKE-WHEN-ATOM))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 6 (:TYPE-PRESCRIPTION ADE::3VP))
 (6 6 (:REWRITE |(< (- x) (- y))|))
 (6 2 (:REWRITE ADE::V-THREEFIX-BVP))
 (6 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (5 5 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (5 5 (:TYPE-PRESCRIPTION STRIP-CARS))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 2 (:DEFINITION ADE::3V-FIX))
 (4 1 (:DEFINITION STRIP-CARS))
 (3 3 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NFIX))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::GCD3$DATA-OUT)
(ADE::LEN-GCD3$DATA-OUT-1
 (21 3 (:DEFINITION LEN))
 (9 1 (:REWRITE ADE::NFIX-OF-NAT))
 (7 7 (:REWRITE NTH-WHEN-PREFIXP))
 (7 1 (:DEFINITION NATP))
 (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 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:META META-INTEGERP-CORRECT))
 (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))|))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (1 1 (:REWRITE |(< (- x) 0)|))
 )
(ADE::LEN-GCD3$DATA-OUT-2
 (144 16 (:REWRITE ADE::NFIX-OF-NAT))
 (112 16 (:DEFINITION NATP))
 (64 64 (:REWRITE REDUCE-INTEGERP-+))
 (64 64 (:REWRITE INTEGERP-MINUS-X))
 (64 64 (:META META-INTEGERP-CORRECT))
 (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))
 (17 17 (:REWRITE SIMPLIFY-SUMS-<))
 (17 17 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (17 17 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (17 17 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (17 17 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (17 17 (:REWRITE DEFAULT-<-2))
 (17 17 (:REWRITE DEFAULT-<-1))
 (17 17 (:REWRITE |(< (- x) (- y))|))
 (16 16 (:TYPE-PRESCRIPTION NATP))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (16 16 (:REWRITE NTH-WHEN-PREFIXP))
 (16 16 (:REWRITE |(equal (- x) (- y))|))
 (16 16 (:REWRITE |(< (- x) 0)|))
 (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-GCD3$DATA-OUT
 (2012 32 (:REWRITE TAKE-OF-TOO-MANY))
 (1020 24 (:REWRITE ADE::LEN-NTHCDR))
 (608 16 (:REWRITE |(< x (if a b c))|))
 (568 48 (:DEFINITION NTHCDR))
 (440 40 (:REWRITE |(+ (+ x y) z)|))
 (384 192 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (384 32 (:REWRITE |(+ (if a b c) x)|))
 (279 111 (:REWRITE DEFAULT-CAR))
 (272 272 (:REWRITE NTH-WHEN-PREFIXP))
 (260 192 (:REWRITE DEFAULT-+-2))
 (260 52 (:REWRITE |(+ y x)|))
 (245 93 (:REWRITE SIMPLIFY-SUMS-<))
 (192 192 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (192 192 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (192 192 (:REWRITE DEFAULT-+-1))
 (192 24 (:DEFINITION BINARY-APPEND))
 (188 32 (:REWRITE TAKE-WHEN-ATOM))
 (184 184 (:REWRITE DEFAULT-CDR))
 (157 93 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (129 89 (:REWRITE DEFAULT-<-1))
 (128 128 (:LINEAR LEN-WHEN-PREFIXP))
 (120 48 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (113 113 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (113 113 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (113 89 (:REWRITE DEFAULT-<-2))
 (112 16 (:DEFINITION NATP))
 (108 27 (:DEFINITION STRIP-CARS))
 (97 97 (:REWRITE |(< (- x) (- y))|))
 (96 16 (:REWRITE ADE::GCD3$OUT-ACT-INACTIVE))
 (88 40 (:REWRITE ADE::F-GATES=B-GATES))
 (84 4 (:REWRITE ADE::NTHCDR-APPEND))
 (80 80 (:TYPE-PRESCRIPTION BOOLEANP))
 (80 8 (:DEFINITION ADE::V-THREEFIX))
 (68 4 (:REWRITE LEN-OF-APPEND))
 (64 64 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (56 40 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (56 40 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (56 40 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (56 8 (:REWRITE ADE::CAR-V-THREEFIX))
 (48 48 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (48 48 (:TYPE-PRESCRIPTION ADE::3VP))
 (48 48 (:REWRITE REDUCE-INTEGERP-+))
 (48 48 (:REWRITE INTEGERP-MINUS-X))
 (48 48 (:META META-INTEGERP-CORRECT))
 (48 16 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (48 16 (:REWRITE ADE::F-BUF-OF-3VP))
 (43 43 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (43 43 (:REWRITE DEFAULT-*-2))
 (43 43 (:REWRITE DEFAULT-*-1))
 (40 40 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (40 40 (:REWRITE |(equal (- x) (- y))|))
 (40 4 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (32 32 (:TYPE-PRESCRIPTION NFIX))
 (32 16 (:DEFINITION ADE::3V-FIX))
 (24 24 (:REWRITE |(< d (+ c x))|))
 (24 4 (:REWRITE |(+ y (+ x z))|))
 (16 16 (:TYPE-PRESCRIPTION NATP))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (16 16 (:REWRITE |(< (- x) 0)|))
 (12 12 (:REWRITE |(* (- x) y)|))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (8 8 (:REWRITE DEFAULT-UNARY-/))
 (8 8 (:REWRITE CDR-CONS))
 (8 8 (:REWRITE |(< 0 (- x))|))
 (8 8 (:REWRITE |(* c (* d x))|))
 (8 4 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (4 4 (:REWRITE |(< 0 (* x y))|))
 (4 4 (:DEFINITION ADE::GCD-COND$BR-INPUTS))
 (4 4 (:DEFINITION ADE::BRANCH$ACT0))
 )
(ADE::GCD3$OUTPUTS)
(ADE::GCD3$VALUE
 (1672 243 (:DEFINITION BINARY-APPEND))
 (692 382 (:REWRITE DEFAULT-+-2))
 (382 382 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (382 382 (:REWRITE DEFAULT-+-1))
 (306 102 (:REWRITE ADE::CAR-V-THREEFIX))
 (238 20 (:REWRITE LEN-OF-APPEND))
 (229 78 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (204 102 (:DEFINITION ADE::3V-FIX))
 (197 92 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (197 92 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (197 92 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (195 195 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (191 191 (:TYPE-PRESCRIPTION PAIRLIS$))
 (178 140 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (178 140 (:REWRITE ADE::F-BUF-OF-3VP))
 (172 68 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (170 33 (:REWRITE ADE::DISJOINT-ATOM))
 (140 140 (:TYPE-PRESCRIPTION ADE::3VP))
 (128 8 (:REWRITE ADE::MERGE$ACT-INACTIVE))
 (121 10 (:REWRITE ADE::MERGE$ACT1-INACTIVE))
 (117 89 (:REWRITE ADE::V-THREEFIX-BVP))
 (92 92 (:TYPE-PRESCRIPTION POSP))
 (92 92 (:REWRITE |(equal (- x) (- y))|))
 (92 92 (:DEFINITION STRIP-CARS))
 (92 2 (:REWRITE ADE::GCD-COND$ACT-INACTIVE))
 (89 4 (:REWRITE ADE::GCD-COND$ACT0-INACTIVE))
 (81 1 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-WHEN-DISJOINT))
 (78 3 (:REWRITE ADE::MERGE$ACT0-INACTIVE))
 (67 4 (:REWRITE ADE::GCD-BODY3$OUT-ACT-INACTIVE))
 (60 20 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (60 2 (:REWRITE ADE::GCD-COND$ACT1-INACTIVE))
 (56 56 (:TYPE-PRESCRIPTION ADE::F-OR))
 (56 1 (:REWRITE ADE::LEN-NTHCDR))
 (55 5 (:REWRITE |(+ y (+ x z))|))
 (53 14 (:REWRITE TAKE-WHEN-ATOM))
 (50 50 (:LINEAR LEN-WHEN-PREFIXP))
 (44 33 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (44 33 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (43 43 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (43 43 (:REWRITE DEFAULT-*-2))
 (43 43 (:REWRITE DEFAULT-*-1))
 (39 13 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (36 3 (:REWRITE |(< (if a b c) x)|))
 (35 5 (:DEFINITION NATP))
 (30 3 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (30 3 (:DEFINITION ATOM))
 (25 25 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (25 13 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (21 3 (:REWRITE ADE::GCD-BODY3$IN-ACT-INACTIVE))
 (21 3 (:REWRITE CAR-OF-APPEND))
 (21 1 (:DEFINITION SUBSETP-EQUAL))
 (20 5 (:REWRITE |(+ x x)|))
 (19 19 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (19 19 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (18 3 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM-NAMES))
 (16 16 (:REWRITE REDUCE-INTEGERP-+))
 (16 16 (:REWRITE INTEGERP-MINUS-X))
 (16 16 (:META META-INTEGERP-CORRECT))
 (16 2 (:REWRITE ADE::STRIP-CARS-PAIRLIS$))
 (15 15 (:REWRITE SIMPLIFY-SUMS-<))
 (15 15 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (15 15 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (15 15 (:REWRITE DEFAULT-<-2))
 (15 15 (:REWRITE DEFAULT-<-1))
 (15 15 (:REWRITE |(< (- x) (- y))|))
 (11 2 (:REWRITE |(+ (+ x y) z)|))
 (10 10 (:TYPE-PRESCRIPTION ADE::GCD3$DATA-IN))
 (10 1 (:REWRITE ADE::GCD3$OUT-ACT-INACTIVE))
 (8 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (7 1 (:REWRITE ADE::MEMBER-APPEND))
 (6 6 (:TYPE-PRESCRIPTION ADE::GCD-COND$DATA1-OUT))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (6 6 (:REWRITE |(< (- x) 0)|))
 (6 2 (:REWRITE |(equal (if a b c) x)|))
 (5 5 (:TYPE-PRESCRIPTION NATP))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (5 5 (:REWRITE DEFAULT-SYMBOL-NAME))
 (5 5 (:REWRITE |(< 0 (- x))|))
 (4 4 (:REWRITE ADE::GCD-BODY3$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (4 1 (:REWRITE ADE::GCD3$IN-ACT-INACTIVE))
 (4 1 (:DEFINITION MEMBER-EQUAL))
 (2 2 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (2 1 (:REWRITE |(- (if a b c))|))
 (1 1 (:REWRITE |(< x (if a b c))|))
 )
(ADE::GCD3$STEP
 (12 12 (:TYPE-PRESCRIPTION ADE::GCD-BODY3$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-GCD-BODY3$OUT-ACT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-GCD-BODY3$IN-ACT))
 )
(ADE::GCD3$STATE
 (4594 668 (:DEFINITION BINARY-APPEND))
 (1423 791 (:REWRITE DEFAULT-+-2))
 (1125 375 (:REWRITE ADE::CAR-V-THREEFIX))
 (791 791 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (791 791 (:REWRITE DEFAULT-+-1))
 (750 375 (:DEFINITION ADE::3V-FIX))
 (561 187 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (503 457 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (503 457 (:REWRITE ADE::F-BUF-OF-3VP))
 (498 498 (:TYPE-PRESCRIPTION PAIRLIS$))
 (477 40 (:REWRITE LEN-OF-APPEND))
 (421 421 (:TYPE-PRESCRIPTION ADE::3VP))
 (400 400 (:DEFINITION STRIP-CARS))
 (361 331 (:REWRITE ADE::V-THREEFIX-BVP))
 (341 130 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (320 64 (:REWRITE ADE::DISJOINT-ATOM))
 (294 140 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (270 140 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (270 140 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (263 263 (:TYPE-PRESCRIPTION POSP))
 (250 25 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (230 230 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (204 85 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (175 25 (:REWRITE CAR-OF-APPEND))
 (164 91 (:REWRITE TAKE-WHEN-ATOM))
 (154 12 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-WHEN-DISJOINT))
 (140 140 (:REWRITE |(equal (- x) (- y))|))
 (139 34 (:REWRITE ADE::GCD-BODY3$OUT-ACT-INACTIVE))
 (135 29 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM-NAMES))
 (120 12 (:REWRITE |(+ y (+ x z))|))
 (118 2 (:DEFINITION SUBSETP-EQUAL))
 (104 2 (:REWRITE ADE::MEMBER-APPEND))
 (103 4 (:REWRITE ADE::MERGE$ACT1-INACTIVE))
 (100 100 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
 (94 4 (:DEFINITION MEMBER-EQUAL))
 (90 3 (:REWRITE ADE::MERGE$ACT0-INACTIVE))
 (73 73 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (73 73 (:REWRITE DEFAULT-*-2))
 (73 73 (:REWRITE DEFAULT-*-1))
 (70 2 (:REWRITE ADE::MERGE$ACT-INACTIVE))
 (64 64 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (64 64 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (56 26 (:REWRITE ADE::GCD-BODY3$IN-ACT-INACTIVE))
 (56 1 (:REWRITE ADE::LEN-NTHCDR))
 (53 8 (:REWRITE ADE::GCD-COND$ACT-INACTIVE))
 (40 10 (:REWRITE |(+ x x)|))
 (39 13 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (37 8 (:REWRITE ADE::GCD-COND$ACT1-INACTIVE))
 (36 12 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (34 34 (:REWRITE ADE::GCD-BODY3$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (34 34 (:LINEAR LEN-WHEN-PREFIXP))
 (34 7 (:REWRITE ADE::GCD-COND$ACT0-INACTIVE))
 (32 4 (:REWRITE ADE::STRIP-CARS-PAIRLIS$))
 (28 4 (:DEFINITION NATP))
 (25 25 (:REWRITE DEFAULT-UNARY-MINUS))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (24 24 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (18 18 (:REWRITE |(< (- x) (- y))|))
 (18 1 (:REWRITE |(equal (if a b c) x)|))
 (17 17 (:TYPE-PRESCRIPTION ADE::GCD-COND$DATA0-OUT))
 (17 17 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (15 15 (:REWRITE SIMPLIFY-SUMS-<))
 (15 15 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (15 15 (:REWRITE DEFAULT-<-2))
 (15 15 (:REWRITE DEFAULT-<-1))
 (13 13 (:REWRITE REDUCE-INTEGERP-+))
 (13 13 (:REWRITE INTEGERP-MINUS-X))
 (13 13 (:META META-INTEGERP-CORRECT))
 (11 2 (:REWRITE |(+ (+ x y) z)|))
 (9 3 (:REWRITE ADE::BOOLEANP-GCD-BODY3$OUT-ACT))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (8 8 (:REWRITE |(< 0 (- x))|))
 (6 6 (:TYPE-PRESCRIPTION ADE::SE))
 (6 6 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (6 6 (:REWRITE DEFAULT-UNARY-/))
 (5 5 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (5 5 (:REWRITE ADE::LEN-GCD-BODY3$DATA-OUT-2))
 (5 5 (:REWRITE |(< (- x) 0)|))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (3 3 (:REWRITE DEFAULT-SYMBOL-NAME))
 (3 1 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (2 1 (:REWRITE |(- (if a b c))|))
 (1 1 (:REWRITE CONSP-OF-APPEND))
 (1 1 (:REWRITE |(< x (if a b c))|))
 )
(ADE::GCD3$INPUT-FORMAT)
(ADE::GCD3$INPUT-FORMAT=>BODY$INPUT-FORMAT
 (4768 128 (:REWRITE TAKE-OF-TOO-MANY))
 (1728 32 (:DEFINITION TAKE))
 (1040 50 (:REWRITE ADE::LEN-NTHCDR))
 (944 112 (:REWRITE TAKE-WHEN-ATOM))
 (683 415 (:REWRITE DEFAULT-+-2))
 (657 203 (:REWRITE SIMPLIFY-SUMS-<))
 (633 441 (:REWRITE DEFAULT-CDR))
 (444 50 (:DEFINITION BINARY-APPEND))
 (440 176 (:REWRITE DEFAULT-CAR))
 (415 415 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (415 415 (:REWRITE DEFAULT-+-1))
 (321 203 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (295 295 (:REWRITE NTH-WHEN-PREFIXP))
 (267 187 (:REWRITE DEFAULT-<-2))
 (255 33 (:DEFINITION NTHCDR))
 (239 239 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (239 239 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (236 236 (:LINEAR LEN-WHEN-PREFIXP))
 (225 187 (:REWRITE DEFAULT-<-1))
 (219 219 (:REWRITE |(< (- x) (- y))|))
 (202 100 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (192 32 (:REWRITE CONSP-OF-APPEND))
 (187 17 (:REWRITE |(+ (+ x y) z)|))
 (178 50 (:REWRITE |(< d (+ c x))|))
 (168 24 (:REWRITE ADE::CAR-V-THREEFIX))
 (160 16 (:DEFINITION ADE::V-THREEFIX))
 (152 38 (:DEFINITION STRIP-CARS))
 (128 128 (:TYPE-PRESCRIPTION NFIX))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (119 119 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (119 119 (:REWRITE DEFAULT-*-2))
 (119 119 (:REWRITE DEFAULT-*-1))
 (118 118 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (96 16 (:REWRITE |(+ y (+ x z))|))
 (80 40 (:DEFINITION ADE::3V-FIX))
 (64 64 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (64 64 (:REWRITE |(< 0 (- x))|))
 (64 64 (:REWRITE |(* (- x) y)|))
 (46 36 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (46 36 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (46 36 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (40 40 (:TYPE-PRESCRIPTION ADE::3VP))
 (38 8 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (36 36 (:REWRITE |(equal (- x) (- y))|))
 (32 32 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (32 32 (:REWRITE DEFAULT-UNARY-/))
 (32 32 (:REWRITE CONSP-OF-TAKE))
 (32 32 (:REWRITE |(< 0 (* x y))|))
 (32 32 (:REWRITE |(* c (* d x))|))
 (28 4 (:DEFINITION TRUE-LISTP))
 (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-GCD3$IN-ACT
 (1904 32 (:REWRITE TAKE-OF-TOO-MANY))
 (1024 34 (:REWRITE ADE::LEN-NTHCDR))
 (527 527 (:REWRITE NTH-WHEN-PREFIXP))
 (492 66 (:DEFINITION BINARY-APPEND))
 (464 224 (:REWRITE DEFAULT-CAR))
 (415 37 (:DEFINITION NTHCDR))
 (330 132 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (269 245 (:REWRITE DEFAULT-CDR))
 (247 163 (:REWRITE DEFAULT-+-2))
 (231 21 (:REWRITE |(+ (+ x y) z)|))
 (224 32 (:REWRITE TAKE-WHEN-ATOM))
 (163 163 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (163 163 (:REWRITE DEFAULT-+-1))
 (162 162 (:TYPE-PRESCRIPTION STRIP-CARS))
 (160 16 (:DEFINITION ADE::V-THREEFIX))
 (153 83 (:REWRITE SIMPLIFY-SUMS-<))
 (153 83 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (153 83 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (152 38 (:DEFINITION STRIP-CARS))
 (140 140 (:LINEAR LEN-WHEN-PREFIXP))
 (121 83 (:REWRITE DEFAULT-<-1))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (115 83 (: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))
 (95 95 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (87 87 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (86 26 (:REWRITE |(< d (+ c x))|))
 (84 4 (:DEFINITION POSP))
 (83 83 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (83 83 (:REWRITE DEFAULT-*-2))
 (83 83 (:REWRITE DEFAULT-*-1))
 (83 83 (:REWRITE |(< (- x) (- y))|))
 (82 82 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (80 4 (:REWRITE ZP-OPEN))
 (70 70 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (64 64 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (64 32 (:REWRITE ADE::GCD3$IN-ACT-INACTIVE))
 (64 32 (:DEFINITION ADE::3V-FIX))
 (48 8 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (46 36 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (46 36 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (46 36 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (38 8 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (36 36 (:REWRITE |(equal (- x) (- y))|))
 (32 32 (:TYPE-PRESCRIPTION NFIX))
 (28 4 (:DEFINITION TRUE-LISTP))
 (22 22 (:META META-INTEGERP-CORRECT))
 (16 8 (:REWRITE ADE::BOOLEANP-OF-F-BUF))
 (14 14 (:REWRITE REDUCE-INTEGERP-+))
 (14 14 (:REWRITE INTEGERP-MINUS-X))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (: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-GCD3$OUT-ACT
 (1680 24 (:DEFINITION TAKE))
 (1151 121 (:DEFINITION NTHCDR))
 (925 199 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (851 851 (:REWRITE NTH-WHEN-PREFIXP))
 (847 575 (:REWRITE DEFAULT-+-2))
 (729 585 (:REWRITE DEFAULT-CDR))
 (715 65 (:REWRITE |(+ (+ x y) z)|))
 (636 300 (:REWRITE DEFAULT-CAR))
 (575 575 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (575 575 (:REWRITE DEFAULT-+-1))
 (453 175 (:REWRITE SIMPLIFY-SUMS-<))
 (452 104 (:REWRITE TAKE-WHEN-ATOM))
 (372 46 (:DEFINITION BINARY-APPEND))
 (344 86 (:DEFINITION STRIP-CARS))
 (284 284 (:LINEAR LEN-WHEN-PREFIXP))
 (272 16 (:REWRITE LEN-OF-APPEND))
 (262 176 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (262 176 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (262 176 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (235 235 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (223 167 (:REWRITE DEFAULT-<-2))
 (219 219 (:REWRITE |(< (- x) (- y))|))
 (213 167 (:REWRITE DEFAULT-<-1))
 (192 32 (:REWRITE ADE::GCD3$OUT-ACT-INACTIVE))
 (190 40 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (176 176 (:REWRITE |(equal (- x) (- y))|))
 (160 16 (:DEFINITION ADE::V-THREEFIX))
 (154 66 (:REWRITE |(< d (+ c x))|))
 (142 142 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (140 20 (:DEFINITION TRUE-LISTP))
 (136 136 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (135 135 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (135 135 (:REWRITE DEFAULT-*-2))
 (135 135 (:REWRITE DEFAULT-*-1))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (112 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (112 8 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (80 80 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (72 72 (:TYPE-PRESCRIPTION ADE::3VP))
 (64 32 (:DEFINITION ADE::3V-FIX))
 (60 20 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (60 20 (:REWRITE ADE::F-BUF-OF-3VP))
 (48 8 (:REWRITE |(+ y (+ x z))|))
 (40 40 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (40 40 (:REWRITE DEFAULT-UNARY-/))
 (36 36 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (36 36 (:REWRITE |(< 0 (- x))|))
 (36 36 (:REWRITE |(* (- x) y)|))
 (30 10 (:REWRITE ADE::BVP-NTHCDR))
 (28 28 (:REWRITE |(* c (* d x))|))
 (24 24 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (24 24 (:REWRITE CDR-CONS))
 (24 24 (:REWRITE |(< (+ c x) d)|))
 (16 16 (:REWRITE |(< 0 (* x y))|))
 (16 8 (:REWRITE ADE::BOOLEANP-OF-F-BUF))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (8 8 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 6 (:REWRITE REDUCE-INTEGERP-+))
 (6 6 (:REWRITE INTEGERP-MINUS-X))
 (6 6 (:META META-INTEGERP-CORRECT))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::GCD3$ST-FORMAT-PRESERVED
 (147 147 (:REWRITE NTH-WHEN-PREFIXP))
 (76 12 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (48 12 (:DEFINITION STRIP-CARS))
 (44 44 (:REWRITE DEFAULT-CAR))
 (32 4 (:REWRITE ADE::GCD-COND$ACT-INACTIVE))
 (30 6 (:DEFINITION PAIRLIS$))
 (28 28 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (28 28 (:REWRITE DEFAULT-CDR))
 (28 28 (:REWRITE DEFAULT-*-2))
 (28 28 (:REWRITE DEFAULT-*-1))
 (27 5 (:REWRITE ADE::MERGE$ACT-INACTIVE))
 (24 18 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (24 18 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (24 18 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (22 4 (:REWRITE ADE::GCD-COND$ACT1-INACTIVE))
 (20 20 (:TYPE-PRESCRIPTION BOOLEANP))
 (20 2 (:REWRITE ADE::MERGE$ACT1-INACTIVE))
 (18 18 (:REWRITE |(equal (- x) (- y))|))
 (18 9 (:REWRITE DEFAULT-+-2))
 (18 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-GCD-BODY3$OUT-ACT))
 (18 1 (:REWRITE REPEAT-WHEN-ZP))
 (16 1 (:REWRITE ZP-OPEN))
 (14 4 (:REWRITE ADE::GCD-BODY3$OUT-ACT-INACTIVE))
 (12 2 (:REWRITE ADE::F-GATES=B-GATES))
 (12 2 (:REWRITE ADE::BOOLEANP-GCD-BODY3$OUT-ACT))
 (10 10 (:TYPE-PRESCRIPTION ADE::GCD-BODY3$INPUT-FORMAT))
 (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 DEFAULT-+-1))
 (7 7 (:REWRITE SIMPLIFY-SUMS-<))
 (7 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (7 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (7 7 (:REWRITE DEFAULT-<-2))
 (7 7 (:REWRITE DEFAULT-<-1))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 1 (:DEFINITION NATP))
 (6 6 (:TYPE-PRESCRIPTION ADE::MERGE$ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::GCD3$BODY-INPUTS))
 (6 6 (:TYPE-PRESCRIPTION ADE::GCD-COND$ACT1))
 (6 6 (:TYPE-PRESCRIPTION ADE::GCD-COND$ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::GCD-BODY3$OUT-ACT))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (6 2 (:REWRITE ADE::GCD3$INPUT-FORMAT=>BODY$INPUT-FORMAT))
 (6 1 (:DEFINITION BINARY-APPEND))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT))
 (4 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:REWRITE ADE::GCD-BODY3$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (4 4 (:META META-INTEGERP-CORRECT))
 (4 2 (:REWRITE ADE::GCD-BODY3$IN-ACT-INACTIVE))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (3 3 (:REWRITE ADE::LEN-GCD-BODY3$DATA-OUT-2))
 (3 3 (:REWRITE |(< (- x) 0)|))
 (3 3 (:REWRITE |(* (- x) y)|))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1 1 (:TYPE-PRESCRIPTION ZP))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< 0 (* x y))|))
 (1 1 (:REWRITE |(< (* x y) 0)|))
 )
(ADE::GCD3$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::GCD3$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::GCD3$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::GCD3$RUN)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-GCD3$RUN-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-GCD3$RUN)
(ADE::GCD3$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::GCD3$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-GCD3$INPUT-FORMAT-N-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-GCD3$INPUT-FORMAT-N)
(ADE::GCD3$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::GCD3$DE-N
 (265 30 (:REWRITE ZP-OPEN))
 (108 12 (:REWRITE |(< d (+ c x))|))
 (62 2 (:DEFINITION ADE::GCD3$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::GCD3$INPUT-FORMAT-PLUS))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE ADE::DE-PLUS))
 )
(ADE::GCD3$EXTRACT)
(ADE::GCD3$EXTRACT-NOT-EMPTY
 (1120 32 (:DEFINITION NTHCDR))
 (672 16 (:REWRITE ADE::NTHCDR-APPEND))
 (536 8 (:REWRITE TAKE-OF-TOO-MANY))
 (464 32 (:DEFINITION NATP))
 (458 194 (:REWRITE DEFAULT-CDR))
 (449 449 (:REWRITE NTH-WHEN-PREFIXP))
 (384 16 (:REWRITE ZP-OPEN))
 (356 186 (:REWRITE DEFAULT-+-2))
 (352 96 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (264 8 (:REWRITE ADE::LEN-NTHCDR))
 (257 161 (:REWRITE DEFAULT-CAR))
 (208 16 (:REWRITE |(+ (+ x y) z)|))
 (196 8 (:REWRITE ADE::GCD-COND$ACT0-INACTIVE))
 (196 8 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (194 133 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (194 133 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (194 133 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (187 186 (:REWRITE DEFAULT-+-1))
 (186 186 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (186 186 (:REWRITE NORMALIZE-ADDENDS))
 (184 8 (:REWRITE |(< 0 (* x y))|))
 (172 43 (:DEFINITION STRIP-CARS))
 (168 8 (:REWRITE ADE::LEN-GCD-COND$DATA-IN))
 (160 56 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (158 18 (:DEFINITION BINARY-APPEND))
 (152 88 (:REWRITE SIMPLIFY-SUMS-<))
 (152 88 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (152 88 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (133 133 (:REWRITE |(equal (- x) (- y))|))
 (132 132 (:LINEAR LEN-WHEN-PREFIXP))
 (132 36 (:REWRITE ADE::F-GATES=B-GATES))
 (128 88 (:REWRITE DEFAULT-<-2))
 (112 88 (:REWRITE DEFAULT-<-1))
 (112 8 (:REWRITE CONSP-OF-APPEND))
 (104 104 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (104 104 (:TYPE-PRESCRIPTION ADE::GCD-COND$DATA-IN))
 (96 96 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (96 96 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (88 88 (:REWRITE |(< (- x) (- y))|))
 (87 36 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (80 56 (:REWRITE DEFAULT-*-2))
 (80 8 (:REWRITE TAKE-WHEN-ATOM))
 (80 8 (:DEFINITION ADE::V-THREEFIX))
 (72 8 (:REWRITE ADE::LEN-V-THREEFIX))
 (66 66 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (64 64 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (64 16 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (64 8 (:REWRITE ADE::LEN-STRIP-CARS))
 (56 56 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (56 56 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (56 56 (:REWRITE DEFAULT-*-1))
 (56 28 (:TYPE-PRESCRIPTION ADE::BOOLEANP-GCD3$OUT-ACT))
 (56 8 (:REWRITE ADE::CAR-V-THREEFIX))
 (48 16 (:REWRITE ADE::V-THREEFIX-BVP))
 (48 16 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (48 8 (:REWRITE ADE::GCD3$OUT-ACT-INACTIVE))
 (40 40 (:TYPE-PRESCRIPTION STRIP-CARS))
 (40 40 (:TYPE-PRESCRIPTION ADE::3VP))
 (40 8 (:DEFINITION TRUE-LISTP))
 (36 12 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (36 12 (:REWRITE ADE::F-BUF-OF-3VP))
 (32 32 (:TYPE-PRESCRIPTION NATP))
 (32 32 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (32 32 (:REWRITE REDUCE-INTEGERP-+))
 (32 32 (:REWRITE INTEGERP-MINUS-X))
 (32 32 (:REWRITE |(< (- x) 0)|))
 (32 32 (:META META-INTEGERP-CORRECT))
 (32 16 (:DEFINITION ADE::3V-FIX))
 (28 28 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT))
 (24 24 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (16 16 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (16 16 (:REWRITE |(< 0 (- x))|))
 (16 8 (:REWRITE |(< d (+ c x))|))
 (12 12 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (12 12 (:REWRITE |(equal (- x) 0)|))
 (11 11 (:TYPE-PRESCRIPTION ADE::GCD$OP-MAP))
 (10 10 (:TYPE-PRESCRIPTION ADE::GCD-BODY3$EXTRACT))
 (8 8 (:REWRITE |(integerp (* c x))|))
 (8 8 (:REWRITE |(< (* x y) 0)|))
 (8 8 (:LINEAR ADE::GCD-BODY3$EXTRACT-NOT-EMPTY))
 (8 2 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (8 2 (:DEFINITION ADE::GCD$OP-MAP))
 (1 1 (:REWRITE |(equal (+ c x) d)|))
 )
(ADE::GCD3$INV)
(ADE::GCD3$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::GCD3$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::GCD3$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 ADE::GCD3$INPUT-FORMAT-LEMMA-1))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(ADE::GCD3$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::GCD3$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 ADE::GCD3$INPUT-FORMAT-LEMMA-2))
 (1 1 (:REWRITE ADE::GCD3$INPUT-FORMAT-LEMMA-1))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-*-2))
 (1 1 (:REWRITE DEFAULT-*-1))
 )
(ADE::GCD3$BODY-IN-ACT-INACTIVE
 (410 8 (:REWRITE TAKE-OF-TOO-MANY))
 (216 4 (:DEFINITION TAKE))
 (154 4 (:REWRITE ADE::LEN-NTHCDR))
 (128 64 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (124 124 (:TYPE-PRESCRIPTION LEN))
 (116 12 (:DEFINITION LEN))
 (76 25 (:REWRITE DEFAULT-CAR))
 (64 64 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (56 32 (:REWRITE DEFAULT-CDR))
 (56 8 (:REWRITE TAKE-WHEN-ATOM))
 (48 4 (:DEFINITION BINARY-APPEND))
 (40 4 (:DEFINITION ADE::V-THREEFIX))
 (33 33 (:REWRITE NTH-WHEN-PREFIXP))
 (33 6 (:REWRITE ADE::F-GATES=B-GATES))
 (33 6 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (32 18 (:REWRITE SIMPLIFY-SUMS-<))
 (32 18 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (32 18 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (32 4 (:DEFINITION NTHCDR))
 (31 19 (:REWRITE DEFAULT-+-2))
 (28 28 (:LINEAR LEN-WHEN-PREFIXP))
 (28 4 (:REWRITE ADE::CAR-V-THREEFIX))
 (26 18 (:REWRITE DEFAULT-<-2))
 (24 24 (:TYPE-PRESCRIPTION BOOLEANP))
 (24 18 (:REWRITE DEFAULT-<-1))
 (24 8 (:REWRITE ADE::V-THREEFIX-BVP))
 (24 4 (:DEFINITION STRIP-CARS))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (20 20 (:TYPE-PRESCRIPTION STRIP-CARS))
 (20 20 (:TYPE-PRESCRIPTION ADE::3VP))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (20 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (19 19 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (19 19 (:REWRITE NORMALIZE-ADDENDS))
 (19 19 (:REWRITE DEFAULT-+-1))
 (18 18 (:REWRITE |(< (- x) (- y))|))
 (18 6 (:REWRITE ADE::F-BUF-OF-3VP))
 (16 16 (:TYPE-PRESCRIPTION ADE::BVP))
 (16 8 (:DEFINITION ADE::3V-FIX))
 (16 4 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (16 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (16 4 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (14 14 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (10 2 (:REWRITE |(+ y x)|))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (8 8 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT-LEMMA-2))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (4 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:REWRITE |(equal (- x) (- y))|))
 (4 4 (:REWRITE |(< (- x) 0)|))
 (4 4 (:META META-INTEGERP-CORRECT))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE |(< d (+ c x))|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::GCD3$INV-PRESERVED
 (6853 6853 (:REWRITE NTH-WHEN-PREFIXP))
 (4270 642 (:DEFINITION STRIP-CARS))
 (4038 2539 (:REWRITE DEFAULT-CAR))
 (3936 3298 (:REWRITE DEFAULT-CDR))
 (3360 48 (:DEFINITION TAKE))
 (3217 1880 (:REWRITE DEFAULT-+-2))
 (2732 913 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2732 913 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2732 913 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2155 295 (:REWRITE ADE::GCD-BODY3$OUT-ACT-INACTIVE))
 (1974 182 (:DEFINITION ADE::V-THREEFIX))
 (1884 1880 (:REWRITE DEFAULT-+-1))
 (1880 1880 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1852 502 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (1728 194 (:DEFINITION BINARY-APPEND))
 (1368 174 (:DEFINITION PAIRLIS$))
 (1326 454 (:REWRITE SIMPLIFY-SUMS-<))
 (1170 138 (:DEFINITION TRUE-LISTP))
 (1111 101 (:REWRITE |(+ (+ x y) z)|))
 (917 131 (:REWRITE ADE::CAR-V-THREEFIX))
 (913 913 (:REWRITE |(equal (- x) (- y))|))
 (896 896 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (896 896 (:REWRITE DEFAULT-*-2))
 (896 896 (:REWRITE DEFAULT-*-1))
 (828 276 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (824 824 (:LINEAR LEN-WHEN-PREFIXP))
 (718 214 (:REWRITE TAKE-WHEN-ATOM))
 (684 18 (:REWRITE |(< x (if a b c))|))
 (626 313 (:DEFINITION ADE::3V-FIX))
 (618 618 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (618 618 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (558 558 (:REWRITE |(< (- x) (- y))|))
 (527 143 (:REWRITE |(< d (+ c x))|))
 (485 419 (:REWRITE DEFAULT-<-2))
 (455 419 (:REWRITE DEFAULT-<-1))
 (412 412 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (376 112 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (360 18 (:REWRITE ZP-OPEN))
 (339 339 (:TYPE-PRESCRIPTION ADE::3VP))
 (324 27 (:REWRITE |(+ (if a b c) x)|))
 (210 35 (:REWRITE |(+ y (+ x z))|))
 (192 32 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (184 8 (:REWRITE ADE::MERGE$ACT0-INACTIVE))
 (183 183 (:REWRITE |(* (- x) y)|))
 (178 178 (:META META-INTEGERP-CORRECT))
 (175 28 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (168 14 (:DEFINITION POSP))
 (146 146 (:REWRITE REDUCE-INTEGERP-+))
 (146 146 (:REWRITE INTEGERP-MINUS-X))
 (126 18 (:DEFINITION NATP))
 (120 20 (:REWRITE ADE::GCD-BODY3$IN-ACT-INACTIVE))
 (115 115 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (115 115 (:REWRITE |(< 0 (- x))|))
 (112 112 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (112 112 (:REWRITE DEFAULT-UNARY-/))
 (98 14 (:REWRITE CAR-OF-TAKE))
 (91 13 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (78 6 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (77 77 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (77 77 (:REWRITE |(equal (- x) 0)|))
 (72 4 (:REWRITE ADE::GCD-COND$ACT0-INACTIVE))
 (72 4 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (59 59 (:REWRITE |(< 0 (* x y))|))
 (49 35 (:REWRITE ADE::BVP-TAKE))
 (48 48 (:REWRITE |(< (+ c x) d)|))
 (46 46 (:REWRITE |(integerp (* c x))|))
 (39 13 (:REWRITE ADE::F-BUF-OF-3VP))
 (35 21 (:REWRITE ADE::BVP-NTHCDR))
 (34 34 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (28 28 (:REWRITE CONSP-OF-TAKE))
 (22 7 (:REWRITE ADE::GCD3$INPUT-FORMAT-LEMMA-3))
 (21 21 (:TYPE-PRESCRIPTION ADE::F-NOR3))
 (21 21 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (18 18 (:TYPE-PRESCRIPTION NATP))
 (18 18 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (18 18 (:REWRITE DEFAULT-UNARY-MINUS))
 (18 18 (:REWRITE |(< (- x) 0)|))
 (14 14 (:TYPE-PRESCRIPTION POSP))
 (9 9 (:REWRITE REPEAT-WHEN-ZP))
 )
(ADE::GCD3$EXTRACTED-STEP
 (24 12 (:TYPE-PRESCRIPTION ADE::BOOLEANP-GCD3$IN-ACT))
 (18 18 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-GCD3$OUT-ACT))
 )
(ADE::GCD3-AUX)
(ADE::GCD3$BODY-DATA-IN-REWRITE
 (259 5 (:REWRITE TAKE-OF-TOO-MANY))
 (108 2 (:REWRITE ADE::LEN-NTHCDR))
 (84 4 (:REWRITE |(< x (if a b c))|))
 (54 1 (:DEFINITION TAKE))
 (42 21 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (41 13 (:REWRITE SIMPLIFY-SUMS-<))
 (36 4 (:REWRITE TAKE-WHEN-ATOM))
 (28 28 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT-LEMMA-2))
 (25 15 (:REWRITE DEFAULT-+-2))
 (25 10 (:REWRITE DEFAULT-CAR))
 (24 1 (:REWRITE ADE::NTHCDR-APPEND))
 (23 17 (:REWRITE DEFAULT-CDR))
 (21 21 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (20 13 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (20 4 (:REWRITE |(+ y x)|))
 (20 2 (:DEFINITION ADE::V-THREEFIX))
 (18 18 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT-LEMMA-1))
 (18 18 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (18 18 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (18 1 (:REWRITE LEN-OF-APPEND))
 (16 12 (:REWRITE DEFAULT-<-1))
 (15 15 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (15 15 (:REWRITE DEFAULT-+-1))
 (15 12 (:REWRITE DEFAULT-<-2))
 (15 1 (:DEFINITION NTHCDR))
 (14 14 (:REWRITE |(< (- x) (- y))|))
 (14 14 (:LINEAR LEN-WHEN-PREFIXP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 4 (:REWRITE ADE::V-THREEFIX-BVP))
 (12 2 (:REWRITE ADE::F-GATES=B-GATES))
 (12 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (12 2 (:DEFINITION STRIP-CARS))
 (12 1 (:DEFINITION BINARY-APPEND))
 (11 1 (:REWRITE |(+ (+ x y) z)|))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (7 7 (:TYPE-PRESCRIPTION STRIP-CARS))
 (7 7 (:TYPE-PRESCRIPTION ADE::3VP))
 (7 7 (:REWRITE NTH-WHEN-PREFIXP))
 (7 7 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (7 1 (:REWRITE ADE::CAR-V-THREEFIX))
 (6 6 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (6 6 (:REWRITE DEFAULT-*-2))
 (6 6 (:REWRITE DEFAULT-*-1))
 (6 3 (:DEFINITION ADE::3V-FIX))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (6 1 (:REWRITE CONSP-OF-APPEND))
 (6 1 (:REWRITE |(+ y (+ x z))|))
 (5 5 (:TYPE-PRESCRIPTION NFIX))
 (5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (3 3 (:REWRITE REDUCE-INTEGERP-+))
 (3 3 (:REWRITE INTEGERP-MINUS-X))
 (3 3 (:REWRITE |(< d (+ c x))|))
 (3 3 (:REWRITE |(< 0 (- x))|))
 (3 3 (:REWRITE |(< (- x) 0)|))
 (3 3 (:REWRITE |(* (- x) y)|))
 (3 3 (:META META-INTEGERP-CORRECT))
 (3 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (3 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (3 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (2 2 (:REWRITE LEN-OF-TAKE))
 (2 2 (:REWRITE DEFAULT-UNARY-/))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE |(* c (* d x))|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE CONSP-OF-TAKE))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 (1 1 (:REWRITE |(< 0 (* x y))|))
 )
(ADE::GCD$OP-OF-GCD-BODY3$OP
 (617 6 (:DEFINITION TAKE))
 (284 54 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (242 48 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (239 6 (:DEFINITION NTHCDR))
 (160 10 (:REWRITE REV-WHEN-NOT-CONSP))
 (154 2 (:REWRITE |(< (if a b c) x)|))
 (122 67 (:REWRITE DEFAULT-+-2))
 (111 3 (:REWRITE CONSP-OF-TAKE))
 (90 90 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (90 90 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (90 90 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (85 67 (:REWRITE DEFAULT-CDR))
 (73 73 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (73 73 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (67 67 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (67 67 (:REWRITE DEFAULT-+-1))
 (54 54 (:REWRITE |(< (- x) (- y))|))
 (51 51 (:TYPE-PRESCRIPTION ADE::V-NOT))
 (50 42 (:REWRITE SIMPLIFY-SUMS-<))
 (50 42 (:REWRITE DEFAULT-<-2))
 (48 48 (:LINEAR LEN-WHEN-PREFIXP))
 (47 23 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (44 44 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (44 44 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (44 44 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (42 42 (:REWRITE DEFAULT-<-1))
 (36 22 (:REWRITE DEFAULT-*-2))
 (36 6 (:DEFINITION BINARY-APPEND))
 (31 20 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (31 20 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (31 20 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (30 12 (:REWRITE TAKE-WHEN-ATOM))
 (30 12 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (27 27 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (27 27 (:REWRITE |(< 0 (- x))|))
 (24 24 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (24 3 (:REWRITE ADE::LEN-V-NOT))
 (22 22 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (22 22 (:REWRITE DEFAULT-*-1))
 (21 12 (:REWRITE DEFAULT-CAR))
 (20 20 (:REWRITE |(equal (- x) (- y))|))
 (18 18 (:REWRITE REDUCE-INTEGERP-+))
 (18 18 (:REWRITE INTEGERP-MINUS-X))
 (18 18 (:REWRITE |(integerp (* c x))|))
 (18 18 (:META META-INTEGERP-CORRECT))
 (18 6 (:REWRITE |(* y (* x z))|))
 (17 17 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (17 17 (:REWRITE |(equal (- x) 0)|))
 (12 12 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (12 12 (:REWRITE DEFAULT-UNARY-/))
 (12 12 (:REWRITE |(* a (/ a))|))
 (12 6 (:REWRITE |(< d (+ c x))|))
 (12 6 (:REWRITE |(+ c (+ d x))|))
 (9 9 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (9 9 (:REWRITE |(< (- x) 0)|))
 (6 6 (:REWRITE |(< (+ c x) d)|))
 (6 6 (:REWRITE |(* c (* d x))|))
 (6 6 (:REWRITE |(* (- x) y)|))
 (4 4 (:REWRITE INSERT-0-*))
 )
(ADE::GCD3$EXTRACTED-STEP-CORRECT
 (8284 8284 (:REWRITE NTH-WHEN-PREFIXP))
 (7140 102 (:DEFINITION TAKE))
 (6122 902 (:DEFINITION STRIP-CARS))
 (5971 3551 (:REWRITE DEFAULT-CAR))
 (5078 488 (:DEFINITION ADE::V-THREEFIX))
 (5046 4308 (:REWRITE DEFAULT-CDR))
 (4307 2601 (:REWRITE DEFAULT-+-2))
 (3706 1200 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (3706 1200 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (3706 1200 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3538 673 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (3259 270 (:DEFINITION NTHCDR))
 (3254 154 (:REWRITE ADE::GCD-BODY3$OUT-ACT-INACTIVE))
 (2601 2601 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2601 2601 (:REWRITE DEFAULT-+-1))
 (2594 244 (:DEFINITION PAIRLIS$))
 (1876 268 (:REWRITE ADE::CAR-V-THREEFIX))
 (1848 168 (:REWRITE |(+ (+ x y) z)|))
 (1644 1644 (:LINEAR LEN-WHEN-PREFIXP))
 (1512 756 (:DEFINITION ADE::3V-FIX))
 (1406 37 (:REWRITE |(< x (if a b c))|))
 (1282 154 (:DEFINITION TRUE-LISTP))
 (1268 571 (:REWRITE SIMPLIFY-SUMS-<))
 (1223 362 (:REWRITE TAKE-WHEN-ATOM))
 (1203 1203 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (1203 1203 (:REWRITE DEFAULT-*-2))
 (1203 1203 (:REWRITE DEFAULT-*-1))
 (1200 1200 (:REWRITE |(equal (- x) (- y))|))
 (1134 133 (:DEFINITION BINARY-APPEND))
 (924 308 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (829 829 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (829 829 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (822 822 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (780 780 (:REWRITE |(< (- x) (- y))|))
 (766 766 (:TYPE-PRESCRIPTION ADE::3VP))
 (688 549 (:REWRITE DEFAULT-<-2))
 (660 55 (:REWRITE |(+ (if a b c) x)|))
 (623 549 (:REWRITE DEFAULT-<-1))
 (471 22 (:REWRITE LEN-OF-APPEND))
 (263 161 (:REWRITE |(< d (+ c x))|))
 (259 37 (:DEFINITION NATP))
 (235 235 (:REWRITE |(* (- x) y)|))
 (214 214 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (214 214 (:REWRITE DEFAULT-UNARY-/))
 (198 27 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (165 165 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (165 165 (:REWRITE |(equal (- x) 0)|))
 (132 22 (:REWRITE ADE::GCD-BODY3$IN-ACT-INACTIVE))
 (132 22 (:REWRITE |(+ y (+ x z))|))
 (131 6 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (130 10 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (129 129 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (129 129 (:REWRITE |(< 0 (- x))|))
 (126 18 (:REWRITE CAR-OF-TAKE))
 (111 111 (:REWRITE REDUCE-INTEGERP-+))
 (111 111 (:REWRITE INTEGERP-MINUS-X))
 (111 111 (:META META-INTEGERP-CORRECT))
 (102 102 (:REWRITE |(< (+ c x) d)|))
 (84 84 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (63 45 (:REWRITE ADE::BVP-TAKE))
 (54 9 (:REWRITE ADE::GCD3$OUT-ACT-INACTIVE))
 (49 49 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (49 49 (:REWRITE |(< (- x) 0)|))
 (45 27 (:REWRITE ADE::BVP-NTHCDR))
 (40 40 (:REWRITE DEFAULT-UNARY-MINUS))
 (40 10 (:REWRITE ADE::GCD3$IN-ACT-INACTIVE))
 (36 36 (:REWRITE CONSP-OF-TAKE))
 (32 32 (:REWRITE REPEAT-WHEN-ZP))
 (27 27 (:TYPE-PRESCRIPTION ADE::F-NOR3))
 (27 27 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (22 22 (:REWRITE |(< 0 (* x y))|))
 (17 17 (:TYPE-PRESCRIPTION ADE::GCD-COND$BR-INPUTS))
 (15 5 (:REWRITE ADE::F-BUF-OF-3VP))
 (4 4 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (4 4 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (4 4 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 )
(ADE::GCD3$BODY-OUT-ACT-INACTIVE
 (410 8 (:REWRITE TAKE-OF-TOO-MANY))
 (216 4 (:DEFINITION TAKE))
 (154 4 (:REWRITE ADE::LEN-NTHCDR))
 (132 132 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT-LEMMA-1))
 (128 64 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (124 124 (:TYPE-PRESCRIPTION LEN))
 (116 12 (:DEFINITION LEN))
 (76 25 (:REWRITE DEFAULT-CAR))
 (64 64 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (56 32 (:REWRITE DEFAULT-CDR))
 (56 8 (:REWRITE TAKE-WHEN-ATOM))
 (48 4 (:DEFINITION BINARY-APPEND))
 (40 4 (:DEFINITION ADE::V-THREEFIX))
 (37 37 (:REWRITE NTH-WHEN-PREFIXP))
 (32 18 (:REWRITE SIMPLIFY-SUMS-<))
 (32 18 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (32 18 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (32 4 (:DEFINITION NTHCDR))
 (31 19 (:REWRITE DEFAULT-+-2))
 (30 5 (:REWRITE ADE::F-GATES=B-GATES))
 (30 5 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (28 28 (:LINEAR LEN-WHEN-PREFIXP))
 (28 4 (:REWRITE ADE::CAR-V-THREEFIX))
 (26 18 (:REWRITE DEFAULT-<-2))
 (24 18 (:REWRITE DEFAULT-<-1))
 (24 8 (:REWRITE ADE::V-THREEFIX-BVP))
 (24 4 (:DEFINITION STRIP-CARS))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (20 20 (:TYPE-PRESCRIPTION STRIP-CARS))
 (20 20 (:TYPE-PRESCRIPTION BOOLEANP))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (20 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (20 5 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (20 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (20 5 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (19 19 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (19 19 (:REWRITE NORMALIZE-ADDENDS))
 (19 19 (:REWRITE DEFAULT-+-1))
 (18 18 (:TYPE-PRESCRIPTION ADE::3VP))
 (18 18 (:REWRITE |(< (- x) (- y))|))
 (16 16 (:TYPE-PRESCRIPTION ADE::BVP))
 (16 8 (:DEFINITION ADE::3V-FIX))
 (15 5 (:REWRITE ADE::F-BUF-OF-3VP))
 (14 14 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (10 2 (:REWRITE |(+ y x)|))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (5 5 (:REWRITE |(equal (- x) (- y))|))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (4 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:REWRITE ADE::GCD-BODY3$IN-OUT-ACTS-MUTUALLY-EXCLUSIVE))
 (4 4 (:REWRITE |(< (- x) 0)|))
 (4 4 (:META META-INTEGERP-CORRECT))
 (2 2 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2 2 (:REWRITE DEFAULT-*-2))
 (2 2 (:REWRITE DEFAULT-*-1))
 (2 2 (:REWRITE |(< d (+ c x))|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::GCD3$VALID-ST-PRESERVED
 (13440 192 (:DEFINITION TAKE))
 (11652 11652 (:REWRITE NTH-WHEN-PREFIXP))
 (7300 1036 (:DEFINITION STRIP-CARS))
 (6418 1138 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (6040 3335 (:REWRITE DEFAULT-CAR))
 (5865 4665 (:REWRITE DEFAULT-CDR))
 (5844 3631 (:REWRITE DEFAULT-+-2))
 (5322 450 (:DEFINITION NTHCDR))
 (5077 1516 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5077 1516 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (5077 1516 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3631 3631 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3631 3631 (:REWRITE DEFAULT-+-1))
 (3082 946 (:REWRITE SIMPLIFY-SUMS-<))
 (2838 258 (:REWRITE |(+ (+ x y) z)|))
 (2623 174 (:REWRITE ADE::GCD-BODY3$OUT-ACT-INACTIVE))
 (2316 214 (:DEFINITION ADE::V-THREEFIX))
 (2008 2008 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (2008 2008 (:REWRITE DEFAULT-*-2))
 (2008 2008 (:REWRITE DEFAULT-*-1))
 (1928 1928 (:LINEAR LEN-WHEN-PREFIXP))
 (1888 592 (:REWRITE TAKE-WHEN-ATOM))
 (1861 213 (:DEFINITION TRUE-LISTP))
 (1788 84 (:REWRITE LEN-OF-APPEND))
 (1516 1516 (:REWRITE |(equal (- x) (- y))|))
 (1346 1346 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (1346 1346 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (1314 1314 (:REWRITE |(< (- x) (- y))|))
 (1278 426 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (1272 162 (:DEFINITION BINARY-APPEND))
 (1216 32 (:REWRITE |(< x (if a b c))|))
 (1086 862 (:REWRITE DEFAULT-<-2))
 (964 964 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (955 113 (:DEFINITION PAIRLIS$))
 (926 862 (:REWRITE DEFAULT-<-1))
 (805 115 (:REWRITE ADE::CAR-V-THREEFIX))
 (732 324 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (658 329 (:DEFINITION ADE::3V-FIX))
 (576 48 (:REWRITE |(+ (if a b c) x)|))
 (504 84 (:REWRITE |(+ y (+ x z))|))
 (500 308 (:REWRITE |(< d (+ c x))|))
 (438 73 (:REWRITE ADE::GCD-BODY3$IN-ACT-INACTIVE))
 (416 416 (:REWRITE |(* (- x) y)|))
 (389 389 (:TYPE-PRESCRIPTION ADE::3VP))
 (352 352 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (352 352 (:REWRITE DEFAULT-UNARY-/))
 (260 260 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (260 260 (:REWRITE |(< 0 (- x))|))
 (224 40 (:REWRITE ADE::BVP-OF-V-THREEFIX))
 (224 32 (:DEFINITION NATP))
 (210 30 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (192 192 (:REWRITE |(< (+ c x) d)|))
 (184 8 (:REWRITE ADE::MERGE$ACT0-INACTIVE))
 (148 148 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (144 8 (:REWRITE ADE::GCD-COND$ACT0-INACTIVE))
 (144 8 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (112 68 (:REWRITE ADE::BVP-TAKE))
 (112 16 (:REWRITE CAR-OF-TAKE))
 (104 8 (:REWRITE ADE::BRANCH$ACT1-INACTIVE))
 (96 96 (:REWRITE REDUCE-INTEGERP-+))
 (96 96 (:REWRITE INTEGERP-MINUS-X))
 (96 96 (:META META-INTEGERP-CORRECT))
 (90 30 (:REWRITE ADE::F-BUF-OF-3VP))
 (84 84 (:REWRITE |(< 0 (* x y))|))
 (82 38 (:REWRITE ADE::BVP-NTHCDR))
 (66 66 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (48 48 (:TYPE-PRESCRIPTION ADE::F-NOR3))
 (48 48 (:REWRITE DEFAULT-UNARY-MINUS))
 (32 32 (:TYPE-PRESCRIPTION NATP))
 (32 32 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (32 32 (:REWRITE CONSP-OF-TAKE))
 (32 32 (:REWRITE |(< (- x) 0)|))
 (12 4 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP-LEN))
 )
(ADE::GCD3$EXTRACT-LEMMA
 (10010 365 (:DEFINITION NTHCDR))
 (6459 371 (:REWRITE |(< 0 (* x y))|))
 (5321 320 (:REWRITE REV-WHEN-NOT-CONSP))
 (4461 2685 (:REWRITE DEFAULT-CDR))
 (4440 2280 (:TYPE-PRESCRIPTION NOT-INTEGERP-4A))
 (4080 2420 (:REWRITE DEFAULT-+-2))
 (3752 1317 (:REWRITE SIMPLIFY-SUMS-<))
 (3735 312 (:DEFINITION NATP))
 (2862 160 (:REWRITE CONSP-OF-TAKE))
 (2709 2709 (:TYPE-PRESCRIPTION ADE::V-NOT))
 (2476 705 (:REWRITE TAKE-WHEN-ATOM))
 (2420 2420 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2420 2420 (:REWRITE DEFAULT-+-1))
 (2378 1307 (:REWRITE DEFAULT-CAR))
 (2280 2280 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (2280 2280 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (2280 2280 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (2054 333 (:DEFINITION BINARY-APPEND))
 (2005 2005 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2005 2005 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (1814 1814 (:LINEAR LEN-WHEN-PREFIXP))
 (1708 1221 (:REWRITE DEFAULT-<-2))
 (1701 1701 (:REWRITE |(< (- x) (- y))|))
 (1635 159 (:REWRITE ADE::LEN-V-NOT))
 (1597 652 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1570 1570 (:TYPE-PRESCRIPTION ADE::V-ADDER-OUTPUT))
 (1570 1221 (:REWRITE DEFAULT-<-1))
 (1297 652 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1297 652 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1234 799 (:META META-INTEGERP-CORRECT))
 (1214 1214 (:REWRITE NTH-WHEN-PREFIXP))
 (907 907 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (737 7 (:REWRITE ADE::BRANCH$ACT0-INACTIVE))
 (725 375 (:REWRITE |(< d (+ c x))|))
 (652 652 (:REWRITE |(equal (- x) (- y))|))
 (513 513 (:REWRITE |(integerp (* c x))|))
 (441 5 (:REWRITE REPEAT-WHEN-ZP))
 (439 349 (:REWRITE DEFAULT-*-2))
 (398 398 (:REWRITE |(< 0 (- x))|))
 (391 391 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (377 377 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (377 377 (:REWRITE |(equal (- x) 0)|))
 (360 360 (:REWRITE |(< (+ c x) d)|))
 (349 349 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (349 349 (:REWRITE DEFAULT-*-1))
 (328 328 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
 (222 111 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (200 200 (:REWRITE DEFAULT-UNARY-MINUS))
 (196 3 (:REWRITE LEN-OF-REPEAT))
 (171 9 (:REWRITE ADE::GCD3$OUT-ACT-INACTIVE))
 (144 6 (:REWRITE LEN-OF-APPEND))
 (120 19 (:REWRITE INTP-2))
 (112 56 (:TYPE-PRESCRIPTION ADE::BOOLEANP-GCD3$OUT-ACT))
 (105 105 (:REWRITE |(< (- x) 0)|))
 (99 99 (:TYPE-PRESCRIPTION ZP))
 (96 96 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (96 96 (:REWRITE |(+ x (- x))|))
 (96 18 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (90 10 (:DEFINITION TRUE-LISTP))
 (87 6 (:REWRITE NINTP-2))
 (78 78 (:TYPE-PRESCRIPTION BOOLEANP))
 (70 7 (:DEFINITION ADE::V-THREEFIX))
 (60 20 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (56 56 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT))
 (55 55 (:LINEAR ADE::GCD-BODY3$EXTRACT-NOT-EMPTY))
 (49 7 (:REWRITE ADE::CAR-V-THREEFIX))
 (44 18 (:REWRITE ADE::F-BUF-OF-3VP))
 (43 43 (:TYPE-PRESCRIPTION ADE::F$FAST-ZERO))
 (40 40 (:TYPE-PRESCRIPTION ADE::3VP))
 (40 40 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (40 40 (:REWRITE DEFAULT-UNARY-/))
 (36 36 (:REWRITE ADE::GCD3$INPUT-FORMAT-LEMMA-2))
 (33 33 (:TYPE-PRESCRIPTION INTP-+))
 (30 30 (:REWRITE |(* (- x) y)|))
 (28 14 (:DEFINITION ADE::3V-FIX))
 (27 6 (:REWRITE NINTP-1))
 (25 5 (:REWRITE ADE::BOOLEANP-OF-F-BUF))
 (17 17 (:TYPE-PRESCRIPTION ADE::GCD-COND$DATA-INS-LEN))
 (17 17 (:TYPE-PRESCRIPTION ADE::F-NOR3))
 (16 16 (:DEFINITION FIX))
 (12 12 (:REWRITE INTEGERP-+-REDUCE-LEADING-RATIONAL-CONSTANT))
 (8 8 (:REWRITE-QUOTED-CONSTANT FIX-UNDER-NUMBER-EQUIV))
 (8 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (5 5 (:REWRITE |(< (+ c x y) d)|))
 (4 4 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (4 4 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (4 4 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (4 4 (:REWRITE FOLD-CONSTS-IN-+))
 (4 4 (:REWRITE |(< d (+ c x y))|))
 )
(ADE::GCD3$IN-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-GCD3$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT))
 )
(ADE::GCD3$IN-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT-LEMMA-1))
 )
(ADE::GCD3$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::GCD3$ME-INPUTS))
 (144 36 (:REWRITE ADE::GCD3$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::GCD3$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::GCD3$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::GCD3$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::GCD3$OUT-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-GCD3$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT))
 )
(ADE::GCD3$OUT-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT-LEMMA-2))
 )
(ADE::GCD3$OUT-SEQ-LEMMA
 (1760 40 (:REWRITE ADE::GCD-COND$ACT0-INACTIVE))
 (725 65 (:REWRITE ZP-OPEN))
 (680 680 (:TYPE-PRESCRIPTION ADE::GCD3$BR-INPUTS))
 (522 112 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (522 112 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (522 112 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (398 36 (:REWRITE ADE::GCD3$OUT-ACT-INACTIVE))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (348 188 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT-LEMMA-1))
 (272 272 (:REWRITE NTH-WHEN-PREFIXP))
 (213 35 (:DEFINITION BINARY-APPEND))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (120 120 (:REWRITE DEFAULT-CAR))
 (115 97 (:REWRITE DEFAULT-CDR))
 (112 112 (:REWRITE |(equal (- x) (- y))|))
 (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::GCD3$IN-ACT-INACTIVE))
 (30 6 (:DEFINITION NTHCDR))
 (29 29 (:REWRITE ADE::GCD3$EXTRACT-LEMMA))
 (12 12 (:REWRITE ADE::GCD3$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::GCD3$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::GCD3$DATAFLOW-CORRECT
 (1628 122 (:REWRITE ZP-OPEN))
 (816 87 (:REWRITE |(< d (+ c x))|))
 (576 15 (:DEFINITION NTHCDR))
 (437 72 (:DEFINITION BINARY-APPEND))
 (296 145 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (277 35 (:REWRITE ADE::GCD3$OUT-ACT-INACTIVE))
 (274 4 (:REWRITE TAKE-OF-TOO-MANY))
 (261 29 (:DEFINITION LEN))
 (259 48 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (259 48 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (259 48 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (247 196 (:REWRITE DEFAULT-CDR))
 (228 228 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (217 211 (:REWRITE DEFAULT-CAR))
 (202 202 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (192 140 (:REWRITE DEFAULT-+-2))
 (190 2 (:DEFINITION TAKE))
 (184 55 (:REWRITE ADE::GCD3$IN-ACT-INACTIVE))
 (178 141 (:REWRITE SIMPLIFY-SUMS-<))
 (165 165 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT-LEMMA-2))
 (165 15 (:REWRITE |(+ (+ x y) z)|))
 (162 139 (:REWRITE DEFAULT-<-2))
 (160 145 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (157 35 (:REWRITE |(+ c (+ d x))|))
 (152 144 (:REWRITE NORMALIZE-ADDENDS))
 (145 145 (:REWRITE |(< (- x) (- y))|))
 (140 140 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (140 140 (:REWRITE DEFAULT-+-1))
 (139 139 (:REWRITE DEFAULT-<-1))
 (108 108 (:TYPE-PRESCRIPTION ADE::GCD3$IN-SEQ))
 (102 2 (:REWRITE CONSP-OF-TAKE))
 (91 19 (:REWRITE |(+ y x)|))
 (84 84 (:REWRITE NTH-WHEN-PREFIXP))
 (60 60 (:TYPE-PRESCRIPTION ADE::GCD3$STEP))
 (48 48 (:REWRITE |(equal (- x) (- y))|))
 (44 4 (:REWRITE ADE::NFIX-OF-NAT))
 (44 4 (:LINEAR ADE::GCD3$EXTRACT-NOT-EMPTY))
 (32 4 (:DEFINITION NATP))
 (16 4 (:REWRITE TAKE-WHEN-ATOM))
 (14 14 (:TYPE-PRESCRIPTION ADE::GCD3$RUN))
 (14 14 (:REWRITE ADE::GCD3$RUN-PLUS))
 (12 12 (:REWRITE ADE::GCD3$INPUT-FORMAT-PLUS))
 (12 12 (:LINEAR LEN-WHEN-PREFIXP))
 (10 10 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (10 2 (:REWRITE |(+ y (+ x z))|))
 (8 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 4 (:REWRITE BUBBLE-DOWN-+-MATCH-1))
 (6 6 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (6 4 (:REWRITE |(< (+ c x) d)|))
 (6 4 (:REWRITE |(+ 0 x)|))
 (4 4 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE |(+ x (- x))|))
 )
(ADE::GCD3$FUNCTIONALLY-CORRECT
 (390 4 (:DEFINITION ADE::GCD3$OUT-SEQ))
 (166 4 (:REWRITE ADE::GCD3$EXTRACT-LEMMA))
 (164 4 (:DEFINITION ADE::GCD3$IN-SEQ))
 (120 3 (:DEFINITION NTHCDR))
 (97 37 (:REWRITE ZP-OPEN))
 (80 32 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (76 4 (:REWRITE ADE::GCD3$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::GCD3$INPUT-FORMAT-LEMMA-2))
 (43 34 (:REWRITE DEFAULT-CDR))
 (42 3 (:REWRITE |(< d (+ c x))|))
 (40 40 (:TYPE-PRESCRIPTION ADE::GCD3$INPUT-FORMAT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-GCD3$OUT-ACT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-GCD3$IN-ACT))
 (39 39 (:TYPE-PRESCRIPTION LEN))
 (33 3 (:REWRITE |(+ (+ x y) z)|))
 (28 28 (:TYPE-PRESCRIPTION ADE::GCD3$IN-SEQ))
 (28 28 (:REWRITE DEFAULT-CAR))
 (27 3 (:DEFINITION LEN))
 (26 20 (:REWRITE DEFAULT-+-2))
 (24 6 (:REWRITE ADE::OPEN-GCD3$INPUT-FORMAT-N-ZP))
 (24 6 (:REWRITE ADE::OPEN-GCD3$INPUT-FORMAT-N))
 (20 20 (:TYPE-PRESCRIPTION ADE::GCD3$OUT-ACT))
 (20 20 (:TYPE-PRESCRIPTION ADE::GCD3$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))
 (19 19 (:TYPE-PRESCRIPTION ADE::DE-N))
 (16 4 (:REWRITE ADE::OPEN-DE-N-ZP))
 (16 4 (:REWRITE ADE::OPEN-DE-N))
 (16 4 (:REWRITE ADE::GCD3$IN-ACT-INACTIVE))
 (15 15 (:REWRITE |(equal (- x) (- y))|))
 (15 3 (:REWRITE |(+ y x)|))
 (15 3 (:REWRITE |(+ c (+ d x))|))
 (14 14 (:TYPE-PRESCRIPTION ADE::GCD3$RUN))
 (12 3 (:REWRITE ADE::OPEN-GCD3$RUN-ZP))
 (12 3 (:REWRITE ADE::OPEN-GCD3$RUN))
 (8 8 (:TYPE-PRESCRIPTION ADE::GCD3$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 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 )