tests/gold/problem_set_1_answers.sml

8 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PUSH") (mkpair (
9 mkpair (mksym "M1" "X") (mkpair (mksym "M1" "Y") (mksym "COMMON-LISP" "NIL"))) (
10 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "X") (mkpair (
11 mksym "M1" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
14 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TOP") (mkpair (
15 mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
16 mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP"
20 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "POP") (mkpair (
21 mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
22 mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP"
26 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NTH") (mkpair (
27 mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP" "LIST") (mksym
29 mkpair (mksym "ACL2" "ZP") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP"
32 "M1" "NTH") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym
34 "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (
40 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "MAKE-STATE") (
41 mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "LOCALS") (mkpair (mksym
42 "M1" "STACK") (mkpair (mksym "M1" "PROGRAM") (mksym "COMMON-LISP" "NIL"))))) (
43 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "PC") (mkpair (
44 mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "LOCALS") (mkpair (
45 mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "STACK") (mkpair (
46 mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "PROGRAM") (mkpair (
53 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PC") (mkpair (
54 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
55 "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0"
56 "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym
60 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "LOCALS") (mkpair (
61 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
62 "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1"
63 "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym
67 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "STACK") (mkpair (
68 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
69 "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2"
70 "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym
74 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PROGRAM") (mkpair (
75 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
76 "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "3"
77 "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym
81 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "OP-CODE") (mkpair (
82 mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
83 mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP"
87 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ARG1") (mkpair (
88 mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
89 mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
90 mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
94 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ARG2") (mkpair (
95 mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
96 mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
97 mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
101 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ARG3") (mkpair (
102 mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
103 mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
104 mknum "3" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
108 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "LEN") (mkpair (
109 mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
111 mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
115 "NIL"))) (mkpair (mkpair (mksym "M1" "LEN") (mkpair (mkpair (mksym
116 "COMMON-LISP" "CDR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (
121 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "APP") (mkpair (
122 mkpair (mksym "M1" "X") (mkpair (mksym "M1" "Y") (mksym "COMMON-LISP" "NIL"))) (
124 "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (
125 mkpair (mksym "M1" "Y") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
126 mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "X") (mksym
127 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (
128 mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP"
129 "NIL"))) (mkpair (mksym "M1" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym
134 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "REV") (mkpair (
135 mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
137 mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
139 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (
140 mksym "M1" "REV") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
141 "M1" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
143 "CAR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
149 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "REV1") (mkpair (
150 mkpair (mksym "M1" "X") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
152 "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (
153 mkpair (mksym "M1" "A") (mkpair (mkpair (mksym "M1" "REV1") (mkpair (mkpair (
154 mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP"
156 "COMMON-LISP" "CAR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (
157 mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
161 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "FREV") (mkpair (
162 mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
163 "M1" "REV1") (mkpair (mksym "M1" "X") (mkpair (mkpair (mksym "COMMON-LISP"
168 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "REPEAT") (mkpair (
169 mkpair (mksym "M1" "TH") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
171 mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
174 mksym "M1" "TH") (mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mksym "M1"
177 "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym
182 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "POPN") (mkpair (
183 mkpair (mksym "M1" "N") (mkpair (mksym "M1" "STK") (mksym "COMMON-LISP" "NIL"))) (
185 mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
186 "STK") (mkpair (mkpair (mksym "M1" "POPN") (mkpair (mkpair (mksym "ACL2"
188 "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym
189 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "POP") (mkpair (mksym
190 "M1" "STK") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
194 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "UPDATE-NTH") (
195 mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "M1" "V") (mkpair (mksym
197 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym "M1"
199 "CONS") (mkpair (mksym "M1" "V") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
203 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (
206 mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1"
213 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "MEMBER") (mkpair (
214 mkpair (mksym "M1" "E") (mkpair (mksym "COMMON-LISP" "LIST") (mksym
220 "EQUAL") (mkpair (mksym "M1" "E") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
224 "M1" "MEMBER") (mkpair (mksym "M1" "E") (mkpair (mkpair (mksym "COMMON-LISP"
230 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "INDEX") (mkpair (
231 mkpair (mksym "M1" "E") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (
233 "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (
236 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "E") (mkpair (
237 mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "LST") (mksym
242 "NIL"))) (mkpair (mkpair (mksym "M1" "INDEX") (mkpair (mksym "M1" "E") (
243 mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "LST") (mksym
249 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "SUPPLIEDP") (
250 mkpair (mkpair (mksym "M1" "KEY") (mkpair (mksym "M1" "ARGS") (mksym
252 mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ARGS") (mksym
256 mkpair (mksym "M1" "KEY") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
257 mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
259 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "SUPPLIEDP") (mkpair (
260 mksym "M1" "KEY") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (
261 mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP"
267 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ACTUAL") (mkpair (
268 mkpair (mksym "M1" "KEY") (mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP"
270 "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) (
273 "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "KEY") (
274 mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "ARGS") (mksym
277 mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
278 mkpair (mkpair (mksym "M1" "ACTUAL") (mkpair (mksym "M1" "KEY") (mkpair (
280 mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
285 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "BOUNDP") (mkpair (
286 mkpair (mksym "M1" "VAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP"
288 "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (
291 "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "VAR") (
293 "COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (
296 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "BOUNDP") (mkpair (mksym
297 "M1" "VAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1"
303 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "BINDING") (mkpair (
304 mkpair (mksym "M1" "VAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP"
306 "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (
309 "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "VAR") (
311 "COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (
314 mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") (
316 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "BINDING") (mkpair (mksym
317 "M1" "VAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1"
323 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "BIND") (mkpair (
324 mkpair (mksym "M1" "VAR") (mkpair (mksym "M1" "VAL") (mkpair (mksym "M1"
326 "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "M1"
328 "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1"
329 "VAR") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "VAL") (
335 "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "VAR") (mkpair (mkpair (mksym
337 mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
339 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "VAR") (
340 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "VAL") (
344 mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
346 "COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (
347 mkpair (mkpair (mksym "M1" "BIND") (mkpair (mksym "M1" "VAR") (mkpair (mksym
348 "M1" "VAL") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1"
354 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "U-FIX") (mkpair (
355 mkpair (mksym "M1" "X") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
356 mkpair (mkpair (mksym "COMMON-LISP" "MOD") (mkpair (mksym "M1" "X") (mkpair (
359 mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
363 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "S-FIX") (mkpair (
364 mkpair (mksym "M1" "X") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
366 "M1" "TEMP") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (
368 mkpair (mksym "M1" "TEMP") (mkpair (mkpair (mksym "COMMON-LISP" "EXPT") (
372 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP"
374 mkpair (mksym "M1" "TEMP") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
375 mksym "M1" "TEMP") (mkpair (mkpair (mksym "ACL2" "UNARY--") (mkpair (mkpair (
378 "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym
380 "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "MOD") (mkpair (mksym "M1" "X") (
383 "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym
384 "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (
388 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "U-BIG1") (mkpair (
389 mkpair (mksym "M1" "LST") (mkpair (mksym "M1" "ACC") (mksym "COMMON-LISP"
391 "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (
392 mkpair (mksym "M1" "ACC") (mkpair (mkpair (mksym "M1" "U-BIG1") (mkpair (
393 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "LST") (mksym
395 mkpair (mksym "M1" "U-FIX") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
396 mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
403 "NIL")))) (mkpair (mksym "M1" "ACC") (mksym "COMMON-LISP" "NIL")))) (mksym
408 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "U-BIG") (mkpair (
409 mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
410 "M1" "U-BIG1") (mkpair (mksym "M1" "LST") (mkpair (mkpair (mksym
415 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "S-BIG") (mkpair (
416 mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
417 "M1" "S-FIX") (mkpair (mkpair (mksym "M1" "U-BIG") (mkpair (mksym "M1" "LST") (
420 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "LEN") (mkpair (
421 mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
425 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NEXTN") (mkpair (
426 mkpair (mksym "M1" "N") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (
428 mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
431 mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "LST") (mksym
432 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "NEXTN") (mkpair (mkpair (
435 "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
436 "CDR") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym
441 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "SKIPN") (mkpair (
442 mkpair (mksym "M1" "N") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (
444 mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
445 "LST") (mkpair (mkpair (mksym "M1" "SKIPN") (mkpair (mkpair (mksym "ACL2"
447 "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym
449 mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (