examples/M1/m1_story.sml

8 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NEXT-INST") (
9 mkpair (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
10 mksym "M1" "NTH") (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "S") (
11 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (
12 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
16 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-ICONST") (
17 mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
18 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
19 mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
21 mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
22 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
23 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
24 "PUSH") (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (mksym "M1" "INST") (
25 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "STACK") (mkpair (
26 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
27 mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym
32 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-ILOAD") (
33 mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
34 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
35 mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
37 mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
38 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
39 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
40 "PUSH") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "M1" "ARG1") (
41 mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
42 mksym "M1" "LOCALS") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
43 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "STACK") (mkpair (
44 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
45 mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym
50 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-IADD") (
51 mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
52 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
53 mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
55 mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
56 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
57 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
58 "PUSH") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "M1"
59 "TOP") (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (mksym "M1" "STACK") (
60 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
61 "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "TOP") (
62 mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
64 "NIL")))) (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (mksym "M1"
65 "POP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
67 "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PROGRAM") (
68 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
72 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-ISTORE") (
73 mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
74 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
75 mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
77 mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
78 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (
79 mkpair (mkpair (mksym "M1" "ARG1") (mkpair (mksym "M1" "INST") (mksym
80 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "TOP") (mkpair (mkpair (
81 mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
82 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
83 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
84 mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (mksym "M1" "STACK") (
85 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
86 "NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (
91 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-ISUB") (
92 mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
93 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
94 mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
96 mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
97 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
98 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
99 "PUSH") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "M1"
100 "TOP") (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (mksym "M1" "STACK") (
101 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
102 "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
103 "UNARY--") (mkpair (mkpair (mksym "M1" "TOP") (mkpair (mkpair (mksym "M1"
104 "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym
106 "NIL")))) (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (mksym "M1"
107 "POP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
109 "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PROGRAM") (
110 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
114 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-IMUL") (
115 mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
116 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
117 mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
119 mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
120 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
121 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
122 "PUSH") (mkpair (mkpair (mksym "ACL2" "BINARY-*") (mkpair (mkpair (mksym "M1"
123 "TOP") (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (mksym "M1" "STACK") (
124 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
125 "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "TOP") (
126 mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
128 "NIL")))) (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (mksym "M1"
129 "POP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
131 "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PROGRAM") (
132 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
136 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-GOTO") (
137 mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
138 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
139 mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (
140 mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
141 "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym
142 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (mksym
143 "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "STACK") (
144 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
145 "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym
149 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-IFLE") (
150 mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
151 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
155 mkpair (mkpair (mksym "M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (
156 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
158 mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (
159 mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
160 "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym
161 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
163 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1"
165 "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (mksym
166 "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "POP") (
167 mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
169 "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym
173 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "DO-INST") (mkpair (
174 mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
176 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "OP-CODE") (mkpair (mksym
177 "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
178 "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "ICONST") (mksym "COMMON-LISP"
179 "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1"
180 "EXECUTE-ICONST") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
182 mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "OP-CODE") (
183 mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
184 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "ILOAD") (mksym
186 "M1" "EXECUTE-ILOAD") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
188 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
189 "OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
190 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "ISTORE") (mksym
192 "M1" "EXECUTE-ISTORE") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
194 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
195 "OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
196 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "IADD") (mksym
198 "M1" "EXECUTE-IADD") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
200 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
201 "OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
202 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "ISUB") (mksym
204 "M1" "EXECUTE-ISUB") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
206 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
207 "OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
208 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "IMUL") (mksym
210 "M1" "EXECUTE-IMUL") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
212 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
213 "OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
214 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "GOTO") (mksym
216 "M1" "EXECUTE-GOTO") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
218 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
219 "OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
220 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "IFLE") (mksym
222 "M1" "EXECUTE-IFLE") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
223 mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
230 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "STEP") (mkpair (
231 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
232 "M1" "DO-INST") (mkpair (mkpair (mksym "M1" "NEXT-INST") (mkpair (mksym "M1"
233 "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym
237 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "RUN") (mkpair (
238 mkpair (mksym "M1" "SCHED") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
240 "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "SCHED") (mksym "COMMON-LISP" "NIL"))) (
241 mkpair (mksym "M1" "S") (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (
242 mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "SCHED") (mksym "COMMON-LISP"
243 "NIL"))) (mkpair (mkpair (mksym "M1" "STEP") (mkpair (mksym "M1" "S") (mksym
248 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "FACTORIAL-EXAMPLE-0") (
249 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
293 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
300 mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym
301 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
302 "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
304 mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10" "1" "0" "1") (mksym
305 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
306 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
308 mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
309 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym
310 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
311 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
313 mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
314 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "0" "1" "0" "1") (mksym
315 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "GOTO") (mkpair (mknum
316 "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
318 mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
324 "COMMON-LISP" "NIL")) (mkpair (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (
326 "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
327 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym
328 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum
329 "10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
331 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym
332 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "IMUL") (mksym
333 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
334 "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
336 mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym
337 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISUB") (mksym
338 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
339 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
341 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym
342 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "HALT") (mksym
348 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFACT-LOOP-SCHED") (
349 mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
350 mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym
351 "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "REPEAT") (
355 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (
356 mksym "M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
359 "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1"
360 "IFACT-LOOP-SCHED") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (
362 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (
367 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFACT-SCHED") (
368 mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
369 mksym "M1" "APP") (mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mkpair (
373 "NIL")))) (mkpair (mkpair (mksym "M1" "IFACT-LOOP-SCHED") (mkpair (mksym "M1"
378 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "!") (mkpair (
379 mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
380 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym "M1"
383 mkpair (mkpair (mksym "ACL2" "BINARY-*") (mkpair (mksym "M1" "N") (mkpair (
384 mkpair (mksym "M1" "!") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
386 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (
391 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TEST-IFACT") (
392 mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
393 mksym "M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym
394 "M1" "RUN") (mkpair (mkpair (mksym "M1" "IFACT-SCHED") (mkpair (mksym "M1"
395 "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
398 mkpair (mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
405 "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
406 mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym
407 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
408 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
410 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym
411 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
412 "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
413 "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ISTORE") (
415 mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
416 "NIL"))) (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (
417 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISUB") (mksym
418 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
419 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
421 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym
422 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "HALT") (mksym
429 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "FACTORIAL-EXAMPLE-1") (
430 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
433 mkpair (mkpair (mksym "M1" "!") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
439 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "FACTORIAL-EXAMPLE-2") (
440 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
443 mkpair (mkpair (mksym "M1" "!") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
449 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EVEN-SCHED") (
450 mkpair (mkpair (mksym "M1" "I") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
451 mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym
452 "M1" "I") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "REPEAT") (
457 mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "I") (mkpair (mkpair (
460 "M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
463 "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "APP") (
464 mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP"
468 mksym "M1" "EVEN-SCHED") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
470 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "I") (mksym "COMMON-LISP" "NIL")))) (
476 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TEST-EVEN") (
477 mkpair (mkpair (mksym "M1" "I") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
478 mksym "M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym
479 "M1" "RUN") (mkpair (mkpair (mksym "M1" "EVEN-SCHED") (mkpair (mksym "M1" "I") (
480 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
483 mkpair (mksym "M1" "I") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
487 "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (
489 "M1" "IFLE") (mkpair (mknum "12" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
490 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym
491 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum
492 "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
493 "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "IFLE") (
495 mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
496 "NIL"))) (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "2" "1" "0" "1") (
497 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISUB") (mksym
498 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
499 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
501 mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "0" "1" "0" "1") (mksym
502 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "HALT") (mksym
503 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum
504 "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
511 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "TEST-EVEN-THEOREM") (
513 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "TEST-EVEN") (mkpair (
519 "M1" "TEST-EVEN") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
524 "EQUAL") (mkpair (mkpair (mksym "M1" "TEST-EVEN") (mkpair (mkpair (mksym
529 mkpair (mksym "M1" "TEST-EVEN") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
542 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "COLLECT-AT-END") (
543 mkpair (mkpair (mksym "COMMON-LISP" "LIST") (mkpair (mksym "M1" "E") (mksym
545 mkpair (mksym "M1" "MEMBER") (mkpair (mksym "M1" "E") (mkpair (mksym
547 "COMMON-LISP" "LIST") (mkpair (mkpair (mksym "M1" "APP") (mkpair (mksym
549 mksym "M1" "E") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
555 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "NTH-NIL") (mkpair (
556 mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "NTH") (
557 mkpair (mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
564 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "ACL2-COUNT-NTH") (mkpair (
565 mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (
567 mkpair (mksym "COMMON-LISP" "<") (mkpair (mkpair (mksym "ACL2" "ACL2-COUNT") (
568 mkpair (mkpair (mksym "M1" "NTH") (mkpair (mksym "M1" "N") (mkpair (mksym
570 "NIL"))) (mkpair (mkpair (mksym "ACL2" "ACL2-COUNT") (mkpair (mksym
575 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1"
576 "COLLECT-VARS-IN-EXPR") (mkpair (mkpair (mksym "M1" "VARS") (mkpair (mksym
577 "M1" "EXPR") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
579 mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
581 mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
582 "COLLECT-AT-END") (mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "EXPR") (
583 mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "VARS") (mksym
584 "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-EXPR") (
585 mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-EXPR") (mkpair (mksym "M1" "VARS") (
586 mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP"
588 mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL")))) (mksym
589 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
591 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL")))) (
596 (mkpair (mksym "ACL2" "MUTUAL-RECURSION") (mkpair (mkpair (mksym
597 "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "COLLECT-VARS-IN-STMT*") (mkpair (
598 mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "STMT-LIST") (mksym
600 mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "STMT-LIST") (mksym
601 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "VARS") (mkpair (mkpair (mksym
602 "M1" "COLLECT-VARS-IN-STMT*") (mkpair (mkpair (mksym "M1"
603 "COLLECT-VARS-IN-STMT") (mkpair (mksym "M1" "VARS") (mkpair (mkpair (mksym
604 "COMMON-LISP" "CAR") (mkpair (mksym "M1" "STMT-LIST") (mksym "COMMON-LISP"
606 "CDR") (mkpair (mksym "M1" "STMT-LIST") (mksym "COMMON-LISP" "NIL"))) (mksym
608 "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1"
609 "COLLECT-VARS-IN-STMT") (mkpair (mkpair (mksym "M1" "VARS") (mkpair (mksym
610 "M1" "STMT") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
612 mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
614 "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
615 "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "=") (mksym "COMMON-LISP" "NIL"))) (
616 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1"
617 "COLLECT-VARS-IN-EXPR") (mkpair (mkpair (mksym "M1" "COLLECT-AT-END") (mkpair (
618 mksym "M1" "VARS") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym
620 "NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mksym
621 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
623 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (
625 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
626 "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1"
627 "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STMT") (mksym
629 mksym "M1" "WHILE") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
630 mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-STMT*") (mkpair (mkpair (mksym
631 "M1" "COLLECT-VARS-IN-EXPR") (mkpair (mksym "M1" "VARS") (mkpair (mkpair (
632 mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
633 mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
636 mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
639 "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0"
640 "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STMT") (mksym
642 mksym "M1" "RETURN") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
643 mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-EXPR") (mkpair (mksym "M1" "VARS") (
644 mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP"
646 mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mksym
647 "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "VARS") (mksym "COMMON-LISP"
652 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "OP!") (mkpair (
653 mkpair (mksym "M1" "OP") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
655 mksym "M1" "OP") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
658 "M1" "IADD") (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL")) (mksym
660 mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "OP") (mkpair (
663 "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "ISUB") (mksym
666 "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "OP") (mkpair (mkpair (mksym
669 "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP"
671 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym "M1"
677 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ILOAD!") (mkpair (
678 mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "VAR") (mksym "COMMON-LISP"
681 mksym "M1" "ILOAD") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
682 "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "M1" "INDEX") (mkpair (mksym
683 "M1" "VAR") (mkpair (mksym "M1" "VARS") (mksym "COMMON-LISP" "NIL")))) (
691 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ICONST!") (mkpair (
692 mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
694 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "ICONST") (mksym
696 mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
703 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXPR!") (mkpair (
704 mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP"
706 "COMMON-LISP" "ATOM") (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL"))) (
708 "COMMON-LISP" "SYMBOLP") (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP"
709 "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD!") (mkpair (mksym "M1" "VARS") (
710 mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
711 mksym "M1" "ICONST!") (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL"))) (
712 mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (
713 mkpair (mksym "M1" "EXPR!") (mkpair (mksym "M1" "VARS") (mkpair (mkpair (
714 mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
715 mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
717 mkpair (mksym "M1" "APP") (mkpair (mkpair (mksym "M1" "EXPR!") (mkpair (mksym
718 "M1" "VARS") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym
720 "NIL"))) (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL")))) (mksym
721 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "OP!") (mkpair (mkpair (
722 mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
723 mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
729 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFLE!") (mkpair (
730 mkpair (mksym "M1" "OFFSET") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
732 mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "IFLE") (
734 mkpair (mksym "M1" "OFFSET") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
742 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "GOTO!") (mkpair (
743 mkpair (mksym "M1" "OFFSET") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
745 mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "GOTO") (
747 mkpair (mksym "M1" "OFFSET") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
755 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "WHILE!") (mkpair (
756 mkpair (mksym "M1" "TEST-CODE") (mkpair (mksym "M1" "BODY-CODE") (mksym
757 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mksym "M1"
758 "TEST-CODE") (mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (mksym "M1"
759 "IFLE!") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym
761 "NIL"))) (mkpair (mkpair (mksym "M1" "LEN") (mkpair (mksym "M1" "BODY-CODE") (
763 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mksym "M1"
764 "BODY-CODE") (mkpair (mkpair (mksym "M1" "GOTO!") (mkpair (mkpair (mksym
765 "ACL2" "UNARY--") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (
766 mksym "M1" "LEN") (mkpair (mksym "M1" "TEST-CODE") (mksym "COMMON-LISP" "NIL"))) (
767 mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP"
769 mkpair (mkpair (mksym "M1" "LEN") (mkpair (mksym "M1" "BODY-CODE") (mksym
776 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TEST!") (mkpair (
777 mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "TEST") (mksym "COMMON-LISP"
779 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
781 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "TEST") (mksym "COMMON-LISP" "NIL")))) (
785 mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP"
787 mkpair (mksym "M1" "TEST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
790 "M1" "EXPR!") (mkpair (mksym "M1" "VARS") (mkpair (mkpair (mksym "M1" "NTH") (
792 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "TEST") (mksym "COMMON-LISP"
793 "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "APP") (
794 mkpair (mkpair (mksym "M1" "EXPR!") (mkpair (mksym "M1" "VARS") (mkpair (
795 mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
797 "M1" "TEST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
798 mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (mksym "M1" "EXPR!") (
799 mkpair (mksym "M1" "VARS") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
801 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "TEST") (mksym "COMMON-LISP" "NIL")))) (
803 mkpair (mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (
807 mkpair (mksym "M1" "ILLEGAL") (mksym "COMMON-LISP" "NIL")) (mksym
812 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ISTORE!") (mkpair (
813 mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "VAR") (mksym "COMMON-LISP"
816 mksym "M1" "ISTORE") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
817 "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "M1" "INDEX") (mkpair (mksym
818 "M1" "VAR") (mkpair (mksym "M1" "VARS") (mksym "COMMON-LISP" "NIL")))) (
826 (mkpair (mksym "ACL2" "MUTUAL-RECURSION") (mkpair (mkpair (mksym
827 "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "STMT*!") (mkpair (mkpair (mksym
828 "M1" "VARS") (mkpair (mksym "M1" "STMT-LIST") (mksym "COMMON-LISP" "NIL"))) (
830 "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "STMT-LIST") (mksym "COMMON-LISP"
833 "M1" "APP") (mkpair (mkpair (mksym "M1" "STMT!") (mkpair (mksym "M1" "VARS") (
834 mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "STMT-LIST") (
836 mksym "M1" "STMT*!") (mkpair (mksym "M1" "VARS") (mkpair (mkpair (mksym
837 "COMMON-LISP" "CDR") (mkpair (mksym "M1" "STMT-LIST") (mksym "COMMON-LISP"
840 mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "STMT!") (mkpair (mkpair (
841 mksym "M1" "VARS") (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL"))) (
843 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
845 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (
846 mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "=") (mksym
848 "M1" "APP") (mkpair (mkpair (mksym "M1" "EXPR!") (mkpair (mksym "M1" "VARS") (
849 mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP"
851 mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mksym
852 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "ISTORE!") (mkpair (mksym
853 "M1" "VARS") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym
855 "NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mksym
858 mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
860 "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
861 "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "WHILE") (mksym "COMMON-LISP"
862 "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "WHILE!") (
863 mkpair (mkpair (mksym "M1" "TEST!") (mkpair (mksym "M1" "VARS") (mkpair (
864 mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
866 "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
867 mkpair (mkpair (mksym "M1" "STMT*!") (mkpair (mksym "M1" "VARS") (mkpair (
869 mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
872 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
874 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (
875 mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "RETURN") (
877 mksym "M1" "APP") (mkpair (mkpair (mksym "M1" "EXPR!") (mkpair (mksym "M1"
878 "VARS") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym
880 "NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mksym
882 mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
885 mkpair (mksym "M1" "ILLEGAL") (mksym "COMMON-LISP" "NIL")) (mksym
891 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "COMPILE") (mkpair (
892 mkpair (mksym "M1" "FORMALS") (mkpair (mksym "M1" "STMT-LIST") (mksym
893 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "STMT*!") (mkpair (mkpair (
894 mksym "M1" "COLLECT-VARS-IN-STMT*") (mkpair (mksym "M1" "FORMALS") (mkpair (
895 mksym "M1" "STMT-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1"
899 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-COMPILATION-1") (
900 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
902 mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL"))) (
904 "M1" "A") (mkpair (mksym "M1" "=") (mkpair (mknum "1" "1" "0" "1") (mksym
905 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "WHILE") (mkpair (mkpair (
906 mksym "M1" "N") (mkpair (mksym "COMMON-LISP" ">") (mkpair (mknum "0" "1" "0"
907 "1") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "A") (mkpair (
908 mksym "M1" "=") (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP"
909 "*") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (mksym
910 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "M1"
911 "=") (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP" "-") (
914 mksym "M1" "RETURN") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
917 mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym
918 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
919 "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
921 mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10" "1" "0" "1") (mksym
922 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
923 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
925 mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
926 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym
927 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
928 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
930 mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
931 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "0" "1" "0" "1") (mksym
932 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "GOTO") (mkpair (mknum
933 "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
935 mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
940 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-COMPILATION-2") (
941 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
943 mksym "M1" "N") (mkpair (mksym "M1" "K") (mksym "COMMON-LISP" "NIL"))) (mksym
945 mkpair (mkpair (mksym "M1" "A") (mkpair (mksym "M1" "=") (mkpair (mknum "0"
946 "1" "0" "1") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1"
947 "WHILE") (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP" ">") (
948 mkpair (mksym "M1" "K") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
949 "M1" "A") (mkpair (mksym "M1" "=") (mkpair (mkpair (mksym "M1" "A") (mkpair (
951 "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "N") (
952 mkpair (mksym "M1" "=") (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym
955 mksym "M1" "RETURN") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
958 mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "0" "1" "0" "1") (mksym
959 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
960 "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
962 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym
963 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISUB") (mksym
964 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10"
965 "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
967 mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym
968 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "IADD") (mksym
969 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
970 "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
972 mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym
973 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISUB") (mksym
974 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
975 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
977 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "2" "1" "0" "1") (mksym
978 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "HALT") (mksym
984 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-EXECUTION-1") (
985 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
986 "TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "M1" "RUN") (
987 mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP"
991 mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
997 "M1" "COMPILE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (
998 mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL"))) (
1000 "M1" "A") (mkpair (mksym "M1" "=") (mkpair (mknum "1" "1" "0" "1") (mksym
1001 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "WHILE") (mkpair (mkpair (
1002 mksym "M1" "N") (mkpair (mksym "COMMON-LISP" ">") (mkpair (mknum "0" "1" "0"
1003 "1") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "A") (mkpair (
1004 mksym "M1" "=") (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP"
1005 "*") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (mksym
1006 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "M1"
1007 "=") (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP" "-") (
1010 mksym "M1" "RETURN") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
1019 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-EXECUTION-2") (
1020 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1021 "TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "M1" "RUN") (
1022 mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP"
1026 mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1032 mkpair (mkpair (mksym "M1" "COMPILE") (mkpair (mkpair (mksym "COMMON-LISP"
1033 "QUOTE") (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "M1" "K") (mksym
1035 "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "A") (mkpair (
1036 mksym "M1" "=") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL")))) (
1037 mkpair (mkpair (mksym "M1" "WHILE") (mkpair (mkpair (mksym "M1" "N") (mkpair (
1038 mksym "COMMON-LISP" ">") (mkpair (mksym "M1" "K") (mksym "COMMON-LISP" "NIL")))) (
1039 mkpair (mkpair (mksym "M1" "A") (mkpair (mksym "M1" "=") (mkpair (mkpair (
1040 mksym "M1" "A") (mkpair (mksym "COMMON-LISP" "+") (mkpair (mknum "1" "1" "0"
1042 mkpair (mksym "M1" "N") (mkpair (mksym "M1" "=") (mkpair (mkpair (mksym "M1"
1045 "NIL"))))) (mkpair (mkpair (mksym "M1" "RETURN") (mkpair (mksym "M1" "A") (
1054 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "STACKS") (mkpair (mkpair (
1056 mkpair (mkpair (mksym "M1" "TOP") (mkpair (mkpair (mksym "M1" "PUSH") (mkpair (
1057 mksym "M1" "X") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (
1058 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "X") (mksym "COMMON-LISP"
1060 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (
1061 mksym "M1" "PUSH") (mkpair (mksym "M1" "X") (mkpair (mksym "M1" "S") (mksym
1062 "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (
1064 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1065 "TOP") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "X") (
1066 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1067 "NIL"))) (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (
1068 mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "POP") (
1069 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "X") (mkpair (
1070 mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (
1071 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1081 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "STATES") (mkpair (mkpair (
1083 mkpair (mkpair (mksym "M1" "PC") (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
1084 mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "LOCALS") (mkpair (mksym "M1"
1085 "STACK") (mkpair (mksym "M1" "PROGRAM") (mksym "COMMON-LISP" "NIL")))))) (
1086 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "PC") (mksym "COMMON-LISP"
1088 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (mkpair (
1089 mksym "M1" "MAKE-STATE") (mkpair (mksym "M1" "PC") (mkpair (mksym "M1"
1090 "LOCALS") (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "PROGRAM") (mksym
1091 "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
1094 "M1" "STACK") (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mksym "M1"
1095 "PC") (mkpair (mksym "M1" "LOCALS") (mkpair (mksym "M1" "STACK") (mkpair (
1096 mksym "M1" "PROGRAM") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP"
1097 "NIL"))) (mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" "NIL")))) (mkpair (
1099 "EQUAL") (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mkpair (mksym "M1"
1100 "MAKE-STATE") (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "LOCALS") (mkpair (
1101 mksym "M1" "STACK") (mkpair (mksym "M1" "PROGRAM") (mksym "COMMON-LISP" "NIL")))))) (
1102 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "PROGRAM") (mksym
1104 mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "PC") (
1105 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "PC") (mkpair (
1106 mksym "M1" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (
1107 mkpair (mksym "M1" "PC") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
1109 mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (mkpair (mksym "COMMON-LISP"
1110 "CONS") (mkpair (mksym "M1" "PC") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
1111 mkpair (mksym "M1" "LOCALS") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP"
1113 mkpair (mksym "M1" "LOCALS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
1115 mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "COMMON-LISP"
1116 "CONS") (mkpair (mksym "M1" "PC") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
1117 mkpair (mksym "M1" "LOCALS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
1118 mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP"
1120 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STACK") (mksym
1122 mkpair (mksym "M1" "PROGRAM") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
1123 mkpair (mksym "M1" "PC") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1124 mksym "M1" "LOCALS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1125 mksym "M1" "STACK") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1126 mksym "M1" "PROGRAM") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")))) (
1128 "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
1147 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "STEP-OPENER") (mkpair (
1148 mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (
1149 mkpair (mkpair (mksym "M1" "NEXT-INST") (mkpair (mksym "M1" "S") (mksym
1151 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "STEP") (mkpair (mksym
1152 "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "DO-INST") (
1153 mkpair (mkpair (mksym "M1" "NEXT-INST") (mkpair (mksym "M1" "S") (mksym
1154 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (
1159 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "RUN-APP") (mkpair (
1160 mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "RUN") (
1161 mkpair (mkpair (mksym "M1" "APP") (mkpair (mksym "M1" "A") (mkpair (mksym
1162 "M1" "B") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "S") (mksym
1163 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mksym
1164 "M1" "B") (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mksym "M1" "A") (mkpair (
1165 mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
1169 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "RUN-OPENER") (mkpair (
1171 "EQUAL") (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (mksym
1173 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (
1174 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1175 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (
1176 mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "TH") (mkpair (mksym "M1"
1177 "SCHED") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "S") (mksym
1178 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mksym
1179 "M1" "SCHED") (mkpair (mkpair (mksym "M1" "STEP") (mkpair (mksym "M1" "S") (
1186 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "NTH-ADD1!") (mkpair (
1187 mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (
1188 mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1189 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
1190 mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1192 "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "COMMON-LISP" "LIST") (
1193 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "NTH") (mkpair (
1194 mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
1200 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "NTH-UPDATE-NTH") (mkpair (
1201 mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
1202 mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (mksym "M1" "I") (mksym
1203 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (mksym
1204 "M1" "J") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
1207 mkpair (mkpair (mksym "M1" "NTH") (mkpair (mksym "M1" "I") (mkpair (mkpair (
1208 mksym "M1" "UPDATE-NTH") (mkpair (mksym "M1" "J") (mkpair (mksym "M1" "V") (
1211 mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "I") (mkpair (mksym
1212 "M1" "J") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "V") (mkpair (
1213 mkpair (mksym "M1" "NTH") (mkpair (mksym "M1" "I") (mkpair (mksym
1219 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "UPDATE-NTH-UPDATE-NTH-1") (
1220 mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP"
1221 "IF") (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (mksym "M1" "I") (mksym
1223 mkpair (mksym "ACL2" "NATP") (mkpair (mksym "M1" "J") (mksym "COMMON-LISP"
1225 "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "I") (mkpair (mksym "M1" "J") (
1231 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (mkpair (
1232 mksym "M1" "I") (mkpair (mksym "M1" "V") (mkpair (mkpair (mksym "M1"
1233 "UPDATE-NTH") (mkpair (mksym "M1" "J") (mkpair (mksym "M1" "W") (mkpair (
1235 "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (mkpair (
1236 mksym "M1" "J") (mkpair (mksym "M1" "W") (mkpair (mkpair (mksym "M1"
1237 "UPDATE-NTH") (mkpair (mksym "M1" "I") (mkpair (mksym "M1" "V") (mkpair (
1243 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "UPDATE-NTH-UPDATE-NTH-2") (
1244 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1245 "UPDATE-NTH") (mkpair (mksym "M1" "I") (mkpair (mksym "M1" "V") (mkpair (
1246 mkpair (mksym "M1" "UPDATE-NTH") (mkpair (mksym "M1" "I") (mkpair (mksym "M1"
1248 mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (
1249 mkpair (mksym "M1" "I") (mkpair (mksym "M1" "V") (mkpair (mksym "COMMON-LISP"
1254 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "!") (mkpair (
1255 mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
1256 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym "M1"
1259 mkpair (mkpair (mksym "ACL2" "BINARY-*") (mkpair (mksym "M1" "N") (mkpair (
1260 mkpair (mksym "M1" "!") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
1262 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (
1267 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFACT") (mkpair (
1268 mkpair (mksym "M1" "N") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
1269 mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (
1270 mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "A") (
1271 mkpair (mkpair (mksym "M1" "IFACT") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (
1273 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP"
1274 "NIL")))) (mkpair (mkpair (mksym "ACL2" "BINARY-*") (mkpair (mksym "M1" "N") (
1275 mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1279 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFACT-LOOP-SCHED") (
1280 mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
1281 mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym
1282 "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "REPEAT") (
1286 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (
1287 mksym "M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1290 "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1"
1291 "IFACT-LOOP-SCHED") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (
1293 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (
1298 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFACT-SCHED") (
1299 mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
1300 mksym "M1" "APP") (mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mkpair (
1304 "NIL")))) (mkpair (mkpair (mksym "M1" "IFACT-LOOP-SCHED") (mkpair (mksym "M1"
1309 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TEST-IFACT") (
1310 mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
1311 mksym "M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym
1312 "M1" "RUN") (mkpair (mkpair (mksym "M1" "IFACT-SCHED") (mkpair (mksym "M1"
1313 "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
1316 mkpair (mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1323 "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1324 mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym
1325 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
1326 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1328 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym
1329 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
1330 "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1331 "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ISTORE") (
1333 mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
1334 "NIL"))) (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (
1335 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISUB") (mksym
1336 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
1337 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1339 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym
1340 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "HALT") (mksym
1347 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "TEST-IFACT-EXAMPLES") (
1349 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "TEST-IFACT") (mkpair (
1352 "M1" "!") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "5"
1355 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1358 mkpair (mkpair (mksym "M1" "!") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1361 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "TEST-IFACT") (mkpair (
1364 "M1" "!") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "100"
1373 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "IFACT-LOOP-LEMMA") (
1374 mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP"
1375 "IF") (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (mksym "M1" "N") (mksym
1376 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (mksym
1377 "M1" "A") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
1380 mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (mksym "M1"
1381 "IFACT-LOOP-SCHED") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
1382 mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP"
1384 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "N") (mkpair (
1385 mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "A") (mkpair (mkpair (
1388 "NIL")))) (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "COMMON-LISP"
1389 "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1"
1390 "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISTORE") (
1392 mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
1393 "NIL"))) (mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10" "1" "0" "1") (
1394 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (
1396 "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1397 mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1398 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym
1399 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
1400 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1402 mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1403 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "0" "1" "0" "1") (mksym
1404 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "GOTO") (mkpair (mknum
1405 "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1407 mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1410 mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1414 mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "M1" "IFACT") (mkpair (
1415 mksym "M1" "N") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (
1418 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PUSH") (mkpair (mkpair (
1419 mksym "M1" "IFACT") (mkpair (mksym "M1" "N") (mkpair (mksym "M1" "A") (mksym
1420 "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP"
1422 mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym
1423 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
1424 "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1426 mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10" "1" "0" "1") (mksym
1427 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
1428 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1430 mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1431 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym
1432 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
1433 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1435 mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1436 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "0" "1" "0" "1") (mksym
1437 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "GOTO") (mkpair (mknum
1438 "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1440 mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1446 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "IFACT-LEMMA") (mkpair (
1447 mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (
1448 mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1449 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (
1450 mksym "M1" "IFACT-SCHED") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
1451 mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP"
1453 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "N") (mkpair (
1454 mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "A") (mkpair (mkpair (
1457 "NIL")))) (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "COMMON-LISP"
1458 "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1"
1459 "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISTORE") (
1461 mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
1462 "NIL"))) (mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10" "1" "0" "1") (
1463 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (
1465 "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1466 mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1467 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym
1468 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
1469 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1471 mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1472 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "0" "1" "0" "1") (mksym
1473 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "GOTO") (mkpair (mknum
1474 "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1476 mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1479 mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1483 mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "M1" "IFACT") (mkpair (
1484 mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
1488 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PUSH") (mkpair (mkpair (
1489 mksym "M1" "IFACT") (mkpair (mksym "M1" "N") (mkpair (mkpair (mksym
1491 "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "STACK") (mksym
1493 mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym
1494 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
1495 "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1497 mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10" "1" "0" "1") (mksym
1498 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
1499 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1501 mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1502 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym
1503 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
1504 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1506 mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1507 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "0" "1" "0" "1") (mksym
1508 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "GOTO") (mkpair (mknum
1509 "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1511 mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1517 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "IFACT-IS-FACTORIAL") (
1518 mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP"
1519 "IF") (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (mksym "M1" "N") (mksym
1520 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (mksym
1521 "M1" "A") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
1524 mkpair (mkpair (mksym "M1" "IFACT") (mkpair (mksym "M1" "N") (mkpair (mksym
1525 "M1" "A") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
1526 "BINARY-*") (mkpair (mkpair (mksym "M1" "!") (mkpair (mksym "M1" "N") (mksym
1527 "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (
1532 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "IFACT-CORRECT") (mkpair (
1533 mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (
1534 mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1535 "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (
1536 mksym "M1" "IFACT-SCHED") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
1537 mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP"
1539 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "N") (mkpair (
1540 mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "A") (mkpair (mkpair (
1543 "NIL")))) (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "COMMON-LISP"
1544 "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1"
1545 "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISTORE") (
1547 mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
1548 "NIL"))) (mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10" "1" "0" "1") (
1549 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (
1551 "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1552 mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1553 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym
1554 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
1555 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1557 mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1558 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "0" "1" "0" "1") (mksym
1559 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "GOTO") (mkpair (mknum
1560 "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1562 mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1565 mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1569 mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "M1" "!") (mkpair (mksym
1570 "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
1573 mksym "M1" "PUSH") (mkpair (mkpair (mksym "M1" "!") (mkpair (mksym "M1" "N") (
1574 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STACK") (mksym
1576 mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym
1577 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
1578 "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1580 mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10" "1" "0" "1") (mksym
1581 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
1582 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1584 mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1585 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym
1586 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum
1587 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1589 mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1590 mkpair (mksym "M1" "ISTORE") (mkpair (mknum "0" "1" "0" "1") (mksym
1591 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "GOTO") (mkpair (mknum
1592 "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1594 mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1600 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1"
1601 "IFACT-CORRECT-COROLLARY-1") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
1602 mkpair (mksym "ACL2" "NATP") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP"
1604 "M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "M1"
1605 "RUN") (mkpair (mkpair (mksym "M1" "IFACT-SCHED") (mkpair (mksym "M1" "N") (
1606 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
1609 mkpair (mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1610 mksym "M1" "A") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
1612 mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "STACK") (mkpair (mkpair (
1613 mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "ICONST") (
1615 mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP"
1616 "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (
1617 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "IFLE") (mkpair (
1619 "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1620 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym
1621 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "IMUL") (mksym
1622 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
1623 "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1625 mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym
1626 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ISUB") (mksym
1627 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "M1" "ISTORE") (mkpair (mknum
1628 "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1630 mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym
1631 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "HALT") (mksym
1635 mkpair (mksym "M1" "!") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
1640 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1"
1641 "IFACT-CORRECT-COROLLARY-2") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
1642 mkpair (mksym "ACL2" "NATP") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP"
1644 "M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "M1"
1645 "RUN") (mkpair (mkpair (mksym "M1" "IFACT-SCHED") (mkpair (mksym "M1" "N") (
1646 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
1649 mkpair (mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1650 mksym "M1" "A") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
1652 mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "STACK") (mkpair (mkpair (
1653 mksym "M1" "COMPILE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1654 mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP"
1656 mkpair (mksym "M1" "A") (mkpair (mksym "M1" "=") (mkpair (mknum "1" "1" "0"
1657 "1") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "WHILE") (
1658 mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP" ">") (mkpair (
1660 "M1" "A") (mkpair (mksym "M1" "=") (mkpair (mkpair (mksym "M1" "N") (mkpair (
1661 mksym "COMMON-LISP" "*") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (
1662 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym
1663 "M1" "=") (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP" "-") (
1666 mksym "M1" "RETURN") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
1670 mkpair (mksym "M1" "!") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
1675 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-MODIFY-1") (
1676 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1677 "MAKE-STATE") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (
1679 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1"
1681 mkpair (mksym "M1" "LOCALS") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1682 "NIL"))) (mkpair (mkpair (mksym "M1" "PUSH") (mkpair (mkpair (mksym "M1"
1683 "ARG1") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
1684 mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1685 "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PROGRAM") (
1686 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
1687 "NIL")))))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym
1688 "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1690 "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym
1691 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (mksym
1692 "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PUSH") (
1693 mkpair (mkpair (mksym "M1" "ARG1") (mkpair (mksym "M1" "INST") (mksym
1694 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym
1695 "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
1696 mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym
1701 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-MODIFY-2") (
1702 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1703 "MAKE-STATE") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (
1705 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1"
1707 mkpair (mksym "M1" "UPDATE-NTH") (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (
1708 mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1709 "TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
1711 "M1" "LOCALS") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym
1712 "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (
1713 mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
1714 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (
1715 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (
1716 mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "ACL2"
1718 "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PC") (
1719 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
1720 "NIL")))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (mkpair (mkpair (mksym
1721 "M1" "ARG1") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (
1722 mkpair (mkpair (mksym "M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (
1723 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
1724 "NIL"))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (mksym "M1" "S") (
1726 mksym "M1" "POP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1"
1728 mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1733 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-MODIFY-3") (
1734 mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1735 "MAKE-STATE") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (
1736 mksym "M1" "ARG1") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (
1737 mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym
1739 "M1" "LOCALS") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (
1740 mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1741 "NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (
1743 mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
1744 mkpair (mksym "M1" "ARG1") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP"
1745 "NIL"))) (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym
1747 "M1" "LOCALS") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (
1748 mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1749 "NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (
1754 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PATTERN-BINDINGS") (
1755 mkpair (mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "ARG-EXPRESSIONS") (
1757 mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "VARS") (
1761 "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1"
1763 "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1"
1767 "NIL")))) (mkpair (mkpair (mksym "M1" "PATTERN-BINDINGS") (mkpair (mkpair (
1768 mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "VARS") (mksym "COMMON-LISP"
1769 "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1"
1775 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-SEMANTICS-1") (
1777 "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "M1" "C") (mkpair (mksym "M1"
1778 "-PC-") (mkpair (mksym "M1" "-LOCALS-") (mkpair (mksym "M1" "-STACK-") (
1779 mkpair (mksym "M1" "-PROGRAM-") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1780 "NIL"))))))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym
1781 "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1783 "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym
1784 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (mksym
1785 "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PUSH") (
1786 mkpair (mksym "M1" "C") (mkpair (mksym "M1" "-STACK-") (mksym "COMMON-LISP"
1787 "NIL")))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (
1789 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (mksym
1790 "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PC") (
1791 mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1792 "M1" "LOCALS") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (
1793 mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1794 "NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (
1795 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1796 "NIL")))))))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (
1797 mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1799 mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
1800 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
1801 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1802 "PUSH") (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (mksym "M1" "INST") (
1803 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "STACK") (mkpair (
1804 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
1805 mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym
1810 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "CONCAT-SYMBOLS") (
1811 mkpair (mkpair (mksym "M1" "PART1") (mkpair (mksym "M1" "PART2") (mksym
1812 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
1814 mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (mksym "COMMON-LISP"
1816 "M1" "PART1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1820 mkpair (mksym "M1" "PART2") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1825 "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1"
1830 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "MAKE-DEFUN") (
1831 mkpair (mkpair (mksym "M1" "NAME") (mkpair (mksym "M1" "ARGS") (mkpair (mksym
1832 "M1" "DCL") (mkpair (mksym "M1" "BODY") (mksym "COMMON-LISP" "NIL"))))) (
1833 mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mksym "M1" "DCL") (mkpair (
1836 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "NAME") (
1837 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "ARGS") (
1838 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "DCL") (
1839 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "BODY") (
1846 "COMMON-LISP" "CONS") (mkpair (mksym "M1" "NAME") (mkpair (mkpair (mksym
1847 "COMMON-LISP" "CONS") (mkpair (mksym "M1" "ARGS") (mkpair (mkpair (mksym
1848 "COMMON-LISP" "CONS") (mkpair (mksym "M1" "BODY") (mkpair (mkpair (mksym