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" "FIND-VARIABLES") (
9mkpair (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL")) (mkpair (
10mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
11mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "EQUATION") (
12mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (
13mkpair (mkpair (mksym "ACL2" "BOOLEANP") (mkpair (mksym "ACL2" "EQUATION") (
14mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
15mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
16"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
17"COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "EQUATION") (mkpair (mkpair (
18mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
19"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
20"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
21mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (
22mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (
23mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym
24"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
25"ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (
26mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym
27"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
28"COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym "ACL2" "&") (mkpair (mksym
29"COMMON-LISP" "+") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
30mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
31mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
32"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "SET-UNION") (mkpair (
33mkpair (mksym "ACL2" "FIND-VARIABLES") (mkpair (mkpair (mksym "COMMON-LISP"
34"CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym
35"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "FIND-VARIABLES") (
36mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym
37"COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
38mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
39"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym
40"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
41mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
42"EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2"
43"EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
44"COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP"
45"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
46"EQUAL") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2"
47"EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
48"COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "~") (mksym "COMMON-LISP" "NIL"))) (
49mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
50mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
51"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "FIND-VARIABLES") (
52mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym
53"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP"
54"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
55mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
56mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
57"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
58"NIL")))))
59,
60
61(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2"
62"CONSISTENT-EQUATION-RECORD-P") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (
63mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
64mksym "ACL2" "FORALL") (mkpair (mkpair (mksym "ACL2" "V") (mkpair (mksym
65"ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
66"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (
67mksym "ACL2" "UNIQUEP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
68"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
69"ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "VARS") (
70mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (
71mkpair (mksym "ACL2" "EQUATION") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
72mksym "ACL2" "V") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP"
73"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
74"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
75mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
76mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
77"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (
78mkpair (mksym "ACL2" "FIND-VARIABLES") (mkpair (mksym "ACL2" "EQUATION") (
79mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym
80"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
81"NIL")))) (mksym "COMMON-LISP" "NIL")))))
82,
83
84(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CONS-LIST-P") (
85mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "EQUATIONS") (
86mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
87mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (
88mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
89mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (
90mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
91"CONSP") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
92"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (
93mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) (mksym
94"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "CONS-LIST-P") (mkpair (
95mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym
96"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQUATIONS") (mksym
97"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
98mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
99"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
100,
101
102(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CIRCUITP") (
103mkpair (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")) (mkpair (
104mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
105"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
106mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (
107mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP"
108"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
109"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym
110"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (
111mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
112mkpair (mkpair (mksym "ACL2" "STRICT-EVALUATION-LIST-P") (mkpair (mkpair (
113mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
114mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
115"ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (
116mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
117"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (
118mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
119mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "UNIQUEP") (mkpair (
120mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
121mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair (
122mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (
123mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
124"CONS-LIST-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
125"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym
126"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (
127mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP"
128"QUOTE") (mkpair (mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (
129mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
130"NIL")))) (mkpair (mkpair (mksym "ACL2" "CONSISTENT-EQUATION-RECORD-P") (
131mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP"
132"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (
133mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
134mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
135mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
136"ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
137mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
138"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
139mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
140mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
141mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
142"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
143"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
144"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
145"NIL")))))
146,
147
148(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSIGN-T") (
149mkpair (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "STATES") (mksym
150"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
151mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym
152"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
153mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
154mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym
155"ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
156"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
157"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
158"NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2"
159"ASSIGN-T") (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP"
160"CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mksym
161"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
162"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
163,
164
165(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSIGN-NIL") (
166mkpair (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "STATES") (mksym
167"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
168mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym
169"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
170mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
171mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym
172"ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
173"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
174"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
175"NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2"
176"ASSIGN-NIL") (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP"
177"CDR") (mkpair (mksym "ACL2" "STATES") (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 "ACL2"
183"CREATE-ALL-EVALUATIONS") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (
184mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
185"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
186mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
187"STATES") (mkpair (mkpair (mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair (
188mkpair (mksym "ACL2" "REC-STATES") (mkpair (mksym "ACL2" "VARS") (mksym
189"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-APPEND") (mkpair (
190mkpair (mksym "ACL2" "ASSIGN-T") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
191mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
192"ACL2" "REC-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
193"ACL2" "ASSIGN-NIL") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
194mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
195"REC-STATES") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
196mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
197"CREATE-ALL-EVALUATIONS") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
198mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
199"STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mksym
200"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
201"NIL")))))
202,
203
204(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LABEL-FN-OF-ST") (
205mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym
206"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
207mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym
208"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
209mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
210mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
211mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
212mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
213"ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
214"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP"
215"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
216"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2"
217"VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
218"LABEL-FN-OF-ST") (mkpair (mksym "ACL2" "ST") (mkpair (mkpair (mksym
219"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (
220mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
221mksym "ACL2" "LABEL-FN-OF-ST") (mkpair (mksym "ACL2" "ST") (mkpair (mkpair (
222mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
223"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (
224mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
225,
226
227(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CREATE-LABEL-FN") (
228mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mkpair (
229mksym "ACL2" "LABEL") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
230"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
231mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
232"LABEL") (mkpair (mkpair (mksym "ACL2" "CREATE-LABEL-FN") (mkpair (mkpair (
233mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym
234"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair (mkpair (mksym
235"ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2"
236"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
237"LABEL-FN-OF-ST") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym
238"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (
239mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "LABEL") (mksym
240"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
241"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
242,
243
244(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "APPLY-EQUATION") (
245mkpair (mkpair (mksym "ACL2" "EQUATION") (mkpair (mksym "ACL2" "ST") (mksym
246"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
247mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "EQUATION") (mksym
248"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
249mkpair (mksym "ACL2" "BOOLEANP") (mkpair (mksym "ACL2" "EQUATION") (mksym
250"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQUATION") (mkpair (mkpair (
251mksym "ACL2" "G") (mkpair (mksym "ACL2" "EQUATION") (mkpair (mksym "ACL2"
252"ST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
253mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
254"EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2"
255"EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
256"COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP"
257"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mkpair (mksym
258"COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2"
259"CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mksym "ACL2" "ST") (mkpair (mksym
260"ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
261"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair (
262mksym "ACL2" "CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mkpair (mksym
263"COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "~") (mksym "COMMON-LISP" "NIL"))) (
264mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (
265mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym
266"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
267mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
268"NIL"))) (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mksym
269"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
270mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
271"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
272"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP"
273"NIL"))) (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "EQUATION") (mksym
274"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
275mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (
276mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (
277mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym
278"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mkpair (
279mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2"
280"CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mksym "ACL2" "ST") (mkpair (mksym
281"ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
282"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair (
283mksym "ACL2" "CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mkpair (mksym
284"COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "&") (mksym "COMMON-LISP" "NIL"))) (
285mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
286mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym
287"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP"
288"NIL"))) (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair (
289mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym "COMMON-LISP"
290"CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym
291"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP"
292"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
293mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
294"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
295"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
296"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair (
297mksym "ACL2" "CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mkpair (mksym
298"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "+") (mksym "COMMON-LISP"
299"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
300"IF") (mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym
301"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP"
302"NIL"))) (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair (
303mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym "COMMON-LISP"
304"CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (
305mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
306mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
307mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym
308"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP"
309"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
310mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (
311mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
312"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
313"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
314mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
315mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym
316"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2"
317"EQUATION") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
318"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
319"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
320"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
321,
322
323(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
324"PRODUCE-NEXT-STATE") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym
325"ACL2" "ST") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) (
326mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
327"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
328"NIL"))) (mkpair (mksym "ACL2" "ST") (mkpair (mkpair (mksym "ACL2" "S") (
329mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (
330mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") (
331mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
332mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
333"ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "ST") (
334mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
335"PRODUCE-NEXT-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
336mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "ST") (
337mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) (mksym
338"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
339"NIL")))))
340,
341
342(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
343"CONSISTENT-P-EQUATIONS") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (
344mksym "ACL2" "EQN") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP"
345"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
346"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
347"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
348"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
349"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (
350mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym
351"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQN") (
352mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
353mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym
354"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQUATIONS") (mksym
355"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
356"ACL2" "CONSISTENT-P-EQUATIONS") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
357mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
358"ACL2" "EQN") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) (
359mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
360"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
361"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
362,
363
364(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" "NEXT-STATE-IS-OK") (
365mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym
366"ACL2" "VARS") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) (
367mkpair (mkpair (mksym "ACL2" "EXISTS") (mkpair (mkpair (mksym "ACL2" "EQN") (
368mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
369mkpair (mkpair (mksym "ACL2" "CONSISTENT-P-EQUATIONS") (mkpair (mksym "ACL2"
370"VARS") (mkpair (mksym "ACL2" "EQN") (mkpair (mksym "ACL2" "EQUATIONS") (
371mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (
372mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "PRODUCE-NEXT-STATE") (
373mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2"
374"EQN") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mksym "ACL2" "VARS") (mksym
375"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
376mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
377"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
378"NIL")))))
379,
380
381(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
382"CREATE-NEXT-STATES-OF-P") (mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym
383"ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
384"EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
385"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
386mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
387"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
388"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
389mkpair (mksym "ACL2" "NEXT-STATE-IS-OK") (mkpair (mksym "ACL2" "P") (mkpair (
390mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym
391"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
392"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym
393"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
394mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
395"ACL2" "CREATE-NEXT-STATES-OF-P") (mkpair (mksym "ACL2" "P") (mkpair (mkpair (
396mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym
397"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
398"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) (
399mkpair (mkpair (mksym "ACL2" "CREATE-NEXT-STATES-OF-P") (mkpair (mksym "ACL2"
400"P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2"
401"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair (
402mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mksym
403"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
404"NIL")))))
405,
406
407(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
408"CREATE-NEXT-STATES") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
409"ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
410"EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
411"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
412mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
413"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
414"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair (
415mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym
416"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
417"CREATE-NEXT-STATES-OF-P") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
418mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
419"ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
420"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "ACL2"
421"CREATE-NEXT-STATES") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
422mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
423"STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
424"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL"))))) (
425mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
426,
427
428(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CREATE-KRIPKE") (
429mkpair (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")) (mkpair (
430mkpair (mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2"
431"VARS") (mkpair (mksym "ACL2" "EQUATIONS") (mkpair (mksym "ACL2"
432"INITIAL-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mkpair (
433mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (
434mksym "ACL2" "EQUATIONS") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
435"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mkpair (
436mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "LABEL-FN") (
437mkpair (mksym "ACL2" "EQUATIONS") (mkpair (mksym "ACL2" "VARS") (mkpair (
438mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "INITIAL-STATES") (mksym
439"COMMON-LISP" "NIL")))))) (mkpair (mkpair (mkpair (mksym "COMMON-LISP"
440"LAMBDA") (mkpair (mkpair (mksym "ACL2" "TRANSITION") (mkpair (mksym "ACL2"
441"STATES") (mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2"
442"LABEL-FN") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))))) (
443mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP"
444"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (
445mkpair (mksym "ACL2" "VARS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (
446mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (
447mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "TRANSITION") (mkpair (
448mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
449mkpair (mksym "KEYWORD" "LABEL-FN") (mksym "COMMON-LISP" "NIL"))) (mkpair (
450mksym "ACL2" "LABEL-FN") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair (
451mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (
452mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (
453mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
454mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (
455mkpair (mksym "ACL2" "SET-UNION") (mkpair (mksym "ACL2" "INITIAL-STATES") (
456mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
457mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
458"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
459"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (
460mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
461mksym "ACL2" "CREATE-NEXT-STATES") (mkpair (mkpair (mksym "ACL2" "SET-UNION") (
462mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym
463"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "SET-UNION") (mkpair (
464mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym
465"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
466"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mkpair (mksym "ACL2" "STATES") (
467mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "LABEL-FN") (
468mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mksym
469"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "CREATE-LABEL-FN") (
470mkpair (mkpair (mksym "ACL2" "SET-UNION") (mkpair (mksym "ACL2"
471"INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (
472mkpair (mksym "ACL2" "VARS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
473mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
474"COMMON-LISP" "NIL"))))) (mkpair (mksym "ACL2" "EQUATIONS") (mkpair (mksym
475"ACL2" "VARS") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2"
476"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP"
477"NIL")))) (mkpair (mkpair (mksym "ACL2" "CREATE-ALL-EVALUATIONS") (mkpair (
478mksym "ACL2" "VARS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
479mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
480mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
481mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
482"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2"
483"EQUATIONS") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
484"INITIAL-STATES") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) (
485mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP"
486"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (
487mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
488mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
489mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
490"ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (
491mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
492"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (
493mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym
494"COMMON-LISP" "NIL")))))
495,
496
497(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
498"CREATE-KRIPKE-PRODUCES-CIRCUIT-MODEL") (mkpair (mkpair (mksym "ACL2"
499"IMPLIES") (mkpair (mkpair (mksym "ACL2" "CIRCUITP") (mkpair (mksym "ACL2"
500"C") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
501"CIRCUIT-MODELP") (mkpair (mkpair (mksym "ACL2" "CREATE-KRIPKE") (mkpair (
502mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
503mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
504
505];
506