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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
|
(ADE::T-OR-NOR-BODY)
(ADE::T-OR-NOR*)
(ADE::T-OR-NOR*$DESTRUCTURE
(561 11 (:DEFINITION TAKE))
(517 22 (:REWRITE TAKE-OF-TOO-MANY))
(154 22 (:REWRITE TAKE-WHEN-ATOM))
(144 78 (:REWRITE DEFAULT-CDR))
(143 11 (:DEFINITION NTHCDR))
(121 11 (:DEFINITION LEN))
(106 73 (:REWRITE DEFAULT-CAR))
(77 77 (:TYPE-PRESCRIPTION LEN))
(77 44 (:REWRITE DEFAULT-+-2))
(66 33 (:REWRITE ADE::NFIX-OF-NAT))
(55 44 (:REWRITE DEFAULT-+-1))
(44 44 (:REWRITE ADE::TREE-SIZE-ATOM))
(44 22 (:REWRITE DEFAULT-<-2))
(44 22 (:REWRITE DEFAULT-<-1))
(44 11 (:REWRITE COMMUTATIVITY-OF-+))
(33 11 (:REWRITE ADE::LEN-SIS))
(22 22 (:TYPE-PRESCRIPTION NFIX))
(22 22 (:LINEAR LEN-WHEN-PREFIXP))
(22 22 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(4 1 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
(2 2 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
(1 1 (:REWRITE DEFAULT-SYMBOL-NAME))
)
(ADE::NOT-PRIMP-T-OR-NOR)
(ADE::T-OR-NOR$NETLIST
(166 76 (:REWRITE DEFAULT-+-2))
(108 76 (:REWRITE DEFAULT-+-1))
(84 6 (:DEFINITION LENGTH))
(66 6 (:DEFINITION LEN))
(49 31 (:REWRITE DEFAULT-CDR))
(48 12 (:REWRITE COMMUTATIVITY-OF-+))
(48 12 (:DEFINITION INTEGER-ABS))
(26 26 (:REWRITE FOLD-CONSTS-IN-+))
(26 26 (:REWRITE DEFAULT-CAR))
(24 16 (:REWRITE DEFAULT-<-2))
(20 16 (:REWRITE DEFAULT-<-1))
(18 18 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
(18 12 (:REWRITE STR::CONSP-OF-EXPLODE))
(12 12 (:REWRITE DEFAULT-UNARY-MINUS))
(12 6 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
(8 8 (:TYPE-PRESCRIPTION TRUE-LISTP))
(6 6 (:TYPE-PRESCRIPTION LEN))
(6 6 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
(6 6 (:REWRITE DEFAULT-REALPART))
(6 6 (:REWRITE DEFAULT-NUMERATOR))
(6 6 (:REWRITE DEFAULT-IMAGPART))
(6 6 (:REWRITE DEFAULT-DENOMINATOR))
)
(ADE::T-OR-NOR&
(1764 912 (:REWRITE DEFAULT-+-2))
(1400 100 (:DEFINITION LENGTH))
(1232 912 (:REWRITE DEFAULT-+-1))
(1100 100 (:DEFINITION LEN))
(800 200 (:REWRITE COMMUTATIVITY-OF-+))
(800 200 (:DEFINITION INTEGER-ABS))
(701 401 (:REWRITE DEFAULT-CDR))
(467 467 (:REWRITE DEFAULT-CAR))
(399 9 (:DEFINITION ADE::T-OR-NOR&))
(352 278 (:REWRITE DEFAULT-<-2))
(352 88 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
(348 278 (:REWRITE DEFAULT-<-1))
(300 300 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
(300 200 (:REWRITE STR::CONSP-OF-EXPLODE))
(256 256 (:REWRITE FOLD-CONSTS-IN-+))
(240 16 (:LINEAR ACL2-COUNT-CAR-CDR-LINEAR))
(200 200 (:REWRITE DEFAULT-UNARY-MINUS))
(200 100 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
(176 176 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
(100 100 (:TYPE-PRESCRIPTION LEN))
(100 100 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
(100 100 (:REWRITE DEFAULT-REALPART))
(100 100 (:REWRITE DEFAULT-NUMERATOR))
(100 100 (:REWRITE DEFAULT-IMAGPART))
(100 100 (:REWRITE DEFAULT-DENOMINATOR))
(88 88 (:REWRITE DEFAULT-SYMBOL-NAME))
(9 3 (:DEFINITION ALISTP))
)
(ADE::T-OR-NOR-INDUCTION
(261 120 (:REWRITE DEFAULT-+-2))
(168 120 (:REWRITE DEFAULT-+-1))
(126 9 (:DEFINITION LENGTH))
(119 13 (:DEFINITION LEN))
(96 4 (:REWRITE TAKE-OF-TOO-MANY))
(82 55 (:REWRITE DEFAULT-CDR))
(72 18 (:REWRITE COMMUTATIVITY-OF-+))
(72 18 (:DEFINITION INTEGER-ABS))
(64 2 (:DEFINITION TAKE))
(44 44 (:REWRITE DEFAULT-CAR))
(44 28 (:REWRITE DEFAULT-<-2))
(39 39 (:REWRITE FOLD-CONSTS-IN-+))
(38 28 (:REWRITE DEFAULT-<-1))
(33 33 (:TYPE-PRESCRIPTION LEN))
(27 27 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
(27 18 (:REWRITE STR::CONSP-OF-EXPLODE))
(24 24 (:TYPE-PRESCRIPTION ADE::TREE-SIZE))
(22 2 (:DEFINITION ADE::DELETE-TO-EQ))
(18 18 (:REWRITE DEFAULT-UNARY-MINUS))
(18 9 (:REWRITE STR::COERCE-TO-LIST-REMOVAL))
(9 9 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
(9 9 (:REWRITE DEFAULT-REALPART))
(9 9 (:REWRITE DEFAULT-NUMERATOR))
(9 9 (:REWRITE DEFAULT-IMAGPART))
(9 9 (:REWRITE DEFAULT-DENOMINATOR))
(8 8 (:LINEAR LEN-WHEN-PREFIXP))
(8 8 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(8 4 (:REWRITE ADE::NFIX-OF-NAT))
(8 2 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
(4 4 (:TYPE-PRESCRIPTION NFIX))
(4 4 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
(4 4 (:REWRITE TAKE-WHEN-ATOM))
(2 2 (:REWRITE ADE::TREE-SIZE-ATOM))
(2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
)
(ADE::TR-OR-NOR
(5 5 (:TYPE-PRESCRIPTION ADE::F-BUF))
(2 2 (:REWRITE DEFAULT-CAR))
(1 1 (:REWRITE DEFAULT-CDR))
)
(ADE::TR-OR-NOR-OF-V-THREEFIX-CANCELED-AUX
(2 2 (:REWRITE DEFAULT-CAR))
)
(ADE::TR-OR-NOR-OF-V-THREEFIX-CANCELED
(10846 464 (:REWRITE TAKE-OF-TOO-MANY))
(5418 148 (:DEFINITION TAKE))
(2736 460 (:DEFINITION LEN))
(2735 1691 (:REWRITE DEFAULT-CAR))
(2732 602 (:REWRITE ADE::F-GATES=B-GATES))
(2724 1702 (:REWRITE DEFAULT-CDR))
(2720 2720 (:TYPE-PRESCRIPTION LEN))
(2257 392 (:REWRITE ADE::V-THREEFIX-BVP))
(2010 1090 (:REWRITE DEFAULT-+-2))
(1348 1090 (:REWRITE DEFAULT-+-1))
(1222 1222 (:TYPE-PRESCRIPTION ADE::BVP))
(1170 610 (:REWRITE DEFAULT-<-2))
(1040 610 (:REWRITE DEFAULT-<-1))
(1014 420 (:REWRITE TAKE-WHEN-ATOM))
(848 848 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(792 792 (:LINEAR LEN-WHEN-PREFIXP))
(792 44 (:REWRITE ADE::LEN-NTHCDR))
(462 134 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
(440 22 (:DEFINITION BINARY-APPEND))
(424 212 (:REWRITE CONSP-OF-TAKE))
(418 22 (:REWRITE REPEAT-WHEN-ZP))
(384 104 (:TYPE-PRESCRIPTION ADE::BVP-TAKE))
(364 32 (:REWRITE ADE::TR-OR-NOR-OF-V-THREEFIX-CANCELED-AUX))
(330 22 (:REWRITE ZP-OPEN))
(308 28 (:REWRITE SECOND-OF-TAKE))
(225 61 (:REWRITE ADE::BVP-NTHCDR))
(220 22 (:REWRITE ADE::TREE-SIZE-LEMMAS))
(198 44 (:REWRITE APPEND-WHEN-NOT-CONSP))
(192 46 (:REWRITE ADE::BVP-TAKE))
(156 156 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
(132 44 (:REWRITE LEN-OF-TAKE))
(44 22 (:REWRITE DEFAULT-UNARY-MINUS))
(36 12 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(22 22 (:TYPE-PRESCRIPTION ZP))
(12 12 (:TYPE-PRESCRIPTION REPEAT))
(12 12 (:TYPE-PRESCRIPTION BINARY-APPEND))
(6 2 (:REWRITE ADE::BOOLEANP-OF-F-BUF))
(5 5 (:TYPE-PRESCRIPTION ADE::F-OR))
)
(ADE::NOT-PRIMP-T-OR)
(ADE::NOT-PRIMP-T-NOR)
(ADE::T-OR-NOR$VALUE
(2288 1144 (:REWRITE DEFAULT-+-2))
(1786 1144 (:REWRITE DEFAULT-+-1))
(1701 126 (:REWRITE TAKE-MORE-OF-TAKE-FEWER))
(1678 126 (:REWRITE TAKE-FEWER-OF-TAKE-MORE))
(1503 431 (:REWRITE TAKE-WHEN-ATOM))
(1224 306 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
(508 508 (:LINEAR LEN-WHEN-PREFIXP))
(505 101 (:REWRITE CAR-OF-TAKE))
(470 236 (:REWRITE DEFAULT-<-1))
(450 45 (:REWRITE SECOND-OF-TAKE))
(364 236 (:REWRITE DEFAULT-<-2))
(336 48 (:REWRITE ADE::ASSOC-EQ-VALUE-PAIRLIS$-NOT-MEMBER))
(306 306 (:REWRITE DEFAULT-SYMBOL-NAME))
(260 130 (:REWRITE CONSP-OF-TAKE))
(246 32 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
(240 240 (:TYPE-PRESCRIPTION PAIRLIS$))
(216 108 (:REWRITE DEFAULT-UNARY-MINUS))
(192 48 (:DEFINITION MEMBER-EQUAL))
(192 48 (:DEFINITION BINARY-APPEND))
(156 108 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
(132 44 (:REWRITE ADE::BV-IS-TRUE-LIST))
(96 96 (:TYPE-PRESCRIPTION BOOLEANP))
(96 32 (:REWRITE ADE::TR-OR-NOR-OF-V-THREEFIX-CANCELED-AUX))
(96 32 (:REWRITE ADE::F-BUF-OF-3VP))
(88 88 (:TYPE-PRESCRIPTION ADE::BVP))
(64 64 (:TYPE-PRESCRIPTION ADE::3VP))
(54 54 (:TYPE-PRESCRIPTION ADE::SIS))
(54 54 (:TYPE-PRESCRIPTION ADE::CONSP-SIS))
(32 32 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
(6 6 (:REWRITE NTH-WHEN-PREFIXP))
(4 4 (:TYPE-PRESCRIPTION ADE::F-BUF))
(2 2 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
)
(ADE::BTR-OR-NOR
(2 2 (:REWRITE DEFAULT-CAR))
(1 1 (:REWRITE DEFAULT-CDR))
)
(ADE::TR-OR-NOR=BTR-OR-NOR
(3666 101 (:DEFINITION TAKE))
(1932 1320 (:REWRITE DEFAULT-CAR))
(1831 311 (:DEFINITION LEN))
(1678 1202 (:REWRITE DEFAULT-CDR))
(1662 554 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
(1535 65 (:REWRITE ADE::TR-OR-NOR-OF-V-THREEFIX-CANCELED-AUX))
(1361 740 (:REWRITE DEFAULT-+-2))
(915 740 (:REWRITE DEFAULT-+-1))
(778 403 (:REWRITE DEFAULT-<-2))
(768 64 (:DEFINITION ADE::V-THREEFIX))
(685 403 (:REWRITE DEFAULT-<-1))
(665 287 (:REWRITE TAKE-WHEN-ATOM))
(628 128 (:REWRITE ADE::V-THREEFIX-BVP))
(567 567 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(554 554 (:TYPE-PRESCRIPTION TRUE-LISTP))
(542 542 (:LINEAR LEN-WHEN-PREFIXP))
(504 28 (:REWRITE ADE::LEN-NTHCDR))
(280 14 (:DEFINITION BINARY-APPEND))
(274 18 (:REWRITE REPEAT-WHEN-ZP))
(259 259 (:TYPE-PRESCRIPTION TAKE))
(242 242 (:TYPE-PRESCRIPTION ADE::3VP))
(210 14 (:REWRITE ZP-OPEN))
(200 100 (:DEFINITION ADE::3V-FIX))
(168 84 (:REWRITE CONSP-OF-TAKE))
(154 14 (:REWRITE SECOND-OF-TAKE))
(144 36 (:REWRITE ADE::CAR-V-THREEFIX))
(140 14 (:REWRITE ADE::TREE-SIZE-LEMMAS))
(111 37 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
(87 13 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
(84 28 (:REWRITE LEN-OF-TAKE))
(77 77 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
(39 13 (:REWRITE ADE::F-BUF-OF-3VP))
(28 14 (:REWRITE DEFAULT-UNARY-MINUS))
(14 14 (:TYPE-PRESCRIPTION ZP))
(2 1 (:REWRITE ADE::BOOLEANP-OF-F-BUF))
)
(ADE::BTR-OR-NOR-IS-V-ZP-NZP
(4797 236 (:REWRITE TAKE-OF-TOO-MANY))
(3219 89 (:DEFINITION TAKE))
(2432 24 (:REWRITE TAKE-OF-TAKE-SPLIT))
(1845 980 (:REWRITE DEFAULT-+-2))
(1751 1146 (:REWRITE DEFAULT-CAR))
(1726 1226 (:REWRITE DEFAULT-CDR))
(1582 137 (:DEFINITION NTHCDR))
(1394 58 (:REWRITE ADE::TR-OR-NOR-OF-V-THREEFIX-CANCELED-AUX))
(1346 980 (:REWRITE DEFAULT-+-1))
(956 28 (:REWRITE ADE::NTHCDR-OF-NTHCDR))
(712 143 (:REWRITE COMMUTATIVITY-OF-+))
(590 212 (:REWRITE TAKE-WHEN-ATOM))
(570 60 (:DEFINITION ADE::V-THREEFIX))
(508 120 (:REWRITE ADE::V-THREEFIX-BVP))
(478 274 (:REWRITE DEFAULT-<-1))
(451 274 (:REWRITE DEFAULT-<-2))
(320 320 (:LINEAR LEN-WHEN-PREFIXP))
(234 234 (:TYPE-PRESCRIPTION ADE::3VP))
(232 116 (:DEFINITION ADE::3V-FIX))
(228 12 (:REWRITE REPEAT-WHEN-ZP))
(228 12 (:DEFINITION BINARY-APPEND))
(224 56 (:REWRITE ADE::CAR-V-THREEFIX))
(194 34 (:REWRITE TAKE-OF-1))
(180 12 (:REWRITE ZP-OPEN))
(171 171 (:TYPE-PRESCRIPTION BOOLEANP))
(159 53 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
(144 48 (:DEFINITION ADE::B-NAND))
(120 12 (:REWRITE SECOND-OF-TAKE))
(108 24 (:REWRITE APPEND-WHEN-NOT-CONSP))
(92 46 (:REWRITE DEFAULT-UNARY-MINUS))
(60 60 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
(42 14 (:REWRITE UNICITY-OF-0))
(28 14 (:DEFINITION FIX))
(20 20 (:REWRITE ADE::NTHCDR-0))
(12 12 (:TYPE-PRESCRIPTION ZP))
(11 11 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
)
(ADE::TV-ZP*)
(ADE::TV-ZP*$DESTRUCTURE
(180 6 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
(98 10 (:REWRITE DEFAULT-CDR))
(60 24 (:REWRITE DEFAULT-+-2))
(57 5 (:REWRITE DEFAULT-CAR))
(48 24 (:REWRITE DEFAULT-*-2))
(48 24 (:REWRITE DEFAULT-*-1))
(42 24 (:REWRITE DEFAULT-+-1))
(36 12 (:REWRITE DEFAULT-UNARY-MINUS))
(30 6 (:REWRITE COMMUTATIVITY-OF-+))
(24 12 (:REWRITE DEFAULT-<-1))
(23 23 (:REWRITE ADE::TREE-SIZE-ATOM))
(18 12 (:REWRITE DEFAULT-<-2))
(16 1 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
(13 1 (:REWRITE DEFAULT-SYMBOL-NAME))
(12 6 (:REWRITE ADE::NFIX-OF-NAT))
(12 6 (:REWRITE DEFAULT-NUMERATOR))
(12 6 (:REWRITE DEFAULT-DENOMINATOR))
(12 6 (:DEFINITION IFIX))
(2 2 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
)
(ADE::NOT-PRIMP-TV-ZP)
(ADE::TV-ZP$NETLIST)
(ADE::TV-ZP&)
(ADE::F$TV-ZP)
(ADE::TV-ZP$VALUE
(150 5 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
(90 48 (:REWRITE DEFAULT-+-2))
(67 48 (:REWRITE DEFAULT-+-1))
(64 16 (:DEFINITION LEN))
(56 36 (:REWRITE DEFAULT-*-2))
(56 36 (:REWRITE DEFAULT-*-1))
(40 40 (:TYPE-PRESCRIPTION ADE::BVP))
(40 16 (:REWRITE ADE::TR-OR-NOR=BTR-OR-NOR))
(30 14 (:REWRITE DEFAULT-UNARY-MINUS))
(25 5 (:REWRITE COMMUTATIVITY-OF-+))
(24 8 (:REWRITE ADE::BV-IS-TRUE-LIST))
(20 10 (:REWRITE DEFAULT-<-1))
(20 5 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
(18 9 (:REWRITE DEFAULT-NUMERATOR))
(18 9 (:REWRITE DEFAULT-DENOMINATOR))
(16 4 (:DEFINITION TRUE-LISTP))
(15 10 (:REWRITE DEFAULT-<-2))
(14 14 (:REWRITE ADE::TREE-SIZE-ATOM))
(14 6 (:REWRITE ADE::ASSOC-EQ-VALUE-CONS-2))
(10 10 (:TYPE-PRESCRIPTION ADE::SIS))
(10 10 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
(10 10 (:TYPE-PRESCRIPTION ADE::CONSP-SIS))
(10 5 (:REWRITE ADE::NFIX-OF-NAT))
(10 5 (:DEFINITION IFIX))
(8 4 (:REWRITE PREFIXP-WHEN-PREFIXP))
(5 5 (:REWRITE DEFAULT-SYMBOL-NAME))
(4 4 (:REWRITE TAKE-WHEN-ATOM))
(4 4 (:REWRITE PREFIXP-TRANSITIVE . 2))
(4 4 (:REWRITE PREFIXP-TRANSITIVE . 1))
(4 4 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
(4 4 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
(4 4 (:REWRITE ADE::NTHCDR-OF-POS-CONST-IDX))
(2 2 (:LINEAR LEN-WHEN-PREFIXP))
)
(ADE::F$TV-ZP=V-ZP
(30 1 (:DEFINITION NONNEGATIVE-INTEGER-QUOTIENT))
(16 7 (:REWRITE DEFAULT-+-2))
(15 3 (:DEFINITION LEN))
(10 7 (:REWRITE DEFAULT-+-1))
(8 4 (:REWRITE DEFAULT-*-2))
(8 4 (:REWRITE DEFAULT-*-1))
(6 2 (:REWRITE DEFAULT-UNARY-MINUS))
(5 1 (:REWRITE COMMUTATIVITY-OF-+))
(4 4 (:REWRITE ADE::V-NZP-AS-OR-CROCK))
(4 2 (:REWRITE DEFAULT-<-1))
(3 3 (:REWRITE ADE::TREE-SIZE-ATOM))
(3 3 (:REWRITE ADE::NOT-V-NZP-TAKE-NTHCDR))
(3 3 (:REWRITE DEFAULT-CDR))
(3 2 (:REWRITE DEFAULT-<-2))
(2 2 (:REWRITE ADE::V-ZP-AS-AND-CROCK))
(2 2 (:REWRITE DEFAULT-CAR))
(2 2 (:LINEAR LEN-WHEN-PREFIXP))
(2 1 (:REWRITE ADE::NFIX-OF-NAT))
(2 1 (:REWRITE DEFAULT-NUMERATOR))
(2 1 (:REWRITE DEFAULT-DENOMINATOR))
(2 1 (:DEFINITION IFIX))
)
|
