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))
)
|
