(ADE::READ-REG)
(ADE::WRITE-SHIFT-REG)
(ADE::TRUE-LISTP-WRITE-SHIFT-REG)
(ADE::LEN-WRITE-SHIFT-REG
 (12 2 (:DEFINITION LEN))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (4 2 (:REWRITE DEFAULT-+-2))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (3 1 (:REWRITE ADE::FV-SHIFT-RIGHT=V-SHIFT-RIGHT))
 (2 2 (:TYPE-PRESCRIPTION ADE::FV-SHIFT-RIGHT))
 (2 2 (:TYPE-PRESCRIPTION BOOLEANP))
 (2 2 (:REWRITE DEFAULT-CDR))
 (2 2 (:REWRITE DEFAULT-+-1))
 )
(ADE::WRITE-SHIFT-REG-OF-F-BUF-CANCELED
 (55 22 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-SHIFT-REG))
 (22 22 (:TYPE-PRESCRIPTION ADE::WRITE-SHIFT-REG))
 (22 22 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (11 11 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 2 (:REWRITE ADE::FV-SHIFT-RIGHT=V-SHIFT-RIGHT))
 (3 1 (:REWRITE ADE::F-GATES=B-GATES))
 (3 1 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (3 1 (:REWRITE ADE::F-BUF-OF-3VP))
 (2 2 (:TYPE-PRESCRIPTION ADE::3VP))
 )
(ADE::WRITE-PAR-SHIFT-REG)
(ADE::LEN-WRITE-PAR-SHIFT-REG
 (26 4 (:DEFINITION LEN))
 (8 4 (:REWRITE DEFAULT-+-2))
 (6 6 (:LINEAR LEN-WHEN-PREFIXP))
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 4 (:REWRITE DEFAULT-+-1))
 (3 3 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (3 1 (:REWRITE ADE::FV-SHIFT-RIGHT=V-SHIFT-RIGHT))
 (2 2 (:TYPE-PRESCRIPTION ADE::FV-SHIFT-RIGHT))
 (2 2 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::PRIMP-CALL-SYNTAXP)
(ADE::PRIMP-CALL-ARITYP)
(ADE::SE-PRIMP-APPLY
 (109 109 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-ST))
 (109 109 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-INS))
 (3 3 (:TYPE-PRESCRIPTION ADE::F-BUF))
 (1 1 (:TYPE-PRESCRIPTION ADE::FT-WIRE))
 (1 1 (:TYPE-PRESCRIPTION ADE::FT-BUF))
 (1 1 (:TYPE-PRESCRIPTION ADE::F-XOR))
 (1 1 (:TYPE-PRESCRIPTION ADE::F-XNOR))
 (1 1 (:TYPE-PRESCRIPTION ADE::F-PULLUP))
 (1 1 (:TYPE-PRESCRIPTION ADE::F-EQUV))
 )
(ADE::DE-PRIMP-APPLY
 (14 14 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-ST))
 (14 14 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-INS))
 (2 1 (:TYPE-PRESCRIPTION ADE::TRUE-LISTP-WRITE-SHIFT-REG))
 (1 1 (:TYPE-PRESCRIPTION ADE::WRITE-SHIFT-REG))
 (1 1 (:TYPE-PRESCRIPTION ADE::WRITE-PAR-SHIFT-REG))
 (1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1 1 (:TYPE-PRESCRIPTION ADE::F-SR))
 (1 1 (:TYPE-PRESCRIPTION ADE::F-IF))
 )
