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" "PUSH") (mkpair (
9mkpair (mksym "M1" "X") (mkpair (mksym "M1" "Y") (mksym "COMMON-LISP" "NIL"))) (
10mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "X") (mkpair (
11mksym "M1" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
12,
13
14(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TOP") (mkpair (
15mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
16mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP"
17"NIL"))) (mksym "COMMON-LISP" "NIL")))))
18,
19
20(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "POP") (mkpair (
21mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
22mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP"
23"NIL"))) (mksym "COMMON-LISP" "NIL")))))
24,
25
26(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NTH") (mkpair (
27mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP" "LIST") (mksym
28"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
29mkpair (mksym "ACL2" "ZP") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP"
30"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym
31"COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
32"M1" "NTH") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym
33"COMMON-LISP" "QUOTE") (mkpair (mknum "-1" "1" "0" "1") (mksym "COMMON-LISP"
34"NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (
35mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "COMMON-LISP" "LIST") (
36mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
37"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
38,
39
40(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "MAKE-STATE") (
41mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "LOCALS") (mkpair (mksym
42"M1" "STACK") (mkpair (mksym "M1" "PROGRAM") (mksym "COMMON-LISP" "NIL"))))) (
43mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "PC") (mkpair (
44mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "LOCALS") (mkpair (
45mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "STACK") (mkpair (
46mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "PROGRAM") (mkpair (
47mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
48mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
49"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
50"NIL")))) (mksym "COMMON-LISP" "NIL")))))
51,
52
53(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PC") (mkpair (
54mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
55"M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0"
56"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym
57"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
58,
59
60(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "LOCALS") (mkpair (
61mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
62"M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1"
63"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym
64"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
65,
66
67(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "STACK") (mkpair (
68mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
69"M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2"
70"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym
71"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
72,
73
74(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PROGRAM") (mkpair (
75mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
76"M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "3"
77"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym
78"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
79,
80
81(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "OP-CODE") (mkpair (
82mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
83mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP"
84"NIL"))) (mksym "COMMON-LISP" "NIL")))))
85,
86
87(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ARG1") (mkpair (
88mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
89mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
90mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
91"INST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
92,
93
94(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ARG2") (mkpair (
95mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
96mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
97mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
98"INST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
99,
100
101(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ARG3") (mkpair (
102mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
103mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
104mknum "3" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
105"INST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
106,
107
108(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "LEN") (mkpair (
109mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
110"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
111mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
112"COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
113"NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym
114"COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP"
115"NIL"))) (mkpair (mkpair (mksym "M1" "LEN") (mkpair (mkpair (mksym
116"COMMON-LISP" "CDR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (
117mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
118"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
119,
120
121(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "APP") (mkpair (
122mkpair (mksym "M1" "X") (mkpair (mksym "M1" "Y") (mksym "COMMON-LISP" "NIL"))) (
123mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
124"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (
125mkpair (mksym "M1" "Y") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
126mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "X") (mksym
127"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (
128mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP"
129"NIL"))) (mkpair (mksym "M1" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym
130"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
131"NIL")))))
132,
133
134(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "REV") (mkpair (
135mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
136"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
137mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
138"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
139"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair (
140mksym "M1" "REV") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
141"M1" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
142mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP"
143"CAR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
144mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
145"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
146"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
147,
148
149(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "REV1") (mkpair (
150mkpair (mksym "M1" "X") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) (
151mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
152"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (
153mkpair (mksym "M1" "A") (mkpair (mkpair (mksym "M1" "REV1") (mkpair (mkpair (
154mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP"
155"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym
156"COMMON-LISP" "CAR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (
157mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
158"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
159,
160
161(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "FREV") (mkpair (
162mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
163"M1" "REV1") (mkpair (mksym "M1" "X") (mkpair (mkpair (mksym "COMMON-LISP"
164"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
165mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
166,
167
168(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "REPEAT") (mkpair (
169mkpair (mksym "M1" "TH") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
170mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (
171mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
172"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
173"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
174mksym "M1" "TH") (mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mksym "M1"
175"TH") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym
176"COMMON-LISP" "QUOTE") (mkpair (mknum "-1" "1" "0" "1") (mksym "COMMON-LISP"
177"NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym
178"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
179"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
180,
181
182(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "POPN") (mkpair (
183mkpair (mksym "M1" "N") (mkpair (mksym "M1" "STK") (mksym "COMMON-LISP" "NIL"))) (
184mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (
185mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
186"STK") (mkpair (mkpair (mksym "M1" "POPN") (mkpair (mkpair (mksym "ACL2"
187"BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1"
188"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym
189"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "POP") (mkpair (mksym
190"M1" "STK") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
191mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
192,
193
194(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "UPDATE-NTH") (
195mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "M1" "V") (mkpair (mksym
196"COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
197"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym "M1"
198"N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
199"CONS") (mkpair (mksym "M1" "V") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
200mkpair (mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (mksym
201"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
202mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "COMMON-LISP" "LIST") (
203mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") (
204mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP"
205"QUOTE") (mkpair (mknum "-1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
206mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1"
207"V") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "COMMON-LISP"
208"LIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
209"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
210"NIL")))))
211,
212
213(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "MEMBER") (mkpair (
214mkpair (mksym "M1" "E") (mkpair (mksym "COMMON-LISP" "LIST") (mksym
215"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
216mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "COMMON-LISP" "LIST") (
217mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
218mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (
219mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
220"EQUAL") (mkpair (mksym "M1" "E") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
221mkpair (mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (mksym
222"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
223mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
224"M1" "MEMBER") (mkpair (mksym "M1" "E") (mkpair (mkpair (mksym "COMMON-LISP"
225"CDR") (mkpair (mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (
226mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym
227"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
228,
229
230(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "INDEX") (mkpair (
231mkpair (mksym "M1" "E") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (
232mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
233"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (
234mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
235mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
236mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "E") (mkpair (
237mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "LST") (mksym
238"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
239"COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
240"NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym
241"COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP"
242"NIL"))) (mkpair (mkpair (mksym "M1" "INDEX") (mkpair (mksym "M1" "E") (
243mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "LST") (mksym
244"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
245"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (
246mksym "COMMON-LISP" "NIL")))))
247,
248
249(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "SUPPLIEDP") (
250mkpair (mkpair (mksym "M1" "KEY") (mkpair (mksym "M1" "ARGS") (mksym
251"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
252mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ARGS") (mksym
253"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
254mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
255mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
256mkpair (mksym "M1" "KEY") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
257mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
258mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (
259mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "SUPPLIEDP") (mkpair (
260mksym "M1" "KEY") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (
261mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP"
262"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
263"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
264"NIL")))))
265,
266
267(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ACTUAL") (mkpair (
268mkpair (mksym "M1" "KEY") (mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP"
269"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
270"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) (
271mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
272"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
273"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "KEY") (
274mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "ARGS") (mksym
275"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
276"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
277mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
278mkpair (mkpair (mksym "M1" "ACTUAL") (mkpair (mksym "M1" "KEY") (mkpair (
279mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
280mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
281"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (
282mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
283,
284
285(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "BOUNDP") (mkpair (
286mkpair (mksym "M1" "VAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP"
287"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
288"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (
289mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
290"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
291"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "VAR") (
292mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym
293"COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (
294mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
295mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym
296"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "BOUNDP") (mkpair (mksym
297"M1" "VAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1"
298"ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
299"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
300"NIL")))))
301,
302
303(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "BINDING") (mkpair (
304mkpair (mksym "M1" "VAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP"
305"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
306"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (
307mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
308"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
309"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "VAR") (
310mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym
311"COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (
312mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
313mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
314mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") (
315mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym
316"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "BINDING") (mkpair (mksym
317"M1" "VAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1"
318"ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
319"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
320"NIL")))))
321,
322
323(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "BIND") (mkpair (
324mkpair (mksym "M1" "VAR") (mkpair (mksym "M1" "VAL") (mkpair (mksym "M1"
325"ALIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
326"IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "M1"
327"ALIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
328"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1"
329"VAR") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "VAL") (
330mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
331"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
332"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
333mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
334"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
335"COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "VAR") (mkpair (mkpair (mksym
336"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
337mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
338mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
339mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "VAR") (
340mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "VAL") (
341mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
342"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
343"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
344mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
345mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym
346"COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (
347mkpair (mkpair (mksym "M1" "BIND") (mkpair (mksym "M1" "VAR") (mkpair (mksym
348"M1" "VAL") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1"
349"ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
350"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
351"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
352,
353
354(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "U-FIX") (mkpair (
355mkpair (mksym "M1" "X") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
356mkpair (mkpair (mksym "COMMON-LISP" "MOD") (mkpair (mksym "M1" "X") (mkpair (
357mkpair (mksym "COMMON-LISP" "EXPT") (mkpair (mkpair (mksym "COMMON-LISP"
358"QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (
359mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
360"NIL")))) (mksym "COMMON-LISP" "NIL")))))
361,
362
363(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "S-FIX") (mkpair (
364mkpair (mksym "M1" "X") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (
365mkpair (mkpair (mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym
366"M1" "TEMP") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (
367mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "<") (
368mkpair (mksym "M1" "TEMP") (mkpair (mkpair (mksym "COMMON-LISP" "EXPT") (
369mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (
370mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") (
371mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1" "1" "0" "1") (
372mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP"
373"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
374mkpair (mksym "M1" "TEMP") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
375mksym "M1" "TEMP") (mkpair (mkpair (mksym "ACL2" "UNARY--") (mkpair (mkpair (
376mksym "COMMON-LISP" "EXPT") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
377mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
378"M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym
379"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
380"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "MOD") (mkpair (mksym "M1" "X") (
381mkpair (mkpair (mksym "COMMON-LISP" "EXPT") (mkpair (mkpair (mksym
382"COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP"
383"NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym
384"COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (
385mksym "COMMON-LISP" "NIL")))))
386,
387
388(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "U-BIG1") (mkpair (
389mkpair (mksym "M1" "LST") (mkpair (mksym "M1" "ACC") (mksym "COMMON-LISP"
390"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
391"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (
392mkpair (mksym "M1" "ACC") (mkpair (mkpair (mksym "M1" "U-BIG1") (mkpair (
393mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "LST") (mksym
394"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (
395mkpair (mksym "M1" "U-FIX") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
396mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
397mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "8" "1" "0" "1") (mksym
398"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
399"ACL2" "BINARY-*") (mkpair (mkpair (mksym "COMMON-LISP" "EXPT") (mkpair (
400mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym
401"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
402mknum "8" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
403"NIL")))) (mkpair (mksym "M1" "ACC") (mksym "COMMON-LISP" "NIL")))) (mksym
404"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
405"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
406,
407
408(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "U-BIG") (mkpair (
409mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
410"M1" "U-BIG1") (mkpair (mksym "M1" "LST") (mkpair (mkpair (mksym
411"COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
412"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
413,
414
415(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "S-BIG") (mkpair (
416mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
417"M1" "S-FIX") (mkpair (mkpair (mksym "M1" "U-BIG") (mkpair (mksym "M1" "LST") (
418mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-*") (
419mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "8" "1" "0" "1") (
420mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "LEN") (mkpair (
421mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
422mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
423,
424
425(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NEXTN") (mkpair (
426mkpair (mksym "M1" "N") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (
427mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (
428mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
429"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
430"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
431mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "LST") (mksym
432"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "NEXTN") (mkpair (mkpair (
433mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
434mkpair (mknum "-1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
435"M1" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
436"CDR") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym
437"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
438"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
439,
440
441(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "SKIPN") (mkpair (
442mkpair (mksym "M1" "N") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (
443mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (
444mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1"
445"LST") (mkpair (mkpair (mksym "M1" "SKIPN") (mkpair (mkpair (mksym "ACL2"
446"BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1"
447"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym
448"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
449mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
450mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
451
452];
453