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