1 2val _ = current_package := 3 implode(map chr (cons 65 (cons 67 (cons 76 (cons 50 nil))))); 4 5val _ = sexp.acl2_list_ref := [ 6 7(mkpair (mksym "ACL2" "INCLUDE-BOOK") (mkpair (mk_chars_str (chars_to_string ( 8cons 116 (cons 111 (cons 116 (cons 97 (cons 108 (cons 45 (cons 111 (cons 114 ( 9cons 100 (cons 101 (cons 114 nil))))))))))))) (mksym "COMMON-LISP" "NIL"))) 10, 11 12(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "MEMBERP") ( 13mkpair (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym 14"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 15mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "X") (mksym 16"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 17mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (mkpair ( 18mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 19"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 20"COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym 21"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 22mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 23mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 24mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 25mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 26mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 27"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 28, 29 30(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "DROP") (mkpair ( 31mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 32"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 33"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 34mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 35"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 36"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") ( 37mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 38"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 39"ACL2" "DROP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym 40"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 41mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") ( 42mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 43"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "DROP") (mkpair (mksym 44"ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" 45"X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 46"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 47"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 48, 49 50(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "INSERT") (mkpair ( 51mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 52"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 53"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 54mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "A") ( 55mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 56"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair ( 57mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 58"EQUAL") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" 59"CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym 60"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym 61"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "<<") (mkpair (mksym "ACL2" 62"A") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") ( 63mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 64mksym "COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" 65"X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 66"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") ( 67mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "INSERT") (mkpair ( 68mksym "ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym 69"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 70mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 71"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 72"NIL"))))) 73, 74 75(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ORDEREDP") ( 76mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair ( 77mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") ( 78mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 79"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 80"COMMON-LISP" "ENDP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 81mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 82mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "<<") ( 83mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 84"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 85mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 86"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 87"NIL")))) (mkpair (mkpair (mksym "ACL2" "ORDEREDP") (mkpair (mkpair (mksym 88"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 89mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 90mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 91"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 92"NIL"))))) 93, 94 95(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "UNIQUEP") ( 96mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair ( 97mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") ( 98mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 99mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 100"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 101"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair ( 102mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 103"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" 104"X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 105"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "UNIQUEP") (mkpair ( 106mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 107"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 108"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 109"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 110"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 111, 112 113(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBERP-INSERT-SAME") ( 114mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" 115"MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "INSERT") ( 116mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 117"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 118"QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) ( 119mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 120, 121 122(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBERP-INSERT-DIFF") ( 123mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" 124"NOT") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" 125"A") (mkpair (mksym "ACL2" "B") (mksym "COMMON-LISP" "NIL")))) (mksym 126"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair ( 127mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair ( 128mksym "ACL2" "INSERT") (mkpair (mksym "ACL2" "B") (mkpair (mksym "ACL2" "X") ( 129mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 130mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") ( 131mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 132"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 133, 134 135(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBERP-DROP-SAME") ( 136mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" 137"MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "DROP") ( 138mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 139"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 140"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 141mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 142, 143 144(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBERP-DROP-DIFF") ( 145mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" 146"NOT") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" 147"A") (mkpair (mksym "ACL2" "B") (mksym "COMMON-LISP" "NIL")))) (mksym 148"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair ( 149mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair ( 150mksym "ACL2" "DROP") (mkpair (mksym "ACL2" "B") (mkpair (mksym "ACL2" "X") ( 151mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 152mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") ( 153mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 154"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 155, 156 157(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 158"ORDERED-IMPLIES-UNIQUE") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 159mkpair (mksym "ACL2" "ORDEREDP") (mkpair (mksym "ACL2" "X") (mksym 160"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "UNIQUEP") (mkpair ( 161mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 162mksym "COMMON-LISP" "NIL")))) 163, 164 165(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 166"MEMBERP-YES-REDUCE-INSERT") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 167mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ORDEREDP") ( 168mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 169mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") ( 170mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 171mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 172"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") ( 173mkpair (mkpair (mksym "ACL2" "INSERT") (mkpair (mksym "ACL2" "A") (mkpair ( 174mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "X") ( 175mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 176"COMMON-LISP" "NIL")))) 177, 178 179(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 180"MEMBERP-NO-REDUCE-DROP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 181mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUE-LISTP") ( 182mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 183mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 184mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) ( 185mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 186mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 187"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") ( 188mkpair (mkpair (mksym "ACL2" "DROP") (mkpair (mksym "ACL2" "A") (mkpair ( 189mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "X") ( 190mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 191"COMMON-LISP" "NIL")))) 192, 193 194(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 195"DROP-PRESERVES-ORDEREDP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 196mkpair (mksym "ACL2" "ORDEREDP") (mkpair (mksym "ACL2" "X") (mksym 197"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ORDEREDP") (mkpair ( 198mkpair (mksym "ACL2" "DROP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" 199"X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym 200"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 201, 202 203(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 204"INSERT-PRESERVES-ORDEREDP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 205mkpair (mksym "ACL2" "ORDEREDP") (mkpair (mksym "ACL2" "X") (mksym 206"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ORDEREDP") (mkpair ( 207mkpair (mksym "ACL2" "INSERT") (mkpair (mksym "ACL2" "A") (mkpair (mksym 208"ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) ( 209mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 210, 211 212(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 213"DROP-OF-INSERT-IS-SAME") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 214mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUE-LISTP") ( 215mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 216mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 217mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) ( 218mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 219mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 220"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") ( 221mkpair (mkpair (mksym "ACL2" "DROP") (mkpair (mksym "ACL2" "A") (mkpair ( 222mkpair (mksym "ACL2" "INSERT") (mkpair (mksym "ACL2" "A") (mkpair (mksym 223"ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 224mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 225"NIL")))) (mksym "COMMON-LISP" "NIL")))) 226, 227 228(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 229"INSERT-OF-DROP-IS-SAME") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 230mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ORDEREDP") ( 231mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 232mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUE-LISTP") (mkpair ( 233mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 234"MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym 235"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 236mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 237"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 238"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 239mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" 240"INSERT") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "DROP") ( 241mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 242"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "X") (mksym 243"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 244"NIL")))) 245, 246 247(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 248"INSERT-RETURNS-TRUE-LISTS") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 249mkpair (mksym "ACL2" "TRUE-LISTP") (mkpair (mksym "ACL2" "X") (mksym 250"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "TRUE-LISTP") (mkpair ( 251mkpair (mksym "ACL2" "INSERT") (mkpair (mksym "ACL2" "A") (mkpair (mksym 252"ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) ( 253mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 254 255]; 256