(ADE::LEN-SE-PRIMP-APPLY)
(ADE::LEN-DE-PRIMP-APPLY)
(ADE::LEN-DE-PRIMP-APPLY-LEMMA
 (265 265 (:REWRITE DEFAULT-CDR))
 (125 125 (:REWRITE NTH-WHEN-PREFIXP))
 (29 29 (:REWRITE DEFAULT-CAR))
 (24 24 (:LINEAR LEN-WHEN-PREFIXP))
 (12 12 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (9 3 (:REWRITE ADE::F-GATES=B-GATES))
 (6 6 (:TYPE-PRESCRIPTION BOOLEANP))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(ADE::MD-NAME$INLINE)
(ADE::MD-INS$INLINE)
(ADE::MD-OUTS$INLINE)
(ADE::MD-ST$INLINE)
(ADE::MD-OCCS$INLINE)
(ADE::OCC-NAME$INLINE)
(ADE::OCC-OUTS$INLINE)
(ADE::OCC-FN$INLINE)
(ADE::OCC-INS$INLINE)
(ADE::OCC-SYNTAX-OKP)
(ADE::OCCS-SYNTAX-OKP)
(ADE::OCCS-SYNTAX-OKP-FORWARD-SYMBOL-ALISTP
 (89 89 (:REWRITE DEFAULT-CDR))
 (61 61 (:REWRITE DEFAULT-CAR))
 (33 11 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (32 4 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (24 8 (:DEFINITION SYMBOL-LISTP))
 (22 22 (:TYPE-PRESCRIPTION ADE::BVP))
 (12 4 (:DEFINITION MEMBER-EQUAL))
 (4 4 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 )
(ADE::MODULE-SYNTAX-OKP)
(ADE::NET-SYNTAX-OKP)
(ADE::NET-SYNTAX-OKP-FORWARD-TO-SYMBOL-ALISTP
 (408 8 (:DEFINITION ADE::OCCS-SYNTAX-OKP))
 (388 388 (:REWRITE DEFAULT-CDR))
 (360 8 (:DEFINITION ADE::OCC-SYNTAX-OKP))
 (272 32 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (250 250 (:REWRITE DEFAULT-CAR))
 (136 40 (:DEFINITION MEMBER-EQUAL))
 (96 32 (:DEFINITION SYMBOL-LISTP))
 (81 27 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (80 8 (:DEFINITION SUBSETP-EQUAL))
 (64 16 (:DEFINITION STRIP-CARS))
 (54 54 (:TYPE-PRESCRIPTION ADE::BVP))
 (40 40 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (40 8 (:DEFINITION ADE::OCC-INS$INLINE))
 (32 32 (:TYPE-PRESCRIPTION STRIP-CARS))
 (32 8 (:DEFINITION ADE::OCC-FN$INLINE))
 (24 8 (:DEFINITION ADE::OCC-OUTS$INLINE))
 (16 16 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (16 8 (:DEFINITION ADE::OCC-NAME$INLINE))
 (15 3 (:DEFINITION ASSOC-EQUAL))
 )
(ADE::NET-SYNTAX-OKP
 (306 6 (:DEFINITION ADE::OCCS-SYNTAX-OKP))
 (279 1 (:DEFINITION ADE::NET-SYNTAX-OKP))
 (272 272 (:REWRITE DEFAULT-CDR))
 (270 6 (:DEFINITION ADE::OCC-SYNTAX-OKP))
 (204 24 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (162 162 (:REWRITE DEFAULT-CAR))
 (102 30 (:DEFINITION MEMBER-EQUAL))
 (72 24 (:DEFINITION SYMBOL-LISTP))
 (60 6 (:DEFINITION SUBSETP-EQUAL))
 (54 18 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (48 12 (:DEFINITION STRIP-CARS))
 (45 9 (:DEFINITION TRUE-LISTP))
 (36 36 (:TYPE-PRESCRIPTION ADE::BVP))
 (30 30 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (30 6 (:DEFINITION ADE::OCC-INS$INLINE))
 (24 24 (:TYPE-PRESCRIPTION STRIP-CARS))
 (24 6 (:DEFINITION ADE::OCC-FN$INLINE))
 (18 6 (:DEFINITION ADE::OCC-OUTS$INLINE))
 (12 12 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (12 6 (:DEFINITION ADE::OCC-NAME$INLINE))
 (6 2 (:DEFINITION ALISTP))
 (5 1 (:DEFINITION ASSOC-EQUAL))
 )
(ADE::NET-SYNTAX-OKP-DELETE-TO-EQ-NETLIST
 (1326 26 (:DEFINITION ADE::OCCS-SYNTAX-OKP))
 (1188 1188 (:REWRITE DEFAULT-CDR))
 (1170 26 (:DEFINITION ADE::OCC-SYNTAX-OKP))
 (884 104 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (745 745 (:REWRITE DEFAULT-CAR))
 (442 130 (:DEFINITION MEMBER-EQUAL))
 (312 104 (:DEFINITION SYMBOL-LISTP))
 (260 26 (:DEFINITION SUBSETP-EQUAL))
 (234 78 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (208 52 (:DEFINITION STRIP-CARS))
 (195 39 (:DEFINITION TRUE-LISTP))
 (156 156 (:TYPE-PRESCRIPTION ADE::BVP))
 (130 130 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (130 26 (:DEFINITION ADE::OCC-INS$INLINE))
 (104 104 (:TYPE-PRESCRIPTION STRIP-CARS))
 (104 26 (:DEFINITION ADE::OCC-FN$INLINE))
 (78 26 (:DEFINITION ADE::OCC-OUTS$INLINE))
 (60 12 (:DEFINITION ASSOC-EQUAL))
 (52 52 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (52 26 (:DEFINITION ADE::OCC-NAME$INLINE))
 )
(ADE::ASSOC-EQ-OF-NON-FN-NETLIST)
(ADE::SYMBOL-LISTP-MD-OF-INS-OUTS-AND-ST
 (1091 1091 (:REWRITE DEFAULT-CDR))
 (1020 20 (:DEFINITION ADE::OCCS-SYNTAX-OKP))
 (900 20 (:DEFINITION ADE::OCC-SYNTAX-OKP))
 (718 718 (:REWRITE DEFAULT-CAR))
 (672 79 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (327 97 (:DEFINITION MEMBER-EQUAL))
 (228 76 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (180 18 (:DEFINITION SUBSETP-EQUAL))
 (152 152 (:TYPE-PRESCRIPTION ADE::BVP))
 (152 38 (:DEFINITION STRIP-CARS))
 (100 20 (:DEFINITION ADE::OCC-INS$INLINE))
 (97 97 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (80 20 (:DEFINITION ADE::OCC-FN$INLINE))
 (76 76 (:TYPE-PRESCRIPTION STRIP-CARS))
 (60 20 (:DEFINITION ADE::OCC-OUTS$INLINE))
 (40 20 (:DEFINITION ADE::OCC-NAME$INLINE))
 (36 36 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 )
(ADE::NET-SYNTAX-OKP->MODULE-SYNTAX-OKP
 (66 66 (:REWRITE DEFAULT-CAR))
 (17 17 (:REWRITE DEFAULT-CDR))
 )
(ADE::CONSP-ASSOC-EQ-FN-OF-NON-EMPTY-NETLIST
 (1017 1017 (:REWRITE DEFAULT-CDR))
 (918 18 (:DEFINITION ADE::OCCS-SYNTAX-OKP))
 (810 18 (:DEFINITION ADE::OCC-SYNTAX-OKP))
 (669 669 (:REWRITE DEFAULT-CAR))
 (612 72 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (306 90 (:DEFINITION MEMBER-EQUAL))
 (234 78 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (216 72 (:DEFINITION SYMBOL-LISTP))
 (180 18 (:DEFINITION SUBSETP-EQUAL))
 (156 156 (:TYPE-PRESCRIPTION ADE::BVP))
 (144 36 (:DEFINITION STRIP-CARS))
 (90 90 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (90 18 (:DEFINITION ADE::OCC-INS$INLINE))
 (72 72 (:TYPE-PRESCRIPTION STRIP-CARS))
 (72 18 (:DEFINITION ADE::OCC-FN$INLINE))
 (54 18 (:DEFINITION ADE::OCC-OUTS$INLINE))
 (36 36 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (36 18 (:DEFINITION ADE::OCC-NAME$INLINE))
 )
(ADE::OCC-ARITY-OKP
 (279 1 (:DEFINITION ADE::NET-SYNTAX-OKP))
 (255 1 (:DEFINITION ADE::MODULE-SYNTAX-OKP))
 (168 166 (:REWRITE DEFAULT-CDR))
 (113 106 (:REWRITE DEFAULT-CAR))
 (102 2 (:DEFINITION ADE::OCCS-SYNTAX-OKP))
 (76 9 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (55 11 (:DEFINITION ASSOC-EQUAL))
 (45 9 (:DEFINITION LEN))
 (42 14 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (37 11 (:DEFINITION MEMBER-EQUAL))
 (30 10 (:DEFINITION SYMBOL-LISTP))
 (28 28 (:TYPE-PRESCRIPTION ADE::BVP))
 (27 27 (:TYPE-PRESCRIPTION ATOM))
 (20 2 (:DEFINITION SUBSETP-EQUAL))
 (18 9 (:REWRITE DEFAULT-+-2))
 (16 4 (:DEFINITION STRIP-CARS))
 (11 11 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (9 9 (:REWRITE DEFAULT-+-1))
 (8 8 (:TYPE-PRESCRIPTION STRIP-CARS))
 (6 1 (:DEFINITION ADE::MD-OCCS$INLINE))
 (5 1 (:DEFINITION ADE::MD-ST$INLINE))
 (4 4 (:TYPE-PRESCRIPTION ADE::OCCS-SYNTAX-OKP))
 (4 4 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (2 2 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (2 1 (:DEFINITION ADE::MD-NAME$INLINE))
 )
(ADE::OCCS-ARITY-OKP
 (2 2 (:REWRITE DEFAULT-CAR))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::NET-ARITY-OKP
 (1064 1064 (:REWRITE DEFAULT-CDR))
 (662 662 (:REWRITE DEFAULT-CAR))
 (595 7 (:DEFINITION ADE::NET-ARITY-OKP))
 (516 61 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (476 7 (:DEFINITION ADE::OCCS-ARITY-OKP))
 (399 7 (:DEFINITION ADE::OCC-ARITY-OKP))
 (255 85 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (253 75 (:DEFINITION MEMBER-EQUAL))
 (192 64 (:DEFINITION SYMBOL-LISTP))
 (170 170 (:TYPE-PRESCRIPTION ADE::BVP))
 (140 28 (:DEFINITION LEN))
 (140 28 (:DEFINITION ASSOC-EQUAL))
 (140 14 (:DEFINITION SUBSETP-EQUAL))
 (133 133 (:TYPE-PRESCRIPTION LEN))
 (112 28 (:DEFINITION STRIP-CARS))
 (75 75 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (56 56 (:TYPE-PRESCRIPTION STRIP-CARS))
 (56 28 (:REWRITE DEFAULT-+-2))
 (28 28 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (28 28 (:REWRITE DEFAULT-+-1))
 (21 21 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-INS))
 (14 14 (:TYPE-PRESCRIPTION ADE::POSP-PRIMP-OUTS))
 (9 3 (:DEFINITION ALISTP))
 (5 1 (:DEFINITION SYMBOL-ALISTP))
 )
(ADE::NET-ARITY-OKP-OF-DELETE-TO-EQ
 (490 10 (:DEFINITION ADE::OCCS-ARITY-OKP))
 (380 10 (:DEFINITION ADE::OCC-ARITY-OKP))
 (200 40 (:DEFINITION LEN))
 (190 190 (:TYPE-PRESCRIPTION LEN))
 (105 21 (:DEFINITION ASSOC-EQUAL))
 (98 98 (:REWRITE DEFAULT-CAR))
 (87 87 (:REWRITE DEFAULT-CDR))
 (80 40 (:REWRITE DEFAULT-+-2))
 (40 40 (:REWRITE DEFAULT-+-1))
 (30 30 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-INS))
 (20 20 (:TYPE-PRESCRIPTION ADE::POSP-PRIMP-OUTS))
 )
(ADE::OCCS-SYNTAX-OKP-MD-OCCS-ASSOC-EQ-FN-NETLIST
 (603 603 (:REWRITE DEFAULT-CDR))
 (472 56 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (358 358 (:REWRITE DEFAULT-CAR))
 (228 68 (:DEFINITION MEMBER-EQUAL))
 (186 62 (:DEFINITION SYMBOL-LISTP))
 (174 58 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (120 12 (:DEFINITION SUBSETP-EQUAL))
 (116 116 (:TYPE-PRESCRIPTION ADE::BVP))
 (96 24 (:DEFINITION STRIP-CARS))
 (68 68 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (48 48 (:TYPE-PRESCRIPTION STRIP-CARS))
 (24 24 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 )
(ADE::OCCS-ARITY-OKP-MD-OCCS-ASSOC-EQ-FN-NETLIST
 (220 44 (:DEFINITION LEN))
 (116 116 (:REWRITE DEFAULT-CAR))
 (89 89 (:REWRITE DEFAULT-CDR))
 (88 44 (:REWRITE DEFAULT-+-2))
 (44 44 (:REWRITE DEFAULT-+-1))
 )
(ADE::LEN-FN-DELETE-TO-EQ
 (290 12 (:REWRITE LEN-WHEN-PREFIXP))
 (210 8 (:REWRITE PREFIXP-WHEN-EQUAL-LENGTHS))
 (157 8 (:REWRITE PREFIXP-WHEN-PREFIXP))
 (104 57 (:REWRITE DEFAULT-+-2))
 (61 61 (:REWRITE DEFAULT-CDR))
 (57 57 (:REWRITE DEFAULT-+-1))
 (44 22 (:REWRITE DEFAULT-<-1))
 (38 22 (:REWRITE DEFAULT-<-2))
 (28 28 (:TYPE-PRESCRIPTION PREFIXP))
 (28 28 (:REWRITE DEFAULT-CAR))
 (28 28 (:LINEAR LEN-WHEN-PREFIXP))
 (14 14 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (8 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
 (8 8 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
 (8 8 (:REWRITE PREFIXP-TRANSITIVE . 2))
 (8 8 (:REWRITE PREFIXP-TRANSITIVE . 1))
 (8 8 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
 (8 8 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
 )
(ADE::SE-MEASURE
 (5 1 (:DEFINITION LEN))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE DEFAULT-CDR))
 )
(ADE::ACL2-COUNT-OF-OCCS-FN-CAR-OCCS
 (471 195 (:REWRITE DEFAULT-+-2))
 (274 195 (:REWRITE DEFAULT-+-1))
 (238 17 (:DEFINITION LENGTH))
 (187 17 (:DEFINITION LEN))
 (136 34 (:DEFINITION INTEGER-ABS))
 (56 40 (:REWRITE DEFAULT-<-2))
 (51 51 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (51 34 (:REWRITE STR::CONSP-OF-EXPLODE))
 (43 40 (:REWRITE DEFAULT-<-1))
 (34 34 (:REWRITE DEFAULT-UNARY-MINUS))
 (34 17 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (17 17 (:TYPE-PRESCRIPTION LEN))
 (17 17 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (17 17 (:REWRITE DEFAULT-REALPART))
 (17 17 (:REWRITE DEFAULT-NUMERATOR))
 (17 17 (:REWRITE DEFAULT-IMAGPART))
 (17 17 (:REWRITE DEFAULT-DENOMINATOR))
 )
(ADE::ST-OKP-GUARD)
(ADE::ST-OCCS-OKP-GUARD)
(ADE::ST-OKP
 (1631 1560 (:REWRITE DEFAULT-CDR))
 (1086 198 (:DEFINITION LEN))
 (939 321 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (728 696 (:REWRITE DEFAULT-CAR))
 (681 338 (:REWRITE DEFAULT-+-2))
 (618 618 (:TYPE-PRESCRIPTION ADE::BVP))
 (450 134 (:DEFINITION MEMBER-EQUAL))
 (391 338 (:REWRITE DEFAULT-+-1))
 (224 16 (:DEFINITION LENGTH))
 (180 18 (:DEFINITION SUBSETP-EQUAL))
 (128 32 (:REWRITE COMMUTATIVITY-OF-+))
 (128 32 (:DEFINITION INTEGER-ABS))
 (50 10 (:DEFINITION ADE::DELETE-TO-EQ))
 (48 48 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (48 32 (:REWRITE STR::CONSP-OF-EXPLODE))
 (45 38 (:REWRITE DEFAULT-<-2))
 (40 38 (:REWRITE DEFAULT-<-1))
 (37 37 (:REWRITE FOLD-CONSTS-IN-+))
 (36 36 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (32 32 (:REWRITE DEFAULT-UNARY-MINUS))
 (32 16 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (20 4 (:DEFINITION ASSOC-EQUAL))
 (16 16 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (16 16 (:REWRITE DEFAULT-REALPART))
 (16 16 (:REWRITE DEFAULT-NUMERATOR))
 (16 16 (:REWRITE DEFAULT-IMAGPART))
 (16 16 (:REWRITE DEFAULT-DENOMINATOR))
 (10 2 (:DEFINITION PAIRLIS$))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (3 1 (:REWRITE ADE::NET-SYNTAX-OKP->MODULE-SYNTAX-OKP))
 )
(ADE::ST-OCCS-OKP-UPDATE-ALIST
 (124 42 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (111 3 (:DEFINITION ADE::ST-OKP))
 (108 106 (:REWRITE DEFAULT-CAR))
 (105 21 (:DEFINITION TRUE-LISTP))
 (93 91 (:REWRITE DEFAULT-CDR))
 (82 82 (:TYPE-PRESCRIPTION ADE::BVP))
 (45 9 (:DEFINITION LEN))
 (24 24 (:TYPE-PRESCRIPTION LEN))
 (18 9 (:REWRITE DEFAULT-+-2))
 (15 3 (:DEFINITION PAIRLIS$))
 (15 3 (:DEFINITION ADE::DELETE-TO-EQ))
 (15 3 (:DEFINITION ASSOC-EQUAL))
 (9 9 (:REWRITE DEFAULT-+-1))
 (7 7 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-1))
 (3 3 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-ST))
 )
(ADE::SE-INS-GUARD
 (10 2 (:DEFINITION ASSOC-EQUAL))
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (5 1 (:DEFINITION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION ADE::BVP))
 (4 4 (:REWRITE DEFAULT-CDR))
 )
(ADE::SE-GUARD)
(ADE::SE-OCC-GUARD)
(ADE::SE
 (384 188 (:REWRITE DEFAULT-+-2))
 (277 35 (:DEFINITION LEN))
 (247 188 (:REWRITE DEFAULT-+-1))
 (238 17 (:DEFINITION LENGTH))
 (153 92 (:REWRITE DEFAULT-CDR))
 (136 34 (:REWRITE COMMUTATIVITY-OF-+))
 (136 34 (:DEFINITION INTEGER-ABS))
 (105 81 (:REWRITE DEFAULT-CAR))
 (53 43 (:REWRITE DEFAULT-<-2))
 (51 51 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (51 34 (:REWRITE STR::CONSP-OF-EXPLODE))
 (48 43 (:REWRITE DEFAULT-<-1))
 (42 42 (:REWRITE FOLD-CONSTS-IN-+))
 (34 34 (:REWRITE DEFAULT-UNARY-MINUS))
 (34 17 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (20 4 (:DEFINITION ADE::DELETE-TO-EQ))
 (17 17 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (17 17 (:REWRITE DEFAULT-REALPART))
 (17 17 (:REWRITE DEFAULT-NUMERATOR))
 (17 17 (:REWRITE DEFAULT-IMAGPART))
 (17 17 (:REWRITE DEFAULT-DENOMINATOR))
 (16 8 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (15 3 (:DEFINITION ASSOC-EQUAL))
 (8 8 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::DE
 (384 188 (:REWRITE DEFAULT-+-2))
 (277 35 (:DEFINITION LEN))
 (247 188 (:REWRITE DEFAULT-+-1))
 (238 17 (:DEFINITION LENGTH))
 (153 92 (:REWRITE DEFAULT-CDR))
 (136 34 (:REWRITE COMMUTATIVITY-OF-+))
 (136 34 (:DEFINITION INTEGER-ABS))
 (105 81 (:REWRITE DEFAULT-CAR))
 (53 43 (:REWRITE DEFAULT-<-2))
 (51 51 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (51 34 (:REWRITE STR::CONSP-OF-EXPLODE))
 (48 43 (:REWRITE DEFAULT-<-1))
 (42 42 (:REWRITE FOLD-CONSTS-IN-+))
 (34 34 (:REWRITE DEFAULT-UNARY-MINUS))
 (34 17 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (20 4 (:DEFINITION ADE::DELETE-TO-EQ))
 (17 17 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (17 17 (:REWRITE DEFAULT-REALPART))
 (17 17 (:REWRITE DEFAULT-NUMERATOR))
 (17 17 (:REWRITE DEFAULT-IMAGPART))
 (17 17 (:REWRITE DEFAULT-DENOMINATOR))
 (15 3 (:DEFINITION ASSOC-EQUAL))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::OPEN-SE
 (156 3 (:DEFINITION ADE::SE-OCC))
 (144 8 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (96 87 (:REWRITE DEFAULT-CAR))
 (83 13 (:DEFINITION PAIRLIS$))
 (76 67 (:REWRITE DEFAULT-CDR))
 (70 14 (:DEFINITION ASSOC-EQUAL))
 (56 56 (:TYPE-PRESCRIPTION LEN))
 (40 8 (:DEFINITION LEN))
 (32 32 (:LINEAR LEN-WHEN-PREFIXP))
 (27 3 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (25 5 (:DEFINITION ADE::DELETE-TO-EQ))
 (18 3 (:DEFINITION MEMBER-EQUAL))
 (18 3 (:DEFINITION BINARY-APPEND))
 (16 16 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (16 8 (:REWRITE DEFAULT-+-2))
 (15 15 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (15 6 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (8 8 (:REWRITE DEFAULT-+-1))
 (8 8 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 )
(ADE::SE-OCC-INDUCT
 (16 8 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (8 8 (:TYPE-PRESCRIPTION TRUE-LISTP))
 )
(ADE::SYMBOL-ALISTP-FACT-APPEND-CONS
 (10 10 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-CDR))
 (4 1 (:DEFINITION BINARY-APPEND))
 (2 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
 )
(ADE::SYMBOL-ALISTP-FACT-APPEND-PAIRLIS$
 (111 7 (:DEFINITION SYMBOL-ALISTP))
 (104 84 (:REWRITE DEFAULT-CDR))
 (64 64 (:REWRITE DEFAULT-CAR))
 (55 55 (:TYPE-PRESCRIPTION PAIRLIS$))
 (54 14 (:DEFINITION SYMBOL-LISTP))
 (44 2 (:REWRITE ADE::SYMBOL-ALISTP-APPEND))
 (40 5 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (30 10 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (25 5 (:DEFINITION TRUE-LISTP))
 (20 20 (:TYPE-PRESCRIPTION ADE::BVP))
 (20 4 (:REWRITE CAR-OF-APPEND))
 (18 3 (:DEFINITION BINARY-APPEND))
 (18 2 (:REWRITE ADE::SYMBOL-ALISTP-PAIRLIS$))
 (15 6 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (15 5 (:DEFINITION MEMBER-EQUAL))
 (15 3 (:DEFINITION PAIRLIS$))
 (14 8 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (14 4 (:REWRITE CONSP-OF-APPEND))
 (8 8 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (8 2 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (5 5 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 )
(ADE::SYMBOL-ALISTP-SE-OCC
 (324 4 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-WHEN-DISJOINT))
 (271 16 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (234 186 (:REWRITE DEFAULT-CDR))
 (230 5 (:DEFINITION ADE::SE))
 (213 165 (:REWRITE DEFAULT-CAR))
 (201 21 (:DEFINITION PAIRLIS$))
 (164 24 (:REWRITE ADE::DISJOINT-ATOM))
 (112 8 (:REWRITE ADE::STRIP-CARS-PAIRLIS$))
 (105 105 (:TYPE-PRESCRIPTION LEN))
 (104 24 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
 (96 4 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-DISJOINT))
 (89 13 (:DEFINITION TRUE-LISTP))
 (78 26 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (76 4 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-SUBSET))
 (75 15 (:DEFINITION LEN))
 (68 68 (:TYPE-PRESCRIPTION STRIP-CARS))
 (66 66 (:TYPE-PRESCRIPTION ADE::SE))
 (66 11 (:DEFINITION BINARY-APPEND))
 (64 64 (:TYPE-PRESCRIPTION ADE::DISJOINT))
 (60 60 (:LINEAR LEN-WHEN-PREFIXP))
 (60 4 (:DEFINITION SUBSETP-EQUAL))
 (52 52 (:TYPE-PRESCRIPTION ADE::BVP))
 (52 22 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (48 8 (:DEFINITION STRIP-CARS))
 (40 40 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (40 5 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (39 9 (:DEFINITION MEMBER-EQUAL))
 (30 30 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (30 15 (:REWRITE DEFAULT-+-2))
 (30 10 (:DEFINITION SYMBOL-LISTP))
 (25 25 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (25 5 (:DEFINITION ADE::DELETE-TO-EQ))
 (25 5 (:DEFINITION ASSOC-EQUAL))
 (24 24 (:TYPE-PRESCRIPTION ATOM))
 (20 20 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (20 20 (:TYPE-PRESCRIPTION ADE::ASSOC-EQ-VALUES))
 (16 16 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (15 15 (:REWRITE DEFAULT-+-1))
 (10 10 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (8 8 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (3 3 (:TYPE-PRESCRIPTION ADE::SE-OCC-INDUCT))
 )
(ADE::SYMBOL-LISTP=>TRUE-LISTP)
(ADE::SE
 (2007 1928 (:REWRITE DEFAULT-CDR))
 (1756 1715 (:REWRITE DEFAULT-CAR))
 (1305 261 (:DEFINITION LEN))
 (522 261 (:REWRITE DEFAULT-+-2))
 (516 172 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (344 344 (:TYPE-PRESCRIPTION ADE::BVP))
 (315 85 (:DEFINITION MEMBER-EQUAL))
 (261 261 (:REWRITE DEFAULT-+-1))
 (198 11 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (191 25 (:DEFINITION PAIRLIS$))
 (155 10 (:REWRITE SYMBOL-LISTP-CDR-ASSOC-EQUAL))
 (125 10 (:DEFINITION SYMBOL-LIST-LISTP))
 (104 2 (:DEFINITION ADE::SE-OCC))
 (72 8 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (70 14 (:DEFINITION ADE::DELETE-TO-EQ))
 (66 3 (:REWRITE ADE::SYMBOL-ALISTP-APPEND))
 (60 60 (:LINEAR LEN-WHEN-PREFIXP))
 (50 50 (:TYPE-PRESCRIPTION SYMBOL-LIST-LISTP))
 (42 7 (:DEFINITION BINARY-APPEND))
 (40 4 (:DEFINITION SUBSETP-EQUAL))
 (35 14 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (30 30 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (30 6 (:REWRITE CAR-OF-APPEND))
 (21 6 (:REWRITE CONSP-OF-APPEND))
 (12 3 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (11 11 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (8 8 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (8 8 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (6 6 (:TYPE-PRESCRIPTION ADE::SE-PRIMP-APPLY))
 (6 1 (:REWRITE ADE::NET-SYNTAX-OKP->MODULE-SYNTAX-OKP))
 )
(ADE::B-AND$VALUE
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::B-AND3$VALUE
 (6 6 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-AND4$VALUE
 (12 12 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-AND5$VALUE
 (20 20 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-BOOL$VALUE
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(ADE::B-BUF$VALUE
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (6 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(ADE::B-EQUV$VALUE
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::B-IF$VALUE
 (6 6 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-NAND$VALUE
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::B-NAND3$VALUE
 (6 6 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-NAND4$VALUE
 (12 12 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-NAND5$VALUE
 (20 20 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-NAND6$VALUE
 (30 30 (:REWRITE DEFAULT-CDR))
 (12 12 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-NAND8$VALUE
 (56 56 (:REWRITE DEFAULT-CDR))
 (16 16 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-NOR$VALUE
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::B-NOR3$VALUE
 (6 6 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-NOR4$VALUE
 (12 12 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-NOR5$VALUE
 (20 20 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-NOR6$VALUE
 (30 30 (:REWRITE DEFAULT-CDR))
 (12 12 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-NOR8$VALUE
 (56 56 (:REWRITE DEFAULT-CDR))
 (16 16 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-NOT$VALUE
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(ADE::B-OR$VALUE
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::B-OR3$VALUE
 (6 6 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-OR4$VALUE
 (12 12 (:REWRITE DEFAULT-CDR))
 (8 8 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-OR5$VALUE
 (20 20 (:REWRITE DEFAULT-CDR))
 (10 10 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::B-XNOR$VALUE
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::B-XOR$VALUE
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::FF$VALUE
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (8 4 (:REWRITE ADE::F-GATES=B-GATES))
 (6 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (4 4 (:REWRITE DEFAULT-CAR))
 )
(ADE::LATCH$VALUE
 (20 8 (:REWRITE ADE::F-GATES=B-GATES))
 (12 12 (:TYPE-PRESCRIPTION BOOLEANP))
 (12 12 (:REWRITE DEFAULT-CAR))
 (4 4 (:REWRITE DEFAULT-CDR))
 )
(ADE::LINK-CNTL$VALUE
 (8 8 (:TYPE-PRESCRIPTION BOOLEANP))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (6 2 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
 (6 2 (:REWRITE ADE::F-BUF-OF-3VP))
 (4 4 (:TYPE-PRESCRIPTION ADE::3VP))
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(ADE::PAR-SHIFT-REG32$VALUE
 (64 2 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (36 4 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (34 2 (:DEFINITION TRUE-LISTP))
 (30 2 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (24 4 (:DEFINITION SYMBOL-LISTP))
 (20 20 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (10 10 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (10 2 (:DEFINITION LEN))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE DEFAULT-CAR))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::PULLUP$VALUE
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(ADE::SHIFT-REG32$VALUE
 (64 2 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (36 4 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (34 2 (:DEFINITION TRUE-LISTP))
 (30 2 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (24 4 (:DEFINITION SYMBOL-LISTP))
 (20 20 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (10 10 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (10 2 (:DEFINITION LEN))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 8 (:REWRITE DEFAULT-CDR))
 (6 6 (:REWRITE DEFAULT-CAR))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::T-BUF$VALUE
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::T-WIRE$VALUE
 (4 4 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::VDD$VALUE)
(ADE::VSS$VALUE)
(ADE::WIRE$VALUE
 (2 2 (:REWRITE DEFAULT-CAR))
 )
(ADE::OPEN-DE
 (260 5 (:DEFINITION ADE::SE-OCC))
 (234 13 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (147 132 (:REWRITE DEFAULT-CAR))
 (118 103 (:REWRITE DEFAULT-CDR))
 (115 17 (:DEFINITION PAIRLIS$))
 (114 3 (:DEFINITION ADE::DE-OCC))
 (111 21 (:DEFINITION ASSOC-EQUAL))
 (91 91 (:TYPE-PRESCRIPTION LEN))
 (72 8 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (65 13 (:DEFINITION LEN))
 (52 52 (:LINEAR LEN-WHEN-PREFIXP))
 (48 8 (:DEFINITION MEMBER-EQUAL))
 (40 40 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (35 7 (:DEFINITION ADE::DELETE-TO-EQ))
 (30 30 (:TYPE-PRESCRIPTION ADE::SE))
 (30 5 (:DEFINITION BINARY-APPEND))
 (26 26 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (26 13 (:REWRITE DEFAULT-+-2))
 (25 10 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (13 13 (:REWRITE DEFAULT-+-1))
 (13 13 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 )
(ADE::DE-OCC-INDUCT)
(ADE::SYMBOL-ALISTP-FACT-CONS
 (6 6 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::SYMBOL-ALISTP-FACT-CONS-ONE-PAIR
 (31 4 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (28 2 (:DEFINITION TRUE-LISTP))
 (26 26 (:REWRITE DEFAULT-CDR))
 (26 6 (:DEFINITION SYMBOL-LISTP))
 (23 23 (:REWRITE DEFAULT-CAR))
 (19 19 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (8 1 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (3 1 (:DEFINITION MEMBER-EQUAL))
 (2 2 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (1 1 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (1 1 (:REWRITE ADE::SYMBOL-ALISTP-FACT-CONS))
 )
(ADE::SYMBOL-ALISTP-DE-OCC
 (500 5 (:DEFINITION ADE::DE))
 (361 21 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (270 5 (:DEFINITION ADE::SE-OCC))
 (170 140 (:REWRITE DEFAULT-CAR))
 (140 140 (:TYPE-PRESCRIPTION LEN))
 (135 15 (:DEFINITION PAIRLIS$))
 (132 102 (:REWRITE DEFAULT-CDR))
 (100 20 (:DEFINITION LEN))
 (80 80 (:LINEAR LEN-WHEN-PREFIXP))
 (55 11 (:DEFINITION ASSOC-EQUAL))
 (45 5 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (40 40 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (40 20 (:REWRITE DEFAULT-+-2))
 (30 30 (:TYPE-PRESCRIPTION ADE::SE))
 (30 5 (:DEFINITION MEMBER-EQUAL))
 (30 5 (:DEFINITION BINARY-APPEND))
 (25 25 (:TYPE-PRESCRIPTION PAIRLIS$))
 (25 25 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (25 10 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (25 5 (:DEFINITION ADE::DELETE-TO-EQ))
 (21 21 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (20 20 (:TYPE-PRESCRIPTION ADE::ASSOC-EQ-VALUES))
 (20 20 (:REWRITE DEFAULT-+-1))
 (10 10 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (4 4 (:REWRITE ADE::UPDATE-ALIST-DIFF-KEYS))
 (4 4 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-2))
 (4 4 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-1))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-OCC-INDUCT))
 )
(ADE::UPDATE-ALIST-OF-NOT-A-KEY
 (37 37 (:REWRITE DEFAULT-CAR))
 (9 9 (:REWRITE DEFAULT-CDR))
 (2 2 (:DEFINITION ACONS))
 )
(ADE::DE
 (1809 1757 (:REWRITE DEFAULT-CDR))
 (1766 1720 (:REWRITE DEFAULT-CAR))
 (1030 206 (:DEFINITION LEN))
 (567 9 (:DEFINITION ADE::SE-OCC))
 (532 31 (:REWRITE SYMBOL-LISTP-CDR-ASSOC-EQUAL))
 (439 31 (:DEFINITION SYMBOL-LIST-LISTP))
 (420 140 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (412 206 (:REWRITE DEFAULT-+-2))
 (360 20 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (309 75 (:DEFINITION MEMBER-EQUAL))
 (280 280 (:TYPE-PRESCRIPTION ADE::BVP))
 (227 29 (:DEFINITION PAIRLIS$))
 (206 206 (:REWRITE DEFAULT-+-1))
 (171 19 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (155 155 (:TYPE-PRESCRIPTION SYMBOL-LIST-LISTP))
 (118 2 (:DEFINITION ADE::DE-OCC))
 (96 96 (:LINEAR LEN-WHEN-PREFIXP))
 (65 13 (:DEFINITION ADE::DELETE-TO-EQ))
 (54 54 (:TYPE-PRESCRIPTION ADE::SE))
 (54 9 (:DEFINITION BINARY-APPEND))
 (48 48 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (45 18 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (40 4 (:DEFINITION SUBSETP-EQUAL))
 (20 20 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (10 10 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (8 8 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (6 1 (:REWRITE ADE::NET-SYNTAX-OKP->MODULE-SYNTAX-OKP))
 (2 2 (:REWRITE ADE::CONSP-OF-ASSOC-UPDATE-ALIST-LEMMA))
 (2 2 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-2))
 (2 2 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-1))
 (2 2 (:REWRITE ADE::ALISTP-PAIRLIS$))
 )
(ADE::FF$STATE
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::LATCH$STATE
 (6 6 (:REWRITE DEFAULT-CAR))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::LINK-CNTL$STATE
 (6 6 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::PAR-SHIFT-REG32$STATE
 (434 434 (:REWRITE DEFAULT-CDR))
 (186 186 (:REWRITE NTH-WHEN-PREFIXP))
 (8 8 (:REWRITE DEFAULT-CAR))
 )
(ADE::SHIFT-REG32$STATE
 (6 6 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE DEFAULT-CDR))
 )
(ADE::SE-OCC-BINDINGS
 (6 6 (:TYPE-PRESCRIPTION BINARY-APPEND))
 )
(ADE::OPEN-SE-OCC-BINDINGS
 (368 8 (:DEFINITION ADE::SE))
 (351 3 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-WHEN-DISJOINT))
 (288 16 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (216 24 (:DEFINITION PAIRLIS$))
 (192 6 (:REWRITE ADE::STRIP-CARS-PAIRLIS$))
 (188 140 (:REWRITE DEFAULT-CAR))
 (182 134 (:REWRITE DEFAULT-CDR))
 (123 18 (:REWRITE ADE::DISJOINT-ATOM))
 (112 112 (:TYPE-PRESCRIPTION LEN))
 (108 12 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (102 6 (:DEFINITION TRUE-LISTP))
 (80 16 (:DEFINITION LEN))
 (78 18 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
 (72 12 (:DEFINITION SYMBOL-LISTP))
 (72 3 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-DISJOINT))
 (64 64 (:LINEAR LEN-WHEN-PREFIXP))
 (63 36 (:DEFINITION ATOM))
 (60 60 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (57 3 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-SUBSET))
 (52 52 (:TYPE-PRESCRIPTION PAIRLIS$))
 (51 51 (:TYPE-PRESCRIPTION STRIP-CARS))
 (48 48 (:TYPE-PRESCRIPTION ADE::SE))
 (48 48 (:TYPE-PRESCRIPTION ADE::DISJOINT))
 (48 8 (:DEFINITION BINARY-APPEND))
 (45 3 (:DEFINITION SUBSETP-EQUAL))
 (43 27 (:REWRITE DEFAULT-+-2))
 (40 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (40 8 (:DEFINITION ADE::DELETE-TO-EQ))
 (40 8 (:DEFINITION ASSOC-EQUAL))
 (36 12 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (36 6 (:DEFINITION STRIP-CARS))
 (32 32 (:TYPE-PRESCRIPTION ADE::ASSOC-EQ-VALUES))
 (32 32 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (30 30 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (27 27 (:REWRITE DEFAULT-+-1))
 (24 24 (:TYPE-PRESCRIPTION ADE::BVP))
 (18 18 (:TYPE-PRESCRIPTION ATOM))
 (18 3 (:DEFINITION MEMBER-EQUAL))
 (16 16 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (16 16 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (15 15 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
 (15 15 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (15 6 (:REWRITE ZP-OPEN))
 (9 3 (:REWRITE FOLD-CONSTS-IN-+))
 (6 6 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (3 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 )
(ADE::DE-OCC-BINDINGS)
(ADE::OPEN-DE-OCC-BINDINGS
 (784 8 (:DEFINITION ADE::DE))
 (432 24 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (416 8 (:DEFINITION ADE::SE-OCC))
 (216 24 (:DEFINITION PAIRLIS$))
 (184 136 (:REWRITE DEFAULT-CDR))
 (182 134 (:REWRITE DEFAULT-CAR))
 (168 168 (:TYPE-PRESCRIPTION LEN))
 (120 24 (:DEFINITION LEN))
 (96 96 (:LINEAR LEN-WHEN-PREFIXP))
 (78 8 (:REWRITE ADE::UPDATE-ALIST-OF-NOT-A-KEY))
 (72 8 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (59 35 (:REWRITE DEFAULT-+-2))
 (54 8 (:DEFINITION ALISTP))
 (48 48 (:TYPE-PRESCRIPTION ADE::SE))
 (48 48 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (48 8 (:DEFINITION MEMBER-EQUAL))
 (48 8 (:DEFINITION BINARY-APPEND))
 (40 40 (:TYPE-PRESCRIPTION PAIRLIS$))
 (40 40 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (40 40 (:TYPE-PRESCRIPTION ALISTP))
 (40 16 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (40 8 (:DEFINITION ADE::DELETE-TO-EQ))
 (40 8 (:DEFINITION ASSOC-EQUAL))
 (35 35 (:REWRITE DEFAULT-+-1))
 (24 24 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (16 16 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (15 6 (:REWRITE ZP-OPEN))
 (9 3 (:REWRITE FOLD-CONSTS-IN-+))
 (3 3 (:REWRITE ADE::UPDATE-ALIST-DIFF-KEYS))
 (3 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 (3 3 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-2))
 (3 3 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-1))
 )
(ADE::LEN-DE
 (104 2 (:DEFINITION ADE::SE-OCC))
 (90 5 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (85 17 (:DEFINITION LEN))
 (73 67 (:REWRITE DEFAULT-CAR))
 (70 64 (:REWRITE DEFAULT-CDR))
 (58 1 (:DEFINITION ADE::NET-ARITY-OKP))
 (49 1 (:DEFINITION ADE::OCCS-ARITY-OKP))
 (48 1 (:DEFINITION ADE::DE-OCC))
 (47 7 (:DEFINITION PAIRLIS$))
 (38 1 (:DEFINITION ADE::OCC-ARITY-OKP))
 (37 1 (:DEFINITION ADE::ST-OKP))
 (36 4 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (34 17 (:REWRITE DEFAULT-+-2))
 (28 2 (:DEFINITION TRUE-LISTP))
 (27 3 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (24 4 (:DEFINITION SYMBOL-LISTP))
 (22 22 (:LINEAR LEN-WHEN-PREFIXP))
 (20 20 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (17 17 (:REWRITE DEFAULT-+-1))
 (15 15 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (15 3 (:DEFINITION ADE::DELETE-TO-EQ))
 (14 14 (:TYPE-PRESCRIPTION PAIRLIS$))
 (12 12 (:TYPE-PRESCRIPTION ADE::SE))
 (12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 2 (:DEFINITION BINARY-APPEND))
 (11 11 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (10 1 (:REWRITE ADE::UPDATE-ALIST-OF-NOT-A-KEY))
 (8 8 (:TYPE-PRESCRIPTION ADE::BVP))
 (5 5 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (2 2 (:TYPE-PRESCRIPTION ADE::POSP-PRIMP-OUTS))
 (1 1 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-ST))
 (1 1 (:REWRITE ADE::ALISTP-PAIRLIS$))
 )
(ADE::ST-OKP-DE-PRIMP-APPLY
 (9500 38 (:DEFINITION ADE::NET-ARITY-OKP))
 (9158 38 (:DEFINITION ADE::OCCS-ARITY-OKP))
 (8740 38 (:DEFINITION ADE::OCC-ARITY-OKP))
 (6248 6248 (:REWRITE DEFAULT-CAR))
 (1368 152 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (1064 76 (:DEFINITION TRUE-LISTP))
 (912 152 (:DEFINITION SYMBOL-LISTP))
 (760 760 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (652 652 (:REWRITE DEFAULT-CDR))
 (456 228 (:REWRITE DEFAULT-+-2))
 (456 152 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (304 304 (:TYPE-PRESCRIPTION ADE::BVP))
 (228 228 (:REWRITE DEFAULT-+-1))
 (133 133 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-INS))
 (76 76 (:TYPE-PRESCRIPTION ADE::POSP-PRIMP-OUTS))
 (64 32 (:DEFINITION NTH))
 (32 32 (:REWRITE NTH-WHEN-PREFIXP))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::SE-GUARD-DE-PRIMP-APPLY
 (18316 76 (:DEFINITION ADE::OCCS-ARITY-OKP))
 (17480 76 (:DEFINITION ADE::OCC-ARITY-OKP))
 (12328 12328 (:REWRITE DEFAULT-CAR))
 (1368 152 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (1064 76 (:DEFINITION TRUE-LISTP))
 (994 994 (:REWRITE DEFAULT-CDR))
 (912 152 (:DEFINITION SYMBOL-LISTP))
 (836 418 (:REWRITE DEFAULT-+-2))
 (760 760 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (456 152 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (418 418 (:REWRITE DEFAULT-+-1))
 (304 304 (:TYPE-PRESCRIPTION ADE::BVP))
 (247 247 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-INS))
 (152 152 (:TYPE-PRESCRIPTION ADE::POSP-PRIMP-OUTS))
 (64 32 (:DEFINITION NTH))
 (32 32 (:REWRITE NTH-WHEN-PREFIXP))
 (6 2 (:REWRITE ADE::F-GATES=B-GATES))
 (4 4 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(ADE::ASSOC-EQ-VALUE-DE-OCC
 (600 6 (:DEFINITION ADE::DE))
 (362 22 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (324 6 (:DEFINITION ADE::SE-OCC))
 (223 185 (:REWRITE DEFAULT-CAR))
 (168 130 (:REWRITE DEFAULT-CDR))
 (162 18 (:DEFINITION PAIRLIS$))
 (140 140 (:TYPE-PRESCRIPTION LEN))
 (100 20 (:DEFINITION LEN))
 (80 80 (:LINEAR LEN-WHEN-PREFIXP))
 (80 10 (:REWRITE ADE::UPDATE-ALIST-OF-NOT-A-KEY))
 (56 10 (:DEFINITION ASSOC-EQUAL))
 (54 8 (:DEFINITION ALISTP))
 (54 6 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (40 40 (:TYPE-PRESCRIPTION ALISTP))
 (40 40 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (40 20 (:REWRITE DEFAULT-+-2))
 (36 36 (:TYPE-PRESCRIPTION ADE::SE))
 (36 6 (:DEFINITION BINARY-APPEND))
 (30 30 (:TYPE-PRESCRIPTION PAIRLIS$))
 (30 12 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (30 6 (:DEFINITION ADE::DELETE-TO-EQ))
 (24 24 (:TYPE-PRESCRIPTION ADE::ASSOC-EQ-VALUES))
 (22 22 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (20 20 (:REWRITE DEFAULT-+-1))
 (12 12 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
 (12 12 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (4 4 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-1))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-OCC-INDUCT))
 (3 3 (:REWRITE ADE::UPDATE-ALIST-DIFF-KEYS))
 )
(ADE::DE-OCC-UPDATE-ALIST
 (400 4 (:DEFINITION ADE::DE))
 (307 18 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (230 201 (:REWRITE DEFAULT-CAR))
 (216 4 (:DEFINITION ADE::SE-OCC))
 (169 19 (:REWRITE ADE::UPDATE-ALIST-OF-NOT-A-KEY))
 (166 137 (:REWRITE DEFAULT-CDR))
 (119 119 (:TYPE-PRESCRIPTION LEN))
 (108 12 (:DEFINITION PAIRLIS$))
 (102 13 (:DEFINITION ALISTP))
 (85 17 (:DEFINITION LEN))
 (68 68 (:LINEAR LEN-WHEN-PREFIXP))
 (65 65 (:TYPE-PRESCRIPTION ALISTP))
 (60 10 (:DEFINITION ASSOC-EQUAL))
 (36 4 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (34 34 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (34 17 (:REWRITE DEFAULT-+-2))
 (24 24 (:TYPE-PRESCRIPTION ADE::SE))
 (24 4 (:DEFINITION BINARY-APPEND))
 (22 2 (:REWRITE ADE::SYMBOL-ALISTP-DE-OCC))
 (20 20 (:TYPE-PRESCRIPTION PAIRLIS$))
 (20 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (20 4 (:DEFINITION ADE::DELETE-TO-EQ))
 (18 18 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (17 17 (:REWRITE DEFAULT-+-1))
 (16 16 (:TYPE-PRESCRIPTION ADE::ASSOC-EQ-VALUES))
 (16 2 (:DEFINITION SYMBOL-ALISTP))
 (10 10 (:TYPE-PRESCRIPTION SYMBOL-ALISTP))
 (8 8 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (4 4 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-1))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-OCC-INDUCT))
 )
(ADE::ASSOC-EQ-VALUE-DE-OCC-UPDATE-ALIST-SAME-NAME
 (43 1 (:DEFINITION ADE::DE-OCC))
 (20 2 (:REWRITE ADE::UPDATE-ALIST-OF-NOT-A-KEY))
 (18 1 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (17 1 (:REWRITE ADE::DE-OCC-UPDATE-ALIST))
 (15 15 (:REWRITE DEFAULT-CAR))
 (15 2 (:DEFINITION MEMBER-EQUAL))
 (14 2 (:DEFINITION ALISTP))
 (12 2 (:DEFINITION ASSOC-EQUAL))
 (10 10 (:REWRITE DEFAULT-CDR))
 (8 2 (:DEFINITION STRIP-CARS))
 (7 7 (:TYPE-PRESCRIPTION LEN))
 (5 1 (:DEFINITION LEN))
 (4 4 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-2))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE ADE::UPDATE-ALIST-DIFF-KEYS))
 (1 1 (:REWRITE DEFAULT-+-1))
 (1 1 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 )
(ADE::ASSOC-EQ-VALUE-DE-OCC-UPDATE-ALIST-DIFF-NAMES
 (72 2 (:DEFINITION ADE::DE-OCC))
 (49 4 (:REWRITE ADE::UPDATE-ALIST-OF-NOT-A-KEY))
 (36 2 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (26 4 (:DEFINITION ALISTP))
 (24 24 (:REWRITE DEFAULT-CAR))
 (20 20 (:TYPE-PRESCRIPTION ALISTP))
 (20 3 (:DEFINITION MEMBER-EQUAL))
 (18 2 (:REWRITE ADE::ASSOC-EQ-VALUE-DE-OCC))
 (17 17 (:REWRITE DEFAULT-CDR))
 (14 14 (:TYPE-PRESCRIPTION LEN))
 (12 3 (:DEFINITION STRIP-CARS))
 (11 1 (:REWRITE ADE::SYMBOL-ALISTP-DE-OCC))
 (10 2 (:DEFINITION LEN))
 (10 2 (:DEFINITION ASSOC-EQUAL))
 (8 8 (:LINEAR LEN-WHEN-PREFIXP))
 (8 1 (:DEFINITION SYMBOL-ALISTP))
 (5 5 (:TYPE-PRESCRIPTION SYMBOL-ALISTP))
 (4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (4 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:TYPE-PRESCRIPTION ADE::DE-OCC))
 (2 2 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 )
(ADE::ASSOC-EQ-VALUES-DE-OCC-UPDATE-ALIST
 (72 2 (:DEFINITION ADE::DE-OCC))
 (55 4 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (49 4 (:REWRITE ADE::UPDATE-ALIST-OF-NOT-A-KEY))
 (26 4 (:DEFINITION ALISTP))
 (22 22 (:REWRITE DEFAULT-CAR))
 (21 21 (:TYPE-PRESCRIPTION LEN))
 (20 20 (:TYPE-PRESCRIPTION ALISTP))
 (17 17 (:REWRITE DEFAULT-CDR))
 (15 3 (:DEFINITION LEN))
 (13 3 (:DEFINITION MEMBER-EQUAL))
 (12 12 (:LINEAR LEN-WHEN-PREFIXP))
 (11 1 (:REWRITE ADE::SYMBOL-ALISTP-DE-OCC))
 (10 2 (:DEFINITION ASSOC-EQUAL))
 (8 2 (:DEFINITION STRIP-CARS))
 (8 1 (:DEFINITION SYMBOL-ALISTP))
 (6 6 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (6 3 (:REWRITE DEFAULT-+-2))
 (5 5 (:TYPE-PRESCRIPTION SYMBOL-ALISTP))
 (4 4 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 2 (:TYPE-PRESCRIPTION ADE::DE-OCC))
 )
(ADE::STRIP-CARS-DE-OCC
 (196 2 (:DEFINITION ADE::DE))
 (162 9 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (104 2 (:DEFINITION ADE::SE-OCC))
 (77 65 (:REWRITE DEFAULT-CAR))
 (64 52 (:REWRITE DEFAULT-CDR))
 (63 63 (:TYPE-PRESCRIPTION LEN))
 (54 6 (:DEFINITION PAIRLIS$))
 (49 5 (:REWRITE ADE::UPDATE-ALIST-OF-NOT-A-KEY))
 (45 9 (:DEFINITION LEN))
 (36 36 (:LINEAR LEN-WHEN-PREFIXP))
 (34 5 (:DEFINITION ALISTP))
 (29 5 (:DEFINITION ASSOC-EQUAL))
 (25 25 (:TYPE-PRESCRIPTION ALISTP))
 (18 18 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (18 9 (:REWRITE DEFAULT-+-2))
 (18 2 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (12 12 (:TYPE-PRESCRIPTION ADE::SE))
 (12 2 (:DEFINITION MEMBER-EQUAL))
 (12 2 (:DEFINITION BINARY-APPEND))
 (10 10 (:TYPE-PRESCRIPTION PAIRLIS$))
 (10 10 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (10 4 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (10 2 (:DEFINITION ADE::DELETE-TO-EQ))
 (9 9 (:REWRITE DEFAULT-+-1))
 (9 9 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (8 8 (:TYPE-PRESCRIPTION ADE::ASSOC-EQ-VALUES))
 (4 4 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (3 3 (:TYPE-PRESCRIPTION ADE::DE-OCC-INDUCT))
 (2 2 (:REWRITE ADE::UPDATE-ALIST-DIFF-KEYS))
 (2 2 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-2))
 (2 2 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-1))
 )
(ADE::FLAG-DE
 (424 208 (:REWRITE DEFAULT-+-2))
 (309 39 (:DEFINITION LEN))
 (273 208 (:REWRITE DEFAULT-+-1))
 (266 19 (:DEFINITION LENGTH))
 (178 107 (:REWRITE DEFAULT-CDR))
 (152 38 (:REWRITE COMMUTATIVITY-OF-+))
 (152 38 (:DEFINITION INTEGER-ABS))
 (139 105 (:REWRITE DEFAULT-CAR))
 (62 50 (:REWRITE DEFAULT-<-2))
 (61 50 (:REWRITE DEFAULT-<-1))
 (57 57 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (57 38 (:REWRITE STR::CONSP-OF-EXPLODE))
 (46 46 (:REWRITE FOLD-CONSTS-IN-+))
 (38 38 (:REWRITE DEFAULT-UNARY-MINUS))
 (38 19 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
 (28 2 (:TYPE-PRESCRIPTION RETURN-LAST))
 (20 4 (:DEFINITION ADE::DELETE-TO-EQ))
 (19 19 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (19 19 (:REWRITE DEFAULT-REALPART))
 (19 19 (:REWRITE DEFAULT-NUMERATOR))
 (19 19 (:REWRITE DEFAULT-IMAGPART))
 (19 19 (:REWRITE DEFAULT-DENOMINATOR))
 (15 3 (:DEFINITION ASSOC-EQUAL))
 (6 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
 (3 1 (:DEFINITION POSP))
 (2 2 (:TYPE-PRESCRIPTION THROW-NONEXEC-ERROR))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(FLAG::FLAG-EQUIV-LEMMA)
(ADE::FLAG-DE-EQUIVALENCES)
(ADE::ALISTP-SYMBOL-LISTP-SYMBOL-ALISTP-ARE-TRUE-LISTP)
(ADE::WELL-FORMED-ST)
(ADE::SE-GUARD=>WELL-FORMED-ST
 (196 4 (:DEFINITION ADE::OCCS-ARITY-OKP))
 (174 6 (:REWRITE ADE::ALISTP-SYMBOL-LISTP-SYMBOL-ALISTP-ARE-TRUE-LISTP))
 (152 4 (:DEFINITION ADE::OCC-ARITY-OKP))
 (130 26 (:DEFINITION LEN))
 (129 3 (:DEFINITION TRUE-LISTP))
 (88 88 (:REWRITE DEFAULT-CAR))
 (81 81 (:REWRITE DEFAULT-CDR))
 (72 12 (:DEFINITION SYMBOL-LISTP))
 (66 66 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (60 12 (:DEFINITION ASSOC-EQUAL))
 (54 6 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (52 26 (:REWRITE DEFAULT-+-2))
 (48 6 (:DEFINITION SYMBOL-ALISTP))
 (36 6 (:DEFINITION ALISTP))
 (26 26 (:REWRITE DEFAULT-+-1))
 (18 6 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (12 12 (:TYPE-PRESCRIPTION ADE::BVP))
 (10 2 (:DEFINITION PAIRLIS$))
 (10 2 (:DEFINITION ADE::DELETE-TO-EQ))
 (8 8 (:TYPE-PRESCRIPTION ADE::POSP-PRIMP-OUTS))
 (4 4 (:LINEAR LEN-WHEN-PREFIXP))
 (2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (2 1 (:LINEAR ADE::NATP-PRIMP-INS))
 )
(ADE::WELL-FORMED-ST-OCCS)
(ADE::SE-OCC-GUARD=>WELL-FORMED-ST-OCCS
 (232 8 (:REWRITE ADE::ALISTP-SYMBOL-LISTP-SYMBOL-ALISTP-ARE-TRUE-LISTP))
 (172 4 (:DEFINITION TRUE-LISTP))
 (108 20 (:DEFINITION SYMBOL-LISTP))
 (101 101 (:REWRITE DEFAULT-CDR))
 (101 101 (:REWRITE DEFAULT-CAR))
 (80 16 (:DEFINITION LEN))
 (72 8 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (48 8 (:DEFINITION ALISTP))
 (32 16 (:REWRITE DEFAULT-+-2))
 (30 6 (:DEFINITION ASSOC-EQUAL))
 (24 8 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (16 16 (:TYPE-PRESCRIPTION ADE::BVP))
 (16 16 (:REWRITE DEFAULT-+-1))
 (12 4 (:DEFINITION MEMBER-EQUAL))
 (8 2 (:DEFINITION STRIP-CARS))
 )
(ADE::WELL-FORMED-ST-DE<->WELL-FORMED-ST-OCCS-DE-OCC-AUX
 (41 1 (:LINEAR ADE::NATP-PRIMP-ST))
 (2 2 (:LINEAR LEN-WHEN-PREFIXP))
 (1 1 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 )
(ADE::WELL-FORMED-ST-DE<->WELL-FORMED-ST-OCCS-DE-OCC
 (20815 20206 (:REWRITE DEFAULT-CAR))
 (18635 17429 (:REWRITE DEFAULT-CDR))
 (13094 1122 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (10266 15 (:DEFINITION ADE::SE-GUARD))
 (9640 1306 (:DEFINITION ALISTP))
 (9458 1873 (:DEFINITION ASSOC-EQUAL))
 (6370 6 (:REWRITE ADE::ST-OKP-DE-PRIMP-APPLY))
 (5387 289 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
 (4013 11 (:REWRITE ADE::LEN-DE))
 (3752 67 (:DEFINITION ADE::SE-OCC))
 (3366 1122 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (3302 1651 (:REWRITE DEFAULT-+-2))
 (2244 2244 (:TYPE-PRESCRIPTION ADE::BVP))
 (1971 255 (:DEFINITION PAIRLIS$))
 (1798 1798 (:LINEAR LEN-WHEN-PREFIXP))
 (1651 1651 (:REWRITE DEFAULT-+-1))
 (1586 15 (:DEFINITION ADE::SE-INS-GUARD))
 (1568 224 (:DEFINITION NTH))
 (899 899 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (855 95 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
 (720 144 (:DEFINITION ADE::DELETE-TO-EQ))
 (606 52 (:REWRITE SYMBOL-LISTP-CDR-ASSOC-EQUAL))
 (602 602 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
 (476 39 (:DEFINITION SYMBOL-LIST-LISTP))
 (411 411 (:TYPE-PRESCRIPTION PAIRLIS$))
 (402 402 (:TYPE-PRESCRIPTION ADE::SE))
 (402 67 (:DEFINITION BINARY-APPEND))
 (335 134 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (289 289 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
 (224 224 (:REWRITE NTH-WHEN-PREFIXP))
 (195 195 (:TYPE-PRESCRIPTION SYMBOL-LIST-LISTP))
 (130 65 (:LINEAR ADE::NATP-PRIMP-INS))
 (84 14 (:REWRITE ADE::F-GATES=B-GATES))
 (80 8 (:DEFINITION SUBSETP-EQUAL))
 (28 28 (:TYPE-PRESCRIPTION BOOLEANP))
 (27 27 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-2))
 (27 27 (:REWRITE ADE::ASSOC-EQ-VALUE-UPDATE-ALIST-1))
 (17 17 (:REWRITE ADE::ALISTP-PAIRLIS$))
 (16 16 (:REWRITE ADE::UPDATE-ALIST-DIFF-KEYS))
 (16 16 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
 (16 16 (:REWRITE ADE::ASSOC-EQ-VALUE-DE-OCC-UPDATE-ALIST-DIFF-NAMES))
 (15 15 (:TYPE-PRESCRIPTION ADE::SE-GUARD))
 (4 2 (:TYPE-PRESCRIPTION ADE::SE-OCC))
 (3 1 (:REWRITE ADE::NET-SYNTAX-OKP->MODULE-SYNTAX-OKP))
 )
(ADE::WELL-FORMED-ST-DE)
(ADE::WELL-FORMED-ST-OCCS-DE-OCC)
(ADE::DE-SIM-GUARD)
(ADE::DE-SIM)
(ADE::OPEN-DE-SIM-ATOM
 (19 19 (:TYPE-PRESCRIPTION ADE::DE-SIM))
 )
(ADE::OPEN-DE-SIM
 (6 6 (:REWRITE ADE::OPEN-DE-SIM-ATOM))
 (5 5 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE DEFAULT-CAR))
 )
(ADE::DE-SIM-TRACE)
(ADE::SIMULATE)
(ADE::DE-N)
(ADE::DE-PLUS
 (26 14 (:REWRITE DEFAULT-CDR))
 (25 25 (:REWRITE DEFAULT-+-2))
 (25 25 (:REWRITE DEFAULT-+-1))
 (24 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (21 9 (:REWRITE ZP-OPEN))
 (21 9 (:REWRITE DEFAULT-CAR))
 (17 9 (:REWRITE FOLD-CONSTS-IN-+))
 (12 12 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (7 7 (:REWRITE DEFAULT-<-2))
 (7 7 (:REWRITE DEFAULT-<-1))
 )
(ADE::OPEN-DE-N-ZP
 (19 19 (:TYPE-PRESCRIPTION ADE::DE-N))
 (1 1 (:REWRITE ZP-OPEN))
 )
(ADE::OPEN-DE-N
 (41 6 (:REWRITE ADE::OPEN-DE-N-ZP))
 (39 8 (:REWRITE ZP-OPEN))
 (12 12 (:REWRITE DEFAULT-<-2))
 (12 12 (:REWRITE DEFAULT-<-1))
 (7 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-+-1))
 (6 2 (:REWRITE FOLD-CONSTS-IN-+))
 (5 5 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE DEFAULT-CAR))
 (2 2 (:REWRITE ADE::DE-PLUS))
 )
(ADE::DE-SIM
 (406 14 (:REWRITE ADE::ALISTP-SYMBOL-LISTP-SYMBOL-ALISTP-ARE-TRUE-LISTP))
 (301 7 (:DEFINITION TRUE-LISTP))
 (248 52 (:REWRITE ADE::WELL-FORMED-ST-DE<->WELL-FORMED-ST-OCCS-DE-OCC-AUX))
 (240 24 (:DEFINITION LEN))
 (168 28 (:DEFINITION SYMBOL-LISTP))
 (154 154 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (134 134 (:REWRITE DEFAULT-CAR))
 (126 14 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (114 2 (:DEFINITION ADE::OCCS-ARITY-OKP))
 (112 14 (:DEFINITION SYMBOL-ALISTP))
 (106 106 (:REWRITE DEFAULT-CDR))
 (92 2 (:DEFINITION ADE::OCC-ARITY-OKP))
 (84 14 (:DEFINITION ALISTP))
 (60 60 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-ST))
 (48 24 (:REWRITE DEFAULT-+-2))
 (42 42 (:LINEAR LEN-WHEN-PREFIXP))
 (42 14 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (28 28 (:TYPE-PRESCRIPTION ADE::BVP))
 (24 24 (:REWRITE DEFAULT-+-1))
 (21 21 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (16 8 (:LINEAR ADE::NATP-PRIMP-ST))
 (4 4 (:TYPE-PRESCRIPTION ADE::POSP-PRIMP-OUTS))
 (2 1 (:LINEAR ADE::NATP-PRIMP-INS))
 )
(ADE::DE-SIM-TRACE
 (406 14 (:REWRITE ADE::ALISTP-SYMBOL-LISTP-SYMBOL-ALISTP-ARE-TRUE-LISTP))
 (301 7 (:DEFINITION TRUE-LISTP))
 (248 52 (:REWRITE ADE::WELL-FORMED-ST-DE<->WELL-FORMED-ST-OCCS-DE-OCC-AUX))
 (240 24 (:DEFINITION LEN))
 (168 28 (:DEFINITION SYMBOL-LISTP))
 (154 154 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (134 134 (:REWRITE DEFAULT-CAR))
 (126 14 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (114 2 (:DEFINITION ADE::OCCS-ARITY-OKP))
 (112 14 (:DEFINITION SYMBOL-ALISTP))
 (106 106 (:REWRITE DEFAULT-CDR))
 (92 2 (:DEFINITION ADE::OCC-ARITY-OKP))
 (84 14 (:DEFINITION ALISTP))
 (60 60 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-ST))
 (48 24 (:REWRITE DEFAULT-+-2))
 (42 42 (:LINEAR LEN-WHEN-PREFIXP))
 (42 14 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (28 28 (:TYPE-PRESCRIPTION ADE::BVP))
 (24 24 (:REWRITE DEFAULT-+-1))
 (21 21 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (16 8 (:LINEAR ADE::NATP-PRIMP-ST))
 (4 4 (:TYPE-PRESCRIPTION ADE::POSP-PRIMP-OUTS))
 (2 1 (:LINEAR ADE::NATP-PRIMP-INS))
 )
(ADE::SIMULATE
 (580 20 (:REWRITE ADE::ALISTP-SYMBOL-LISTP-SYMBOL-ALISTP-ARE-TRUE-LISTP))
 (430 10 (:DEFINITION TRUE-LISTP))
 (384 40 (:DEFINITION LEN))
 (380 86 (:REWRITE ADE::WELL-FORMED-ST-DE<->WELL-FORMED-ST-OCCS-DE-OCC-AUX))
 (291 4 (:DEFINITION ADE::OCCS-ARITY-OKP))
 (244 4 (:DEFINITION ADE::OCC-ARITY-OKP))
 (240 40 (:DEFINITION SYMBOL-LISTP))
 (220 220 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (201 201 (:REWRITE DEFAULT-CAR))
 (180 20 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (164 164 (:REWRITE DEFAULT-CDR))
 (160 20 (:DEFINITION SYMBOL-ALISTP))
 (120 20 (:DEFINITION ALISTP))
 (90 90 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-ST))
 (80 40 (:REWRITE DEFAULT-+-2))
 (74 74 (:LINEAR LEN-WHEN-PREFIXP))
 (60 20 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (40 40 (:TYPE-PRESCRIPTION ADE::BVP))
 (40 40 (:REWRITE DEFAULT-+-1))
 (37 37 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (24 12 (:LINEAR ADE::NATP-PRIMP-ST))
 (14 14 (:TYPE-PRESCRIPTION ADE::POSP-PRIMP-OUTS))
 (6 3 (:LINEAR ADE::NATP-PRIMP-INS))
 (4 2 (:LINEAR ADE::POSP-PRIMP-OUTS))
 )
(ADE::DE-N
 (2843 171 (:REWRITE ADE::WELL-FORMED-ST-DE<->WELL-FORMED-ST-OCCS-DE-OCC-AUX))
 (2565 89 (:REWRITE ADE::ALISTP-SYMBOL-LISTP-SYMBOL-ALISTP-ARE-TRUE-LISTP))
 (2010 10 (:DEFINITION ADE::OCCS-ARITY-OKP))
 (1979 45 (:DEFINITION TRUE-LISTP))
 (1900 10 (:DEFINITION ADE::OCC-ARITY-OKP))
 (1066 178 (:DEFINITION SYMBOL-LISTP))
 (956 956 (:TYPE-PRESCRIPTION SYMBOL-LISTP))
 (797 89 (:REWRITE ADE::SYMBOL-LISTP=>TRUE-LISTP))
 (713 89 (:DEFINITION SYMBOL-ALISTP))
 (677 677 (:REWRITE DEFAULT-CAR))
 (551 551 (:REWRITE DEFAULT-CDR))
 (533 89 (:DEFINITION ALISTP))
 (263 89 (:REWRITE ADE::BV-IS-TRUE-LIST))
 (174 174 (:TYPE-PRESCRIPTION ADE::BVP))
 (174 87 (:REWRITE DEFAULT-+-2))
 (105 105 (:TYPE-PRESCRIPTION ADE::NATP-PRIMP-ST))
 (87 87 (:REWRITE DEFAULT-+-1))
 (80 80 (:LINEAR LEN-WHEN-PREFIXP))
 (40 40 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
 (28 14 (:LINEAR ADE::NATP-PRIMP-ST))
 (20 20 (:TYPE-PRESCRIPTION ADE::POSP-PRIMP-OUTS))
 (16 8 (:REWRITE ADE::SYMBOL-LISTP-MD-OF-INS-OUTS-AND-ST))
 (6 3 (:REWRITE DEFAULT-<-2))
 (3 3 (:REWRITE DEFAULT-<-1))
 )