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
|
(ADE::ALT-BRANCH$DATA-INS-LEN
(1 1 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE DEFAULT-<-1))
)
(ADE::ALT-BRANCH$INS-LEN)
(ADE::ALT-BRANCH*
(12 12 (:TYPE-PRESCRIPTION POSP))
)
(ADE::ALT-BRANCH*$DESTRUCTURE
(66 12 (:REWRITE APPEND-WHEN-NOT-CONSP))
(60 60 (:TYPE-PRESCRIPTION POSP))
(60 6 (:DEFINITION BINARY-APPEND))
(16 16 (:REWRITE DEFAULT-CDR))
(11 11 (:REWRITE DEFAULT-CAR))
)
(ADE::NOT-PRIMP-ALT-BRANCH)
(ADE::ALT-BRANCH$NETLIST)
(ADE::ALT-BRANCH&)
(ADE::CHECK-ALT-BRANCH$NETLIST-64)
(ADE::ALT-BRANCH$VALID-ST)
(ADE::ALT-BRANCH$DATA-IN
(6 2 (:REWRITE ADE::BV-IS-TRUE-LIST))
(5 1 (:DEFINITION TRUE-LISTP))
(4 4 (:TYPE-PRESCRIPTION ADE::BVP))
(1 1 (:REWRITE DEFAULT-CDR))
(1 1 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE DEFAULT-<-1))
)
(ADE::LEN-ALT-BRANCH$DATA-IN)
(ADE::ALT-BRANCH$ACT0
(10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
(5 5 (:TYPE-PRESCRIPTION BOOLEANP))
)
(ADE::ALT-BRANCH$ACT0-INACTIVE
(25 8 (:REWRITE ADE::F-GATES=B-GATES))
(20 2 (:DEFINITION NTHCDR))
(19 19 (:REWRITE NTH-WHEN-PREFIXP))
(14 14 (:TYPE-PRESCRIPTION BOOLEANP))
(12 2 (:REWRITE COMMUTATIVITY-OF-+))
(10 2 (:REWRITE ADE::NFIX-OF-NAT))
(8 8 (:REWRITE DEFAULT-+-2))
(8 8 (:REWRITE DEFAULT-+-1))
(6 6 (:REWRITE DEFAULT-CAR))
(6 2 (:REWRITE FOLD-CONSTS-IN-+))
(6 2 (:DEFINITION NATP))
(4 4 (:REWRITE DEFAULT-<-2))
(4 4 (:REWRITE DEFAULT-<-1))
(3 3 (:TYPE-PRESCRIPTION ADE::F-OR))
(2 2 (:TYPE-PRESCRIPTION NATP))
(2 2 (:REWRITE DEFAULT-CDR))
)
(ADE::ALT-BRANCH$ACT1
(10 5 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
(5 5 (:TYPE-PRESCRIPTION BOOLEANP))
)
(ADE::ALT-BRANCH$ACT1-INACTIVE
(31 10 (:REWRITE ADE::F-GATES=B-GATES))
(20 2 (:DEFINITION NTHCDR))
(19 19 (:REWRITE NTH-WHEN-PREFIXP))
(18 18 (:TYPE-PRESCRIPTION BOOLEANP))
(12 2 (:REWRITE COMMUTATIVITY-OF-+))
(10 2 (:REWRITE ADE::NFIX-OF-NAT))
(8 8 (:REWRITE DEFAULT-+-2))
(8 8 (:REWRITE DEFAULT-+-1))
(6 6 (:REWRITE DEFAULT-CAR))
(6 2 (:REWRITE FOLD-CONSTS-IN-+))
(6 2 (:DEFINITION NATP))
(4 4 (:REWRITE DEFAULT-<-2))
(4 4 (:REWRITE DEFAULT-<-1))
(3 3 (:TYPE-PRESCRIPTION ADE::F-OR))
(2 2 (:TYPE-PRESCRIPTION NATP))
(2 2 (:REWRITE DEFAULT-CDR))
)
(ADE::ALT-BRANCH$ACT)
(ADE::ALT-BRANCH$ACT-INACTIVE
(4 4 (:REWRITE NTH-WHEN-PREFIXP))
)
(ADE::ALT-BRANCH$VALUE
(316 158 (:REWRITE DEFAULT-+-2))
(308 2 (:REWRITE ADE::ASSOC-EQ-VALUES-APPEND-PAIRLIS$-WHEN-DISJOINT))
(162 158 (:REWRITE DEFAULT-+-1))
(138 30 (:DEFINITION BINARY-APPEND))
(128 8 (:REWRITE ADE::DISJOINT-ATOM))
(82 8 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
(81 81 (:REWRITE NTH-WHEN-PREFIXP))
(76 60 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
(76 60 (:REWRITE ADE::F-BUF-OF-3VP))
(72 8 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
(72 8 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
(60 4 (:DEFINITION ATOM))
(50 50 (:TYPE-PRESCRIPTION PAIRLIS$))
(45 17 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
(40 2 (:REWRITE ADE::ALT-BRANCH$ACT1-INACTIVE))
(34 2 (:REWRITE ADE::ALT-BRANCH$ACT0-INACTIVE))
(28 28 (:LINEAR LEN-WHEN-PREFIXP))
(27 1 (:REWRITE ADE::ALT-BRANCH$ACT-INACTIVE))
(22 22 (:TYPE-PRESCRIPTION ADE::3VP))
(20 20 (:TYPE-PRESCRIPTION BOOLEANP))
(18 18 (:TYPE-PRESCRIPTION ADE::DISJOINT))
(18 6 (:REWRITE ADE::CAR-V-THREEFIX))
(16 8 (:REWRITE DEFAULT-<-2))
(14 14 (:TYPE-PRESCRIPTION ADE::BVP))
(14 14 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(14 8 (:REWRITE ADE::V-THREEFIX-BVP))
(12 6 (:DEFINITION ADE::3V-FIX))
(12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
(8 8 (:REWRITE ADE::DISJOINT-SIS-DIFF-SYMS))
(8 8 (:REWRITE DEFAULT-<-1))
(8 4 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
(8 4 (:REWRITE DEFAULT-UNARY-MINUS))
(8 2 (:DEFINITION TRUE-LISTP))
(6 6 (:REWRITE ADE::NTHCDR-OF-POS-CONST-IDX))
(4 2 (:REWRITE PREFIXP-WHEN-PREFIXP))
(3 3 (:TYPE-PRESCRIPTION ADE::F-BUF))
(2 2 (:REWRITE TAKE-WHEN-ATOM))
(2 2 (:REWRITE PREFIXP-TRANSITIVE . 2))
(2 2 (:REWRITE PREFIXP-TRANSITIVE . 1))
(2 2 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
(2 2 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
(2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
)
(ADE::ALT-BRANCH$STEP
(12 6 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
(6 6 (:TYPE-PRESCRIPTION BOOLEANP))
)
(ADE::ALT-BRANCH$STATE
(562 281 (:REWRITE DEFAULT-+-2))
(284 281 (:REWRITE DEFAULT-+-1))
(238 54 (:DEFINITION BINARY-APPEND))
(201 177 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
(201 177 (:REWRITE ADE::F-BUF-OF-3VP))
(128 8 (:REWRITE ADE::DISJOINT-ATOM))
(118 118 (:TYPE-PRESCRIPTION ADE::UPDATE-ALIST))
(108 108 (:TYPE-PRESCRIPTION PAIRLIS$))
(106 19 (:REWRITE ADE::ASSOC-EQ-VALUES-OF-SIS-PAIRLIS$-SIS))
(100 100 (:REWRITE NTH-WHEN-PREFIXP))
(92 50 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
(82 19 (:REWRITE ADE::ASSOC-EQ-VALUES-ARGS-PAIRLIS$-ARGS))
(82 8 (:REWRITE ADE::DISJOINT-COMMUTATIVE))
(72 8 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
(72 8 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
(60 30 (:TYPE-PRESCRIPTION ADE::BOOLEANP-JOINT-ACT))
(60 4 (:DEFINITION ATOM))
(54 54 (:TYPE-PRESCRIPTION BOOLEANP))
(54 18 (:REWRITE ADE::CAR-V-THREEFIX))
(46 7 (:DEFINITION TRUE-LISTP))
(42 42 (:TYPE-PRESCRIPTION ADE::3VP))
(36 18 (:DEFINITION ADE::3V-FIX))
(36 14 (:REWRITE ADE::BV-IS-TRUE-LIST))
(30 30 (:LINEAR LEN-WHEN-PREFIXP))
(29 29 (:TYPE-PRESCRIPTION ADE::F-BUF))
(28 28 (:TYPE-PRESCRIPTION ADE::BVP))
(27 1 (:REWRITE ADE::ALT-BRANCH$ACT-INACTIVE))
(24 18 (:REWRITE ADE::V-THREEFIX-BVP))
(20 1 (:REWRITE ADE::ALT-BRANCH$ACT1-INACTIVE))
(17 1 (:REWRITE ADE::ALT-BRANCH$ACT0-INACTIVE))
(16 8 (:REWRITE DEFAULT-<-2))
(15 15 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(8 8 (:REWRITE DEFAULT-<-1))
(6 3 (:REWRITE DEFAULT-UNARY-MINUS))
(3 3 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
(3 3 (:REWRITE ADE::NTHCDR-OF-POS-CONST-IDX))
(3 3 (:REWRITE ADE::NO-DUPLICATESP-SIS))
(2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
(2 1 (:REWRITE ADE::ASSOC-EQ-VALUES-UPDATE-ALIST-NOT-MEMBER))
(1 1 (:REWRITE ADE::ASSOC-EQ-VALUE-DE-OCC-UPDATE-ALIST-DIFF-NAMES))
)
(ADE::ALT-BRANCH$INPUT-FORMAT)
(ADE::BOOLEANP-ALT-BRANCH$ACT0
(453 453 (:REWRITE NTH-WHEN-PREFIXP))
(362 88 (:REWRITE ADE::BV-IS-TRUE-LIST))
(290 61 (:DEFINITION NTHCDR))
(290 58 (:DEFINITION LEN))
(276 44 (:DEFINITION TRUE-LISTP))
(216 14 (:REWRITE ADE::LEN-NTHCDR))
(200 142 (:REWRITE DEFAULT-+-2))
(177 177 (:REWRITE DEFAULT-CDR))
(142 142 (:REWRITE DEFAULT-+-1))
(126 21 (:REWRITE COMMUTATIVITY-OF-+))
(84 14 (:DEFINITION BINARY-APPEND))
(72 12 (:REWRITE ADE::ALT-BRANCH$ACT0-INACTIVE))
(70 28 (:REWRITE APPEND-WHEN-NOT-CONSP))
(63 21 (:REWRITE FOLD-CONSTS-IN-+))
(62 62 (:REWRITE DEFAULT-CAR))
(56 28 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
(48 48 (:LINEAR LEN-WHEN-PREFIXP))
(42 14 (:REWRITE ADE::BVP-NTHCDR))
(40 24 (:REWRITE DEFAULT-<-1))
(24 24 (:REWRITE DEFAULT-<-2))
(24 24 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(18 6 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
(18 6 (:REWRITE ADE::F-BUF-OF-3VP))
(18 6 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
(12 12 (:TYPE-PRESCRIPTION ADE::3VP))
(3 1 (:DEFINITION NATP))
(2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(1 1 (:TYPE-PRESCRIPTION NATP))
)
(ADE::BOOLEANP-ALT-BRANCH$ACT1
(747 747 (:REWRITE NTH-WHEN-PREFIXP))
(662 160 (:REWRITE ADE::BV-IS-TRUE-LIST))
(530 106 (:DEFINITION LEN))
(514 109 (:DEFINITION NTHCDR))
(504 80 (:DEFINITION TRUE-LISTP))
(408 26 (:REWRITE ADE::LEN-NTHCDR))
(360 254 (:REWRITE DEFAULT-+-2))
(321 321 (:REWRITE DEFAULT-CDR))
(254 254 (:REWRITE DEFAULT-+-1))
(222 37 (:REWRITE COMMUTATIVITY-OF-+))
(156 26 (:DEFINITION BINARY-APPEND))
(130 52 (:REWRITE APPEND-WHEN-NOT-CONSP))
(111 37 (:REWRITE FOLD-CONSTS-IN-+))
(104 104 (:REWRITE DEFAULT-CAR))
(104 52 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
(96 96 (:LINEAR LEN-WHEN-PREFIXP))
(78 26 (:REWRITE ADE::BVP-NTHCDR))
(72 12 (:REWRITE ADE::ALT-BRANCH$ACT1-INACTIVE))
(70 40 (:REWRITE DEFAULT-<-1))
(48 48 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(40 40 (:REWRITE DEFAULT-<-2))
(18 6 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
(18 6 (:REWRITE ADE::F-BUF-OF-3VP))
(12 12 (:TYPE-PRESCRIPTION ADE::3VP))
(4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(3 1 (:DEFINITION NATP))
(1 1 (:TYPE-PRESCRIPTION NATP))
)
(ADE::BOOLEANP-ALT-BRANCH$ACT
(13 13 (:REWRITE NTH-WHEN-PREFIXP))
(7 1 (:REWRITE ADE::ALT-BRANCH$ACT-INACTIVE))
(6 1 (:REWRITE ADE::ALT-BRANCH$ACT1-INACTIVE))
(6 1 (:REWRITE ADE::ALT-BRANCH$ACT0-INACTIVE))
)
(ADE::ALT-BRANCH$VALID-ST-PRESERVED
(2610 2610 (:REWRITE NTH-WHEN-PREFIXP))
(1410 301 (:DEFINITION NTHCDR))
(1262 304 (:REWRITE ADE::BV-IS-TRUE-LIST))
(960 152 (:DEFINITION TRUE-LISTP))
(808 606 (:REWRITE DEFAULT-+-2))
(792 50 (:REWRITE ADE::LEN-NTHCDR))
(759 759 (:REWRITE DEFAULT-CDR))
(606 606 (:REWRITE DEFAULT-+-1))
(606 101 (:REWRITE COMMUTATIVITY-OF-+))
(407 407 (:REWRITE DEFAULT-CAR))
(303 101 (:REWRITE FOLD-CONSTS-IN-+))
(300 50 (:DEFINITION BINARY-APPEND))
(250 100 (:REWRITE APPEND-WHEN-NOT-CONSP))
(240 240 (:LINEAR LEN-WHEN-PREFIXP))
(200 100 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
(150 50 (:REWRITE ADE::BVP-NTHCDR))
(144 84 (:REWRITE DEFAULT-<-1))
(120 120 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(108 36 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
(108 36 (:REWRITE ADE::F-BUF-OF-3VP))
(84 84 (:REWRITE DEFAULT-<-2))
(84 12 (:REWRITE ADE::ALT-BRANCH$ACT-INACTIVE))
(72 72 (:TYPE-PRESCRIPTION ADE::3VP))
(72 12 (:REWRITE ADE::ALT-BRANCH$ACT1-INACTIVE))
(72 12 (:REWRITE ADE::ALT-BRANCH$ACT0-INACTIVE))
(18 18 (:TYPE-PRESCRIPTION ADE::F-OR3))
(18 18 (:TYPE-PRESCRIPTION ADE::F-NOT))
(10 10 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(3 1 (:DEFINITION NATP))
(1 1 (:TYPE-PRESCRIPTION NATP))
)
(ADE::ALT-BRANCH$INV)
(ADE::ALT-BRANCH$INV-PRESERVED
(1671 1671 (:REWRITE NTH-WHEN-PREFIXP))
(1046 223 (:DEFINITION NTHCDR))
(962 232 (:REWRITE ADE::BV-IS-TRUE-LIST))
(770 154 (:DEFINITION LEN))
(732 116 (:DEFINITION TRUE-LISTP))
(608 454 (:REWRITE DEFAULT-+-2))
(600 38 (:REWRITE ADE::LEN-NTHCDR))
(531 531 (:REWRITE DEFAULT-CDR))
(454 454 (:REWRITE DEFAULT-+-1))
(450 75 (:REWRITE COMMUTATIVITY-OF-+))
(239 239 (:REWRITE DEFAULT-CAR))
(228 38 (:DEFINITION BINARY-APPEND))
(225 75 (:REWRITE FOLD-CONSTS-IN-+))
(192 192 (:LINEAR LEN-WHEN-PREFIXP))
(190 76 (:REWRITE APPEND-WHEN-NOT-CONSP))
(152 76 (:TYPE-PRESCRIPTION ADE::BVP-NTHCDR))
(114 38 (:REWRITE ADE::BVP-NTHCDR))
(108 62 (:REWRITE DEFAULT-<-1))
(96 96 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(72 24 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
(72 24 (:REWRITE ADE::F-BUF-OF-3VP))
(62 62 (:REWRITE DEFAULT-<-2))
(48 48 (:TYPE-PRESCRIPTION ADE::3VP))
(42 6 (:REWRITE ADE::ALT-BRANCH$ACT-INACTIVE))
(36 6 (:REWRITE ADE::ALT-BRANCH$ACT1-INACTIVE))
(36 6 (:REWRITE ADE::ALT-BRANCH$ACT0-INACTIVE))
(9 9 (:TYPE-PRESCRIPTION ADE::F-OR3))
(9 9 (:TYPE-PRESCRIPTION ADE::F-NOT))
(8 8 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(3 1 (:DEFINITION NATP))
(1 1 (:TYPE-PRESCRIPTION NATP))
)
|
