1open HolKernel Parse boolLib bossLib intSyntax pairSyntax listSyntax stringLib numLib sexp;
2
3val package =
4 implode(map chr (cons 77 (cons 49 nil)));
5
6val events = [
7
8(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NEXT-INST") (
9mkpair (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
10mksym "M1" "NTH") (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "S") (
11mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (
12mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
13mksym "COMMON-LISP" "NIL")))))
14,
15
16(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-ICONST") (
17mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
18"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
19mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
20mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
21mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
22mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
23mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
24"PUSH") (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (mksym "M1" "INST") (
25mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "STACK") (mkpair (
26mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
27mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym
28"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP"
29"NIL")))))
30,
31
32(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-ILOAD") (
33mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
34"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
35mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
36mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
37mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
38mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
39mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
40"PUSH") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "M1" "ARG1") (
41mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
42mksym "M1" "LOCALS") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
43mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "STACK") (mkpair (
44mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
45mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym
46"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP"
47"NIL")))))
48,
49
50(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-IADD") (
51mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
52"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
53mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
54mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
55mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
56mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
57mksym "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") (
60mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
61"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "TOP") (
62mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
63"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
64"NIL")))) (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (mksym "M1"
65"POP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
66"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
67"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PROGRAM") (
68mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
69"NIL")))))) (mksym "COMMON-LISP" "NIL")))))
70,
71
72(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-ISTORE") (
73mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
74"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
75mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
76mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
77mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
78mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (
79mkpair (mkpair (mksym "M1" "ARG1") (mkpair (mksym "M1" "INST") (mksym
80"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "TOP") (mkpair (mkpair (
81mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
82mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
83mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
84mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (mksym "M1" "STACK") (
85mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
86"NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (
87mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym
88"COMMON-LISP" "NIL")))))
89,
90
91(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-ISUB") (
92mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
93"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
94mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
95mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
96mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
97mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
98mksym "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") (
101mkpair (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
105"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
106"NIL")))) (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (mksym "M1"
107"POP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
108"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
109"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PROGRAM") (
110mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
111"NIL")))))) (mksym "COMMON-LISP" "NIL")))))
112,
113
114(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-IMUL") (
115mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
116"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
117mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
118mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
119mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
120mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
121mksym "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") (
124mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
125"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "TOP") (
126mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
127"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
128"NIL")))) (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (mksym "M1"
129"POP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
130"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
131"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PROGRAM") (
132mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
133"NIL")))))) (mksym "COMMON-LISP" "NIL")))))
134,
135
136(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-GOTO") (
137mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
138"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
139mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (
140mksym "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") (
144mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
145"M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym
146"COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))))
147,
148
149(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUTE-IFLE") (
150mkpair (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym
151"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (
152mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (
153mkpair (mkpair (mksym "COMMON-LISP" "<") (mkpair (mkpair (mksym "COMMON-LISP"
154"QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
155mkpair (mkpair (mksym "M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (
156mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
157"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
158mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (
159mksym "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 (
162mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym
163"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1"
164"S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
165"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (mksym
166"M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "POP") (
167mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
168"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
169"M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym
170"COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))))
171,
172
173(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "DO-INST") (mkpair (
174mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
175"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
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
181"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
182mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "OP-CODE") (
183mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
184mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "ILOAD") (mksym
185"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
186"M1" "EXECUTE-ILOAD") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
187mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
188mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
189"OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
190mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "ISTORE") (mksym
191"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
192"M1" "EXECUTE-ISTORE") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
193mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
194mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
195"OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
196mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "IADD") (mksym
197"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
198"M1" "EXECUTE-IADD") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
199mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
200mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
201"OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
202mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "ISUB") (mksym
203"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
204"M1" "EXECUTE-ISUB") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
205mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
206mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
207"OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
208mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "IMUL") (mksym
209"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
210"M1" "EXECUTE-IMUL") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
211mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
212mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
213"OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
214mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "GOTO") (mksym
215"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
216"M1" "EXECUTE-GOTO") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
217mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
218mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
219"OP-CODE") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
220mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "IFLE") (mksym
221"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
222"M1" "EXECUTE-IFLE") (mkpair (mksym "M1" "INST") (mkpair (mksym "M1" "S") (
223mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
224"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (
225mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym
226"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
227"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
228,
229
230(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "STEP") (mkpair (
231mkpair (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
234"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
235,
236
237(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "RUN") (mkpair (
238mkpair (mksym "M1" "SCHED") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
239"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
240"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "SCHED") (mksym "COMMON-LISP" "NIL"))) (
241mkpair (mksym "M1" "S") (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (
242mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "SCHED") (mksym "COMMON-LISP"
243"NIL"))) (mkpair (mkpair (mksym "M1" "STEP") (mkpair (mksym "M1" "S") (mksym
244"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
245"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
246,
247
248(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "FACTORIAL-EXAMPLE-0") (
249mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
250"RUN") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mknum
251"0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0"
252"1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (
253mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1"
254"0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (
255mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum
256"0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0"
257"1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (
258mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1"
259"0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (
260mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum
261"0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0"
262"1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (
263mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1"
264"0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (
265mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum
266"0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0"
267"1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (
268mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1"
269"0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (
270mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum
271"0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0"
272"1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (
273mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1"
274"0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (
275mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum
276"0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0"
277"1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (
278mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1"
279"0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (
280mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum
281"0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0"
282"1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (
283mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1"
284"0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (
285mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum
286"0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0"
287"1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (
288mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1"
289"0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (
290mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum
291"0" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "0" "1" "0"
292"1") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (
293mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
294mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
295mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
296mkpair (mkpair (mknum "5" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mksym
297"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
298"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
299"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
300mkpair (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"
303"ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
304mkpair (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"
307"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
308mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
309mkpair (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"
312"ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
313mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
314mkpair (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"
317"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
318mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
319"COMMON-LISP" "NIL")))))))))))))))) (mksym "COMMON-LISP" "NIL"))) (mksym
320"COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
321mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mknum "14" "1" "0" "1") (mkpair (
322mkpair (mknum "0" "1" "0" "1") (mkpair (mknum "120" "1" "0" "1") (mksym
323"COMMON-LISP" "NIL"))) (mkpair (mkpair (mknum "120" "1" "0" "1") (mksym
324"COMMON-LISP" "NIL")) (mkpair (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (
325mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
326"M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
327mkpair (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"
330"ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
331mkpair (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"
335"ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
336mkpair (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"
340"GOTO") (mkpair (mknum "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
341mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym
342"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "HALT") (mksym
343"COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL")))))))))))))))) (mksym
344"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
345"NIL")))) (mksym "COMMON-LISP" "NIL"))))
346,
347
348(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFACT-LOOP-SCHED") (
349mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
350mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym
351"M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "REPEAT") (
352mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
353mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
354mkpair (mknum "4" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
355"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (
356mksym "M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
357mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
358"COMMON-LISP" "QUOTE") (mkpair (mknum "11" "1" "0" "1") (mksym "COMMON-LISP"
359"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1"
360"IFACT-LOOP-SCHED") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (
361mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1" "1" "0" "1") (mksym
362"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (
363mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
364"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
365,
366
367(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFACT-SCHED") (
368mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
369mksym "M1" "APP") (mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mkpair (
370mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym
371"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
372mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
373"NIL")))) (mkpair (mkpair (mksym "M1" "IFACT-LOOP-SCHED") (mkpair (mksym "M1"
374"N") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
375"COMMON-LISP" "NIL")))))
376,
377
378(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "!") (mkpair (
379mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
380"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym "M1"
381"N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
382"QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
383mkpair (mkpair (mksym "ACL2" "BINARY-*") (mkpair (mksym "M1" "N") (mkpair (
384mkpair (mksym "M1" "!") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
385mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1" "1" "0" "1") (mksym
386"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (
387mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
388"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
389,
390
391(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TEST-IFACT") (
392mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
393mksym "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") (
396mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
397mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
398mkpair (mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
399mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym
400"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
401mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
402"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
403"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
404mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym
405"M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
406mkpair (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"
409"IFLE") (mkpair (mknum "10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
410mkpair (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") (
414mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
415mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
416"NIL"))) (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (
417mksym "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"
420"GOTO") (mkpair (mknum "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
421mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym
422"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "HALT") (mksym
423"COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL")))))))))))))))) (mksym
424"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP"
425"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym
426"COMMON-LISP" "NIL")))))
427,
428
429(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "FACTORIAL-EXAMPLE-1") (
430mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
431"TEST-IFACT") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
432"5" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
433mkpair (mkpair (mksym "M1" "!") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
434mkpair (mknum "5" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
435"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
436"NIL"))))
437,
438
439(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "FACTORIAL-EXAMPLE-2") (
440mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
441"TEST-IFACT") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
442"1000" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
443mkpair (mkpair (mksym "M1" "!") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
444mkpair (mknum "1000" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
445"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
446"NIL"))))
447,
448
449(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EVEN-SCHED") (
450mkpair (mkpair (mksym "M1" "I") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
451mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym
452"M1" "I") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "REPEAT") (
453mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
454mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
455mkpair (mknum "4" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
456"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
457mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "I") (mkpair (mkpair (
458mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym
459"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
460"M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
461"0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
462"COMMON-LISP" "QUOTE") (mkpair (mknum "8" "1" "0" "1") (mksym "COMMON-LISP"
463"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "APP") (
464mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP"
465"QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
466mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "11" "1" "0" "1") (
467mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
468mksym "M1" "EVEN-SCHED") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
469mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-2" "1" "0" "1") (mksym
470"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "I") (mksym "COMMON-LISP" "NIL")))) (
471mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
472"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
473"NIL")))))
474,
475
476(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TEST-EVEN") (
477mkpair (mkpair (mksym "M1" "I") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
478mksym "M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym
479"M1" "RUN") (mkpair (mkpair (mksym "M1" "EVEN-SCHED") (mkpair (mksym "M1" "I") (
480mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
481mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
482mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
483mkpair (mksym "M1" "I") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
484mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
485"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
486"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
487"COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (
488mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
489"M1" "IFLE") (mkpair (mknum "12" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
490mkpair (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") (
494mkpair (mknum "6" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
495mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
496"NIL"))) (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "2" "1" "0" "1") (
497mksym "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"
500"GOTO") (mkpair (mknum "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
501mkpair (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"
505"HALT") (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL")))))))))))))))) (
506mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym
507"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
508"NIL"))) (mksym "COMMON-LISP" "NIL")))))
509,
510
511(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "TEST-EVEN-THEOREM") (
512mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
513"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "TEST-EVEN") (mkpair (
514mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "18" "1" "0" "1") (mksym
515"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
516"COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP"
517"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
518"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym
519"M1" "TEST-EVEN") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
520mknum "19" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
521"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1"
522"0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
523mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
524"EQUAL") (mkpair (mkpair (mksym "M1" "TEST-EVEN") (mkpair (mkpair (mksym
525"COMMON-LISP" "QUOTE") (mkpair (mknum "235" "1" "0" "1") (mksym "COMMON-LISP"
526"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
527"QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
528"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
529mkpair (mksym "M1" "TEST-EVEN") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
530mkpair (mknum "234" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
531"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
532mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
533"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
534"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
535mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
536"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
537mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
538mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
539"COMMON-LISP" "NIL"))))
540,
541
542(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "COLLECT-AT-END") (
543mkpair (mkpair (mksym "COMMON-LISP" "LIST") (mkpair (mksym "M1" "E") (mksym
544"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
545mkpair (mksym "M1" "MEMBER") (mkpair (mksym "M1" "E") (mkpair (mksym
546"COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym
547"COMMON-LISP" "LIST") (mkpair (mkpair (mksym "M1" "APP") (mkpair (mksym
548"COMMON-LISP" "LIST") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
549mksym "M1" "E") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
550"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
551mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym
552"COMMON-LISP" "NIL")))))
553,
554
555(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "NTH-NIL") (mkpair (
556mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "NTH") (
557mkpair (mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
558mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
559"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
560"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
561mksym "COMMON-LISP" "NIL"))))
562,
563
564(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "ACL2-COUNT-NTH") (mkpair (
565mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (
566mkpair (mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
567mkpair (mksym "COMMON-LISP" "<") (mkpair (mkpair (mksym "ACL2" "ACL2-COUNT") (
568mkpair (mkpair (mksym "M1" "NTH") (mkpair (mksym "M1" "N") (mkpair (mksym
569"COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
570"NIL"))) (mkpair (mkpair (mksym "ACL2" "ACL2-COUNT") (mkpair (mksym
571"COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
572"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
573,
574
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
578"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (
579mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
580"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "SYMBOLP") (mkpair (
581mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
582"COLLECT-AT-END") (mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "EXPR") (
583mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "VARS") (mksym
584"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-EXPR") (
585mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-EXPR") (mkpair (mksym "M1" "VARS") (
586mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP"
587"QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
588mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL")))) (mksym
589"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
590mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym
591"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL")))) (
592mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym
593"COMMON-LISP" "NIL")))))
594,
595
596(mkpair (mksym "ACL2" "MUTUAL-RECURSION") (mkpair (mkpair (mksym
597"COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "COLLECT-VARS-IN-STMT*") (mkpair (
598mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "STMT-LIST") (mksym
599"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
600mkpair (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"
605"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
606"CDR") (mkpair (mksym "M1" "STMT-LIST") (mksym "COMMON-LISP" "NIL"))) (mksym
607"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
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
611"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
612mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
613mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
614"M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
615"COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "=") (mksym "COMMON-LISP" "NIL"))) (
616mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1"
617"COLLECT-VARS-IN-EXPR") (mkpair (mkpair (mksym "M1" "COLLECT-AT-END") (mkpair (
618mksym "M1" "VARS") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym
619"COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
620"NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mksym
621"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
622mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym
623"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (
624mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
625mkpair (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
628"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
629mksym "M1" "WHILE") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
630mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-STMT*") (mkpair (mkpair (mksym
631"M1" "COLLECT-VARS-IN-EXPR") (mkpair (mksym "M1" "VARS") (mkpair (mkpair (
632mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
633mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
634"STMT") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
635mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
636mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
637"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
638"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym
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
641"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
642mksym "M1" "RETURN") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
643mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-EXPR") (mkpair (mksym "M1" "VARS") (
644mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP"
645"QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
646mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mksym
647"COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "VARS") (mksym "COMMON-LISP"
648"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (
649mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))
650,
651
652(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "OP!") (mkpair (
653mkpair (mksym "M1" "OP") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
654"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
655mksym "M1" "OP") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
656"COMMON-LISP" "+") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
657mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym
658"M1" "IADD") (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL")) (mksym
659"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
660mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "OP") (mkpair (
661mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "-") (mksym
662"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
663"COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "ISUB") (mksym
664"COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL"))) (
665mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
666"COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "OP") (mkpair (mkpair (mksym
667"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "*") (mksym "COMMON-LISP"
668"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
669"QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP"
670"NIL")) (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL"))) (mkpair (
671mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym "M1"
672"ILLEGAL") (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL")) (mksym
673"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
674"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
675,
676
677(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ILOAD!") (mkpair (
678mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "VAR") (mksym "COMMON-LISP"
679"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym
680"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
681mksym "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")))) (
684mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
685"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
686"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
687mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
688"NIL")))) (mksym "COMMON-LISP" "NIL")))))
689,
690
691(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ICONST!") (mkpair (
692mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
693"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
694mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "ICONST") (mksym
695"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
696mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
697"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
698mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
699mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
700"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
701,
702
703(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXPR!") (mkpair (
704mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP"
705"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
706"COMMON-LISP" "ATOM") (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL"))) (
707mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
708"COMMON-LISP" "SYMBOLP") (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP"
709"NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD!") (mkpair (mksym "M1" "VARS") (
710mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
711mksym "M1" "ICONST!") (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL"))) (
712mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (
713mkpair (mksym "M1" "EXPR!") (mkpair (mksym "M1" "VARS") (mkpair (mkpair (
714mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
715mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
716"EXPR") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
717mkpair (mksym "M1" "APP") (mkpair (mkpair (mksym "M1" "EXPR!") (mkpair (mksym
718"M1" "VARS") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym
719"COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP"
720"NIL"))) (mkpair (mksym "M1" "EXPR") (mksym "COMMON-LISP" "NIL")))) (mksym
721"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "OP!") (mkpair (mkpair (
722mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
723mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
724"EXPR") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym
725"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
726"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
727,
728
729(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFLE!") (mkpair (
730mkpair (mksym "M1" "OFFSET") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
731mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
732mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "IFLE") (
733mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
734mkpair (mksym "M1" "OFFSET") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
735mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
736"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
737"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
738"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
739"NIL")))))
740,
741
742(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "GOTO!") (mkpair (
743mkpair (mksym "M1" "OFFSET") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
744mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
745mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "GOTO") (
746mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
747mkpair (mksym "M1" "OFFSET") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
748mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
749"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
750"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
751"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
752"NIL")))))
753,
754
755(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "WHILE!") (mkpair (
756mkpair (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
760"COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP"
761"NIL"))) (mkpair (mkpair (mksym "M1" "LEN") (mkpair (mksym "M1" "BODY-CODE") (
762mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
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 (
766mksym "M1" "LEN") (mkpair (mksym "M1" "TEST-CODE") (mksym "COMMON-LISP" "NIL"))) (
767mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP"
768"QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
769mkpair (mkpair (mksym "M1" "LEN") (mkpair (mksym "M1" "BODY-CODE") (mksym
770"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
771"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym
772"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
773"NIL")))) (mksym "COMMON-LISP" "NIL")))))
774,
775
776(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TEST!") (mkpair (
777mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "TEST") (mksym "COMMON-LISP"
778"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
779"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
780mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym
781"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "TEST") (mksym "COMMON-LISP" "NIL")))) (
782mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" ">") (
783mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
784mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
785mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP"
786"QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
787mkpair (mksym "M1" "TEST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
788mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym
789"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
790"M1" "EXPR!") (mkpair (mksym "M1" "VARS") (mkpair (mkpair (mksym "M1" "NTH") (
791mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
792mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "TEST") (mksym "COMMON-LISP"
793"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "APP") (
794mkpair (mkpair (mksym "M1" "EXPR!") (mkpair (mksym "M1" "VARS") (mkpair (
795mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
796mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
797"M1" "TEST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
798mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (mksym "M1" "EXPR!") (
799mkpair (mksym "M1" "VARS") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
800mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym
801"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "TEST") (mksym "COMMON-LISP" "NIL")))) (
802mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
803mkpair (mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (
804mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL"))) (mksym
805"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
806"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (
807mkpair (mksym "M1" "ILLEGAL") (mksym "COMMON-LISP" "NIL")) (mksym
808"COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
809"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
810,
811
812(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ISTORE!") (mkpair (
813mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "VAR") (mksym "COMMON-LISP"
814"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym
815"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
816mksym "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")))) (
819mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
820"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
821"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
822mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
823"NIL")))) (mksym "COMMON-LISP" "NIL")))))
824,
825
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"))) (
829mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
830"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "STMT-LIST") (mksym "COMMON-LISP"
831"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
832"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
833"M1" "APP") (mkpair (mkpair (mksym "M1" "STMT!") (mkpair (mksym "M1" "VARS") (
834mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "STMT-LIST") (
835mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
836mksym "M1" "STMT*!") (mkpair (mksym "M1" "VARS") (mkpair (mkpair (mksym
837"COMMON-LISP" "CDR") (mkpair (mksym "M1" "STMT-LIST") (mksym "COMMON-LISP"
838"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
839"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
840mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "STMT!") (mkpair (mkpair (
841mksym "M1" "VARS") (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL"))) (
842mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
843"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
844mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym
845"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (
846mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "=") (mksym
847"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
848"M1" "APP") (mkpair (mkpair (mksym "M1" "EXPR!") (mkpair (mksym "M1" "VARS") (
849mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP"
850"QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
851mkpair (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
854"COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
855"NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mksym
856"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
857"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
858mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
859mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
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!") (
863mkpair (mkpair (mksym "M1" "TEST!") (mkpair (mksym "M1" "VARS") (mkpair (
864mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
865mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
866"M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
867mkpair (mkpair (mksym "M1" "STMT*!") (mkpair (mksym "M1" "VARS") (mkpair (
868mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
869mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
870"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
871mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
872"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
873mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym
874"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (
875mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1" "RETURN") (
876mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
877mksym "M1" "APP") (mkpair (mkpair (mksym "M1" "EXPR!") (mkpair (mksym "M1"
878"VARS") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (mksym
879"COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP"
880"NIL"))) (mkpair (mksym "M1" "STMT") (mksym "COMMON-LISP" "NIL")))) (mksym
881"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
882mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
883"COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
884"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (
885mkpair (mksym "M1" "ILLEGAL") (mksym "COMMON-LISP" "NIL")) (mksym
886"COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
887"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (
888mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))
889,
890
891(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "COMPILE") (mkpair (
892mkpair (mksym "M1" "FORMALS") (mkpair (mksym "M1" "STMT-LIST") (mksym
893"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "STMT*!") (mkpair (mkpair (
894mksym "M1" "COLLECT-VARS-IN-STMT*") (mkpair (mksym "M1" "FORMALS") (mkpair (
895mksym "M1" "STMT-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1"
896"STMT-LIST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
897,
898
899(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-COMPILATION-1") (
900mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
901"COMPILE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (
902mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL"))) (
903mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym
904"M1" "A") (mkpair (mksym "M1" "=") (mkpair (mknum "1" "1" "0" "1") (mksym
905"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "WHILE") (mkpair (mkpair (
906mksym "M1" "N") (mkpair (mksym "COMMON-LISP" ">") (mkpair (mknum "0" "1" "0"
907"1") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "A") (mkpair (
908mksym "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" "-") (
912mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL")))) (mksym
913"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
914mksym "M1" "RETURN") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
915mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym
916"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
917mkpair (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"
920"ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
921mkpair (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"
924"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
925mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
926mkpair (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"
929"ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
930mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
931mkpair (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"
934"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
935mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
936"COMMON-LISP" "NIL")))))))))))))))) (mksym "COMMON-LISP" "NIL"))) (mksym
937"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
938,
939
940(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-COMPILATION-2") (
941mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
942"COMPILE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (
943mksym "M1" "N") (mkpair (mksym "M1" "K") (mksym "COMMON-LISP" "NIL"))) (mksym
944"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
945mkpair (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" ">") (
948mkpair (mksym "M1" "K") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
949"M1" "A") (mkpair (mksym "M1" "=") (mkpair (mkpair (mksym "M1" "A") (mkpair (
950mksym "COMMON-LISP" "+") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP"
951"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "N") (
952mkpair (mksym "M1" "=") (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym
953"COMMON-LISP" "-") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL")))) (
954mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
955mksym "M1" "RETURN") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
956mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym
957"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
958mkpair (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"
961"ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
962mkpair (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"
966"ILOAD") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
967mkpair (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"
971"ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
972mkpair (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"
976"GOTO") (mkpair (mknum "-12" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
977mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "2" "1" "0" "1") (mksym
978"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "HALT") (mksym
979"COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL")))))))))))))))))) (mksym
980"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
981"NIL"))))
982,
983
984(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-EXECUTION-1") (
985mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
986"TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "M1" "RUN") (
987mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP"
988"QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
989mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1000" "1" "0"
990"1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
991mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
992mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
993mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mknum "5" "1" "0" "1") (mkpair (
994mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
995"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
996"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
997"M1" "COMPILE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (
998mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL"))) (
999mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym
1000"M1" "A") (mkpair (mksym "M1" "=") (mkpair (mknum "1" "1" "0" "1") (mksym
1001"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "WHILE") (mkpair (mkpair (
1002mksym "M1" "N") (mkpair (mksym "COMMON-LISP" ">") (mkpair (mknum "0" "1" "0"
1003"1") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "A") (mkpair (
1004mksym "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" "-") (
1008mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL")))) (mksym
1009"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
1010mksym "M1" "RETURN") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
1011mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym
1012"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP"
1013"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
1014mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "120" "1" "0" "1") (mksym
1015"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1016"NIL"))))
1017,
1018
1019(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-EXECUTION-2") (
1020mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1021"TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "M1" "RUN") (
1022mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP"
1023"QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1024mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1000" "1" "0"
1025"1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
1026mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1027mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1028mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mknum "10" "1" "0" "1") (mkpair (
1029mknum "4" "1" "0" "1") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
1030"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
1031"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
1032mkpair (mkpair (mksym "M1" "COMPILE") (mkpair (mkpair (mksym "COMMON-LISP"
1033"QUOTE") (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "M1" "K") (mksym
1034"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1035"COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "A") (mkpair (
1036mksym "M1" "=") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL")))) (
1037mkpair (mkpair (mksym "M1" "WHILE") (mkpair (mkpair (mksym "M1" "N") (mkpair (
1038mksym "COMMON-LISP" ">") (mkpair (mksym "M1" "K") (mksym "COMMON-LISP" "NIL")))) (
1039mkpair (mkpair (mksym "M1" "A") (mkpair (mksym "M1" "=") (mkpair (mkpair (
1040mksym "M1" "A") (mkpair (mksym "COMMON-LISP" "+") (mkpair (mknum "1" "1" "0"
1041"1") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
1042mkpair (mksym "M1" "N") (mkpair (mksym "M1" "=") (mkpair (mkpair (mksym "M1"
1043"N") (mkpair (mksym "COMMON-LISP" "-") (mkpair (mknum "1" "1" "0" "1") (mksym
1044"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1045"NIL"))))) (mkpair (mkpair (mksym "M1" "RETURN") (mkpair (mksym "M1" "A") (
1046mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
1047"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1048"NIL")))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (
1049mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1050mkpair (mknum "6" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
1051"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
1052,
1053
1054(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "STACKS") (mkpair (mkpair (
1055mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
1056mkpair (mkpair (mksym "M1" "TOP") (mkpair (mkpair (mksym "M1" "PUSH") (mkpair (
1057mksym "M1" "X") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (
1058mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "X") (mksym "COMMON-LISP"
1059"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
1060"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (
1061mksym "M1" "PUSH") (mkpair (mksym "M1" "X") (mkpair (mksym "M1" "S") (mksym
1062"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (
1063mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
1064mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1065"TOP") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "X") (
1066mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1067"NIL"))) (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (
1068mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "POP") (
1069mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "X") (mkpair (
1070mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (
1071mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1072"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1073"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1074"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1075"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1076"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1077"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
1078"NIL"))))
1079,
1080
1081(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "STATES") (mkpair (mkpair (
1082mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
1083mkpair (mkpair (mksym "M1" "PC") (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
1084mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "LOCALS") (mkpair (mksym "M1"
1085"STACK") (mkpair (mksym "M1" "PROGRAM") (mksym "COMMON-LISP" "NIL")))))) (
1086mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "PC") (mksym "COMMON-LISP"
1087"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
1088"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (mkpair (
1089mksym "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"
1092"LOCALS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
1093"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym
1094"M1" "STACK") (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mksym "M1"
1095"PC") (mkpair (mksym "M1" "LOCALS") (mkpair (mksym "M1" "STACK") (mkpair (
1096mksym "M1" "PROGRAM") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP"
1097"NIL"))) (mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" "NIL")))) (mkpair (
1098mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
1099"EQUAL") (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mkpair (mksym "M1"
1100"MAKE-STATE") (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "LOCALS") (mkpair (
1101mksym "M1" "STACK") (mkpair (mksym "M1" "PROGRAM") (mksym "COMMON-LISP" "NIL")))))) (
1102mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "PROGRAM") (mksym
1103"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
1104mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "PC") (
1105mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "PC") (mkpair (
1106mksym "M1" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (
1107mkpair (mksym "M1" "PC") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
1108mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
1109mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (mkpair (mksym "COMMON-LISP"
1110"CONS") (mkpair (mksym "M1" "PC") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
1111mkpair (mksym "M1" "LOCALS") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP"
1112"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (
1113mkpair (mksym "M1" "LOCALS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
1114mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
1115mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "COMMON-LISP"
1116"CONS") (mkpair (mksym "M1" "PC") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
1117mkpair (mksym "M1" "LOCALS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
1118mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP"
1119"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
1120mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STACK") (mksym
1121"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
1122mkpair (mksym "M1" "PROGRAM") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
1123mkpair (mksym "M1" "PC") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1124mksym "M1" "LOCALS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1125mksym "M1" "STACK") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1126mksym "M1" "PROGRAM") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")))) (
1127mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
1128"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
1129"PROGRAM") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1130"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1131"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1132"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1133"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1134"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1135"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1136"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1137"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1138"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1139"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1140"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1141"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1142"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1143"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
1144"NIL"))))
1145,
1146
1147(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "STEP-OPENER") (mkpair (
1148mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (
1149mkpair (mkpair (mksym "M1" "NEXT-INST") (mkpair (mksym "M1" "S") (mksym
1150"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (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") (
1153mkpair (mkpair (mksym "M1" "NEXT-INST") (mkpair (mksym "M1" "S") (mksym
1154"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (
1155mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
1156"COMMON-LISP" "NIL"))))
1157,
1158
1159(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "RUN-APP") (mkpair (
1160mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "RUN") (
1161mkpair (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 (
1165mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
1166mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
1167,
1168
1169(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "RUN-OPENER") (mkpair (
1170mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
1171"EQUAL") (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (mksym
1172"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1173"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (
1174mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1175"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (
1176mksym "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") (
1180mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
1181"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1182mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
1183"NIL"))))) (mksym "COMMON-LISP" "NIL"))))
1184,
1185
1186(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "NTH-ADD1!") (mkpair (
1187mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (
1188mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1189"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "NTH") (mkpair (mkpair (
1190mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1191mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
1192"M1" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "COMMON-LISP" "LIST") (
1193mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "NTH") (mkpair (
1194mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
1195"COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
1196"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
1197mksym "COMMON-LISP" "NIL"))))
1198,
1199
1200(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "NTH-UPDATE-NTH") (mkpair (
1201mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
1202mkpair (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"
1205"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
1206mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
1207mkpair (mkpair (mksym "M1" "NTH") (mkpair (mksym "M1" "I") (mkpair (mkpair (
1208mksym "M1" "UPDATE-NTH") (mkpair (mksym "M1" "J") (mkpair (mksym "M1" "V") (
1209mkpair (mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))))) (mksym
1210"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
1211mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "I") (mkpair (mksym
1212"M1" "J") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "V") (mkpair (
1213mkpair (mksym "M1" "NTH") (mkpair (mksym "M1" "I") (mkpair (mksym
1214"COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1215"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
1216mksym "COMMON-LISP" "NIL"))))
1217,
1218
1219(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "UPDATE-NTH-UPDATE-NTH-1") (
1220mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP"
1221"IF") (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (mksym "M1" "I") (mksym
1222"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
1223mkpair (mksym "ACL2" "NATP") (mkpair (mksym "M1" "J") (mksym "COMMON-LISP"
1224"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym
1225"COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "I") (mkpair (mksym "M1" "J") (
1226mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1227mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1228"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1229"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1230"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1231"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (mkpair (
1232mksym "M1" "I") (mkpair (mksym "M1" "V") (mkpair (mkpair (mksym "M1"
1233"UPDATE-NTH") (mkpair (mksym "M1" "J") (mkpair (mksym "M1" "W") (mkpair (
1234mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))))) (mksym
1235"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (mkpair (
1236mksym "M1" "J") (mkpair (mksym "M1" "W") (mkpair (mkpair (mksym "M1"
1237"UPDATE-NTH") (mkpair (mksym "M1" "I") (mkpair (mksym "M1" "V") (mkpair (
1238mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))))) (mksym
1239"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1240"NIL")))) (mksym "COMMON-LISP" "NIL"))))
1241,
1242
1243(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "UPDATE-NTH-UPDATE-NTH-2") (
1244mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1245"UPDATE-NTH") (mkpair (mksym "M1" "I") (mkpair (mksym "M1" "V") (mkpair (
1246mkpair (mksym "M1" "UPDATE-NTH") (mkpair (mksym "M1" "I") (mkpair (mksym "M1"
1247"W") (mkpair (mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))))) (
1248mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (
1249mkpair (mksym "M1" "I") (mkpair (mksym "M1" "V") (mkpair (mksym "COMMON-LISP"
1250"LIST") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym
1251"COMMON-LISP" "NIL"))))
1252,
1253
1254(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "!") (mkpair (
1255mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
1256"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym "M1"
1257"N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
1258"QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1259mkpair (mkpair (mksym "ACL2" "BINARY-*") (mkpair (mksym "M1" "N") (mkpair (
1260mkpair (mksym "M1" "!") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
1261mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1" "1" "0" "1") (mksym
1262"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (
1263mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
1264"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
1265,
1266
1267(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFACT") (mkpair (
1268mkpair (mksym "M1" "N") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
1269mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (
1270mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "A") (
1271mkpair (mkpair (mksym "M1" "IFACT") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (
1272mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1" "1" "0" "1") (
1273mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP"
1274"NIL")))) (mkpair (mkpair (mksym "ACL2" "BINARY-*") (mkpair (mksym "M1" "N") (
1275mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1276"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
1277,
1278
1279(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFACT-LOOP-SCHED") (
1280mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
1281mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym
1282"M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "REPEAT") (
1283mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
1284mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1285mkpair (mknum "4" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
1286"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (
1287mksym "M1" "REPEAT") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1288mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1289"COMMON-LISP" "QUOTE") (mkpair (mknum "11" "1" "0" "1") (mksym "COMMON-LISP"
1290"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1"
1291"IFACT-LOOP-SCHED") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (
1292mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1" "1" "0" "1") (mksym
1293"COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (
1294mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
1295"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
1296,
1297
1298(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "IFACT-SCHED") (
1299mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
1300mksym "M1" "APP") (mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mkpair (
1301mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym
1302"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1303mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
1304"NIL")))) (mkpair (mkpair (mksym "M1" "IFACT-LOOP-SCHED") (mkpair (mksym "M1"
1305"N") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
1306"COMMON-LISP" "NIL")))))
1307,
1308
1309(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TEST-IFACT") (
1310mkpair (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
1311mksym "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") (
1314mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
1315mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
1316mkpair (mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1317mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym
1318"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1319mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
1320"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
1321"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
1322mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym
1323"M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1324mkpair (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"
1327"IFLE") (mkpair (mknum "10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1328mkpair (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") (
1332mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1333mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
1334"NIL"))) (mkpair (mkpair (mksym "M1" "ICONST") (mkpair (mknum "1" "1" "0" "1") (
1335mksym "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"
1338"GOTO") (mkpair (mknum "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1339mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym
1340"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "HALT") (mksym
1341"COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL")))))))))))))))) (mksym
1342"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP"
1343"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym
1344"COMMON-LISP" "NIL")))))
1345,
1346
1347(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "TEST-IFACT-EXAMPLES") (
1348mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
1349"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "TEST-IFACT") (mkpair (
1350mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "5" "1" "0" "1") (mksym
1351"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1352"M1" "!") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "5"
1353"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
1354mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
1355mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1356"TEST-IFACT") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
1357"10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
1358mkpair (mkpair (mksym "M1" "!") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1359mkpair (mknum "10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
1360"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1361"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "TEST-IFACT") (mkpair (
1362mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "100" "1" "0" "1") (mksym
1363"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1364"M1" "!") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "100"
1365"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
1366mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1367mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
1368"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1369mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
1370"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))
1371,
1372
1373(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "IFACT-LOOP-LEMMA") (
1374mkpair (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"
1378"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
1379mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
1380mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (mksym "M1"
1381"IFACT-LOOP-SCHED") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
1382mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP"
1383"QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1384mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "N") (mkpair (
1385mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "A") (mkpair (mkpair (
1386mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1387"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
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") (
1391mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1392mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
1393"NIL"))) (mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10" "1" "0" "1") (
1394mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (
1395mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1396"M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1397mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1398mkpair (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"
1401"ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1402mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1403mkpair (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"
1406"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1407mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1408"COMMON-LISP" "NIL")))))))))))))))) (mksym "COMMON-LISP" "NIL"))) (mksym
1409"COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
1410mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1411mkpair (mknum "14" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1412mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1413mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1414mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "M1" "IFACT") (mkpair (
1415mksym "M1" "N") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (
1416mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
1417"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
1418"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PUSH") (mkpair (mkpair (
1419mksym "M1" "IFACT") (mkpair (mksym "M1" "N") (mkpair (mksym "M1" "A") (mksym
1420"COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP"
1421"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (
1422mkpair (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"
1425"ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1426mkpair (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"
1429"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1430mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1431mkpair (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"
1434"ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1435mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1436mkpair (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"
1439"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1440mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1441"COMMON-LISP" "NIL")))))))))))))))) (mksym "COMMON-LISP" "NIL"))) (mksym
1442"COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1443"NIL")))) (mksym "COMMON-LISP" "NIL"))))
1444,
1445
1446(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "IFACT-LEMMA") (mkpair (
1447mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (
1448mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1449"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (
1450mksym "M1" "IFACT-SCHED") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
1451mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP"
1452"QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1453mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "N") (mkpair (
1454mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "A") (mkpair (mkpair (
1455mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1456"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
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") (
1460mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1461mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
1462"NIL"))) (mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10" "1" "0" "1") (
1463mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (
1464mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1465"M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1466mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1467mkpair (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"
1470"ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1471mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1472mkpair (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"
1475"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1476mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1477"COMMON-LISP" "NIL")))))))))))))))) (mksym "COMMON-LISP" "NIL"))) (mksym
1478"COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
1479mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1480mkpair (mknum "14" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1481mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1482mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1483mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "M1" "IFACT") (mkpair (
1484mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum
1485"1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
1486mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
1487"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
1488"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PUSH") (mkpair (mkpair (
1489mksym "M1" "IFACT") (mkpair (mksym "M1" "N") (mkpair (mkpair (mksym
1490"COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP"
1491"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "STACK") (mksym
1492"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1493mkpair (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"
1496"ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1497mkpair (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"
1500"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1501mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1502mkpair (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"
1505"ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1506mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1507mkpair (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"
1510"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1511mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1512"COMMON-LISP" "NIL")))))))))))))))) (mksym "COMMON-LISP" "NIL"))) (mksym
1513"COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1514"NIL")))) (mksym "COMMON-LISP" "NIL"))))
1515,
1516
1517(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "IFACT-IS-FACTORIAL") (
1518mkpair (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"
1522"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
1523mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
1524mkpair (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")))) (
1528mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
1529"COMMON-LISP" "NIL"))))
1530,
1531
1532(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "IFACT-CORRECT") (mkpair (
1533mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "NATP") (mkpair (
1534mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1535"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1" "RUN") (mkpair (mkpair (
1536mksym "M1" "IFACT-SCHED") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
1537mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP"
1538"QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1539mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "N") (mkpair (
1540mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "A") (mkpair (mkpair (
1541mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1542"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
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") (
1546mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1547mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
1548"NIL"))) (mkpair (mkpair (mksym "M1" "IFLE") (mkpair (mknum "10" "1" "0" "1") (
1549mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (
1550mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1551"M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1552mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1553mkpair (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"
1556"ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1557mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1558mkpair (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"
1561"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1562mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1563"COMMON-LISP" "NIL")))))))))))))))) (mksym "COMMON-LISP" "NIL"))) (mksym
1564"COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
1565mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1566mkpair (mknum "14" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1567mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1568mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1569mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "M1" "!") (mkpair (mksym
1570"M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
1571"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
1572mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
1573mksym "M1" "PUSH") (mkpair (mkpair (mksym "M1" "!") (mkpair (mksym "M1" "N") (
1574mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "STACK") (mksym
1575"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1576mkpair (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"
1579"ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1580mkpair (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"
1583"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1584mkpair (mkpair (mksym "M1" "IMUL") (mksym "COMMON-LISP" "NIL")) (mkpair (
1585mkpair (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"
1588"ICONST") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1589mkpair (mkpair (mksym "M1" "ISUB") (mksym "COMMON-LISP" "NIL")) (mkpair (
1590mkpair (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"
1593"ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1594mkpair (mkpair (mksym "M1" "HALT") (mksym "COMMON-LISP" "NIL")) (mksym
1595"COMMON-LISP" "NIL")))))))))))))))) (mksym "COMMON-LISP" "NIL"))) (mksym
1596"COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1597"NIL")))) (mksym "COMMON-LISP" "NIL"))))
1598,
1599
1600(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1"
1601"IFACT-CORRECT-COROLLARY-1") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
1602mkpair (mksym "ACL2" "NATP") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP"
1603"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym
1604"M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "M1"
1605"RUN") (mkpair (mkpair (mksym "M1" "IFACT-SCHED") (mkpair (mksym "M1" "N") (
1606mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
1607mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
1608mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
1609mkpair (mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1610mksym "M1" "A") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
1611"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
1612mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "STACK") (mkpair (mkpair (
1613mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mkpair (mksym "M1" "ICONST") (
1614mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1615mksym "M1" "ISTORE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP"
1616"NIL"))) (mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (
1617mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "IFLE") (mkpair (
1618mknum "10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1619"M1" "ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1620mkpair (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"
1624"ILOAD") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1625mkpair (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"
1629"GOTO") (mkpair (mknum "-10" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
1630mkpair (mkpair (mksym "M1" "ILOAD") (mkpair (mknum "1" "1" "0" "1") (mksym
1631"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "HALT") (mksym
1632"COMMON-LISP" "NIL")) (mksym "COMMON-LISP" "NIL")))))))))))))))) (mksym
1633"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP"
1634"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
1635mkpair (mksym "M1" "!") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
1636mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
1637"COMMON-LISP" "NIL"))))
1638,
1639
1640(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1"
1641"IFACT-CORRECT-COROLLARY-2") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
1642mkpair (mksym "ACL2" "NATP") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP"
1643"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym
1644"M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mkpair (mksym "M1"
1645"RUN") (mkpair (mkpair (mksym "M1" "IFACT-SCHED") (mkpair (mksym "M1" "N") (
1646mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (
1647mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
1648mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
1649mkpair (mksym "M1" "N") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
1650mksym "M1" "A") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
1651"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
1652mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "STACK") (mkpair (mkpair (
1653mksym "M1" "COMPILE") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1654mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")) (mksym "COMMON-LISP"
1655"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (
1656mkpair (mksym "M1" "A") (mkpair (mksym "M1" "=") (mkpair (mknum "1" "1" "0"
1657"1") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "WHILE") (
1658mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP" ">") (mkpair (
1659mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1660"M1" "A") (mkpair (mksym "M1" "=") (mkpair (mkpair (mksym "M1" "N") (mkpair (
1661mksym "COMMON-LISP" "*") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (
1662mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym
1663"M1" "=") (mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP" "-") (
1664mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL")))) (mksym
1665"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
1666mksym "M1" "RETURN") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
1667mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym
1668"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP"
1669"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
1670mkpair (mksym "M1" "!") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
1671mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
1672"COMMON-LISP" "NIL"))))
1673,
1674
1675(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-MODIFY-1") (
1676mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1677"MAKE-STATE") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (
1678mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym
1679"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1"
1680"S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
1681mkpair (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 (
1684mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1685"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "PROGRAM") (
1686mkpair (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 (
1689mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
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") (
1693mkpair (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")))) (
1696mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym
1697"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP"
1698"NIL")))) (mksym "COMMON-LISP" "NIL"))))
1699,
1700
1701(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-MODIFY-2") (
1702mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1703"MAKE-STATE") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (
1704mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym
1705"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1"
1706"S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
1707mkpair (mksym "M1" "UPDATE-NTH") (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (
1708mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1709"TOP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym
1710"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1711"M1" "LOCALS") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym
1712"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "POP") (mkpair (mkpair (
1713mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
1714mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (
1715mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (
1716mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "ACL2"
1717"BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1"
1718"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PC") (
1719mkpair (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"))) (
1722mkpair (mkpair (mksym "M1" "TOP") (mkpair (mkpair (mksym "M1" "STACK") (
1723mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
1724"NIL"))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (mksym "M1" "S") (
1725mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
1726mksym "M1" "POP") (mkpair (mkpair (mksym "M1" "STACK") (mkpair (mksym "M1"
1727"S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
1728mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1729"NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) (
1730mksym "COMMON-LISP" "NIL"))))
1731,
1732
1733(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-MODIFY-3") (
1734mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "M1"
1735"MAKE-STATE") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (
1736mksym "M1" "ARG1") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL"))) (
1737mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym
1738"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1739"M1" "LOCALS") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (
1740mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1741"NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (
1742mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (
1743mksym "M1" "MAKE-STATE") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
1744mkpair (mksym "M1" "ARG1") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP"
1745"NIL"))) (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym
1746"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1747"M1" "LOCALS") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (
1748mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1749"NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (
1750mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym
1751"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
1752,
1753
1754(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PATTERN-BINDINGS") (
1755mkpair (mkpair (mksym "M1" "VARS") (mkpair (mksym "M1" "ARG-EXPRESSIONS") (
1756mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
1757mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "VARS") (
1758mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1759mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (
1760mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP"
1761"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1"
1762"VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
1763"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1"
1764"ARG-EXPRESSIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1765"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1766"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1767"NIL")))) (mkpair (mkpair (mksym "M1" "PATTERN-BINDINGS") (mkpair (mkpair (
1768mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "VARS") (mksym "COMMON-LISP"
1769"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1"
1770"ARG-EXPRESSIONS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
1771mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym
1772"COMMON-LISP" "NIL")))))
1773,
1774
1775(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "M1" "EXAMPLE-SEMANTICS-1") (
1776mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mkpair (mksym
1777"COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "M1" "C") (mkpair (mksym "M1"
1778"-PC-") (mkpair (mksym "M1" "-LOCALS-") (mkpair (mksym "M1" "-STACK-") (
1779mkpair (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 (
1782mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
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") (
1786mkpair (mksym "M1" "C") (mkpair (mksym "M1" "-STACK-") (mksym "COMMON-LISP"
1787"NIL")))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (
1788mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym
1789"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (mksym
1790"M1" "INST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PC") (
1791mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1792"M1" "LOCALS") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (
1793mkpair (mksym "M1" "STACK") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1794"NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (
1795mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym "COMMON-LISP"
1796"NIL")))))))) (mkpair (mkpair (mksym "M1" "MAKE-STATE") (mkpair (mkpair (
1797mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1798mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1799mksym "M1" "PC") (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (
1800mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "LOCALS") (mkpair (
1801mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1"
1802"PUSH") (mkpair (mkpair (mksym "M1" "ARG1") (mkpair (mksym "M1" "INST") (
1803mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "STACK") (mkpair (
1804mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
1805mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (mksym "M1" "S") (mksym
1806"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP"
1807"NIL")))) (mksym "COMMON-LISP" "NIL"))))
1808,
1809
1810(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "CONCAT-SYMBOLS") (
1811mkpair (mkpair (mksym "M1" "PART1") (mkpair (mksym "M1" "PART2") (mksym
1812"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
1813"INTERN-IN-PACKAGE-OF-SYMBOL") (mkpair (mkpair (mksym "COMMON-LISP" "COERCE") (
1814mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (mksym "COMMON-LISP"
1815"COERCE") (mkpair (mkpair (mksym "COMMON-LISP" "SYMBOL-NAME") (mkpair (mksym
1816"M1" "PART1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1817"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "LIST") (mksym
1818"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1819"COMMON-LISP" "COERCE") (mkpair (mkpair (mksym "COMMON-LISP" "SYMBOL-NAME") (
1820mkpair (mksym "M1" "PART2") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1821mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "LIST") (mksym
1822"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1823"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
1824"COMMON-LISP" "STRING") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
1825"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "M1"
1826"RUN") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
1827"COMMON-LISP" "NIL")))))
1828,
1829
1830(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "MAKE-DEFUN") (
1831mkpair (mkpair (mksym "M1" "NAME") (mkpair (mksym "M1" "ARGS") (mkpair (mksym
1832"M1" "DCL") (mkpair (mksym "M1" "BODY") (mksym "COMMON-LISP" "NIL"))))) (
1833mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mksym "M1" "DCL") (mkpair (
1834mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP"
1835"QUOTE") (mkpair (mksym "COMMON-LISP" "DEFUN") (mksym "COMMON-LISP" "NIL"))) (
1836mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "NAME") (
1837mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "ARGS") (
1838mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "DCL") (
1839mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "BODY") (
1840mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
1841"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
1842"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1843"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
1844"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
1845"COMMON-LISP" "DEFUN") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
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
1849"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1850"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1851"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
1852mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
1853
1854];
1855