1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
|
(ADE::UNBOUND-IN-BODY)
(ADE::UNBOUND-IN-BODY-ATOM)
(ADE::UNBOUND-IN-BODY-LISTP
(15 5 (:DEFINITION MEMBER-EQUAL))
(8 8 (:REWRITE DEFAULT-CDR))
(8 8 (:REWRITE DEFAULT-CAR))
(6 6 (:REWRITE ADE::UNBOUND-IN-BODY-ATOM))
)
(ADE::ALL-UNBOUND-IN-BODY)
(ADE::ALL-UNBOUND-IN-BODY-ATOM)
(ADE::ALL-UNBOUND-IN-BODY-LISTP
(45 10 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
(40 10 (:REWRITE ADE::DISJOINT-ATOM))
(20 20 (:DEFINITION ATOM))
(10 10 (:TYPE-PRESCRIPTION ATOM))
(6 6 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM))
(3 3 (:REWRITE DEFAULT-CDR))
(3 3 (:REWRITE DEFAULT-CAR))
)
(ADE::ALL-UNBOUND-IN-BODY-APPEND
(331 100 (:REWRITE ADE::DISJOINT-ATOM))
(77 77 (:TYPE-PRESCRIPTION ATOM))
(40 10 (:DEFINITION BINARY-APPEND))
(36 36 (:REWRITE DEFAULT-CAR))
(25 25 (:REWRITE DEFAULT-CDR))
(20 20 (:REWRITE APPEND-WHEN-NOT-CONSP))
)
(ADE::ALL-UNBOUND-IN-BODY-CONS
(460 115 (:REWRITE ADE::DISJOINT-ATOM))
(246 63 (:DEFINITION MEMBER-EQUAL))
(119 119 (:REWRITE DEFAULT-CDR))
(115 115 (:TYPE-PRESCRIPTION ATOM))
(114 114 (:REWRITE DEFAULT-CAR))
)
(ADE::ALL-UNBOUND-IN-BODY-ATOM-NAMES
(5 5 (:REWRITE DEFAULT-CAR))
(2 2 (:REWRITE DEFAULT-CDR))
)
(ADE::UNBOUND-IN-BODY-SE-OCC
(648 8 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-WHEN-DISJOINT))
(381 24 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
(328 48 (:REWRITE ADE::DISJOINT-ATOM))
(275 25 (:DEFINITION PAIRLIS$))
(261 186 (:REWRITE DEFAULT-CAR))
(239 164 (:REWRITE DEFAULT-CDR))
(224 16 (:REWRITE ADE::STRIP-CARS-PAIRLIS$))
(208 48 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
(192 8 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-DISJOINT))
(152 8 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-SUBSET))
(150 150 (:TYPE-PRESCRIPTION ADE::SE))
(147 147 (:TYPE-PRESCRIPTION LEN))
(136 136 (:TYPE-PRESCRIPTION STRIP-CARS))
(129 129 (:TYPE-PRESCRIPTION PAIRLIS$))
(128 128 (:TYPE-PRESCRIPTION ADE::DISJOINT))
(128 16 (:DEFINITION TRUE-LISTP))
(120 20 (:DEFINITION BINARY-APPEND))
(120 8 (:DEFINITION SUBSETP-EQUAL))
(105 21 (:DEFINITION LEN))
(97 40 (:REWRITE APPEND-WHEN-NOT-CONSP))
(96 32 (:REWRITE ADE::BV-IS-TRUE-LIST))
(96 16 (:DEFINITION STRIP-CARS))
(84 84 (:LINEAR LEN-WHEN-PREFIXP))
(80 80 (:TYPE-PRESCRIPTION TRUE-LISTP))
(64 64 (:TYPE-PRESCRIPTION ADE::BVP))
(57 11 (:DEFINITION MEMBER-EQUAL))
(48 48 (:TYPE-PRESCRIPTION ATOM))
(42 42 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(42 21 (:REWRITE DEFAULT-+-2))
(40 40 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(24 24 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
(21 21 (:REWRITE DEFAULT-+-1))
(16 16 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
(5 5 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
(3 3 (:TYPE-PRESCRIPTION ADE::SE-OCC-INDUCT))
)
(ADE::ALL-UNBOUND-IN-BODY-SE-OCC
(1053 13 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-WHEN-DISJOINT))
(612 51 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
(541 80 (:REWRITE ADE::DISJOINT-ATOM))
(364 26 (:REWRITE ADE::STRIP-CARS-PAIRLIS$))
(347 80 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
(286 211 (:REWRITE DEFAULT-CAR))
(281 206 (:REWRITE DEFAULT-CDR))
(275 25 (:DEFINITION PAIRLIS$))
(247 13 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-SUBSET))
(231 231 (:TYPE-PRESCRIPTION LEN))
(221 221 (:TYPE-PRESCRIPTION STRIP-CARS))
(208 26 (:DEFINITION TRUE-LISTP))
(195 13 (:DEFINITION SUBSETP-EQUAL))
(165 165 (:TYPE-PRESCRIPTION PAIRLIS$))
(165 33 (:DEFINITION LEN))
(156 52 (:REWRITE ADE::BV-IS-TRUE-LIST))
(156 26 (:DEFINITION STRIP-CARS))
(150 150 (:TYPE-PRESCRIPTION ADE::SE))
(150 25 (:DEFINITION BINARY-APPEND))
(132 132 (:LINEAR LEN-WHEN-PREFIXP))
(130 130 (:TYPE-PRESCRIPTION TRUE-LISTP))
(113 50 (:REWRITE APPEND-WHEN-NOT-CONSP))
(104 104 (:TYPE-PRESCRIPTION ADE::BVP))
(80 80 (:TYPE-PRESCRIPTION ATOM))
(78 13 (:DEFINITION MEMBER-EQUAL))
(66 66 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(66 33 (:REWRITE DEFAULT-+-2))
(65 65 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(65 65 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
(49 49 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
(33 33 (:REWRITE DEFAULT-+-1))
(26 26 (:REWRITE ADE::SUBSETP-TRANSITIVITY))
(11 11 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM-NAMES))
(3 3 (:TYPE-PRESCRIPTION ADE::SE-OCC-INDUCT))
)
|