(ADE::WIG-WAG$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::WIG-WAG$INS-LEN)
(ADE::WIG-WAG*
 (44 44 (:TYPE-PRESCRIPTION POSP))
 )
(ADE::WIG-WAG*$DESTRUCTURE
 (240 24 (:DEFINITION BINARY-APPEND))
 (219 48 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (135 135 (:TYPE-PRESCRIPTION POSP))
 (34 34 (:REWRITE DEFAULT-CDR))
 (29 29 (:REWRITE DEFAULT-CAR))
 )
(ADE::NOT-PRIMP-WIG-WAG
 (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::WIG-WAG$NETLIST)
(ADE::WIG-WAG&)
(ADE::CHECK-WIG-WAG$NETLIST-64)
(ADE::WIG-WAG$ST-FORMAT)
(ADE::WIG-WAG$ST-FORMAT=>CONSTRAINT
 (7 1 (:DEFINITION LEN))
 (3 3 (:REWRITE NTH-WHEN-PREFIXP))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (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 PREFER-POSITIVE-ADDENDS-<))
 (1 1 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1 1 (:REWRITE NORMALIZE-ADDENDS))
 (1 1 (:REWRITE DEFAULT-CDR))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< (- x) (- y))|))
 )
(ADE::WIG-WAG$VALID-ST)
(ADE::WIG-WAG$VALID-ST=>CONSTRAINT
 (14 2 (:DEFINITION LEN))
 (10 10 (:REWRITE NTH-WHEN-PREFIXP))
 (10 8 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (10 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (10 8 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (8 8 (:REWRITE |(equal (- x) (- y))|))
 (8 2 (:DEFINITION STRIP-CARS))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (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-CDR))
 (4 4 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 (4 4 (:REWRITE |(< 0 (- x))|))
 (4 4 (:REWRITE |(< (- x) (- y))|))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2 2 (:REWRITE NORMALIZE-ADDENDS))
 (2 2 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 )
(ADE::WIG-WAG$VALID-ST=>ST-FORMAT
 (4 4 (:REWRITE NTH-WHEN-PREFIXP))
 )
(ADE::WIG-WAG$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-WIG-WAG$DATA-IN)
(ADE::WIG-WAG$BR-INPUTS
 (2 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::WIG-WAG$ME-INPUTS
 (2 2 (:TYPE-PRESCRIPTION ADE::F-BUF))
 )
(ADE::WIG-WAG$IN-ACT
 (10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-ALT-BRANCH$ACT))
 (5 5 (:TYPE-PRESCRIPTION ADE::ALT-BRANCH$INPUT-FORMAT))
 )
(ADE::WIG-WAG$IN-ACT-INACTIVE
 (410 8 (:REWRITE TAKE-OF-TOO-MANY))
 (154 4 (:REWRITE ADE::LEN-NTHCDR))
 (152 76 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (124 124 (:TYPE-PRESCRIPTION LEN))
 (116 12 (:DEFINITION LEN))
 (76 76 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (68 20 (:REWRITE DEFAULT-CAR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (56 8 (:REWRITE TAKE-WHEN-ATOM))
 (48 24 (:REWRITE DEFAULT-CDR))
 (33 33 (:REWRITE NTH-WHEN-PREFIXP))
 (32 32 (:TYPE-PRESCRIPTION BOOLEANP))
 (32 18 (:REWRITE SIMPLIFY-SUMS-<))
 (32 18 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (32 18 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (32 4 (:DEFINITION NTHCDR))
 (30 18 (:REWRITE DEFAULT-+-2))
 (28 28 (:LINEAR LEN-WHEN-PREFIXP))
 (26 18 (:REWRITE DEFAULT-<-2))
 (24 18 (:REWRITE DEFAULT-<-1))
 (24 8 (:REWRITE ADE::F-GATES=B-GATES))
 (24 8 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (24 8 (:REWRITE ADE::F-BUF-OF-3VP))
 (24 4 (:DEFINITION BINARY-APPEND))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (20 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (18 18 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (18 18 (:REWRITE NORMALIZE-ADDENDS))
 (18 18 (:REWRITE DEFAULT-+-1))
 (18 18 (:REWRITE |(< (- x) (- y))|))
 (16 16 (:TYPE-PRESCRIPTION ADE::3VP))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (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)|))
 (10 2 (:REWRITE |(+ c (+ d x))|))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (4 4 (:REWRITE REDUCE-INTEGERP-+))
 (4 4 (:REWRITE INTEGERP-MINUS-X))
 (4 4 (:REWRITE |(< (- x) 0)|))
 (4 4 (:META META-INTEGERP-CORRECT))
 (2 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE |(< d (+ c x))|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::WIG-WAG$OUT-ACT
 (10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-ALT-MERGE$ACT))
 (5 5 (:TYPE-PRESCRIPTION ADE::ALT-MERGE$INPUT-FORMAT))
 )
(ADE::WIG-WAG$OUT-ACT-INACTIVE
 (136 2 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (43 43 (:TYPE-PRESCRIPTION LEN))
 (38 19 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (30 12 (:REWRITE DEFAULT-CAR))
 (30 2 (:DEFINITION NTHCDR))
 (29 3 (:DEFINITION LEN))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (24 2 (:DEFINITION BINARY-APPEND))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (20 2 (:DEFINITION ADE::V-THREEFIX))
 (19 19 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (18 12 (:REWRITE DEFAULT-CDR))
 (16 16 (:TYPE-PRESCRIPTION BOOLEANP))
 (15 15 (:REWRITE NTH-WHEN-PREFIXP))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 2 (:REWRITE ADE::CAR-V-THREEFIX))
 (14 1 (:DEFINITION NATP))
 (12 12 (:TYPE-PRESCRIPTION ADE::3VP))
 (12 9 (:REWRITE DEFAULT-+-2))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 4 (:REWRITE ADE::V-THREEFIX-BVP))
 (12 4 (:REWRITE ADE::F-GATES=B-GATES))
 (12 4 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (12 4 (:REWRITE ADE::F-BUF-OF-3VP))
 (10 10 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (10 10 (:TYPE-PRESCRIPTION STRIP-CARS))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (10 2 (:REWRITE |(+ y x)|))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE NORMALIZE-ADDENDS))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 7 (:REWRITE DEFAULT-<-2))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:DEFINITION ADE::3V-FIX))
 (8 2 (:DEFINITION STRIP-CARS))
 (7 7 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (1 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (1 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::WIG-WAG$DATA-OUT)
(ADE::LEN-WIG-WAG$DATA-OUT-1
 (11 11 (:REWRITE NTH-WHEN-PREFIXP))
 (8 2 (:DEFINITION STRIP-CARS))
 (6 3 (:REWRITE DEFAULT-+-2))
 (5 5 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE DEFAULT-CAR))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (4 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (4 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE DEFAULT-+-1))
 (3 1 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (2 2 (:TYPE-PRESCRIPTION BOOLEANP))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (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 PREFER-POSITIVE-ADDENDS-<))
 (1 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE |(< 0 (- x))|))
 (1 1 (:REWRITE |(< (- x) (- y))|))
 )
(ADE::LEN-WIG-WAG$DATA-OUT-2
 (40 10 (:DEFINITION STRIP-CARS))
 (38 38 (:REWRITE NTH-WHEN-PREFIXP))
 (24 24 (:REWRITE DEFAULT-CAR))
 (16 16 (:REWRITE DEFAULT-CDR))
 (12 6 (:REWRITE DEFAULT-+-2))
 (12 4 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (10 8 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (10 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (10 8 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (8 8 (:REWRITE |(equal (- 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))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::BVP-WIG-WAG$DATA-OUT
 (1472 32 (:REWRITE TAKE-OF-TOO-MANY))
 (608 304 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (596 596 (:REWRITE NTH-WHEN-PREFIXP))
 (488 248 (:REWRITE DEFAULT-CAR))
 (448 16 (:REWRITE ADE::LEN-NTHCDR))
 (416 280 (:REWRITE DEFAULT-+-2))
 (416 32 (:DEFINITION NTHCDR))
 (398 302 (:REWRITE DEFAULT-CDR))
 (352 32 (:REWRITE |(+ (+ x y) z)|))
 (304 304 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (288 32 (:DEFINITION BINARY-APPEND))
 (280 280 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (280 280 (:REWRITE DEFAULT-+-1))
 (264 66 (:DEFINITION STRIP-CARS))
 (224 32 (:REWRITE TAKE-WHEN-ATOM))
 (180 18 (:DEFINITION ADE::V-THREEFIX))
 (160 64 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (116 116 (:TYPE-PRESCRIPTION BOOLEANP))
 (112 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (97 49 (:REWRITE SIMPLIFY-SUMS-<))
 (97 49 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (97 49 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (96 96 (:LINEAR LEN-WHEN-PREFIXP))
 (96 16 (:REWRITE ADE::WIG-WAG$OUT-ACT-INACTIVE))
 (81 49 (:REWRITE DEFAULT-<-2))
 (80 80 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
 (72 68 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (72 68 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (72 68 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (68 68 (:REWRITE |(equal (- x) (- y))|))
 (68 34 (:DEFINITION ADE::3V-FIX))
 (65 49 (:REWRITE DEFAULT-<-1))
 (54 54 (:TYPE-PRESCRIPTION ADE::3VP))
 (49 49 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (49 49 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (49 49 (:REWRITE |(< (- x) (- y))|))
 (48 48 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (42 10 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (32 32 (:TYPE-PRESCRIPTION NFIX))
 (32 32 (:REWRITE DEFAULT-UNARY-MINUS))
 (30 10 (:REWRITE ADE::F-BUF-OF-3VP))
 (16 16 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (16 16 (:REWRITE DEFAULT-*-2))
 (16 16 (:REWRITE DEFAULT-*-1))
 (16 16 (:REWRITE |(< d (+ c x))|))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 4 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
 (10 2 (:DEFINITION TRUE-LISTP))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP-LEN))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE |(< 0 (- x))|))
 )
(ADE::WIG-WAG$OUTPUTS)
(ADE::WIG-WAG$VALUE
 (1212 68 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (712 100 (:DEFINITION BINARY-APPEND))
 (504 200 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (335 190 (:REWRITE DEFAULT-+-2))
 (190 190 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (190 190 (:REWRITE DEFAULT-+-1))
 (182 5 (:REWRITE ADE::ALT-BRANCH$ACT-INACTIVE))
 (172 172 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (156 36 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (142 142 (:REWRITE NTH-WHEN-PREFIXP))
 (141 13 (:REWRITE LEN-OF-APPEND))
 (134 4 (:REWRITE ADE::ALT-MERGE$ACT-INACTIVE))
 (126 42 (:REWRITE ADE::CAR-V-THREEFIX))
 (102 34 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (91 67 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (91 67 (:REWRITE ADE::F-BUF-OF-3VP))
 (84 42 (:DEFINITION ADE::3V-FIX))
 (80 16 (:REWRITE ADE::DISJOINT-ATOM))
 (76 6 (:REWRITE ADE::ALT-BRANCH$ACT1-INACTIVE))
 (73 5 (:REWRITE ADE::ALT-MERGE$ACT1-INACTIVE))
 (71 33 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (71 33 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (71 33 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (69 5 (:REWRITE ADE::ALT-BRANCH$ACT0-INACTIVE))
 (68 68 (:TYPE-PRESCRIPTION PAIRLIS$))
 (66 66 (:TYPE-PRESCRIPTION ADE::3VP))
 (60 16 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
 (60 4 (:REWRITE ADE::ALT-MERGE$ACT0-INACTIVE))
 (58 12 (:REWRITE |(+ y x)|))
 (57 41 (:REWRITE ADE::V-THREEFIX-BVP))
 (49 5 (:REWRITE |(+ y (+ x z))|))
 (44 30 (:REWRITE TAKE-WHEN-ATOM))
 (43 1 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (41 41 (:DEFINITION STRIP-CARS))
 (33 33 (:REWRITE |(equal (- x) (- y))|))
 (30 30 (:TYPE-PRESCRIPTION BOOLEANP))
 (28 28 (:TYPE-PRESCRIPTION ADE::BVP))
 (26 26 (:LINEAR LEN-WHEN-PREFIXP))
 (18 8 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (16 16 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (16 16 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (16 4 (:REWRITE |(+ x x)|))
 (15 6 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (15 6 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (15 2 (:REWRITE SIMPLIFY-SUMS-<))
 (13 13 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 1 (:REWRITE ADE::WIG-WAG$OUT-ACT-INACTIVE))
 (9 9 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (9 9 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (9 9 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (9 9 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (8 2 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
 (8 2 (:DEFINITION TRUE-LISTP))
 (5 1 (:REWRITE ADE::WIG-WAG$IN-ACT-INACTIVE))
 (4 4 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (4 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (4 4 (:REWRITE DEFAULT-*-2))
 (4 4 (:REWRITE DEFAULT-*-1))
 (3 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE CONSP-OF-APPEND))
 (1 1 (:REWRITE |(< d (+ c x))|))
 (1 1 (:REWRITE |(< 0 (- x))|))
 )
(ADE::WIG-WAG$STEP
 (12 12 (:TYPE-PRESCRIPTION ADE::ALT-MERGE$INPUT-FORMAT))
 (12 12 (:TYPE-PRESCRIPTION ADE::ALT-BRANCH$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-ALT-MERGE$ACT1))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-ALT-MERGE$ACT0))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-ALT-BRANCH$ACT1))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-ALT-BRANCH$ACT0))
 )
(ADE::WIG-WAG$STATE
 (1526 224 (:DEFINITION BINARY-APPEND))
 (987 448 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (667 374 (:REWRITE DEFAULT-+-2))
 (374 374 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (374 374 (:REWRITE DEFAULT-+-1))
 (318 106 (:REWRITE ADE::CAR-V-THREEFIX))
 (312 72 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (288 22 (:REWRITE ADE::UPDATE-ALIST-OF-NOT-A-KEY))
 (282 26 (:REWRITE LEN-OF-APPEND))
 (264 88 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (249 249 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (214 180 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (214 180 (:REWRITE ADE::F-BUF-OF-3VP))
 (212 106 (:DEFINITION ADE::3V-FIX))
 (203 203 (:REWRITE NTH-WHEN-PREFIXP))
 (185 8 (:REWRITE ADE::ALT-BRANCH$ACT-INACTIVE))
 (180 36 (:DEFINITION ALISTP))
 (170 22 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (160 32 (:REWRITE ADE::DISJOINT-ATOM))
 (158 14 (:REWRITE ADE::ALT-MERGE$ACT0-INACTIVE))
 (157 17 (:REWRITE ADE::ALT-BRANCH$ACT1-INACTIVE))
 (154 14 (:REWRITE ADE::ALT-MERGE$ACT1-INACTIVE))
 (146 18 (:REWRITE ADE::ALT-BRANCH$ACT0-INACTIVE))
 (141 113 (:REWRITE ADE::V-THREEFIX-BVP))
 (140 140 (:TYPE-PRESCRIPTION ADE::3VP))
 (133 7 (:REWRITE ADE::ALT-MERGE$ACT-INACTIVE))
 (123 123 (:TYPE-PRESCRIPTION PAIRLIS$))
 (120 32 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
 (110 110 (:DEFINITION STRIP-CARS))
 (108 91 (:REWRITE TAKE-WHEN-ATOM))
 (108 56 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (108 56 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (108 56 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (103 21 (:REWRITE |(+ y x)|))
 (102 102 (:TYPE-PRESCRIPTION ALISTP))
 (93 9 (:REWRITE |(+ y (+ x z))|))
 (56 56 (:REWRITE |(equal (- x) (- y))|))
 (52 52 (:TYPE-PRESCRIPTION BOOLEANP))
 (43 1 (:REWRITE PREFIXP-OF-APPEND-ARG1))
 (42 42 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
 (42 42 (:LINEAR LEN-WHEN-PREFIXP))
 (40 40 (:TYPE-PRESCRIPTION ADE::BVP))
 (32 32 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
 (32 32 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
 (32 8 (:REWRITE |(+ x x)|))
 (22 22 (:TYPE-PRESCRIPTION ADE::FV-IF))
 (21 21 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (20 20 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (20 20 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (20 20 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (20 20 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 (20 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (20 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (15 2 (:REWRITE SIMPLIFY-SUMS-<))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (9 3 (:REWRITE ADE::BOOLEANP-ALT-BRANCH$ACT1))
 (9 3 (:REWRITE ADE::BOOLEANP-ALT-BRANCH$ACT0))
 (8 8 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (8 8 (:REWRITE DEFAULT-*-2))
 (8 8 (:REWRITE DEFAULT-*-1))
 (8 2 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
 (8 2 (:DEFINITION TRUE-LISTP))
 (4 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-RIGHT))
 (2 2 (:REWRITE LIST-EQUIV-WHEN-ATOM-LEFT))
 (2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 1 (:REWRITE DEFAULT-<-2))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (1 1 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE CONSP-OF-APPEND))
 (1 1 (:REWRITE |(< d (+ c x))|))
 (1 1 (:REWRITE |(< 0 (- x))|))
 )
(ADE::WIG-WAG$INPUT-FORMAT)
(ADE::WIG-WAG$INPUT-FORMAT=>BR$INPUT-FORMAT
 (840 16 (:REWRITE TAKE-OF-TOO-MANY))
 (296 128 (:REWRITE DEFAULT-CDR))
 (275 21 (:DEFINITION NTHCDR))
 (256 6 (:REWRITE ADE::LEN-NTHCDR))
 (250 58 (:REWRITE DEFAULT-CAR))
 (231 21 (:REWRITE |(+ (+ x y) z)|))
 (200 4 (:REWRITE LEN-OF-APPEND))
 (157 33 (:REWRITE |(+ y x)|))
 (153 116 (:REWRITE DEFAULT-+-2))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (116 116 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (116 116 (:REWRITE DEFAULT-+-1))
 (101 35 (:REWRITE SIMPLIFY-SUMS-<))
 (84 14 (:DEFINITION BINARY-APPEND))
 (76 16 (:REWRITE TAKE-WHEN-ATOM))
 (73 73 (:REWRITE NTH-WHEN-PREFIXP))
 (70 28 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (53 35 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (43 43 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (43 43 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (41 31 (:REWRITE DEFAULT-<-1))
 (39 39 (:REWRITE |(< (- x) (- y))|))
 (39 31 (:REWRITE DEFAULT-<-2))
 (36 36 (:LINEAR LEN-WHEN-PREFIXP))
 (26 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (20 4 (:REWRITE |(+ y (+ x z))|))
 (18 18 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (18 2 (:DEFINITION TRUE-LISTP))
 (16 16 (:TYPE-PRESCRIPTION NFIX))
 (16 16 (:REWRITE DEFAULT-UNARY-MINUS))
 (16 12 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (16 12 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (16 12 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (:REWRITE |(equal (- x) (- y))|))
 (11 11 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (11 11 (:REWRITE |(< 0 (- x))|))
 (10 10 (:REWRITE |(< d (+ c x))|))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (8 8 (:REWRITE DEFAULT-UNARY-/))
 (8 4 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (8 2 (:DEFINITION STRIP-CARS))
 (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::WIG-WAG$INPUT-FORMAT=>ME$INPUT-FORMAT
 (1612 24 (:REWRITE TAKE-OF-TOO-MANY))
 (764 16 (:REWRITE LEN-OF-APPEND))
 (379 29 (:DEFINITION NTHCDR))
 (356 212 (:REWRITE DEFAULT-CDR))
 (341 236 (:REWRITE DEFAULT-+-2))
 (319 29 (:REWRITE |(+ (+ x y) z)|))
 (262 70 (:REWRITE DEFAULT-CAR))
 (256 6 (:REWRITE ADE::LEN-NTHCDR))
 (236 236 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (236 236 (:REWRITE DEFAULT-+-1))
 (225 55 (:REWRITE SIMPLIFY-SUMS-<))
 (156 18 (:DEFINITION BINARY-APPEND))
 (120 24 (:REWRITE TAKE-WHEN-ATOM))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (100 12 (:REWRITE |(+ y (+ x z))|))
 (90 36 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (86 22 (:REWRITE |(< d (+ c x))|))
 (81 81 (:REWRITE NTH-WHEN-PREFIXP))
 (75 75 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (75 75 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (73 55 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (63 63 (:REWRITE |(< (- x) (- y))|))
 (57 47 (:REWRITE DEFAULT-<-1))
 (56 8 (:REWRITE ADE::CAR-V-THREEFIX))
 (55 47 (:REWRITE DEFAULT-<-2))
 (40 10 (:DEFINITION STRIP-CARS))
 (40 4 (:DEFINITION ADE::V-THREEFIX))
 (36 36 (:REWRITE DEFAULT-UNARY-MINUS))
 (36 36 (:LINEAR LEN-WHEN-PREFIXP))
 (26 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (24 24 (:TYPE-PRESCRIPTION NFIX))
 (24 12 (:DEFINITION ADE::3V-FIX))
 (19 19 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (19 19 (:REWRITE |(< 0 (- x))|))
 (18 18 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (18 2 (:DEFINITION TRUE-LISTP))
 (16 16 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (16 16 (:REWRITE DEFAULT-UNARY-/))
 (16 12 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (16 12 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (16 12 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (16 4 (:REWRITE |(+ x x)|))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 12 (:TYPE-PRESCRIPTION ADE::3VP))
 (12 12 (:REWRITE |(equal (- x) (- y))|))
 (8 8 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (8 8 (:REWRITE DEFAULT-*-2))
 (8 8 (:REWRITE DEFAULT-*-1))
 (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-WIG-WAG$IN-ACT
 (78 78 (:REWRITE NTH-WHEN-PREFIXP))
 (60 4 (:REWRITE ADE::ALT-BRANCH$ACT-INACTIVE))
 (24 6 (:DEFINITION STRIP-CARS))
 (20 10 (:REWRITE DEFAULT-+-2))
 (18 16 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (18 16 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (18 16 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (16 16 (:REWRITE DEFAULT-CDR))
 (16 16 (:REWRITE |(equal (- x) (- y))|))
 (12 12 (:REWRITE DEFAULT-CAR))
 (10 10 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (10 10 (:REWRITE NORMALIZE-ADDENDS))
 (10 10 (:REWRITE DEFAULT-+-1))
 (8 4 (:REWRITE ADE::WIG-WAG$IN-ACT-INACTIVE))
 )
(ADE::BOOLEANP-WIG-WAG$OUT-ACT
 (78 78 (:REWRITE NTH-WHEN-PREFIXP))
 (48 4 (:REWRITE ADE::ALT-MERGE$ACT-INACTIVE))
 (24 6 (:DEFINITION STRIP-CARS))
 (24 4 (:REWRITE ADE::WIG-WAG$OUT-ACT-INACTIVE))
 (20 10 (:REWRITE DEFAULT-+-2))
 (18 16 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (18 16 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (18 16 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (16 16 (:REWRITE DEFAULT-CDR))
 (16 16 (:REWRITE |(equal (- x) (- y))|))
 (12 12 (:REWRITE DEFAULT-CAR))
 (10 10 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (10 10 (:REWRITE NORMALIZE-ADDENDS))
 (10 10 (:REWRITE DEFAULT-+-1))
 )
(ADE::WIG-WAG$ST-FORMAT-PRESERVED
 (82 4 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (55 55 (:REWRITE NTH-WHEN-PREFIXP))
 (20 20 (:TYPE-PRESCRIPTION ADE::ALT-BRANCH$INPUT-FORMAT))
 (20 2 (:REWRITE ADE::ALT-BRANCH$ACT1-INACTIVE))
 (20 2 (:REWRITE ADE::ALT-BRANCH$ACT0-INACTIVE))
 (18 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-ALT-BRANCH$ACT1))
 (18 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-ALT-BRANCH$ACT0))
 (16 4 (:DEFINITION STRIP-CARS))
 (14 2 (:DEFINITION LEN))
 (12 12 (:TYPE-PRESCRIPTION ADE::WIG-WAG$BR-INPUTS))
 (12 12 (:REWRITE DEFAULT-CAR))
 (12 2 (:REWRITE ADE::BOOLEANP-ALT-BRANCH$ACT0))
 (10 8 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (10 8 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (10 8 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (10 4 (:REWRITE ADE::WIG-WAG$INPUT-FORMAT=>BR$INPUT-FORMAT))
 (10 2 (:REWRITE ADE::BOOLEANP-ALT-BRANCH$ACT1))
 (10 2 (:DEFINITION PAIRLIS$))
 (10 1 (:REWRITE ADE::ALT-MERGE$ACT1-INACTIVE))
 (10 1 (:REWRITE ADE::ALT-MERGE$ACT0-INACTIVE))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE |(equal (- x) (- y))|))
 (6 6 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT))
 (6 6 (:TYPE-PRESCRIPTION ADE::ALT-BRANCH$ACT1))
 (6 6 (:TYPE-PRESCRIPTION ADE::ALT-BRANCH$ACT0))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2 2 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE |(< 0 (- x))|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 )
(ADE::WIG-WAG$VALUE-ALT
 (416 32 (:DEFINITION NTHCDR))
 (352 32 (:REWRITE |(+ (+ x y) z)|))
 (252 9 (:REWRITE ADE::LEN-NTHCDR))
 (160 32 (:REWRITE |(+ y x)|))
 (150 21 (:DEFINITION BINARY-APPEND))
 (140 122 (:REWRITE DEFAULT-+-2))
 (126 18 (:DEFINITION LEN))
 (122 122 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (122 122 (:REWRITE DEFAULT-+-1))
 (117 18 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (90 42 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (81 9 (:DEFINITION TRUE-LISTP))
 (80 80 (:REWRITE DEFAULT-CDR))
 (65 65 (:REWRITE NTH-WHEN-PREFIXP))
 (48 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (45 11 (:REWRITE ADE::WIG-WAG$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 |(equal (- x) (- y))|))
 (21 21 (: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 DEFAULT-UNARY-MINUS))
 )
(ADE::WIG-WAG$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))
 (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 DEFAULT-UNARY-MINUS))
 )
(ADE::WIG-WAG$RUN)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-WIG-WAG$RUN-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-WIG-WAG$RUN)
(ADE::WIG-WAG$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::WIG-WAG$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-WIG-WAG$INPUT-FORMAT-N-ZP)
(DEFOPENER-HINT
 (5 5 (:TYPE-PRESCRIPTION LAST))
 )
(DEFOPENER-TEMP)
(ADE::OPEN-WIG-WAG$INPUT-FORMAT-N)
(ADE::WIG-WAG$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::WIG-WAG$DE-N
 (265 30 (:REWRITE ZP-OPEN))
 (108 12 (:REWRITE |(< d (+ c x))|))
 (62 2 (:DEFINITION ADE::WIG-WAG$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::WIG-WAG$INPUT-FORMAT-PLUS))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE ADE::DE-PLUS))
 )
(ADE::WIG-WAG$EXTRACT)
(ADE::WIG-WAG$EXTRACT-NOT-EMPTY
 (952 14 (:REWRITE TAKE-OF-TOO-MANY))
 (504 7 (:REWRITE ADE::LEN-NTHCDR))
 (420 14 (:REWRITE |(< x (if a b c))|))
 (386 386 (:REWRITE NTH-WHEN-PREFIXP))
 (304 160 (:REWRITE DEFAULT-CAR))
 (284 142 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (236 16 (:DEFINITION NTHCDR))
 (229 181 (:REWRITE DEFAULT-CDR))
 (192 48 (:DEFINITION STRIP-CARS))
 (192 16 (:DEFINITION BINARY-APPEND))
 (182 28 (:REWRITE |(+ (if a b c) x)|))
 (176 16 (:REWRITE |(+ (+ x y) z)|))
 (166 107 (:REWRITE DEFAULT-+-2))
 (160 16 (:DEFINITION ADE::V-THREEFIX))
 (142 142 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (114 114 (:LINEAR LEN-WHEN-PREFIXP))
 (112 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (107 107 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (107 107 (:REWRITE NORMALIZE-ADDENDS))
 (107 107 (:REWRITE DEFAULT-+-1))
 (98 14 (:REWRITE TAKE-WHEN-ATOM))
 (98 7 (:DEFINITION NATP))
 (96 32 (:REWRITE ADE::V-THREEFIX-BVP))
 (84 49 (:REWRITE SIMPLIFY-SUMS-<))
 (84 49 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (84 49 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (80 80 (:TYPE-PRESCRIPTION STRIP-CARS))
 (80 32 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (80 16 (:REWRITE |(+ y x)|))
 (75 60 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (75 60 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (75 60 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (70 49 (:REWRITE DEFAULT-<-1))
 (64 64 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (64 32 (:DEFINITION ADE::3V-FIX))
 (63 49 (:REWRITE DEFAULT-<-2))
 (60 60 (:REWRITE |(equal (- x) (- y))|))
 (57 57 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (54 27 (:TYPE-PRESCRIPTION ADE::BOOLEANP-WIG-WAG$OUT-ACT))
 (49 49 (:REWRITE |(< (- x) (- y))|))
 (46 46 (:TYPE-PRESCRIPTION ADE::3VP))
 (42 7 (:REWRITE ADE::WIG-WAG$OUT-ACT-INACTIVE))
 (28 28 (:TYPE-PRESCRIPTION BOOLEANP))
 (21 7 (:REWRITE ADE::F-GATES=B-GATES))
 (21 7 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (21 7 (:REWRITE ADE::F-BUF-OF-3VP))
 (14 14 (:TYPE-PRESCRIPTION NFIX))
 (14 14 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (14 14 (:REWRITE REDUCE-INTEGERP-+))
 (14 14 (:REWRITE INTEGERP-MINUS-X))
 (14 14 (:REWRITE |(< (- x) 0)|))
 (14 14 (:META META-INTEGERP-CORRECT))
 (10 10 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (7 7 (:TYPE-PRESCRIPTION NATP))
 (7 7 (:REWRITE |(< d (+ c x))|))
 (7 7 (:DEFINITION ADE::ALT-MERGE$ACT))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-=-0))
 (1 1 (:REWRITE |(equal (- x) 0)|))
 )
(ADE::WIG-WAG$INV)
(ADE::WIG-WAG$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 DEFAULT-CDR))
 )
(ADE::WIG-WAG$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::WIG-WAG$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 ADE::WIG-WAG$INPUT-FORMAT-LEMMA-1))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::WIG-WAG$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::WIG-WAG$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 ADE::WIG-WAG$INPUT-FORMAT-LEMMA-2))
 (1 1 (:REWRITE ADE::WIG-WAG$INPUT-FORMAT-LEMMA-1))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::WIG-WAG$INV-PRESERVED
 (13650 13650 (:REWRITE NTH-WHEN-PREFIXP))
 (7362 2242 (:REWRITE DEFAULT-CAR))
 (6916 532 (:DEFINITION NTHCDR))
 (5852 532 (:REWRITE |(+ (+ x y) z)|))
 (5152 3566 (:REWRITE DEFAULT-+-2))
 (4378 3226 (:REWRITE DEFAULT-CDR))
 (4342 948 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (4342 948 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (4342 948 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3566 3566 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3566 3566 (:REWRITE DEFAULT-+-1))
 (2708 324 (:DEFINITION TRUE-LISTP))
 (1968 246 (:DEFINITION STRIP-CARS))
 (1944 648 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (1152 1152 (:LINEAR LEN-WHEN-PREFIXP))
 (1080 108 (:DEFINITION ADE::V-THREEFIX))
 (974 94 (:DEFINITION PAIRLIS$))
 (948 948 (:REWRITE |(equal (- x) (- y))|))
 (896 32 (:REWRITE ADE::LEN-NTHCDR))
 (756 108 (:REWRITE ADE::CAR-V-THREEFIX))
 (588 84 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (576 576 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (576 72 (:DEFINITION BINARY-APPEND))
 (544 72 (:REWRITE ADE::FV-IF-WHEN-BVP))
 (448 64 (:REWRITE TAKE-WHEN-ATOM))
 (432 216 (:DEFINITION ADE::3V-FIX))
 (384 384 (:TYPE-PRESCRIPTION ADE::3VP))
 (360 144 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (302 86 (:REWRITE ADE::WIG-WAG$INPUT-FORMAT-LEMMA-3))
 (252 84 (:REWRITE ADE::F-BUF-OF-3VP))
 (236 236 (:REWRITE DEFAULT-UNARY-MINUS))
 (192 96 (:REWRITE SIMPLIFY-SUMS-<))
 (192 96 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (192 96 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (160 96 (:REWRITE DEFAULT-<-2))
 (128 96 (:REWRITE DEFAULT-<-1))
 (108 108 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (96 96 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (96 96 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (96 96 (:REWRITE |(< (- x) (- y))|))
 (64 64 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (64 64 (:REWRITE DEFAULT-*-2))
 (64 64 (:REWRITE DEFAULT-*-1))
 (32 32 (:REWRITE |(< d (+ c x))|))
 (24 8 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
 (20 20 (:TYPE-PRESCRIPTION ADE::FV-IF))
 )
(ADE::WIG-WAG$EXTRACTED-STEP
 (24 12 (:TYPE-PRESCRIPTION ADE::BOOLEANP-WIG-WAG$IN-ACT))
 (18 18 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT))
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-WIG-WAG$OUT-ACT))
 )
(ADE::WIG-WAG$EXTRACTED-STEP-CORRECT
 (16412 16412 (:REWRITE NTH-WHEN-PREFIXP))
 (9466 3542 (:REWRITE DEFAULT-CAR))
 (7748 596 (:DEFINITION NTHCDR))
 (7228 4766 (:REWRITE DEFAULT-+-2))
 (6658 5122 (:REWRITE DEFAULT-CDR))
 (6556 596 (:REWRITE |(+ (+ x y) z)|))
 (6448 3224 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (4848 606 (:DEFINITION STRIP-CARS))
 (4766 4766 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (4766 4766 (:REWRITE DEFAULT-+-1))
 (4580 1016 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (4580 1016 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (4580 1016 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2820 340 (:DEFINITION TRUE-LISTP))
 (2480 92 (:REWRITE ADE::LEN-NTHCDR))
 (2040 680 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (2024 2024 (:TYPE-PRESCRIPTION ADE::BOOLEANP-WIG-WAG$IN-ACT))
 (2016 280 (:DEFINITION BINARY-APPEND))
 (1520 152 (:DEFINITION ADE::V-THREEFIX))
 (1496 1496 (:LINEAR LEN-WHEN-PREFIXP))
 (1340 560 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (1298 194 (:REWRITE TAKE-WHEN-ATOM))
 (1176 120 (:DEFINITION PAIRLIS$))
 (1064 152 (:REWRITE ADE::CAR-V-THREEFIX))
 (1016 1016 (:REWRITE |(equal (- x) (- y))|))
 (1012 1012 (:TYPE-PRESCRIPTION ADE::BOOLEANP-WIG-WAG$OUT-ACT))
 (748 748 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (608 304 (:DEFINITION ADE::3V-FIX))
 (552 276 (:REWRITE SIMPLIFY-SUMS-<))
 (552 276 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (552 276 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (460 276 (:REWRITE DEFAULT-<-2))
 (432 432 (:REWRITE DEFAULT-UNARY-MINUS))
 (404 404 (:TYPE-PRESCRIPTION ADE::3VP))
 (368 276 (:REWRITE DEFAULT-<-1))
 (334 50 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (276 276 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (276 276 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (276 276 (:REWRITE |(< (- x) (- y))|))
 (150 50 (:REWRITE ADE::F-BUF-OF-3VP))
 (144 36 (:REWRITE ADE::WIG-WAG$IN-ACT-INACTIVE))
 (136 136 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (136 136 (:REWRITE DEFAULT-*-2))
 (136 136 (:REWRITE DEFAULT-*-1))
 (105 105 (:TYPE-PRESCRIPTION ADE::F-NOT))
 (92 92 (:REWRITE |(< d (+ c x))|))
 (36 12 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
 )
(ADE::WIG-WAG$BR-ACT0-INACTIVE
 (410 8 (:REWRITE TAKE-OF-TOO-MANY))
 (186 93 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (154 4 (:REWRITE ADE::LEN-NTHCDR))
 (124 124 (:TYPE-PRESCRIPTION LEN))
 (116 12 (:DEFINITION LEN))
 (93 93 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (88 16 (:REWRITE DEFAULT-CAR))
 (65 5 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (65 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (65 5 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (56 8 (:REWRITE TAKE-WHEN-ATOM))
 (51 51 (:REWRITE NTH-WHEN-PREFIXP))
 (48 24 (:REWRITE DEFAULT-CDR))
 (36 4 (:REWRITE ADE::F-GATES=B-GATES))
 (36 4 (: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))
 (30 18 (:REWRITE DEFAULT-+-2))
 (28 28 (:LINEAR LEN-WHEN-PREFIXP))
 (26 18 (:REWRITE DEFAULT-<-2))
 (24 18 (:REWRITE DEFAULT-<-1))
 (24 4 (:DEFINITION BINARY-APPEND))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (20 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (18 18 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (18 18 (:REWRITE NORMALIZE-ADDENDS))
 (18 18 (:REWRITE DEFAULT-+-1))
 (18 18 (:REWRITE |(< (- x) (- y))|))
 (16 16 (:TYPE-PRESCRIPTION BOOLEANP))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (14 14 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 4 (:REWRITE ADE::F-BUF-OF-3VP))
 (10 2 (:REWRITE |(+ y x)|))
 (10 2 (:REWRITE |(+ c (+ d x))|))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (8 8 (:TYPE-PRESCRIPTION ADE::3VP))
 (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 |(< (- x) 0)|))
 (4 4 (:META META-INTEGERP-CORRECT))
 (2 2 (:REWRITE |(< d (+ c x))|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::WIG-WAG$BR-ACT1-INACTIVE
 (410 8 (:REWRITE TAKE-OF-TOO-MANY))
 (160 80 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (154 4 (:REWRITE ADE::LEN-NTHCDR))
 (124 124 (:TYPE-PRESCRIPTION LEN))
 (116 12 (:DEFINITION LEN))
 (101 101 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT-LEMMA-2))
 (88 16 (:REWRITE DEFAULT-CAR))
 (80 80 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (56 8 (:REWRITE TAKE-WHEN-ATOM))
 (54 54 (:REWRITE NTH-WHEN-PREFIXP))
 (48 24 (:REWRITE DEFAULT-CDR))
 (36 4 (:REWRITE ADE::F-GATES=B-GATES))
 (36 4 (: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))
 (30 18 (:REWRITE DEFAULT-+-2))
 (29 5 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (29 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (29 5 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (28 28 (:LINEAR LEN-WHEN-PREFIXP))
 (26 18 (:REWRITE DEFAULT-<-2))
 (24 18 (:REWRITE DEFAULT-<-1))
 (24 4 (:DEFINITION BINARY-APPEND))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (20 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (18 18 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (18 18 (:REWRITE NORMALIZE-ADDENDS))
 (18 18 (:REWRITE DEFAULT-+-1))
 (18 18 (:REWRITE |(< (- x) (- y))|))
 (16 16 (:TYPE-PRESCRIPTION BOOLEANP))
 (16 1 (:REWRITE ADE::NFIX-OF-NAT))
 (14 14 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (14 1 (:DEFINITION NATP))
 (13 2 (:REWRITE |(+ (if a b c) x)|))
 (12 4 (:REWRITE ADE::F-BUF-OF-3VP))
 (10 2 (:REWRITE |(+ y x)|))
 (10 2 (:REWRITE |(+ c (+ d x))|))
 (8 8 (:TYPE-PRESCRIPTION NFIX))
 (8 8 (:TYPE-PRESCRIPTION ADE::3VP))
 (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 |(< (- x) 0)|))
 (4 4 (:META META-INTEGERP-CORRECT))
 (2 2 (:REWRITE |(< d (+ c x))|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(ADE::WIG-WAG$ME-ACT0-INACTIVE
 (136 2 (:REWRITE TAKE-OF-TOO-MANY))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (43 43 (:TYPE-PRESCRIPTION LEN))
 (38 19 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (35 11 (:REWRITE DEFAULT-CAR))
 (30 2 (:DEFINITION NTHCDR))
 (29 3 (:DEFINITION LEN))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (24 2 (:DEFINITION BINARY-APPEND))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (20 2 (:DEFINITION ADE::V-THREEFIX))
 (19 19 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (18 12 (:REWRITE DEFAULT-CDR))
 (17 15 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT-LEMMA-2))
 (16 2 (:DEFINITION STRIP-CARS))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 2 (:REWRITE ADE::CAR-V-THREEFIX))
 (14 1 (:DEFINITION NATP))
 (12 9 (:REWRITE DEFAULT-+-2))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 4 (:REWRITE ADE::V-THREEFIX-BVP))
 (11 11 (:REWRITE NTH-WHEN-PREFIXP))
 (10 10 (:TYPE-PRESCRIPTION STRIP-CARS))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (10 2 (:REWRITE |(+ y x)|))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE NORMALIZE-ADDENDS))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 7 (:REWRITE DEFAULT-<-2))
 (9 1 (:REWRITE ADE::F-GATES=B-GATES))
 (9 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:DEFINITION ADE::3V-FIX))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (7 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (7 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (6 6 (:TYPE-PRESCRIPTION ADE::3VP))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::WIG-WAG$ME-ACT1-INACTIVE
 (136 2 (:REWRITE TAKE-OF-TOO-MANY))
 (72 46 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT-LEMMA-1))
 (72 1 (:REWRITE ADE::LEN-NTHCDR))
 (60 2 (:REWRITE |(< x (if a b c))|))
 (43 43 (:TYPE-PRESCRIPTION LEN))
 (38 19 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (35 11 (:REWRITE DEFAULT-CAR))
 (30 2 (:DEFINITION NTHCDR))
 (29 3 (:DEFINITION LEN))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (24 2 (:DEFINITION BINARY-APPEND))
 (22 2 (:REWRITE |(+ (+ x y) z)|))
 (20 2 (:DEFINITION ADE::V-THREEFIX))
 (19 19 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (18 12 (:REWRITE DEFAULT-CDR))
 (16 2 (:DEFINITION STRIP-CARS))
 (14 2 (:REWRITE TAKE-WHEN-ATOM))
 (14 2 (:REWRITE ADE::CAR-V-THREEFIX))
 (14 1 (:DEFINITION NATP))
 (12 12 (:REWRITE NTH-WHEN-PREFIXP))
 (12 9 (:REWRITE DEFAULT-+-2))
 (12 7 (:REWRITE SIMPLIFY-SUMS-<))
 (12 7 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (12 7 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (12 4 (:REWRITE ADE::V-THREEFIX-BVP))
 (10 10 (:TYPE-PRESCRIPTION STRIP-CARS))
 (10 10 (:LINEAR LEN-WHEN-PREFIXP))
 (10 7 (:REWRITE DEFAULT-<-1))
 (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (10 2 (:REWRITE |(+ y x)|))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (9 9 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (9 9 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (9 9 (:REWRITE NORMALIZE-ADDENDS))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 7 (:REWRITE DEFAULT-<-2))
 (9 1 (:REWRITE ADE::F-GATES=B-GATES))
 (9 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 4 (:DEFINITION ADE::3V-FIX))
 (7 7 (:REWRITE |(< (- x) (- y))|))
 (7 1 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (7 1 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (7 1 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (6 6 (:TYPE-PRESCRIPTION ADE::3VP))
 (5 5 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION NFIX))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:REWRITE |(< (- x) 0)|))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 (1 1 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE |(< d (+ c x))|))
 )
(ADE::WIG-WAG$BR-ACTS-INACTIVE
 (820 16 (:REWRITE TAKE-OF-TOO-MANY))
 (308 8 (:REWRITE ADE::LEN-NTHCDR))
 (248 248 (:TYPE-PRESCRIPTION LEN))
 (232 40 (:REWRITE DEFAULT-CAR))
 (232 24 (:DEFINITION LEN))
 (144 16 (:REWRITE ADE::F-GATES=B-GATES))
 (144 16 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (120 4 (:REWRITE |(< x (if a b c))|))
 (112 16 (:REWRITE TAKE-WHEN-ATOM))
 (96 48 (:REWRITE DEFAULT-CDR))
 (64 64 (:TYPE-PRESCRIPTION BOOLEANP))
 (64 36 (:REWRITE SIMPLIFY-SUMS-<))
 (64 36 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (64 36 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (64 8 (:DEFINITION NTHCDR))
 (63 63 (:REWRITE NTH-WHEN-PREFIXP))
 (60 36 (:REWRITE DEFAULT-+-2))
 (56 56 (:LINEAR LEN-WHEN-PREFIXP))
 (52 36 (:REWRITE DEFAULT-<-2))
 (48 36 (:REWRITE DEFAULT-<-1))
 (48 16 (:REWRITE ADE::F-BUF-OF-3VP))
 (48 8 (:DEFINITION BINARY-APPEND))
 (44 4 (:REWRITE |(+ (+ x y) z)|))
 (40 40 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (40 40 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (40 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (36 36 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (36 36 (:REWRITE NORMALIZE-ADDENDS))
 (36 36 (:REWRITE DEFAULT-+-1))
 (36 36 (:REWRITE |(< (- x) (- y))|))
 (35 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (35 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (35 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (32 32 (:TYPE-PRESCRIPTION ADE::3VP))
 (32 2 (:REWRITE ADE::NFIX-OF-NAT))
 (28 28 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (28 2 (:DEFINITION NATP))
 (26 4 (:REWRITE |(+ (if a b c) x)|))
 (20 4 (:REWRITE |(+ y x)|))
 (20 4 (:REWRITE |(+ c (+ d x))|))
 (16 16 (:TYPE-PRESCRIPTION NFIX))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (8 8 (:REWRITE REDUCE-INTEGERP-+))
 (8 8 (:REWRITE INTEGERP-MINUS-X))
 (8 8 (:REWRITE |(< (- x) 0)|))
 (8 8 (:META META-INTEGERP-CORRECT))
 (4 4 (:REWRITE |(< d (+ c x))|))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 )
(ADE::WIG-WAG$VALID-ST-PRESERVED
 (21302 536 (:REWRITE ADE::LEN-NTHCDR))
 (9216 304 (:REWRITE |(< x (if a b c))|))
 (6682 1028 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (6550 6550 (:REWRITE NTH-WHEN-PREFIXP))
 (5077 2870 (:REWRITE DEFAULT-+-2))
 (4914 514 (:DEFINITION TRUE-LISTP))
 (3848 3848 (:REWRITE DEFAULT-CDR))
 (3275 346 (:DEFINITION NTHCDR))
 (3204 534 (:DEFINITION BINARY-APPEND))
 (2870 2870 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2870 2870 (:REWRITE DEFAULT-+-1))
 (2670 1068 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (2562 1386 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2562 1386 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2562 1386 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (2431 221 (:REWRITE |(+ (+ x y) z)|))
 (2363 1499 (:REWRITE SIMPLIFY-SUMS-<))
 (2363 1499 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2363 1499 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2339 1499 (:REWRITE DEFAULT-<-1))
 (2056 1028 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
 (1776 1776 (:LINEAR LEN-WHEN-PREFIXP))
 (1542 514 (:REWRITE ADE::BVP-NTHCDR))
 (1523 1499 (:REWRITE DEFAULT-<-2))
 (1512 189 (:DEFINITION STRIP-CARS))
 (1499 1499 (:REWRITE |(< (- x) (- y))|))
 (1386 1386 (:REWRITE |(equal (- x) (- y))|))
 (1176 89 (:DEFINITION NATP))
 (1105 221 (:REWRITE |(+ y x)|))
 (1105 221 (:REWRITE |(+ c (+ d x))|))
 (1021 152 (:REWRITE |(+ (if a b c) x)|))
 (994 970 (:REWRITE DEFAULT-CAR))
 (888 888 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (630 28 (:REWRITE ADE::ALT-BRANCH$ACT0-INACTIVE))
 (443 443 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-A+AB))
 (443 443 (:REWRITE |(< 0 (- x))|))
 (360 20 (:REWRITE ADE::ALT-MERGE$ACT1-INACTIVE))
 (360 20 (:REWRITE ADE::ALT-MERGE$ACT0-INACTIVE))
 (286 286 (:REWRITE |(< d (+ c x))|))
 (266 28 (:REWRITE ADE::ALT-BRANCH$ACT1-INACTIVE))
 (240 240 (:REWRITE REDUCE-INTEGERP-+))
 (240 240 (:REWRITE INTEGERP-MINUS-X))
 (240 240 (:META META-INTEGERP-CORRECT))
 (216 216 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-A+AB-<-0))
 (216 216 (:REWRITE |(< (- x) 0)|))
 (200 20 (:DEFINITION ADE::V-THREEFIX))
 (183 183 (:REWRITE ADE::WIG-WAG$INPUT-FORMAT-LEMMA-2))
 (182 182 (:REWRITE ADE::WIG-WAG$INPUT-FORMAT-LEMMA-1))
 (148 20 (:DEFINITION PAIRLIS$))
 (89 89 (:TYPE-PRESCRIPTION NATP))
 (64 64 (:TYPE-PRESCRIPTION STRIP-CARS))
 (56 28 (:DEFINITION ADE::3V-FIX))
 (56 8 (:REWRITE ADE::CAR-V-THREEFIX))
 (28 28 (:TYPE-PRESCRIPTION ADE::3VP))
 (24 24 (:REWRITE DEFAULT-UNARY-MINUS))
 (6 2 (:REWRITE ADE::BOOLEANP-ALT-BRANCH$ACT1))
 (6 2 (:REWRITE ADE::BOOLEANP-ALT-BRANCH$ACT0))
 )
(ADE::WIG-WAG$EXTRACT-LEMMA
 (1472 32 (:REWRITE TAKE-OF-TOO-MANY))
 (1264 158 (:DEFINITION STRIP-CARS))
 (1104 1104 (:REWRITE NTH-WHEN-PREFIXP))
 (1008 564 (:REWRITE DEFAULT-CAR))
 (610 514 (:REWRITE DEFAULT-CDR))
 (490 34 (:DEFINITION NTHCDR))
 (448 16 (:REWRITE ADE::LEN-NTHCDR))
 (432 290 (:REWRITE DEFAULT-+-2))
 (374 34 (:REWRITE |(+ (+ x y) z)|))
 (304 304 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (304 16 (:REWRITE ADE::WIG-WAG$OUT-ACT-INACTIVE))
 (290 290 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (290 290 (:REWRITE DEFAULT-+-1))
 (288 32 (:DEFINITION BINARY-APPEND))
 (224 88 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (224 88 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (224 88 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (224 32 (:REWRITE TAKE-WHEN-ATOM))
 (180 18 (:DEFINITION ADE::V-THREEFIX))
 (160 64 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (116 116 (:TYPE-PRESCRIPTION BOOLEANP))
 (112 16 (:REWRITE ADE::CAR-V-THREEFIX))
 (100 50 (:REWRITE SIMPLIFY-SUMS-<))
 (100 50 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (100 50 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (96 96 (:LINEAR LEN-WHEN-PREFIXP))
 (88 88 (:REWRITE |(equal (- x) (- y))|))
 (84 50 (:REWRITE DEFAULT-<-2))
 (74 10 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (68 34 (:DEFINITION ADE::3V-FIX))
 (66 50 (:REWRITE DEFAULT-<-1))
 (62 31 (:TYPE-PRESCRIPTION ADE::BOOLEANP-WIG-WAG$OUT-ACT))
 (54 54 (:TYPE-PRESCRIPTION ADE::3VP))
 (52 52 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (52 52 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (50 50 (:REWRITE |(< (- x) (- y))|))
 (48 48 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (44 18 (:REWRITE |(< d (+ c x))|))
 (42 2 (:REWRITE ZP-OPEN))
 (32 32 (:TYPE-PRESCRIPTION NFIX))
 (32 32 (:REWRITE DEFAULT-UNARY-MINUS))
 (30 10 (:REWRITE ADE::F-BUF-OF-3VP))
 (24 24 (:REWRITE ADE::WIG-WAG$INPUT-FORMAT-LEMMA-2))
 (18 2 (:DEFINITION TRUE-LISTP))
 (16 16 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (16 16 (:REWRITE DEFAULT-*-2))
 (16 16 (:REWRITE DEFAULT-*-1))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 4 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP-LEN))
 )
(ADE::WIG-WAG$IN-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-WIG-WAG$IN-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT))
 )
(ADE::WIG-WAG$IN-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT-LEMMA-1))
 )
(ADE::WIG-WAG$IN-SEQ-LEMMA
 (2040 40 (:REWRITE ADE::ALT-BRANCH$ACT-INACTIVE))
 (1162 602 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT-LEMMA-2))
 (725 65 (:REWRITE ZP-OPEN))
 (590 138 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (590 138 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (590 138 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (330 330 (:REWRITE NTH-WHEN-PREFIXP))
 (213 35 (:DEFINITION BINARY-APPEND))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (144 36 (:REWRITE ADE::WIG-WAG$IN-ACT-INACTIVE))
 (138 138 (:REWRITE |(equal (- x) (- y))|))
 (120 120 (:REWRITE DEFAULT-CAR))
 (104 104 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (92 92 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (91 91 (:REWRITE DEFAULT-CDR))
 (84 14 (:REWRITE ADE::WIG-WAG$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))
 (12 12 (:REWRITE ADE::WIG-WAG$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::WIG-WAG$OUT-SEQ
 (12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-WIG-WAG$OUT-ACT))
 (6 6 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT))
 )
(ADE::WIG-WAG$OUT-SEQ-NETLIST
 (6 6 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT-LEMMA-2))
 )
(ADE::WIG-WAG$OUT-SEQ-LEMMA
 (1200 40 (:REWRITE ADE::ALT-MERGE$ACT-INACTIVE))
 (725 65 (:REWRITE ZP-OPEN))
 (428 228 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT-LEMMA-1))
 (398 36 (:REWRITE ADE::WIG-WAG$OUT-ACT-INACTIVE))
 (366 112 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (366 112 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (366 112 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (360 40 (:REWRITE |(< d (+ c x))|))
 (352 352 (:REWRITE NTH-WHEN-PREFIXP))
 (213 35 (:DEFINITION BINARY-APPEND))
 (166 70 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (117 117 (: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::WIG-WAG$IN-ACT-INACTIVE))
 (30 6 (:DEFINITION NTHCDR))
 (29 29 (:REWRITE ADE::WIG-WAG$EXTRACT-LEMMA))
 (12 12 (:REWRITE ADE::WIG-WAG$INPUT-FORMAT-PLUS))
 (6 6 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 )
(ADE::WIG-WAG$DATAFLOW-CORRECT-AUX
 (184 172 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (86 2 (:DEFINITION ADE::WIG-WAG$IN-SEQ))
 (53 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (24 10 (:REWRITE DEFAULT-CDR))
 (20 10 (:TYPE-PRESCRIPTION ADE::BOOLEANP-WIG-WAG$IN-ACT))
 (18 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (18 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (18 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (12 12 (:REWRITE DEFAULT-CAR))
 (10 10 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT))
 (10 10 (:TYPE-PRESCRIPTION ADE::WIG-WAG$IN-ACT))
 (8 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (8 2 (:REWRITE ADE::WIG-WAG$IN-ACT-INACTIVE))
 (6 2 (:REWRITE CAR-OF-APPEND))
 (5 5 (:REWRITE CONSP-OF-APPEND))
 (4 4 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT-LEMMA-1))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE ZP-OPEN))
 (2 2 (:REWRITE NTH-WHEN-PREFIXP))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2 2 (:REWRITE NORMALIZE-ADDENDS))
 (2 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 )
(ADE::WIG-WAG$DATAFLOW-CORRECT
 (1654 124 (:REWRITE ZP-OPEN))
 (834 89 (:REWRITE |(< d (+ c x))|))
 (576 15 (:DEFINITION NTHCDR))
 (444 71 (:DEFINITION BINARY-APPEND))
 (298 147 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (277 35 (:REWRITE ADE::WIG-WAG$OUT-ACT-INACTIVE))
 (274 4 (:REWRITE TAKE-OF-TOO-MANY))
 (269 50 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (269 50 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (269 50 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (261 29 (:DEFINITION LEN))
 (232 232 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (226 175 (:REWRITE DEFAULT-CDR))
 (206 206 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (196 190 (:REWRITE DEFAULT-CAR))
 (194 142 (:REWRITE DEFAULT-+-2))
 (192 57 (:REWRITE ADE::WIG-WAG$IN-ACT-INACTIVE))
 (190 2 (:DEFINITION TAKE))
 (180 143 (:REWRITE SIMPLIFY-SUMS-<))
 (167 37 (:REWRITE |(+ c (+ d x))|))
 (165 165 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT-LEMMA-2))
 (165 15 (:REWRITE |(+ (+ x y) z)|))
 (164 141 (:REWRITE DEFAULT-<-2))
 (162 147 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (154 146 (:REWRITE NORMALIZE-ADDENDS))
 (147 147 (:REWRITE |(< (- x) (- y))|))
 (142 142 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (142 142 (:REWRITE DEFAULT-+-1))
 (141 141 (:REWRITE DEFAULT-<-1))
 (102 2 (:REWRITE CONSP-OF-TAKE))
 (91 19 (:REWRITE |(+ y x)|))
 (86 86 (:REWRITE NTH-WHEN-PREFIXP))
 (70 70 (:TYPE-PRESCRIPTION ADE::WIG-WAG$STEP))
 (50 50 (:REWRITE |(equal (- x) (- y))|))
 (44 4 (:REWRITE ADE::NFIX-OF-NAT))
 (44 4 (:LINEAR ADE::WIG-WAG$EXTRACT-NOT-EMPTY))
 (36 36 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (32 4 (:DEFINITION NATP))
 (16 4 (:REWRITE TAKE-WHEN-ATOM))
 (14 14 (:REWRITE ADE::WIG-WAG$RUN-PLUS))
 (12 12 (:REWRITE ADE::WIG-WAG$INPUT-FORMAT-PLUS))
 (12 12 (:LINEAR LEN-WHEN-PREFIXP))
 (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))|))
 (3 3 (:TYPE-PRESCRIPTION ADE::WIG-WAG$RUN))
 )
(ADE::WIG-WAG$FUNCTIONALLY-CORRECT
 (390 4 (:DEFINITION ADE::WIG-WAG$OUT-SEQ))
 (172 4 (:DEFINITION ADE::WIG-WAG$IN-SEQ))
 (166 4 (:REWRITE ADE::WIG-WAG$EXTRACT-LEMMA))
 (120 3 (:DEFINITION NTHCDR))
 (97 37 (:REWRITE ZP-OPEN))
 (80 32 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (76 4 (:REWRITE ADE::WIG-WAG$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::WIG-WAG$INPUT-FORMAT-LEMMA-2))
 (42 3 (:REWRITE |(< d (+ c x))|))
 (40 40 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-WIG-WAG$OUT-ACT))
 (40 20 (:TYPE-PRESCRIPTION ADE::BOOLEANP-WIG-WAG$IN-ACT))
 (39 39 (:TYPE-PRESCRIPTION LEN))
 (39 30 (:REWRITE DEFAULT-CDR))
 (33 3 (:REWRITE |(+ (+ x y) z)|))
 (27 3 (:DEFINITION LEN))
 (26 20 (:REWRITE DEFAULT-+-2))
 (24 24 (:REWRITE DEFAULT-CAR))
 (24 6 (:REWRITE ADE::OPEN-WIG-WAG$INPUT-FORMAT-N-ZP))
 (24 6 (:REWRITE ADE::OPEN-WIG-WAG$INPUT-FORMAT-N))
 (20 20 (:TYPE-PRESCRIPTION ADE::WIG-WAG$OUT-ACT))
 (20 20 (:TYPE-PRESCRIPTION ADE::WIG-WAG$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))
 (16 4 (:REWRITE ADE::WIG-WAG$IN-ACT-INACTIVE))
 (16 4 (:REWRITE ADE::OPEN-DE-N-ZP))
 (16 4 (:REWRITE ADE::OPEN-DE-N))
 (15 15 (:REWRITE |(equal (- x) (- y))|))
 (15 3 (:REWRITE |(+ y x)|))
 (15 3 (:REWRITE |(+ c (+ d x))|))
 (12 3 (:REWRITE ADE::OPEN-WIG-WAG$RUN-ZP))
 (12 3 (:REWRITE ADE::OPEN-WIG-WAG$RUN))
 (8 8 (:TYPE-PRESCRIPTION ADE::WIG-WAG$INPUT-FORMAT-LEMMA-1))
 (8 8 (:REWRITE NTH-WHEN-PREFIXP))
 (8 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (6 6 (:REWRITE REMOVE-WEAK-INEQUALITIES-TWO))
 (6 6 (:REWRITE REMOVE-WEAK-INEQUALITIES-ONE))
 (6 3 (:REWRITE SIMPLIFY-SUMS-<))
 (6 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (6 3 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (6 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:TYPE-PRESCRIPTION ADE::WIG-WAG$RUN))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-N))
 (3 3 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE |(< (- x) (- y))|))
 )