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
|
(MAKE-BLOCKS
(20 1 (:REWRITE NFIX-WHEN-ZP))
(16 1 (:REWRITE ZP-OPEN))
(16 1 (:REWRITE NFIX-WHEN-NATP))
(15 3 (:DEFINITION LEN))
(12 1 (:DEFINITION NATP))
(9 5 (:REWRITE DEFAULT-<-1))
(9 5 (:REWRITE DEFAULT-+-2))
(8 5 (:REWRITE DEFAULT-<-2))
(6 5 (:REWRITE DEFAULT-+-1))
(3 3 (:REWRITE DEFAULT-CDR))
(2 2 (:LINEAR POSITION-WHEN-MEMBER))
(2 2 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(2 1 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
(1 1 (:TYPE-PRESCRIPTION ZP))
(1 1 (:TYPE-PRESCRIPTION TRUE-LISTP))
(1 1 (:TYPE-PRESCRIPTION NATP))
)
(MAKE-BLOCKS-CORRECTNESS-5
(306 18 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
(240 6 (:DEFINITION MAKE-CHARACTER-LIST))
(234 24 (:DEFINITION CHARACTER-LISTP))
(182 12 (:REWRITE TAKE-OF-LEN-FREE))
(156 6 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
(131 77 (:REWRITE DEFAULT-CDR))
(126 126 (:TYPE-PRESCRIPTION TRUE-LISTP-TAKE))
(120 120 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
(114 6 (:DEFINITION TAKE))
(108 12 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(90 54 (:REWRITE DEFAULT-CAR))
(84 6 (:DEFINITION TRUE-LISTP))
(84 3 (:DEFINITION NTHCDR))
(72 12 (:DEFINITION STRING-LISTP))
(70 14 (:DEFINITION LEN))
(60 60 (:TYPE-PRESCRIPTION STRING-LISTP))
(54 6 (:REWRITE CHARACTER-LISTP-OF-TAKE))
(42 42 (:REWRITE CONSP-OF-TAKE))
(33 33 (:TYPE-PRESCRIPTION TRUE-LISTP))
(28 14 (:REWRITE DEFAULT-+-2))
(21 21 (:LINEAR POSITION-WHEN-MEMBER))
(21 21 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(14 14 (:REWRITE DEFAULT-+-1))
(6 3 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
(2 1 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE DEFAULT-<-1))
)
(BLOCK-LISTP)
(MAKE-BLOCKS-CORRECTNESS-2
(135 9 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
(120 3 (:DEFINITION MAKE-CHARACTER-LIST))
(101 19 (:DEFINITION LEN))
(96 6 (:REWRITE TAKE-OF-LEN-FREE))
(85 46 (:REWRITE DEFAULT-CDR))
(64 4 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
(63 3 (:REWRITE CHARACTER-LISTP-OF-TAKE))
(61 29 (:REWRITE DEFAULT-CAR))
(57 3 (:DEFINITION TAKE))
(43 9 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
(39 39 (:TYPE-PRESCRIPTION TRUE-LISTP-TAKE))
(38 19 (:REWRITE DEFAULT-+-2))
(36 2 (:DEFINITION NTHCDR))
(31 3 (:REWRITE CONSP-OF-NTHCDR))
(21 21 (:LINEAR POSITION-WHEN-MEMBER))
(21 21 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(19 19 (:REWRITE DEFAULT-+-1))
(19 13 (:REWRITE DEFAULT-<-1))
(18 13 (:REWRITE DEFAULT-<-2))
(12 12 (:REWRITE CONSP-OF-TAKE))
(3 3 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
)
(BLOCK-LISTP-CORRECTNESS-1
(36 4 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(24 4 (:DEFINITION STRING-LISTP))
(22 2 (:DEFINITION TRUE-LISTP))
(20 20 (:TYPE-PRESCRIPTION STRING-LISTP))
(15 3 (:DEFINITION LEN))
(14 14 (:REWRITE DEFAULT-CDR))
(13 13 (:REWRITE DEFAULT-CAR))
(9 3 (:DEFINITION CHARACTER-LISTP))
(6 3 (:REWRITE DEFAULT-+-2))
(3 3 (:REWRITE DEFAULT-+-1))
)
(BLOCK-LISTP-CORRECTNESS-2
(234 117 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(205 128 (:REWRITE DEFAULT-CAR))
(175 113 (:REWRITE DEFAULT-CDR))
(117 117 (:TYPE-PRESCRIPTION BINARY-APPEND))
(100 14 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(64 32 (:REWRITE DEFAULT-+-2))
(63 14 (:DEFINITION STRING-LISTP))
(50 50 (:TYPE-PRESCRIPTION STRING-LISTP))
(32 32 (:REWRITE DEFAULT-+-1))
(24 24 (:REWRITE CONSP-OF-APPEND))
(3 3 (:LINEAR POSITION-WHEN-MEMBER))
(3 3 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
)
(FEASIBLE-FILE-LENGTH-P)
(UNMAKE-BLOCKS
(257 133 (:REWRITE DEFAULT-+-2))
(143 143 (:REWRITE DEFAULT-CDR))
(133 133 (:REWRITE DEFAULT-+-1))
(100 50 (:REWRITE DEFAULT-*-2))
(97 97 (:REWRITE DEFAULT-CAR))
(89 55 (:REWRITE DEFAULT-<-1))
(72 8 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(55 55 (:REWRITE DEFAULT-<-2))
(50 50 (:REWRITE DEFAULT-*-1))
(48 8 (:DEFINITION STRING-LISTP))
(44 4 (:DEFINITION TRUE-LISTP))
(40 40 (:TYPE-PRESCRIPTION STRING-LISTP))
(31 31 (:LINEAR POSITION-WHEN-MEMBER))
(31 31 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
)
(UNMAKE-BLOCKS-CORRECTNESS-1
(367 322 (:REWRITE DEFAULT-CDR))
(340 214 (:REWRITE DEFAULT-+-2))
(296 251 (:REWRITE DEFAULT-CAR))
(217 30 (:REWRITE TAKE-OF-LEN-FREE))
(214 214 (:REWRITE DEFAULT-+-1))
(114 83 (:REWRITE DEFAULT-<-1))
(90 30 (:DEFINITION BINARY-APPEND))
(90 10 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(84 43 (:REWRITE DEFAULT-*-2))
(83 83 (:REWRITE DEFAULT-<-2))
(75 40 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(70 5 (:DEFINITION TRUE-LISTP))
(62 62 (:LINEAR POSITION-WHEN-MEMBER))
(62 62 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(60 10 (:DEFINITION STRING-LISTP))
(50 50 (:TYPE-PRESCRIPTION STRING-LISTP))
(43 43 (:REWRITE DEFAULT-*-1))
(40 40 (:TYPE-PRESCRIPTION BINARY-APPEND))
(40 15 (:REWRITE CONSP-OF-APPEND))
(25 25 (:TYPE-PRESCRIPTION TRUE-LISTP))
(11 5 (:REWRITE ZP-OPEN))
(2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(1 1 (:REWRITE NFIX-WHEN-ZP))
)
(UNMAKE-BLOCKS-CORRECTNESS-2
(403 38 (:REWRITE TAKE-OF-LEN-FREE))
(324 182 (:REWRITE DEFAULT-+-2))
(259 259 (:REWRITE DEFAULT-CDR))
(187 187 (:REWRITE DEFAULT-CAR))
(182 182 (:REWRITE DEFAULT-+-1))
(111 37 (:DEFINITION BINARY-APPEND))
(87 87 (:LINEAR POSITION-WHEN-MEMBER))
(87 87 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(75 25 (:DEFINITION CHARACTER-LISTP))
(70 35 (:REWRITE DEFAULT-*-2))
(60 38 (:REWRITE DEFAULT-<-1))
(38 38 (:REWRITE DEFAULT-<-2))
(35 35 (:REWRITE DEFAULT-*-1))
(8 8 (:REWRITE ZP-OPEN))
(1 1 (:REWRITE NFIX-WHEN-ZP))
)
(UNMAKE-MAKE-BLOCKS-LEMMA-1
(32 20 (:REWRITE DEFAULT-+-2))
(20 20 (:REWRITE DEFAULT-+-1))
(15 15 (:REWRITE DEFAULT-CDR))
(13 9 (:REWRITE DEFAULT-<-2))
(10 5 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
(9 9 (:REWRITE DEFAULT-<-1))
(9 2 (:REWRITE NFIX-WHEN-ZP))
(7 2 (:REWRITE ZP-OPEN))
(5 5 (:TYPE-PRESCRIPTION TRUE-LISTP))
)
(UNMAKE-MAKE-BLOCKS
(634 12 (:DEFINITION TAKE))
(565 99 (:DEFINITION LEN))
(390 23 (:REWRITE TAKE-OF-LEN-FREE))
(290 170 (:REWRITE DEFAULT-CDR))
(237 133 (:REWRITE DEFAULT-+-2))
(200 5 (:DEFINITION MAKE-CHARACTER-LIST))
(191 14 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
(187 57 (:REWRITE DEFAULT-CAR))
(172 23 (:REWRITE NFIX-WHEN-ZP))
(166 111 (:REWRITE DEFAULT-<-2))
(151 16 (:REWRITE ZP-OPEN))
(138 133 (:REWRITE DEFAULT-+-1))
(127 111 (:REWRITE DEFAULT-<-1))
(126 7 (:DEFINITION NTHCDR))
(103 103 (:LINEAR POSITION-WHEN-MEMBER))
(103 103 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(86 25 (:REWRITE TAKE-WHEN-ATOM))
(46 8 (:DEFINITION BINARY-APPEND))
(39 5 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
(29 1 (:REWRITE NTHCDR-OF-NTHCDR))
(29 1 (:REWRITE CAR-OF-NTHCDR))
(26 2 (:REWRITE NTH-WHEN->=-N-LEN-L))
(23 23 (:REWRITE CONSP-OF-TAKE))
(18 1 (:DEFINITION NTH))
(13 2 (:DEFINITION NATP))
(12 12 (:TYPE-PRESCRIPTION ZP))
(9 3 (:REWRITE FOLD-CONSTS-IN-+))
(4 2 (:REWRITE LEN-OF-MAKE-CHARACTER-LIST))
(4 2 (:REWRITE DEFAULT-UNARY-MINUS))
(2 2 (:TYPE-PRESCRIPTION NATP))
(1 1 (:REWRITE CHARACTER-LISTP-OF-NTHCDR))
)
(MAKE-BLOCKS-CORRECTNESS-1
(166 12 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
(160 4 (:DEFINITION MAKE-CHARACTER-LIST))
(149 61 (:REWRITE DEFAULT-CDR))
(118 8 (:REWRITE TAKE-OF-LEN-FREE))
(109 57 (:REWRITE DEFAULT-+-2))
(82 12 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
(76 4 (:DEFINITION TAKE))
(70 4 (:REWRITE CHARACTER-LISTP-OF-TAKE))
(62 57 (:REWRITE DEFAULT-+-1))
(58 12 (:REWRITE UNMAKE-MAKE-BLOCKS-LEMMA-1))
(55 38 (:REWRITE DEFAULT-<-2))
(53 38 (:REWRITE DEFAULT-<-1))
(52 52 (:TYPE-PRESCRIPTION TRUE-LISTP-TAKE))
(40 2 (:REWRITE NFIX-WHEN-ZP))
(36 36 (:LINEAR POSITION-WHEN-MEMBER))
(36 36 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(36 24 (:REWRITE DEFAULT-CAR))
(32 2 (:REWRITE ZP-OPEN))
(32 2 (:REWRITE NFIX-WHEN-NATP))
(24 2 (:DEFINITION NATP))
(20 10 (:REWRITE DEFAULT-*-2))
(18 1 (:DEFINITION NTHCDR))
(16 16 (:REWRITE CONSP-OF-TAKE))
(12 12 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
(10 10 (:REWRITE DEFAULT-*-1))
(2 2 (:TYPE-PRESCRIPTION ZP))
(2 2 (:TYPE-PRESCRIPTION NATP))
)
(MAKE-BLOCKS-CORRECTNESS-3
(45 6 (:DEFINITION LEN))
(19 10 (:REWRITE DEFAULT-+-2))
(17 8 (:REWRITE DEFAULT-CDR))
(11 10 (:REWRITE DEFAULT-+-1))
(10 5 (:REWRITE DEFAULT-*-2))
(9 9 (:TYPE-PRESCRIPTION MAKE-BLOCKS))
(8 4 (:REWRITE DEFAULT-<-2))
(8 4 (:REWRITE DEFAULT-<-1))
(6 6 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
(5 5 (:REWRITE DEFAULT-*-1))
(2 2 (:REWRITE DEFAULT-CAR))
)
(NTHCDR-*BLOCKSIZE*-INDUCTION-2
(126 2 (:DEFINITION ACL2-COUNT))
(52 2 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
(36 4 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(31 1 (:REWRITE CAR-OF-NTHCDR))
(30 1 (:DEFINITION NTHCDR))
(29 15 (:REWRITE DEFAULT-CDR))
(29 14 (:REWRITE DEFAULT-+-2))
(28 2 (:REWRITE NTH-WHEN->=-N-LEN-L))
(28 2 (:DEFINITION TRUE-LISTP))
(25 5 (:DEFINITION LEN))
(24 4 (:DEFINITION STRING-LISTP))
(22 11 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
(21 21 (:TYPE-PRESCRIPTION TRUE-LISTP))
(20 20 (:TYPE-PRESCRIPTION STRING-LISTP))
(20 2 (:REWRITE UNMAKE-MAKE-BLOCKS-LEMMA-1))
(18 14 (:REWRITE DEFAULT-+-1))
(18 1 (:DEFINITION NTH))
(16 16 (:TYPE-PRESCRIPTION LEN))
(8 6 (:REWRITE DEFAULT-<-2))
(8 2 (:REWRITE COMMUTATIVITY-OF-+))
(8 2 (:DEFINITION INTEGER-ABS))
(8 1 (:REWRITE LENGTH-WHEN-STRINGP))
(6 6 (:REWRITE DEFAULT-<-1))
(5 5 (:REWRITE DEFAULT-CAR))
(3 3 (:REWRITE FOLD-CONSTS-IN-+))
(3 3 (:LINEAR POSITION-WHEN-MEMBER))
(3 3 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(2 2 (:TYPE-PRESCRIPTION NFIX))
(2 2 (:REWRITE NTHCDR-WHEN-ZP))
(2 2 (:REWRITE NTHCDR-WHEN-ATOM))
(2 2 (:REWRITE DEFAULT-UNARY-MINUS))
(1 1 (:REWRITE OPEN-SMALL-NTHCDR))
(1 1 (:REWRITE DEFAULT-REALPART))
(1 1 (:REWRITE DEFAULT-NUMERATOR))
(1 1 (:REWRITE DEFAULT-IMAGPART))
(1 1 (:REWRITE DEFAULT-DENOMINATOR))
(1 1 (:REWRITE DEFAULT-COERCE-2))
(1 1 (:REWRITE DEFAULT-COERCE-1))
)
(MAKE-BLOCKS-CORRECTNESS-4
(998 36 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
(836 54 (:DEFINITION CHARACTER-LISTP))
(832 32 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
(672 316 (:REWRITE DEFAULT-CDR))
(602 12 (:DEFINITION TAKE))
(576 64 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(554 24 (:REWRITE TAKE-OF-LEN-FREE))
(494 12 (:REWRITE CHARACTER-LISTP-OF-TAKE))
(480 16 (:DEFINITION NTHCDR))
(480 12 (:DEFINITION MAKE-CHARACTER-LIST))
(448 32 (:DEFINITION TRUE-LISTP))
(384 64 (:DEFINITION STRING-LISTP))
(360 6 (:REWRITE NTHCDR-OF-NTHCDR))
(352 12 (:REWRITE CAR-OF-NTHCDR))
(320 320 (:TYPE-PRESCRIPTION STRING-LISTP))
(316 24 (:REWRITE NTH-WHEN->=-N-LEN-L))
(296 38 (:REWRITE UNMAKE-MAKE-BLOCKS-LEMMA-1))
(288 288 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
(252 252 (:TYPE-PRESCRIPTION TRUE-LISTP-TAKE))
(234 234 (:TYPE-PRESCRIPTION TRUE-LISTP))
(216 12 (:DEFINITION NTH))
(214 142 (:REWRITE DEFAULT-CAR))
(202 108 (:REWRITE DEFAULT-+-2))
(148 74 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
(133 103 (:REWRITE DEFAULT-<-2))
(116 38 (:REWRITE NTHCDR-WHEN-ATOM))
(110 108 (:REWRITE DEFAULT-+-1))
(106 103 (:REWRITE DEFAULT-<-1))
(84 84 (:REWRITE CONSP-OF-TAKE))
(73 8 (:REWRITE NFIX-WHEN-ZP))
(72 12 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
(60 12 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
(56 7 (:REWRITE ZP-OPEN))
(54 6 (:REWRITE CHARACTER-LISTP-OF-NTHCDR))
(52 52 (:LINEAR POSITION-WHEN-MEMBER))
(52 52 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(51 8 (:REWRITE NFIX-WHEN-NATP))
(38 38 (:REWRITE NTHCDR-WHEN-ZP))
(34 7 (:DEFINITION NATP))
(24 6 (:REWRITE CHARACTERP-NTH))
(22 22 (:REWRITE OPEN-SMALL-NTHCDR))
(7 7 (:TYPE-PRESCRIPTION ZP))
(7 7 (:TYPE-PRESCRIPTION NATP))
)
(LEN-OF-MAKE-UNMAKE
(1199 564 (:REWRITE DEFAULT-CDR))
(1101 64 (:REWRITE TAKE-OF-LEN-FREE))
(982 58 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-2))
(757 422 (:REWRITE DEFAULT-+-2))
(640 16 (:DEFINITION MAKE-CHARACTER-LIST))
(497 318 (:REWRITE DEFAULT-CAR))
(486 19 (:DEFINITION NTHCDR))
(473 18 (:REWRITE CHARACTER-LISTP-OF-TAKE))
(472 56 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
(422 422 (:REWRITE DEFAULT-+-1))
(392 28 (:DEFINITION TRUE-LISTP))
(312 156 (:REWRITE DEFAULT-*-2))
(312 52 (:DEFINITION STRING-LISTP))
(260 260 (:TYPE-PRESCRIPTION STRING-LISTP))
(201 201 (:LINEAR POSITION-WHEN-MEMBER))
(201 201 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
(186 16 (:REWRITE MAKE-BLOCKS-CORRECTNESS-5 . 1))
(185 140 (:REWRITE DEFAULT-<-1))
(173 140 (:REWRITE DEFAULT-<-2))
(156 156 (:REWRITE DEFAULT-*-1))
(144 144 (:TYPE-PRESCRIPTION TRUE-LISTP))
(128 14 (:REWRITE UNMAKE-BLOCKS-CORRECTNESS-1))
(84 4 (:REWRITE LEN-OF-APPEND))
(37 16 (:REWRITE ZP-OPEN))
(25 25 (:TYPE-PRESCRIPTION NATP))
(14 2 (:REWRITE TAKE-FEWER-OF-TAKE-MORE))
(9 9 (:REWRITE NFIX-WHEN-ZP))
(8 8 (:REWRITE MAKE-BLOCKS-CORRECTNESS-4))
(8 4 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
)
|
