1(* File created from HOL using print_acl2_defun_script on Mon Jun 19 15:43:10 2006 *)
2
3open HolKernel Parse boolLib bossLib;
4open stringLib complex_rationalTheory gcdTheory sexp sexpTheory;
5val _ = new_theory "basic_defaxioms";
6
7val name_alist =
8[("acl2_colon__colon_iff","ACL2::IFF"),("acl2_colon__colon_booleanp","ACL2::BOOLEANP"),("acl2_colon__colon_implies","ACL2::IMPLIES"),("common_lisp_colon__colon_not","COMMON-LISP::NOT"),("acl2_colon__colon_hide","ACL2::HIDE"),("common_lisp_colon__colon_eq","COMMON-LISP::EQ"),("acl2_colon__colon_true_listp","ACL2::TRUE-LISTP"),("acl2_colon__colon_list_macro","ACL2::LIST-MACRO"),("acl2_colon__colon_and_macro","ACL2::AND-MACRO"),("acl2_colon__colon_or_macro","ACL2::OR-MACRO"),("acl2_colon__colon_integer_abs","ACL2::INTEGER-ABS"),("acl2_colon__colon_xxxjoin","ACL2::XXXJOIN"),("acl2_colon__colon_len","ACL2::LEN"),("common_lisp_colon__colon_length","COMMON-LISP::LENGTH"),("acl2_colon__colon_acl2_count","ACL2::ACL2-COUNT"),("acl2_colon__colon_cond_clausesp","ACL2::COND-CLAUSESP"),("acl2_colon__colon_cond_macro","ACL2::COND-MACRO"),("acl2_colon__colon_eqlablep","ACL2::EQLABLEP"),("acl2_colon__colon_eqlable_listp","ACL2::EQLABLE-LISTP"),("common_lisp_colon__colon_atom","COMMON-LISP::ATOM"),("acl2_colon__colon_make_character_list","ACL2::MAKE-CHARACTER-LIST"),("acl2_colon__colon_eqlable_alistp","ACL2::EQLABLE-ALISTP"),("acl2_colon__colon_alistp","ACL2::ALISTP"),("common_lisp_colon__colon_acons","COMMON-LISP::ACONS"),("common_lisp_colon__colon_endp","COMMON-LISP::ENDP"),("acl2_colon__colon_must_be_equal","ACL2::MUST-BE-EQUAL"),("acl2_colon__colon_member_equal","ACL2::MEMBER-EQUAL"),("acl2_colon__colon_union_equal","ACL2::UNION-EQUAL"),("acl2_colon__colon_subsetp_equal","ACL2::SUBSETP-EQUAL"),("acl2_colon__colon_symbol_listp","ACL2::SYMBOL-LISTP"),("common_lisp_colon__colon_null","COMMON-LISP::NULL"),("acl2_colon__colon_member_eq","ACL2::MEMBER-EQ"),("acl2_colon__colon_subsetp_eq","ACL2::SUBSETP-EQ"),("acl2_colon__colon_symbol_alistp","ACL2::SYMBOL-ALISTP"),("acl2_colon__colon_assoc_eq","ACL2::ASSOC-EQ"),("acl2_colon__colon_assoc_equal","ACL2::ASSOC-EQUAL"),("acl2_colon__colon_assoc_eq_equal_alistp","ACL2::ASSOC-EQ-EQUAL-ALISTP"),("acl2_colon__colon_assoc_eq_equal","ACL2::ASSOC-EQ-EQUAL"),("acl2_colon__colon_no_duplicatesp_equal","ACL2::NO-DUPLICATESP-EQUAL"),("acl2_colon__colon_strip_cars","ACL2::STRIP-CARS"),("common_lisp_colon__colon_eql","COMMON-LISP::EQL"),("common_lisp_colon__colon__eq_","COMMON-LISP::="),("common_lisp_colon__colon__slash__eq_","COMMON-LISP::/="),("acl2_colon__colon_zp","ACL2::ZP"),("acl2_colon__colon_zip","ACL2::ZIP"),("common_lisp_colon__colon_nth","COMMON-LISP::NTH"),("common_lisp_colon__colon_char","COMMON-LISP::CHAR"),("acl2_colon__colon_proper_consp","ACL2::PROPER-CONSP"),("acl2_colon__colon_improper_consp","ACL2::IMPROPER-CONSP"),("common_lisp_colon__colon_conjugate","COMMON-LISP::CONJUGATE"),("acl2_colon__colon_prog2_dollar_","ACL2::PROG2$"),("acl2_colon__colon_time_dollar_","ACL2::TIME$"),("acl2_colon__colon_fix","ACL2::FIX"),("acl2_colon__colon_force","ACL2::FORCE"),("acl2_colon__colon_immediate_force_modep","ACL2::IMMEDIATE-FORCE-MODEP"),("acl2_colon__colon_case_split","ACL2::CASE-SPLIT"),("acl2_colon__colon_synp","ACL2::SYNP"),("common_lisp_colon__colon_member","COMMON-LISP::MEMBER"),("acl2_colon__colon_no_duplicatesp","ACL2::NO-DUPLICATESP"),("common_lisp_colon__colon_assoc","COMMON-LISP::ASSOC"),("acl2_colon__colon_r_eqlable_alistp","ACL2::R-EQLABLE-ALISTP"),("common_lisp_colon__colon_rassoc","COMMON-LISP::RASSOC"),("acl2_colon__colon_rassoc_equal","ACL2::RASSOC-EQUAL"),("acl2_colon__colon_r_symbol_alistp","ACL2::R-SYMBOL-ALISTP"),("acl2_colon__colon_rassoc_eq","ACL2::RASSOC-EQ")];
9
10
11val _ = current_package :=
12 implode(map chr (cons 65 (cons 67 (cons 76 (cons 50 nil)))));
13
14val _ = sexp.acl2_list_ref := [
15
16(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "IFF") (mkpair (
17mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mksym "COMMON-LISP"
18"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mksym "ACL2" "P") (
19mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mksym "ACL2" "Q") (mkpair (
20mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym
21"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
22mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
23"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mksym "ACL2"
24"Q") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
25"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
26"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP"
27"NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (
28mksym "COMMON-LISP" "NIL")))))
29,
30
31(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "BOOLEANP") (
32mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
33mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
34"EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP"
35"QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (
36mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
37mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (
38mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (
39mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
40mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
41"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
42,
43
44(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "IMPLIES") (
45mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mksym
46"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
47mksym "ACL2" "P") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mksym
48"ACL2" "Q") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
49"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
50"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
51"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
52"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP"
53"NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
54,
55
56(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "NOT") (
57mkpair (mkpair (mksym "ACL2" "P") (mksym "COMMON-LISP" "NIL")) (mkpair (
58mkpair (mksym "COMMON-LISP" "IF") (mkpair (mksym "ACL2" "P") (mkpair (mkpair (
59mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
60"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
61mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
62"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
63,
64
65(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "HIDE") (mkpair (
66mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mksym "ACL2"
67"X") (mksym "COMMON-LISP" "NIL")))))
68,
69
70(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "EQ") (
71mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
72"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
73mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
74mksym "COMMON-LISP" "NIL")))))
75,
76
77(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "TRUE-LISTP") (
78mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
79mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
80"CONSP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (
81mkpair (mksym "ACL2" "TRUE-LISTP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
82mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
83"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQ") (mkpair (mksym "ACL2" "X") (
84mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
85"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
86"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
87,
88
89(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LIST-MACRO") (
90mkpair (mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL")) (mkpair (
91mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
92"CONSP") (mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
93mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP"
94"QUOTE") (mkpair (mksym "COMMON-LISP" "CONS") (mksym "COMMON-LISP" "NIL"))) (
95mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym
96"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (
97mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "ACL2"
98"LIST-MACRO") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
99"ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
100mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
101"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
102"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
103"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
104"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
105"NIL")))))
106,
107
108(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "AND-MACRO") (
109mkpair (mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL")) (mkpair (
110mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
111"CONSP") (mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
112mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
113"CONSP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2"
114"LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
115mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP"
116"QUOTE") (mkpair (mksym "COMMON-LISP" "IF") (mksym "COMMON-LISP" "NIL"))) (
117mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym
118"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (
119mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "ACL2"
120"AND-MACRO") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
121"ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
122mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym
123"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
124"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
125mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
126"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
127mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
128mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym
129"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
130mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mksym
131"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
132,
133
134(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "OR-MACRO") (
135mkpair (mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL")) (mkpair (
136mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
137"CONSP") (mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mkpair (
138mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
139"CONSP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2"
140"LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
141mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP"
142"QUOTE") (mkpair (mksym "COMMON-LISP" "IF") (mksym "COMMON-LISP" "NIL"))) (
143mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym
144"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (
145mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym
146"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (
147mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "ACL2"
148"OR-MACRO") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2"
149"LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
150mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
151mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
152"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
153"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2"
154"LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
155mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
156mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
157"COMMON-LISP" "NIL")))))
158,
159
160(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "INTEGER-ABS") (
161mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
162mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
163"INTEGERP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (
164mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "<") (
165mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
166mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
167"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "UNARY--") (mkpair (
168mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "X") (
169mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
170mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym
171"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
172,
173
174(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "XXXJOIN") (
175mkpair (mkpair (mksym "ACL2" "FN") (mkpair (mksym "ACL2" "ARGS") (mksym
176"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
177mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
178mkpair (mksym "ACL2" "ARGS") (mksym "COMMON-LISP" "NIL"))) (mksym
179"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
180mksym "ACL2" "FN") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
181mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ARGS") (mksym
182"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
183mkpair (mksym "ACL2" "XXXJOIN") (mkpair (mksym "ACL2" "FN") (mkpair (mkpair (
184mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ARGS") (mksym "COMMON-LISP"
185"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
186"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (
187mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
188"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
189mksym "ACL2" "FN") (mkpair (mksym "ACL2" "ARGS") (mksym "COMMON-LISP" "NIL")))) (
190mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
191,
192
193(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LEN") (mkpair (
194mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
195"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (
196mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
197"BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1"
198"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
199"LEN") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (
200mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym
201"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
202mknum "0" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
203"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
204,
205
206(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "LENGTH") (
207mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
208mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
209"STRINGP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (
210mkpair (mksym "ACL2" "LEN") (mkpair (mkpair (mksym "COMMON-LISP" "COERCE") (
211mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
212mkpair (mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (mksym
213"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
214"ACL2" "LEN") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym
215"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
216,
217
218(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ACL2-COUNT") (
219mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
220mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
221"CONSP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (
222mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
223mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
224mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "ACL2" "ACL2-COUNT") (mkpair (
225mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
226"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
227"ACL2" "ACL2-COUNT") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
228mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
229mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
230mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "RATIONALP") (
231mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
232mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "INTEGERP") (
233mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
234mksym "ACL2" "INTEGER-ABS") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
235"NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym
236"ACL2" "INTEGER-ABS") (mkpair (mkpair (mksym "COMMON-LISP" "NUMERATOR") (
237mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
238"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "DENOMINATOR") (mkpair (mksym
239"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
240mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
241mkpair (mkpair (mksym "ACL2" "COMPLEX-RATIONALP") (mkpair (mksym "ACL2" "X") (
242mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") (
243mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (
244mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") (
245mkpair (mkpair (mksym "ACL2" "ACL2-COUNT") (mkpair (mkpair (mksym
246"COMMON-LISP" "REALPART") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
247"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
248"ACL2-COUNT") (mkpair (mkpair (mksym "COMMON-LISP" "IMAGPART") (mkpair (mksym
249"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
250mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
251mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "STRINGP") (
252mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
253mksym "COMMON-LISP" "LENGTH") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
254"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1"
255"0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
256"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
257"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
258,
259
260(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "COND-CLAUSESP") (
261mkpair (mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP" "NIL")) (mkpair (
262mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
263"CONSP") (mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP" "NIL"))) (
264mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
265"COMMON-LISP" "CONSP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
266mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
267"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
268"ACL2" "TRUE-LISTP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
269mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
270"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
271"COMMON-LISP" "<") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mkpair (
272mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "CLAUSES") (mksym
273"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
274"COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym "COMMON-LISP"
275"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
276"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQ") (mkpair (mkpair (mksym
277"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
278mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
279"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
280"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
281mkpair (mkpair (mksym "COMMON-LISP" "EQ") (mkpair (mkpair (mksym
282"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP"
283"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
284"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
285mkpair (mkpair (mksym "ACL2" "COND-CLAUSESP") (mkpair (mkpair (mksym
286"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP"
287"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
288mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
289"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
290mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
291mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (
292mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
293"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
294"COMMON-LISP" "EQ") (mkpair (mksym "ACL2" "CLAUSES") (mkpair (mkpair (mksym
295"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
296"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
297"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
298,
299
300(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "COND-MACRO") (
301mkpair (mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP" "NIL")) (mkpair (
302mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
303"CONSP") (mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP" "NIL"))) (
304mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
305"COMMON-LISP" "EQ") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
306mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "CLAUSES") (mksym
307"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
308"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP"
309"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
310"IF") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym
311"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP"
312"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
313"CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym
314"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP"
315"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
316mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
317mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP" "NIL"))) (mksym
318"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
319"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
320mksym "COMMON-LISP" "IF") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
321mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
322mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "CLAUSES") (
323mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
324mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
325mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym
326"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP"
327"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
328"CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym
329"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP"
330"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
331mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
332mkpair (mksym "ACL2" "CLAUSES") (mksym "COMMON-LISP" "NIL"))) (mksym
333"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
334"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "ACL2" "COND-MACRO") (mkpair (
335mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "CLAUSES") (mksym
336"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
337"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
338"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
339"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
340mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
341mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym
342"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
343,
344
345(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "EQLABLEP") (
346mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
347mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
348"ACL2-NUMBERP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
349mkpair (mkpair (mksym "ACL2" "ACL2-NUMBERP") (mkpair (mksym "ACL2" "X") (
350mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (
351mkpair (mkpair (mksym "COMMON-LISP" "SYMBOLP") (mkpair (mksym "ACL2" "X") (
352mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "SYMBOLP") (
353mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
354mksym "COMMON-LISP" "CHARACTERP") (mkpair (mksym "ACL2" "X") (mksym
355"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
356"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
357,
358
359(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "EQLABLE-LISTP") (
360mkpair (mkpair (mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL")) (mkpair (
361mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
362"CONSP") (mkpair (mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (mkpair (
363mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EQLABLEP") (
364mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "L") (mksym
365"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
366"ACL2" "EQLABLE-LISTP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
367mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
368mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
369"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
370mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "L") (mkpair (
371mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
372mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
373"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
374,
375
376(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "ATOM") (
377mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
378mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "COMMON-LISP"
379"CONSP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym
380"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))
381,
382
383(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
384"MAKE-CHARACTER-LIST") (mkpair (mkpair (mksym "ACL2" "X") (mksym
385"COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
386mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "X") (mksym
387"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
388mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
389mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CHARACTERP") (
390mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
391"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
392"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
393mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
394"MAKE-CHARACTER-LIST") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
395mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
396mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (
397mkpair (mkpair (mksym "COMMON-LISP" "CODE-CHAR") (mkpair (mkpair (mksym
398"COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
399"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
400"MAKE-CHARACTER-LIST") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
401mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
402mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym
403"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
404,
405
406(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "EQLABLE-ALISTP") (
407mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
408mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (
409mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
410mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (
411mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
412"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
413"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (
414mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
415"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
416"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EQLABLEP") (mkpair (mkpair (
417mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
418mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
419"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
420"EQLABLE-ALISTP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
421"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
422mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
423"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
424mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
425mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
426"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
427,
428
429(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ALISTP") (mkpair (
430mkpair (mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
431"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (
432mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
433"COMMON-LISP" "EQ") (mkpair (mksym "ACL2" "L") (mkpair (mkpair (mksym
434"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
435"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
436"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (
437mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "L") (mksym
438"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
439"ACL2" "ALISTP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
440"ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
441mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
442"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
443"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
444,
445
446(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "ACONS") (
447mkpair (mkpair (mksym "ACL2" "KEY") (mkpair (mksym "ACL2" "DATUM") (mkpair (
448mksym "ACL2" "ALIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
449"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
450mksym "ACL2" "KEY") (mkpair (mksym "ACL2" "DATUM") (mksym "COMMON-LISP" "NIL")))) (
451mkpair (mksym "ACL2" "ALIST") (mksym "COMMON-LISP" "NIL")))) (mksym
452"COMMON-LISP" "NIL")))))
453,
454
455(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "ENDP") (
456mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
457mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "X") (mksym
458"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))
459,
460
461(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "MUST-BE-EQUAL") (
462mkpair (mkpair (mksym "ACL2" "LOGIC") (mkpair (mksym "ACL2" "EXEC") (mksym
463"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "LOGIC") (mksym "COMMON-LISP"
464"NIL")))))
465,
466
467(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "MEMBER-EQUAL") (
468mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "LST") (mksym
469"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
470mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "LST") (mksym
471"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
472mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
473mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
474mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
475mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
476mkpair (mksym "ACL2" "LST") (mkpair (mkpair (mksym "ACL2" "MEMBER-EQUAL") (
477mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
478mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
479mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym
480"COMMON-LISP" "NIL")))))
481,
482
483(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "UNION-EQUAL") (
484mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
485"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
486mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym
487"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mkpair (mkpair (mksym
488"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBER-EQUAL") (mkpair (
489mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
490"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
491mkpair (mkpair (mksym "ACL2" "UNION-EQUAL") (mkpair (mkpair (mksym
492"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
493mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
494mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
495mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
496mksym "ACL2" "UNION-EQUAL") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
497mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
498"Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym
499"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
500"NIL")))))
501,
502
503(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SUBSETP-EQUAL") (
504mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
505"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
506mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym
507"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
508mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
509"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBER-EQUAL") (mkpair (
510mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
511"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
512mkpair (mkpair (mksym "ACL2" "SUBSETP-EQUAL") (mkpair (mkpair (mksym
513"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
514mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
515mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
516"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
517"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
518,
519
520(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SYMBOL-LISTP") (
521mkpair (mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL")) (mkpair (
522mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (
523mkpair (mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
524mksym "COMMON-LISP" "EQ") (mkpair (mksym "ACL2" "LST") (mkpair (mkpair (mksym
525"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
526"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
527"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "SYMBOLP") (mkpair (
528mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "LST") (mksym
529"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
530"ACL2" "SYMBOL-LISTP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
531mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
532mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
533"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
534"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
535,
536
537(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "NULL") (
538mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
539mkpair (mksym "COMMON-LISP" "EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (
540mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
541"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
542"NIL")))))
543,
544
545(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "MEMBER-EQ") (
546mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "LST") (mksym
547"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
548mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "LST") (mksym
549"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
550mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
551mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQ") (mkpair (
552mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym
553"ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
554mkpair (mksym "ACL2" "LST") (mkpair (mkpair (mksym "ACL2" "MEMBER-EQ") (
555mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
556mksym "ACL2" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
557mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym
558"COMMON-LISP" "NIL")))))
559,
560
561(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SUBSETP-EQ") (
562mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
563"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
564mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym
565"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
566mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
567"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBER-EQ") (mkpair (
568mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
569"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
570mkpair (mkpair (mksym "ACL2" "SUBSETP-EQ") (mkpair (mkpair (mksym
571"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
572mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
573mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
574"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
575"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
576,
577
578(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SYMBOL-ALISTP") (
579mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
580mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (
581mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
582mksym "COMMON-LISP" "EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
583"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
584"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
585"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (
586mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
587"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
588"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "SYMBOLP") (mkpair (
589mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
590mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
591"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
592"SYMBOL-ALISTP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
593"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
594mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
595"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
596mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
597mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
598"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
599,
600
601(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ") (
602mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "ALIST") (mksym
603"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
604mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "ALIST") (mksym
605"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
606mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
607mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQ") (mkpair (
608mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (
609mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ALIST") (mksym
610"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
611"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2"
612"ALIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
613"ASSOC-EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP"
614"CDR") (mkpair (mksym "ACL2" "ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym
615"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
616"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
617,
618
619(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQUAL") (
620mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "ALIST") (mksym
621"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
622mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "ALIST") (mksym
623"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
624mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
625mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
626mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
627mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ALIST") (mksym
628"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
629"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2"
630"ALIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
631"ASSOC-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
632"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ALIST") (mksym "COMMON-LISP"
633"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (
634mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
635,
636
637(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
638"ASSOC-EQ-EQUAL-ALISTP") (mkpair (mkpair (mksym "ACL2" "X") (mksym
639"COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
640mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "X") (mksym
641"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQ") (mkpair (
642mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
643mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
644"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
645"COMMON-LISP" "CONSP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
646mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
647mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
648"COMMON-LISP" "SYMBOLP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
649mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
650"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
651"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
652"COMMON-LISP" "CONSP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
653mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
654"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
655"NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL-ALISTP") (mkpair (
656mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym
657"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
658"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
659"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
660"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
661"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym
662"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
663"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
664"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
665,
666
667(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") (
668mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mkpair (mksym
669"ACL2" "ALIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
670"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (
671mksym "ACL2" "ALIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
672"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
673"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
674mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQ") (
675mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym
676"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ALIST") (mksym "COMMON-LISP"
677"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "X") (mksym
678"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
679mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
680mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ALIST") (
681mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym
682"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
683mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
684"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
685mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ALIST") (mksym
686"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") (
687mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mkpair (mkpair (mksym
688"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ALIST") (mksym "COMMON-LISP"
689"NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (
690mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
691,
692
693(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
694"NO-DUPLICATESP-EQUAL") (mkpair (mkpair (mksym "ACL2" "L") (mksym
695"COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
696mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "L") (mksym
697"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
698mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
699"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBER-EQUAL") (mkpair (
700mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "L") (mksym
701"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
702mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
703mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
704"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
705"NO-DUPLICATESP-EQUAL") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
706mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
707mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym
708"COMMON-LISP" "NIL")))))
709,
710
711(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "STRIP-CARS") (
712mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
713mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (
714mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
715mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
716"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (
717mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
718mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
719"NIL"))) (mkpair (mkpair (mksym "ACL2" "STRIP-CARS") (mkpair (mkpair (mksym
720"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
721mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym
722"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
723,
724
725(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "EQL") (
726mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
727"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
728mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
729mksym "COMMON-LISP" "NIL")))))
730,
731
732(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "=") (
733mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
734"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (
735mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (
736mksym "COMMON-LISP" "NIL")))))
737,
738
739(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "/=") (
740mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym
741"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (
742mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (
743mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (
744mksym "COMMON-LISP" "NIL")))))
745,
746
747(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ZP") (mkpair (
748mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
749"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "INTEGERP") (mkpair (
750mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
751"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "COMMON-LISP" "<") (mkpair (
752mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym
753"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (
754mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
755mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mksym
756"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
757,
758
759(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ZIP") (mkpair (
760mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
761"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "INTEGERP") (mkpair (
762mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
763"COMMON-LISP" "=") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
764"COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP"
765"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP"
766"QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (
767mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
768,
769
770(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "NTH") (
771mkpair (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "L") (mksym
772"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
773mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "L") (mksym
774"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
775mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
776mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym
777"ACL2" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
778"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (
779mkpair (mkpair (mksym "COMMON-LISP" "NTH") (mkpair (mkpair (mksym "ACL2"
780"BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1"
781"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym
782"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
783mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
784mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym
785"COMMON-LISP" "NIL")))))
786,
787
788(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "CHAR") (
789mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "N") (mksym
790"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "NTH") (mkpair (
791mksym "ACL2" "N") (mkpair (mkpair (mksym "COMMON-LISP" "COERCE") (mkpair (
792mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
793mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (mksym
794"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP"
795"NIL")))))
796,
797
798(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "PROPER-CONSP") (
799mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
800mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
801"CONSP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (
802mkpair (mksym "ACL2" "TRUE-LISTP") (mkpair (mksym "ACL2" "X") (mksym
803"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
804mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
805"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
806,
807
808(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "IMPROPER-CONSP") (
809mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
810mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
811"CONSP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (
812mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "TRUE-LISTP") (
813mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
814"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
815"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
816mksym "COMMON-LISP" "NIL")))))
817,
818
819(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP"
820"CONJUGATE") (mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (
821mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2"
822"COMPLEX-RATIONALP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
823mkpair (mkpair (mksym "COMMON-LISP" "COMPLEX") (mkpair (mkpair (mksym
824"COMMON-LISP" "REALPART") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
825"NIL"))) (mkpair (mkpair (mksym "ACL2" "UNARY--") (mkpair (mkpair (mksym
826"COMMON-LISP" "IMAGPART") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
827"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
828mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
829,
830
831(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "PROG2$") (mkpair (
832mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP"
833"NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))))
834,
835
836(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "TIME$") (mkpair (
837mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mksym "ACL2"
838"X") (mksym "COMMON-LISP" "NIL")))))
839,
840
841(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "FIX") (mkpair (
842mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
843"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ACL2-NUMBERP") (mkpair (
844mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "X") (
845mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (
846mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
847"COMMON-LISP" "NIL")))))
848,
849
850(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "FORCE") (mkpair (
851mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mksym "ACL2"
852"X") (mksym "COMMON-LISP" "NIL")))))
853,
854
855(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
856"IMMEDIATE-FORCE-MODEP") (mkpair (mksym "COMMON-LISP" "NIL") (mkpair (mkpair (
857mksym "COMMON-LISP" "QUOTE") (mkpair (mk_chars_str (chars_to_string (cons 83 (
858cons 101 (cons 101 (cons 32 (cons 58 (cons 68 (cons 79 (cons 67 (cons 32 (
859cons 105 (cons 109 (cons 109 (cons 101 (cons 100 (cons 105 (cons 97 (cons 116 (
860cons 101 (cons 45 (cons 102 (cons 111 (cons 114 (cons 99 (cons 101 (cons 45 (
861cons 109 (cons 111 (cons 100 (cons 101 (cons 112 (cons 46 nil))))))))))))))))))))))))))))))))) (
862mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))))
863,
864
865(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CASE-SPLIT") (
866mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mksym
867"ACL2" "X") (mksym "COMMON-LISP" "NIL")))))
868,
869
870(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SYNP") (mkpair (
871mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "FORM") (mkpair (mksym
872"ACL2" "TERM") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
873"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP"
874"NIL"))) (mksym "COMMON-LISP" "NIL")))))
875,
876
877(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "MEMBER") (
878mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "L") (mksym
879"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
880mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "L") (mksym
881"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
882mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
883mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair (
884mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym
885"ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
886mkpair (mksym "ACL2" "L") (mkpair (mkpair (mksym "COMMON-LISP" "MEMBER") (
887mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
888mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
889mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym
890"COMMON-LISP" "NIL")))))
891,
892
893(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "NO-DUPLICATESP") (
894mkpair (mkpair (mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL")) (mkpair (
895mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (
896mkpair (mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
897mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym
898"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
899mkpair (mksym "COMMON-LISP" "MEMBER") (mkpair (mkpair (mksym "COMMON-LISP"
900"CAR") (mkpair (mksym "ACL2" "L") (mksym "COMMON-LISP" "NIL"))) (mkpair (
901mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "L") (mksym
902"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
903"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
904"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "NO-DUPLICATESP") (
905mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "L") (mksym
906"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
907"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
908,
909
910(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "ASSOC") (
911mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "ALIST") (mksym
912"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
913mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "ALIST") (mksym
914"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
915mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
916mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair (
917mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (
918mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ALIST") (mksym
919"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
920"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2"
921"ALIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
922"ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP"
923"CDR") (mkpair (mksym "ACL2" "ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym
924"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
925"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
926,
927
928(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2"
929"R-EQLABLE-ALISTP") (mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
930"NIL")) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym
931"COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
932mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "X") (
933mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
934"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (
935mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP"
936"CONSP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2"
937"X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (
938mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EQLABLEP") (
939mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym
940"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (
941mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
942mksym "ACL2" "R-EQLABLE-ALISTP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (
943mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
944"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
945"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (
946mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
947"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
948"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
949,
950
951(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "RASSOC") (
952mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "ALIST") (mksym
953"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
954mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "ALIST") (mksym
955"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
956mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
957mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair (
958mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (
959mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ALIST") (mksym
960"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
961"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2"
962"ALIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP"
963"RASSOC") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP"
964"CDR") (mkpair (mksym "ACL2" "ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym
965"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
966"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
967,
968
969(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "RASSOC-EQUAL") (
970mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "ALIST") (mksym
971"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
972mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "ALIST") (mksym
973"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
974mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
975mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (
976mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
977mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ALIST") (mksym
978"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
979"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2"
980"ALIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
981"RASSOC-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
982"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ALIST") (mksym "COMMON-LISP"
983"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (
984mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
985,
986
987(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "R-SYMBOL-ALISTP") (
988mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (
989mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (
990mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
991mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (
992mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym
993"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
994"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (
995mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym
996"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
997"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "SYMBOLP") (mkpair (
998mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
999mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
1000"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
1001"R-SYMBOL-ALISTP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym
1002"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (
1003mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP"
1004"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
1005mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (
1006mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym
1007"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))))
1008,
1009
1010(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "RASSOC-EQ") (
1011mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "ALIST") (mksym
1012"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (
1013mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "ALIST") (mksym
1014"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
1015mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1016mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQ") (mkpair (
1017mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (
1018mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ALIST") (mksym
1019"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
1020"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2"
1021"ALIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
1022"RASSOC-EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP"
1023"CDR") (mkpair (mksym "ACL2" "ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym
1024"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP"
1025"NIL"))))) (mksym "COMMON-LISP" "NIL")))))
1026
1027];
1028
1029val thl = map (install_and_print o mk_acl2def) (!acl2_list_ref);
1030
1031val _ = (acl2_simps := (!acl2_simps) @ thl);
1032
1033val _ = export_acl2_theory();
1034
1035