1open HolKernel Parse boolLib bossLib intSyntax pairSyntax listSyntax stringLib numLib sexp;
2
3val package =
4 implode(map chr (cons 65 (cons 67 (cons 76 (cons 50 nil)))));
5
6val events = [
7
8(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LTL-CONSTANTP") (
9mkpair (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL")) (mkpair (
10mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
11"EQUAL") (mkpair (mksym "ACL2" "F") (mkpair (mkpair (mksym "COMMON-LISP"
12"QUOTE") (mkpair (mksym "ACL2" "TRUE") (mksym "COMMON-LISP" "NIL"))) (mksym
13"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
14mksym "ACL2" "F") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
15mksym "ACL2" "TRUE") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
16mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "F") (
17mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "FALSE") (
18mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
19"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
20,
21
22(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LTL-VARIABLEP") (
23mkpair (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL")) (mkpair (
24mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
25"SYMBOLP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (
26mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (
27mkpair (mksym "ACL2" "F") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
28mkpair (mkpair (mksym "COMMON-LISP" "+") (mkpair (mksym "ACL2" "&") (mkpair (
29mksym "ACL2" "U") (mkpair (mksym "ACL2" "W") (mkpair (mksym "ACL2" "X") (
30mkpair (mksym "ACL2" "F") (mkpair (mksym "ACL2" "G") (mksym "COMMON-LISP"
31"NIL")))))))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
32mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
33mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
34"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
35,
36
37(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LTL-FORMULAP") (
38mkpair (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL")) (mkpair (
39mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (
40mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
41mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "LTL-CONSTANTP") (
42mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
43mksym "ACL2" "LTL-CONSTANTP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP"
44"NIL"))) (mkpair (mkpair (mksym "ACL2" "LTL-VARIABLEP") (mkpair (mksym "ACL2"
45"F") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
46mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
47"EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" "F") (
48mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
49mkpair (mknum "3" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
50"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
51mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
52mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym
53"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
54"COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym "COMMON-LISP" "+") (mkpair (
55mksym "ACL2" "&") (mkpair (mksym "ACL2" "U") (mkpair (mksym "ACL2" "W") (
56mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))) (mksym
57"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
58mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP"
59"CAR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mksym
60"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (
61mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
62mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym
63"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
64"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
65"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
66mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
67mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
68"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
69mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (
70mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
71mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym
72"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
73"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (
74mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP"
75"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym
76"ACL2" "~") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "F") (mkpair (
77mksym "ACL2" "G") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))) (
78mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (
79mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym
80"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (
81mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
82mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
83"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
84"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
85"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
86"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
87,
88
89(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
90"RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "ACL2" "F") (mkpair (mksym
91"ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
92"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (
93mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
94"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "LTL-CONSTANTP") (mkpair (
95mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
96"LTL-CONSTANTP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (
97mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
98"LTL-VARIABLEP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (
99mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "F") (mkpair (
100mksym "ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
101"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
102"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
103"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
104"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym
105"ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
106"COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym "COMMON-LISP"
107"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
108"IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym
109"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
110mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
111mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym "ACL2"
112"&") (mkpair (mksym "COMMON-LISP" "+") (mkpair (mksym "ACL2" "U") (mkpair (
113mksym "ACL2" "W") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))) (
114mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
115mkpair (mkpair (mksym "ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym
116"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (
117mkpair (mksym "ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
118mksym "ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP"
119"CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym
120"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (
121mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
122"ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
123"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
124"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
125"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
126"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
127"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
128mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP"
129"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1"
130"0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
131mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (
132mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "F") (mksym
133"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
134mkpair (mksym "ACL2" "~") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2"
135"F") (mkpair (mksym "ACL2" "G") (mksym "COMMON-LISP" "NIL"))))) (mksym
136"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
137"ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
138mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym
139"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
140"V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
141"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
142mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
143mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
144"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
145"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
146,
147
148(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
149"RESTRICTED-FORMULA-IS-AN-LTL-FORMULA") (mkpair (mkpair (mksym "ACL2"
150"IMPLIES") (mkpair (mkpair (mksym "ACL2" "RESTRICTED-FORMULAP") (mkpair (
151mksym "ACL2" "F") (mkpair (mksym "ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL")))) (
152mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (mksym "ACL2" "F") (
153mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
154"COMMON-LISP" "NIL"))))
155,
156
157(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
158"CREATE-RESTRICTED-VAR-SET") (mkpair (mkpair (mksym "ACL2" "F") (mksym
159"COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
160mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "F") (mksym
161"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
162mkpair (mksym "ACL2" "LTL-CONSTANTP") (mkpair (mksym "ACL2" "F") (mksym
163"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
164mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
165mksym "COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "F") (mkpair (mkpair (mksym
166"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
167"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
168"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
169"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym
170"ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
171"COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym "COMMON-LISP"
172"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
173"SET-UNION") (mkpair (mkpair (mksym "ACL2" "CREATE-RESTRICTED-VAR-SET") (
174mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "F") (mksym
175"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
176"ACL2" "CREATE-RESTRICTED-VAR-SET") (mkpair (mkpair (mksym "COMMON-LISP"
177"CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym
178"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (
179mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym
180"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
181"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
182mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP"
183"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1"
184"0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
185mkpair (mksym "ACL2" "CREATE-RESTRICTED-VAR-SET") (mkpair (mkpair (mksym
186"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
187mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
188mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
189mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
190"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
191"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
192,
193
194(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
195"LTL-FORMULA-IS-A-RESTRICTED-FORMULA") (mkpair (mkpair (mksym "ACL2"
196"IMPLIES") (mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (mksym
197"ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
198"RESTRICTED-FORMULAP") (mkpair (mksym "ACL2" "F") (mkpair (mkpair (mksym
199"ACL2" "CREATE-RESTRICTED-VAR-SET") (mkpair (mksym "ACL2" "F") (mksym
200"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
201"NIL")))) (mksym "COMMON-LISP" "NIL"))))
202,
203
204(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "NEXT-STATEP") (
205mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym
206"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
207"MEMBERP") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "G") (
208mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
209mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym
210"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
211mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
212"COMMON-LISP" "NIL")))))
213,
214
215(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "INITIAL-STATEP") (
216mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (mksym
217"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
218mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
219"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym
220"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
221mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
222,
223
224(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LABEL-OF") (
225mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "M") (mksym
226"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym
227"ACL2" "S") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
228"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "LABEL-FN") (mksym
229"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
230mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
231,
232
233(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
234"NEXT-STATES-IN-STATES") (mkpair (mkpair (mksym "ACL2" "M") (mkpair (mksym
235"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
236"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
237mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
238"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP"
239"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
240"ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
241"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
242"NIL"))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
243"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym
244"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
245mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
246mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
247mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP"
248"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
249"NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym
250"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
251"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
252"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
253mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym
254"COMMON-LISP" "NIL")))))
255,
256
257(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
258"NEXT-STATES-IN-STATES-CLARIFIED-AUX") (mkpair (mkpair (mksym "ACL2"
259"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
260"ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "STATES") (
261mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
262mkpair (mkpair (mksym "ACL2" "NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2"
263"M") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (
264mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mksym
265"ACL2" "Q") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))))) (
266mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
267"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
268mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
269mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
270mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym
271"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
272"KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
273mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
274"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
275,
276
277(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
278"NEXT-STATES-IN-STATES-CLARIFIED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
279mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
280"NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym
281"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
282"KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
283mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
284mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
285mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
286"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
287"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
288mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") (
289mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2"
290"M") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP"
291"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
292mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
293mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
294"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
295mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
296"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
297"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
298mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
299"COMMON-LISP" "NIL"))))
300
301];
302