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" "EVALUATION-EQ") (
9mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym
10"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
11"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
12mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
13"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP"
14"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
15"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
16mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
17"NIL"))) (mkpair (mksym "ACL2" "P") (mksym "COMMON-LISP" "NIL")))) (mkpair (
18mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
19mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Q") (
20mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
21mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (mksym
22"ACL2" "Q") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2"
23"VARS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
24mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
25mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
26"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
27,
28
29(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
30"EVALUATION-EQ-IS-SYMMETRIC") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
31mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (
32mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
33"NIL"))))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym
34"ACL2" "Q") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "VARS") (mksym
35"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
36"NIL"))))
37,
38
39(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
40"EVALUATION-EQ-MEMBER-P") (mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym
41"ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
42mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
43"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
44"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
45"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
46"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (
47mksym "ACL2" "ST") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym
48"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (
49mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
50mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (
51mkpair (mksym "ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "ST") (
52mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (
53mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym
54"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
55"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
56,
57
58(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
59"EVALUATION-EQ-MEMBER") (mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym
60"ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
61mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
62"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
63"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
64"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
65"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (
66mksym "ACL2" "ST") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym
67"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (
68mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
69mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
70mksym "ACL2" "EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "ST") (mkpair (
71mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym
72"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
73"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (
74mksym "COMMON-LISP" "NIL")))))
75,
76
77(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBER-IS-MEMBERP") (
78mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2"
79"EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2"
80"STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
81mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "ACL2"
82"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2"
83"STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
84mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mksym
85"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
86,
87
88(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
89"MEMBER-IS-EVALUATION-EQ") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
90mkpair (mksym "ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "P") (
91mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym
92"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (
93mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2"
94"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2"
95"STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
96mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mksym
97"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
98,
99
100(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" "STRICT-EVALUATION-P") (
101mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym
102"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "FORALL") (mkpair (
103mkpair (mksym "ACL2" "V") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
104"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (
105mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2"
106"VARS") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
107mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
108mksym "ACL2" "V") (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (
109mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
110"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
111,
112
113(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
114"STRICT-EVALUATION-P-EXPANDED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
115mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
116"STRICT-EVALUATION-P") (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2"
117"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
118"NOT") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (
119mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym
120"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
121mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
122"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym
123"ACL2" "G") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "ST") (mksym
124"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
125"NIL")))) (mksym "COMMON-LISP" "NIL"))))
126,
127
128(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
129"STRICT-EVALUATION-LIST-P") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (
130mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
131"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
132mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
133"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP"
134"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
135"ACL2" "STRICT-EVALUATION-P") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
136mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
137"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
138"STRICT-EVALUATION-LIST-P") (mkpair (mksym "ACL2" "VARS") (mkpair (mkpair (
139mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym
140"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
141"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
142"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
143"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
144,
145
146(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "EVALUATION-P") (
147mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym
148"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
149mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym
150"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
151mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
152"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "BOOLEANP") (mkpair (mkpair (
153mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym
154"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "ST") (
155mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
156mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" "ST") (mkpair (mkpair (
157mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
158"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
159"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
160mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym
161"COMMON-LISP" "NIL")))))
162,
163
164(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
165"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
166"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
167"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
168mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
169"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP"
170"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
171"ACL2" "EVALUATION-P") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
172mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
173"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
174"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
175mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
176"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
177"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
178mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym
179"COMMON-LISP" "NIL")))))
180,
181
182(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" "ALL-EVALUATIONS-P") (
183mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym
184"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "FORALL") (mkpair (
185mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
186mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (mkpair (
187mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
188mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2"
189"ST") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym
190"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
191"NIL")))) (mksym "COMMON-LISP" "NIL")))))
192,
193
194(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
195"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "M-STATES") (mkpair (
196mksym "ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
197"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
198"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "M-STATES") (mksym "COMMON-LISP"
199"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
200"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
201"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ-MEMBER-P") (
202mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "M-STATES") (
203mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N-STATES") (mkpair (mksym
204"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2"
205"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
206mksym "ACL2" "M-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
207"N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
208mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
209"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
210"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
211,
212
213(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
214"EVALUATION-EQ-SUBSET-TO-MEMBER") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
215mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
216"EVALUATION-EQ-SUBSET-P") (mkpair (mksym "ACL2" "M-STATES") (mkpair (mksym
217"ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
218mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (
219mksym "ACL2" "M-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
220mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
221"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
222"ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "P") (mkpair (mksym
223"ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
224mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
225,
226
227(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "TRUTHP-LABEL") (
228mkpair (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "S") (mksym
229"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
230mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "LABEL") (mksym
231"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
232mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
233"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
234mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
235mksym "ACL2" "LABEL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "S") (
236mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
237mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mksym
238"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (
239mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "LABEL") (mksym
240"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "S") (mksym "COMMON-LISP" "NIL")))) (
241mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
242"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
243"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
244,
245
246(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ONLY-TRUTH-P") (
247mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "M") (mksym
248"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
249mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym
250"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
251mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
252"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (
253mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
254mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
255"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
256"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
257"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
258"ONLY-TRUTH-P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
259"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
260mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
261mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
262"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
263"NIL")))))
264,
265
266(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
267"ALL-TRUTHSP-LABEL") (mkpair (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym
268"ACL2" "S") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
269mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
270"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
271"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
272"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
273"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (
274mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
275mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym
276"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "S") (mksym "COMMON-LISP" "NIL")))) (
277mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (
278mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
279mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
280mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
281"LABEL") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
282mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2"
283"LABEL") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP"
284"CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mksym
285"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
286mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
287"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
288"NIL")))))
289,
290
291(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
292"ALL-TRUTHSP-LABEL-EXPANDED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
293mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
294"ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "S") (
295mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
296mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
297mksym "ACL2" "V") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
298mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2"
299"G") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "S") (mksym
300"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
301mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
302"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
303"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
304mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
305"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
306mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym
307"ACL2" "LABEL") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
308mksym "COMMON-LISP" "NIL"))))
309,
310
311(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
312"ONLY-ALL-TRUTHS-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
313"ACL2" "M") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
314mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
315"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
316"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
317"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
318"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (
319mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP"
320"CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (
321mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
322"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
323"NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
324mkpair (mkpair (mksym "ACL2" "ONLY-ALL-TRUTHS-P") (mkpair (mkpair (mksym
325"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
326"NIL"))) (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "VARS") (mksym
327"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
328mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
329"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
330"NIL")))))
331,
332
333(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
334"LABEL-SUBSET-VARS") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
335"ACL2" "M") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
336mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
337"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
338"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
339"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
340"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mkpair (
341mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
342mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
343"M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mksym
344"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "LABEL-SUBSET-VARS") (
345mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (
346mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2"
347"VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP"
348"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
349mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym
350"COMMON-LISP" "NIL")))))
351,
352
353(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
354"LABEL-SUBSET-SUBSET-REDUCTION") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
355mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
356"LABEL-SUBSET-VARS") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2"
357"M") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (
358mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym
359"ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
360"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
361"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
362"ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym
363"ACL2" "P") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (
364mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
365"NIL")))) (mksym "COMMON-LISP" "NIL"))))
366,
367
368(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2"
369"WELL-FORMED-TRANSITION-P") (mkpair (mkpair (mksym "ACL2" "STATES-M") (mkpair (
370mksym "ACL2" "TRANS-M") (mkpair (mksym "ACL2" "STATES-N") (mkpair (mksym
371"ACL2" "TRANS-N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))))) (
372mkpair (mkpair (mksym "ACL2" "FORALL") (mkpair (mkpair (mksym "ACL2" "P") (
373mkpair (mksym "ACL2" "Q") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
374mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
375mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (
376mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
377mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
378"EVALUATION-P") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "VARS") (
379mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
380mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (
381mksym "ACL2" "STATES-M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
382mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
383mksym "ACL2" "Q") (mkpair (mksym "ACL2" "STATES-N") (mksym "COMMON-LISP"
384"NIL")))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2"
385"Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (
386mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
387mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
388mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
389"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
390"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
391"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
392"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
393"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
394"ACL2" "EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
395mksym "ACL2" "P") (mkpair (mksym "ACL2" "TRANS-M") (mksym "COMMON-LISP" "NIL")))) (
396mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "Q") (mkpair (mksym
397"ACL2" "TRANS-N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (
398mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym
399"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
400,
401
402(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
403"WELL-FORMED-TRANSITION-P-EXPANDED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
404mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
405"WELL-FORMED-TRANSITION-P") (mkpair (mksym "ACL2" "STATES-M") (mkpair (mksym
406"ACL2" "TRANS-M") (mkpair (mksym "ACL2" "STATES-N") (mkpair (mksym "ACL2"
407"TRANS-N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (
408mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
409"EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (
410mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
411mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (
412mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
413"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
414"ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "STATES-M") (
415mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
416mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "Q") (mkpair (
417mksym "ACL2" "STATES-N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
418mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2"
419"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
420"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
421mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
422mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
423"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
424mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
425"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
426mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
427"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
428mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
429"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2"
430"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym
431"ACL2" "P") (mkpair (mksym "ACL2" "TRANS-M") (mksym "COMMON-LISP" "NIL")))) (
432mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "Q") (mkpair (mksym
433"ACL2" "TRANS-N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (
434mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym
435"COMMON-LISP" "NIL"))))
436,
437
438(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
439"TRANSITION-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
440"ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "TRANS") (mksym "COMMON-LISP"
441"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
442"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
443"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
444"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
445"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mkpair (
446mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym
447"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "TRANS") (
448mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "STATES-PRIME") (mksym
449"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "TRANSITION-SUBSET-P") (
450mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (
451mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "STATES-PRIME") (mkpair (
452mksym "ACL2" "TRANS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
453"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
454"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
455"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
456,
457
458(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
459"TRANSITION-SUBSET-P-EXPANDED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
460mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
461"TRANSITION-SUBSET-P") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2"
462"STATES-PRIME") (mkpair (mksym "ACL2" "TRANS") (mksym "COMMON-LISP" "NIL"))))) (
463mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
464"MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "STATES") (mksym
465"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
466mksym "ACL2" "R") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2"
467"P") (mkpair (mksym "ACL2" "TRANS") (mksym "COMMON-LISP" "NIL")))) (mksym
468"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
469mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
470"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
471"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
472mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "R") (mkpair (
473mksym "ACL2" "STATES-PRIME") (mksym "COMMON-LISP" "NIL")))) (mksym
474"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
475,
476
477(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CIRCUIT-MODELP") (
478mkpair (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")) (mkpair (
479mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
480"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
481mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
482"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
483mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP"
484"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (
485mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
486"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
487"ACL2" "ALL-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
488mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
489mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP"
490"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
491"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym
492"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
493mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
494mkpair (mkpair (mksym "ACL2" "STRICT-EVALUATION-LIST-P") (mkpair (mkpair (
495mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
496mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
497"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (
498mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
499"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym
500"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
501"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ONLY-ALL-TRUTHS-P") (
502mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP"
503"QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (
504mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym
505"ACL2" "M") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
506"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym
507"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
508mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
509mkpair (mkpair (mksym "ACL2" "ONLY-TRUTH-P") (mkpair (mkpair (mksym "ACL2"
510"G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
511"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym
512"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
513mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
514"LABEL-SUBSET-VARS") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
515mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
516"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
517mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
518mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym
519"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
520mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
521mkpair (mkpair (mksym "ACL2" "TRANSITION-SUBSET-P") (mkpair (mkpair (mksym
522"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
523"KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
524mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
525mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
526mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP"
527"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
528"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym
529"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
530mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
531mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "G") (
532mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
533"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
534mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
535mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
536mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP"
537"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
538"IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mkpair (mksym
539"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
540"KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
541mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
542mksym "ACL2" "NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair (
543mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
544mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (
545mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
546mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
547"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
548mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
549mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
550mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
551"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
552"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
553"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
554"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
555"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
556"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
557"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
558"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
559"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
560"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
561"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
562"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
563"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
564"NIL")))))
565,
566
567(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "C-BISIM-EQUIV") (
568mkpair (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym
569"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
570"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair (
571mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
572"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair (
573mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
574"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym
575"ACL2" "VARS") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
576"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym
577"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
578mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
579mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair (
580mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
581mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair (
582mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
583mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
584"WELL-FORMED-TRANSITION-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
585mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
586mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP"
587"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
588"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym
589"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
590mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP"
591"QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (
592mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
593mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
594mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
595"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (
596mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
597mkpair (mkpair (mksym "ACL2" "WELL-FORMED-TRANSITION-P") (mkpair (mkpair (
598mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
599mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
600"N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (
601mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
602"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym
603"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
604mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
605"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
606mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP"
607"QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) (
608mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym
609"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym
610"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ-SUBSET-P") (
611mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP"
612"QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP"
613"NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (
614mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
615mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (
616mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym
617"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2"
618"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
619mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (
620mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP"
621"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
622"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym
623"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
624mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
625mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
626"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
627"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
628"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
629"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
630"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
631"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
632"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
633"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
634"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
635"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
636"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
637"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
638"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
639"NIL")))))
640,
641
642(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CIRCUIT-BISIM") (
643mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (mkpair (mksym
644"ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym
645"COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
646mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair (mksym "ACL2" "M") (mksym
647"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
648mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair (mksym "ACL2" "N") (mksym
649"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
650mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mkpair (
651mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
652mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
653"M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
654mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (
655mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
656mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
657"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (
658mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
659mkpair (mkpair (mksym "ACL2" "WELL-FORMED-TRANSITION-P") (mkpair (mkpair (
660mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
661mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
662"M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (
663mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
664"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym
665"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
666mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
667"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (
668mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP"
669"QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) (
670mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym
671"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym
672"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "WELL-FORMED-TRANSITION-P") (
673mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP"
674"QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (
675mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
676mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
677mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
678"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (
679mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
680"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym
681"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
682mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym
683"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
684mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (
685mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
686"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
687mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (
688mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP"
689"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
690"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym
691"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (
692mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
693mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
694"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
695mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (
696mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP"
697"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym
698"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym
699"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
700mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
701mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (
702mksym "ACL2" "VARS") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
703mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym
704"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
705mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
706mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair (
707mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
708mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair (
709mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
710mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (
711mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
712"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
713"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
714mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
715"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
716mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
717mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
718mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
719"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
720"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
721"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
722"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
723"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
724"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
725"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
726"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
727"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
728"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
729"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
730"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
731"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
732"NIL")))))
733,
734
735(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
736"C-BISIMILAR-INITIAL-STATE-WITNESS-M->N") (mkpair (mkpair (mksym "ACL2" "S") (
737mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2"
738"VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2"
739"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym
740"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
741"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
742"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (
743mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
744,
745
746(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
747"C-BISIMILAR-INITIAL-STATE-WITNESS-N->M") (mkpair (mkpair (mksym "ACL2" "M") (
748mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2"
749"VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2"
750"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym
751"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
752"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
753"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (
754mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
755,
756
757(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
758"ALL-EVALUATIONS-CONSIDERS-AN-EVALUATION-A-MEMBER") (mkpair (mkpair (mksym
759"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (
760mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" "ST") (mkpair (mksym
761"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
762"ALL-EVALUATIONS-P") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2"
763"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
764"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
765mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2"
766"EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2"
767"STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
768mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
769,
770
771(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
772"TRUTHP-LABEL-FROM-ONLY-TRUTHP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
773mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
774"ONLY-TRUTH-P") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "M") (
775mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (
776mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "STATES") (mksym
777"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
778mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
779"NIL"))))) (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (mkpair (
780mksym "ACL2" "LABEL-OF") (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "M") (
781mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "S") (mksym "COMMON-LISP"
782"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
783,
784
785(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
786"ALL-TRUTHS-P-FROM-ONLY-ALL-TRUTHS-P") (mkpair (mkpair (mksym "ACL2"
787"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
788"ACL2" "ONLY-ALL-TRUTHS-P") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
789"ACL2" "M") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
790mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair (
791mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
792"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
793"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
794"ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (
795mksym "ACL2" "S") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
796mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
797"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
798,
799
800(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
801"MEMBERP-TO-INTERSECT-REDUCTION") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
802mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (
803mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mksym "ACL2" "X") (mkpair (
804mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
805mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
806"MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "X") (mksym
807"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
808mksym "ACL2" "V") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
809mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
810"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
811"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
812,
813
814(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
815"EVALUATION-EQ-VARS-REDUCTION") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
816mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
817"EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (
818mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
819mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2"
820"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
821"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
822mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
823mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "V") (mkpair (mksym
824"ACL2" "P") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (
825mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "Q") (mksym "COMMON-LISP"
826"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
827mksym "COMMON-LISP" "NIL"))))
828,
829
830(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
831"VARIABLES-IN-LABEL-ARE-T-IN-Q") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
832mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
833"MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2"
834"SET-INTERSECT") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "VARS") (
835mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
836mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (
837mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "P") (mksym "COMMON-LISP"
838"NIL")))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym
839"ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym
840"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
841mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
842"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
843mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
844"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
845mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "V") (mkpair (mksym
846"ACL2" "Q") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
847"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP"
848"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
849"COMMON-LISP" "NIL"))))
850,
851
852(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
853"ONLY-TRUTHSP-AND-SUBSET-TO-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
854mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
855"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym
856"ACL2" "V") (mkpair (mksym "ACL2" "Q") (mksym "COMMON-LISP" "NIL")))) (mkpair (
857mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym
858"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
859"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym
860"ACL2" "V") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
861mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
862"SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "VARIABLES") (
863mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
864"ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "Q") (
865mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" "NIL"))))) (mkpair (
866mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
867mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
868mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
869"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
870"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
871"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
872"ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "LABEL") (
873mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
874"COMMON-LISP" "NIL"))))
875,
876
877(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
878"TRUTHP-LABEL-TO-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
879mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (
880mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (
881mkpair (mksym "ACL2" "LP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
882"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
883"IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (mksym "ACL2"
884"LP") (mkpair (mksym "ACL2" "P") (mksym "COMMON-LISP" "NIL")))) (mkpair (
885mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
886"EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (
887mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
888mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (
889mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP"
890"NIL")))) (mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mksym
891"ACL2" "LQ") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARIABLES") (
892mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
893mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
894"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
895mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
896"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
897mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
898"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
899mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
900"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
901mksym "ACL2" "V") (mkpair (mksym "ACL2" "LQ") (mksym "COMMON-LISP" "NIL")))) (
902mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
903,
904
905(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
906"TRUTHP-LABEL-IS-A-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
907mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
908"TRUTHP-LABEL") (mkpair (mksym "ACL2" "LP") (mkpair (mksym "ACL2" "P") (mksym
909"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
910mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (
911mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
912mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
913"SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "VARIABLES") (
914mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
915"ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LQ") (mkpair (mksym "ACL2" "Q") (
916mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" "NIL"))))) (mkpair (
917mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
918mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
919mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
920"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
921"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
922"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
923"ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (
924mksym "ACL2" "LP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
925mkpair (mksym "ACL2" "LQ") (mksym "COMMON-LISP" "NIL")))) (mksym
926"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
927,
928
929(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
930"C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair (mkpair (mksym "ACL2" "P") (
931mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2"
932"Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym
933"COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2"
934"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym
935"ACL2" "G") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "G") (
936mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
937"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym
938"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2"
939"VARS") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
940,
941
942(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
943"C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mkpair (mksym "ACL2" "P") (
944mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2"
945"R") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym
946"COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2"
947"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym
948"ACL2" "G") (mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") (
949mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
950"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym
951"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2"
952"VARS") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
953,
954
955(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
956"EVALUATIONP-FOR-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
957mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
958"EVALUATION-P") (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARIABLES") (
959mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (
960mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP"
961"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
962"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
963mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" "ST") (
964mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym
965"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
966,
967
968(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
969"EVALUATION-P-ONLY-EVALUATIONS-REDUCTION") (mkpair (mkpair (mksym "ACL2"
970"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
971"ACL2" "ONLY-EVALUATIONS-P") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
972"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
973"MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "STATES") (mksym
974"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
975mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
976"NIL"))))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (mkpair (mksym
977"ACL2" "P") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
978mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
979,
980
981(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
982"R-IS-EVALUATION-EQ-MEMBER-P") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
983mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
984"EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (
985mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
986mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
987"WELL-FORMED-TRANSITION-P") (mkpair (mksym "ACL2" "STATES-M") (mkpair (mksym
988"ACL2" "TRANS-M") (mkpair (mksym "ACL2" "STATES-N") (mkpair (mksym "ACL2"
989"TRANS-N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (
990mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
991"MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "STATES-M") (
992mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
993mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "Q") (mkpair (
994mksym "ACL2" "STATES-N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
995mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (
996mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
997"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
998"ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2"
999"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2"
1000"MEMBERP") (mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym "ACL2" "G") (
1001mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "TRANS-M") (mksym
1002"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1003"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1004"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1005"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1006"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1007"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1008"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1009"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1010"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1011"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1012"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1013"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1014"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1015"ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "R") (mkpair (mkpair (
1016mksym "ACL2" "G") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "TRANS-N") (
1017mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mksym
1018"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1019"NIL"))))
1020,
1021
1022(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
1023"C-BISIMILAR-EQUIV-IMPLIES-INIT->INIT-M->N") (mkpair (mkpair (mksym "ACL2"
1024"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
1025"ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (
1026mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
1027mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym
1028"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
1029"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
1030"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
1031mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
1032"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
1033mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "ACL2"
1034"C-BISIMILAR-INITIAL-STATE-WITNESS-M->N") (mkpair (mksym "ACL2" "S") (mkpair (
1035mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (
1036mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
1037mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
1038"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (
1039mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
1040"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
1041,
1042
1043(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
1044"C-BISIMILAR-EQUIV-IMPLIES-INIT->INIT-N->M") (mkpair (mkpair (mksym "ACL2"
1045"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
1046"ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (
1047mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
1048mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym
1049"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
1050"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
1051"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
1052mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
1053"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
1054mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "ACL2"
1055"C-BISIMILAR-INITIAL-STATE-WITNESS-N->M") (mkpair (mksym "ACL2" "M") (mkpair (
1056mksym "ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (
1057mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
1058mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD"
1059"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
1060mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
1061"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
1062,
1063
1064(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
1065"C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-M->N") (mkpair (mkpair (
1066mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
1067mkpair (mksym "ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair (
1068mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
1069mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair (
1070mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1071mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (
1072mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1073"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
1074"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
1075mkpair (mkpair (mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "S") (
1076mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym "ACL2"
1077"C-BISIMILAR-INITIAL-STATE-WITNESS-M->N") (mkpair (mksym "ACL2" "S") (mkpair (
1078mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (
1079mksym "COMMON-LISP" "NIL")))))) (mkpair (mksym "ACL2" "N") (mkpair (mksym
1080"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP" "NIL")))) (
1081mksym "COMMON-LISP" "NIL"))))
1082,
1083
1084(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
1085"C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-N->M") (mkpair (mkpair (
1086mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
1087mkpair (mksym "ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair (
1088mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
1089mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair (
1090mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1091mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (
1092mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1093"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
1094"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
1095mkpair (mkpair (mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mkpair (mksym "ACL2"
1096"C-BISIMILAR-INITIAL-STATE-WITNESS-N->M") (mkpair (mksym "ACL2" "M") (mkpair (
1097mksym "ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (
1098mksym "COMMON-LISP" "NIL")))))) (mkpair (mksym "ACL2" "M") (mkpair (mksym
1099"ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym
1100"COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP" "NIL")))) (mksym
1101"COMMON-LISP" "NIL"))))
1102,
1103
1104(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
1105"C-BISIMILAR-STATES-HAVE-LABELS-EQUAL") (mkpair (mkpair (mksym "ACL2"
1106"IMPLIES") (mkpair (mkpair (mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym
1107"ACL2" "P") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (
1108mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (
1109mkpair (mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mkpair (mksym "ACL2"
1110"SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym
1111"ACL2" "Q") (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (
1112mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1113"ACL2" "SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (
1114mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
1115mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym
1116"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
1117"NIL"))))
1118,
1119
1120(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
1121"C-BISIMILAR-WITNESS-MEMBER-OF-STATES-M->N") (mkpair (mkpair (mksym "ACL2"
1122"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
1123"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (
1124mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2"
1125"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym
1126"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair (
1127mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (
1128mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (
1129mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
1130mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
1131"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (
1132mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1133mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
1134"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1135mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
1136"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
1137mkpair (mksym "ACL2" "C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair (mksym
1138"ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (mkpair (
1139mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (
1140mksym "COMMON-LISP" "NIL")))))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
1141mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
1142mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP"
1143"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
1144mksym "COMMON-LISP" "NIL"))))
1145,
1146
1147(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
1148"C-BISIMILAR-WITNESS-MEMBER-OF-STATES-N->M") (mkpair (mkpair (mksym "ACL2"
1149"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
1150"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (
1151mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2"
1152"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym
1153"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair (
1154mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "N") (
1155mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (
1156mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
1157mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
1158"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (
1159mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1160mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
1161"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
1162mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
1163"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (
1164mkpair (mksym "ACL2" "C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mksym
1165"ACL2" "P") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (
1166mksym "ACL2" "R") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (
1167mksym "COMMON-LISP" "NIL")))))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (
1168mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
1169mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP"
1170"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
1171mksym "COMMON-LISP" "NIL"))))
1172,
1173
1174(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
1175"C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-M->N") (mkpair (mkpair (mksym
1176"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (
1177mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym
1178"ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (
1179mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym
1180"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (
1181mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
1182mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1183"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1184"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (
1185mkpair (mkpair (mksym "ACL2" "C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair (
1186mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (
1187mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2"
1188"VARS") (mksym "COMMON-LISP" "NIL")))))))) (mkpair (mksym "ACL2" "N") (mkpair (
1189mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP"
1190"NIL")))) (mksym "COMMON-LISP" "NIL"))))
1191,
1192
1193(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
1194"C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-N->M") (mkpair (mkpair (mksym
1195"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (
1196mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym
1197"ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (
1198mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym
1199"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") (
1200mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
1201mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1202"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1203"ACL2" "CIRCUIT-BISIM") (mkpair (mkpair (mksym "ACL2"
1204"C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mksym "ACL2" "P") (mkpair (
1205mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") (
1206mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
1207"NIL")))))))) (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "R") (mkpair (
1208mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (
1209mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
1210,
1211
1212(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
1213"C-BISIMILAR-WITNESS-MATCHES-TRANSITION-M->N") (mkpair (mkpair (mksym "ACL2"
1214"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
1215"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (
1216mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2"
1217"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2"
1218"NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair (
1219mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1220"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1221"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1222"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym
1223"ACL2" "C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair (mksym "ACL2" "P") (
1224mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2"
1225"Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym
1226"COMMON-LISP" "NIL")))))))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP"
1227"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
1228,
1229
1230(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2"
1231"C-BISIMILAR-WITNESS-MATCHES-TRANSITION-N->M") (mkpair (mkpair (mksym "ACL2"
1232"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
1233"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (
1234mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2"
1235"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2"
1236"NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") (mkpair (
1237mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1238"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
1239"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
1240"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym
1241"ACL2" "C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mksym "ACL2" "P") (
1242mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2"
1243"R") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym
1244"COMMON-LISP" "NIL")))))))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP"
1245"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
1246
1247];
1248