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
|
(SET-INDICES
(115 12 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(80 13 (:DEFINITION STRING-LISTP))
(62 62 (:TYPE-PRESCRIPTION STRING-LISTP))
(43 43 (:REWRITE DEFAULT-CDR))
(32 16 (:REWRITE DEFAULT-+-2))
(21 21 (:REWRITE DEFAULT-CAR))
(16 16 (:REWRITE DEFAULT-+-1))
(11 11 (:LINEAR POSITION-WHEN-MEMBER))
(11 11 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(8 8 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
(4 4 (:REWRITE DEFAULT-<-2))
(4 4 (:REWRITE DEFAULT-<-1))
)
(SET-INDICES-CORRECTNESS-1
(513 21 (:REWRITE NTH-WHEN->=-N-LEN-L))
(136 20 (:DEFINITION LEN))
(118 23 (:REWRITE NFIX-WHEN-ZP))
(94 30 (:REWRITE ZP-OPEN))
(84 63 (:REWRITE DEFAULT-<-2))
(67 47 (:REWRITE DEFAULT-CDR))
(64 63 (:REWRITE DEFAULT-<-1))
(54 34 (:REWRITE DEFAULT-+-2))
(50 1 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
(49 37 (:REWRITE DEFAULT-CAR))
(46 23 (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH))
(34 34 (:REWRITE DEFAULT-+-1))
(32 10 (:REWRITE SUBSETP-MEMBER . 1))
(31 1 (:REWRITE LEN-UPDATE-NTH))
(30 3 (:DEFINITION UPDATE-NTH))
(23 23 (:TYPE-PRESCRIPTION ZP))
(23 23 (:TYPE-PRESCRIPTION TRUE-LISTP))
(20 1 (:DEFINITION SUBSETP-EQUAL))
(19 19 (:LINEAR POSITION-WHEN-MEMBER))
(19 19 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(15 15 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
(10 10 (:REWRITE SUBSETP-MEMBER . 2))
(8 8 (:REWRITE SUBSETP-MEMBER . 4))
(8 8 (:REWRITE SUBSETP-MEMBER . 3))
(8 4 (:TYPE-PRESCRIPTION MAX))
(7 1 (:DEFINITION MAX))
(5 5 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(2 2 (:REWRITE SUBSETP-TRANS2))
(2 2 (:REWRITE SUBSETP-TRANS))
(1 1 (:TYPE-PRESCRIPTION NATP))
)
(SET-INDICES-CORRECTNESS-2
(2266 81 (:REWRITE NTH-WHEN->=-N-LEN-L))
(930 120 (:REWRITE NFIX-WHEN-ZP))
(813 32 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
(382 40 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(369 273 (:REWRITE DEFAULT-<-2))
(338 273 (:REWRITE DEFAULT-<-1))
(318 180 (:REWRITE DEFAULT-+-2))
(291 270 (:REWRITE DEFAULT-CDR))
(267 44 (:DEFINITION STRING-LISTP))
(204 204 (:TYPE-PRESCRIPTION STRING-LISTP))
(180 180 (:REWRITE DEFAULT-+-1))
(169 157 (:REWRITE DEFAULT-CAR))
(156 4 (:REWRITE MEMBER-OF-NTH-WHEN-NOT-INTERSECTP))
(93 19 (:DEFINITION MEMBER-EQUAL))
(86 86 (:LINEAR POSITION-WHEN-MEMBER))
(86 86 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(73 11 (:DEFINITION NFIX))
(68 4 (:REWRITE INTERSECTP-WHEN-SUBSETP))
(60 6 (:DEFINITION UPDATE-NTH))
(51 24 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(48 4 (:DEFINITION SUBSETP-EQUAL))
(39 4 (:REWRITE MEMBER-EQUAL-NTH))
(39 2 (:DEFINITION INTEGER-LISTP))
(32 4 (:DEFINITION INTERSECTP-EQUAL))
(30 30 (:REWRITE SUBSETP-MEMBER . 2))
(30 30 (:REWRITE SUBSETP-MEMBER . 1))
(26 26 (:TYPE-PRESCRIPTION NATP))
(26 26 (:REWRITE SUBSETP-MEMBER . 4))
(26 26 (:REWRITE SUBSETP-MEMBER . 3))
(21 21 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
(20 20 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(17 1 (:REWRITE LEN-UPDATE-NTH))
(8 8 (:REWRITE SUBSETP-TRANS2))
(8 8 (:REWRITE SUBSETP-TRANS))
(7 1 (:DEFINITION MAX))
(4 4 (:TYPE-PRESCRIPTION INTERSECTP-EQUAL))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 12))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 11))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 10))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 9))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 8))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 7))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 6))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 5))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 4))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 3))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 2))
(4 4 (:REWRITE INTERSECT-WITH-SUBSET . 1))
)
(SET-INDICES-CORRECTNESS-3
(87 65 (:REWRITE DEFAULT-CDR))
(79 44 (:REWRITE DEFAULT-+-2))
(56 46 (:REWRITE DEFAULT-<-2))
(51 48 (:REWRITE DEFAULT-CAR))
(49 4 (:DEFINITION UPDATE-NTH))
(48 46 (:REWRITE DEFAULT-<-1))
(44 44 (:REWRITE DEFAULT-+-1))
(40 8 (:REWRITE ZP-OPEN))
(32 4 (:REWRITE NFIX-WHEN-ZP))
(30 10 (:DEFINITION NATP))
(28 1 (:REWRITE UPDATE-NTH-OF-UPDATE-NTH-1))
(22 11 (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH))
(21 21 (:LINEAR POSITION-WHEN-MEMBER))
(21 21 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(16 4 (:REWRITE NFIX-WHEN-NATP))
(11 11 (:TYPE-PRESCRIPTION TRUE-LISTP))
(4 4 (:TYPE-PRESCRIPTION ZP))
(3 3 (:TYPE-PRESCRIPTION NATP))
)
(SET-INDICES-CORRECTNESS-4
(90 72 (:REWRITE DEFAULT-CAR))
(70 52 (:REWRITE DEFAULT-CDR))
(37 21 (:REWRITE DEFAULT-+-2))
(30 3 (:DEFINITION UPDATE-NTH))
(21 21 (:REWRITE DEFAULT-+-1))
(19 19 (:LINEAR POSITION-WHEN-MEMBER))
(19 19 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(14 14 (:REWRITE DEFAULT-<-2))
(14 14 (:REWRITE DEFAULT-<-1))
(12 3 (:REWRITE ZP-OPEN))
(10 10 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
(4 4 (:TYPE-PRESCRIPTION TRUE-LISTP))
)
(SET-INDICES-IN-ALV
(20 1 (:REWRITE NFIX-WHEN-ZP))
(16 1 (:REWRITE ZP-OPEN))
(10 2 (:DEFINITION LEN))
(7 4 (:REWRITE DEFAULT-+-2))
(7 1 (:DEFINITION NAT-LISTP))
(5 5 (:REWRITE DEFAULT-CDR))
(5 4 (:REWRITE DEFAULT-+-1))
(5 3 (:REWRITE DEFAULT-<-2))
(5 1 (:DEFINITION BOOLEAN-LISTP))
(3 3 (:REWRITE DEFAULT-CAR))
(3 3 (:REWRITE DEFAULT-<-1))
(3 1 (:DEFINITION NATP))
(2 2 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
(2 2 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
(2 2 (:LINEAR POSITION-WHEN-MEMBER))
(2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(1 1 (:TYPE-PRESCRIPTION ZP))
)
(SET-INDICES-IN-ALV-CORRECTNESS-1
(318 15 (:REWRITE SET-INDICES-CORRECTNESS-4))
(255 159 (:REWRITE DEFAULT-CDR))
(231 21 (:DEFINITION UPDATE-NTH))
(206 122 (:REWRITE DEFAULT-CAR))
(194 17 (:DEFINITION NAT-LISTP))
(167 127 (:REWRITE DEFAULT-<-2))
(163 5 (:REWRITE UPDATE-NTH-OF-UPDATE-NTH-1))
(138 109 (:REWRITE DEFAULT-+-2))
(127 127 (:REWRITE DEFAULT-<-1))
(111 109 (:REWRITE DEFAULT-+-1))
(81 27 (:DEFINITION NATP))
(73 73 (:TYPE-PRESCRIPTION NAT-LISTP))
(68 10 (:REWRITE NFIX-WHEN-ZP))
(50 10 (:REWRITE NFIX-WHEN-NATP))
(44 2 (:REWRITE BOOLEANP-OF-CAR-MAKE-LIST))
(34 34 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
(30 10 (:DEFINITION NFIX))
(19 19 (:TYPE-PRESCRIPTION TRUE-LISTP))
(14 2 (:REWRITE COMMUTATIVITY-OF-+))
(13 13 (:TYPE-PRESCRIPTION ZP))
(10 10 (:TYPE-PRESCRIPTION NFIX))
(10 10 (:TYPE-PRESCRIPTION NATP))
(5 5 (:LINEAR POSITION-WHEN-MEMBER))
(5 5 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(2 1 (:TYPE-PRESCRIPTION SET-INDICES-IN-ALV-CORRECTNESS-1))
)
(SET-INDICES-IN-ALV-CORRECTNESS-2
(49 1 (:DEFINITION SET-INDICES))
(32 5 (:REWRITE ZP-OPEN))
(24 2 (:DEFINITION MAKE-LIST-AC))
(24 1 (:REWRITE CDR-OF-MAKE-LIST))
(20 4 (:DEFINITION LEN))
(13 9 (:REWRITE DEFAULT-+-2))
(13 1 (:DEFINITION BOUNDED-NAT-LISTP))
(12 1 (:REWRITE CAR-OF-MAKE-LIST))
(11 7 (:REWRITE DEFAULT-<-2))
(10 10 (:REWRITE DEFAULT-CDR))
(10 1 (:DEFINITION UPDATE-NTH))
(9 9 (:REWRITE DEFAULT-+-1))
(7 7 (:REWRITE DEFAULT-<-1))
(6 6 (:REWRITE DEFAULT-CAR))
(5 1 (:DEFINITION BOOLEAN-LISTP))
(3 3 (:LINEAR POSITION-WHEN-MEMBER))
(3 3 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(3 1 (:REWRITE FOLD-CONSTS-IN-+))
(3 1 (:DEFINITION NATP))
)
(SET-INDICES-IN-ALV-CORRECTNESS-3
(3258 69 (:REWRITE NTH-WHEN->=-N-LEN-L))
(1408 34 (:DEFINITION NTH))
(1351 34 (:REWRITE SET-INDICES-CORRECTNESS-3))
(1015 307 (:TYPE-PRESCRIPTION SET-INDICES))
(901 48 (:DEFINITION BOUNDED-NAT-LISTP))
(862 604 (:REWRITE DEFAULT-CDR))
(798 576 (:REWRITE DEFAULT-<-2))
(736 14 (:LINEAR NATP-OF-NTH-WHEN-NAT-LISTP))
(678 462 (:REWRITE DEFAULT-+-2))
(664 110 (:REWRITE NFIX-WHEN-ZP))
(637 460 (:REWRITE DEFAULT-CAR))
(587 576 (:REWRITE DEFAULT-<-1))
(513 267 (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH))
(500 47 (:DEFINITION UPDATE-NTH))
(462 462 (:REWRITE DEFAULT-+-1))
(280 11 (:REWRITE UPDATE-NTH-OF-UPDATE-NTH-1))
(267 267 (:TYPE-PRESCRIPTION UPDATE-NTH))
(218 82 (:REWRITE SUBSETP-MEMBER . 1))
(217 13 (:DEFINITION SUBSETP-EQUAL))
(198 198 (:TYPE-PRESCRIPTION BOUNDED-NAT-LISTP))
(182 100 (:TYPE-PRESCRIPTION TRUE-LISTP-OF-MAKE-LIST-AC))
(171 58 (:REWRITE SUBSETP-MEMBER . 3))
(131 131 (:TYPE-PRESCRIPTION ZP))
(115 23 (:DEFINITION BOOLEAN-LISTP))
(100 100 (:TYPE-PRESCRIPTION MAKE-LIST-AC))
(84 84 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
(82 82 (:REWRITE SUBSETP-MEMBER . 2))
(58 58 (:REWRITE SUBSETP-MEMBER . 4))
(46 46 (:TYPE-PRESCRIPTION SUBSETP-EQUAL))
(30 7 (:DEFINITION POSITION-EQUAL-AC))
(22 22 (:REWRITE SUBSETP-TRANS2))
(22 22 (:REWRITE SUBSETP-TRANS))
(17 17 (:TYPE-PRESCRIPTION NATP))
(2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER-OF-TAKE))
)
(SET-INDICES-IN-ALV-CORRECTNESS-4
(66 4 (:REWRITE NTH-WHEN->=-N-LEN-L))
(62 2 (:DEFINITION NTH))
(49 1 (:DEFINITION SET-INDICES))
(47 10 (:REWRITE ZP-OPEN))
(25 5 (:DEFINITION LEN))
(24 2 (:DEFINITION MAKE-LIST-AC))
(24 1 (:REWRITE CDR-OF-MAKE-LIST))
(21 15 (:REWRITE DEFAULT-<-2))
(20 3 (:REWRITE NFIX-WHEN-ZP))
(17 12 (:REWRITE DEFAULT-+-2))
(15 15 (:REWRITE DEFAULT-<-1))
(14 14 (:REWRITE DEFAULT-CDR))
(12 12 (:REWRITE DEFAULT-+-1))
(12 1 (:REWRITE CAR-OF-MAKE-LIST))
(10 1 (:DEFINITION UPDATE-NTH))
(8 8 (:REWRITE DEFAULT-CAR))
(7 1 (:DEFINITION NAT-LISTP))
(7 1 (:DEFINITION MEMBER-EQUAL))
(5 1 (:DEFINITION BOOLEAN-LISTP))
(4 4 (:TYPE-PRESCRIPTION ZP))
(3 3 (:REWRITE NFIX-WHEN-NATP))
(3 3 (:LINEAR POSITION-WHEN-MEMBER))
(3 3 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(3 1 (:REWRITE FOLD-CONSTS-IN-+))
(2 2 (:REWRITE SUBSETP-MEMBER . 4))
(2 2 (:REWRITE SUBSETP-MEMBER . 3))
(2 2 (:REWRITE SUBSETP-MEMBER . 2))
(2 2 (:REWRITE SUBSETP-MEMBER . 1))
(2 2 (:REWRITE BOUNDED-NAT-LISTP-CORRECTNESS-1))
)
|
