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 99 (cons 105 (cons 114 (cons 99 (cons 117 (cons 105 (cons 116 (cons 115 9nil)))))))))) (mksym "COMMON-LISP" "NIL"))) 10, 11 12(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "FIND-VARIABLES*") ( 13mkpair (mkpair (mksym "ACL2" "EQUATION-LIST") (mksym "COMMON-LISP" "NIL")) ( 14mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 15"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "EQUATION-LIST") (mksym 16"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 17mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 18mksym "ACL2" "SET-UNION") (mkpair (mkpair (mksym "ACL2" "FIND-VARIABLES") ( 19mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" 20"EQUATION-LIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 21mkpair (mkpair (mksym "ACL2" "FIND-VARIABLES*") (mkpair (mkpair (mksym 22"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION-LIST") (mksym 23"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 24"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 25, 26 27(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 28"FIND-ALL-VARIABLES-1-PASS") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair ( 29mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 30mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") ( 31mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 32mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 33"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "SET-UNION") (mkpair ( 34mkpair (mksym "ACL2" "FIND-VARIABLES*") (mkpair (mkpair (mksym "ACL2" "G") ( 35mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") ( 36mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQUATIONS") (mksym 37"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 38"ACL2" "FIND-ALL-VARIABLES-1-PASS") (mkpair (mkpair (mksym "COMMON-LISP" 39"CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 40mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 41"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 42, 43 44(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "DEL") (mkpair ( 45mkpair (mksym "ACL2" "E") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 46"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 47"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 48mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 49mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "E") (mkpair ( 50mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 51"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 52"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 53mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym 54"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 55mkpair (mkpair (mksym "ACL2" "DEL") (mkpair (mksym "ACL2" "E") (mkpair ( 56mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 57"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 58"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) ( 59mksym "COMMON-LISP" "NIL"))))) 60, 61 62(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 63"INDUCTION-HINT-FOR-LEN-<=") (mkpair (mkpair (mksym "ACL2" "X") (mkpair ( 64mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 65"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 66mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 67"COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym 68"COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "Y") (mkpair (mkpair (mksym 69"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 70"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 71"NIL")))) (mkpair (mkpair (mksym "ACL2" "INDUCTION-HINT-FOR-LEN-<=") (mkpair ( 72mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 73"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "DEL") (mkpair (mkpair ( 74mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 75"NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym 76"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 77"NIL"))))) 78, 79 80(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 81"FIND-ALL-VARIABLES") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym 82"ACL2" "VARIABLES") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" 83"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 84"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair ( 85mkpair (mksym "ACL2" "UNIQUEP") (mkpair (mksym "ACL2" "VARIABLES") (mksym 86"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 87"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "UNIQUEP") (mkpair (mksym 88"ACL2" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 89mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 90"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "UNIQUEP") (mkpair (mksym 91"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 92mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" 93"UNIQUEP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mksym 94"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair ( 95mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym 96"ACL2" "VARIABLES") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) ( 97mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mksym 98"ACL2" "VARS") (mkpair (mkpair (mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair ( 99mkpair (mksym "ACL2" "NEW-VARS") (mkpair (mksym "ACL2" "EQUATIONS") (mkpair ( 100mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" 101"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 102"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym 103"ACL2" "NEW-VARS") (mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" 104"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 105"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 106mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 107"SET-EQUAL") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "NEW-VARS") ( 108mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mkpair (mkpair ( 109mksym "ACL2" "FIND-ALL-VARIABLES") (mkpair (mksym "ACL2" "NEW-VARS") (mkpair ( 110mksym "ACL2" "VARIABLES") (mkpair (mksym "ACL2" "EQUATIONS") (mksym 111"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 112"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 113"SET-UNION") (mkpair (mkpair (mksym "ACL2" "FIND-ALL-VARIABLES-1-PASS") ( 114mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "EQUATIONS") (mksym 115"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 116"NIL")))) (mkpair (mksym "ACL2" "EQUATIONS") (mkpair (mksym "ACL2" "VARS") ( 117mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" "NIL")))))) (mksym 118"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 119, 120 121(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 122"FIND-ALL-EQUATIONS") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym 123"ACL2" "EQUATIONS") (mkpair (mksym "ACL2" "EQ-REC") (mksym "COMMON-LISP" 124"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 125"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 126"NIL"))) (mkpair (mksym "ACL2" "EQ-REC") (mkpair (mkpair (mksym "ACL2" 127"FIND-ALL-EQUATIONS") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 128mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 129"EQUATIONS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym 130"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) ( 131mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 132mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 133"ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" 134"EQ-REC") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) ( 135mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 136, 137 138(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 139"REMOVE-DUPLICATE-OCCURRENCES") (mkpair (mkpair (mksym "ACL2" "X") (mksym 140"COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 141mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym 142"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym 143"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair ( 144mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 145"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" 146"X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair ( 147mkpair (mksym "ACL2" "REMOVE-DUPLICATE-OCCURRENCES") (mkpair (mkpair (mksym 148"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 149mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") ( 150mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 151"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 152"REMOVE-DUPLICATE-OCCURRENCES") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 153mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 154"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) ( 155mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 156, 157 158(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 159"CORRESPONDING-STATE") (mkpair (mkpair (mksym "ACL2" "INIT") (mkpair (mksym 160"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 161"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 162mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 163"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 164"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair ( 165mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 166"NIL"))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 167"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) ( 168mkpair (mksym "ACL2" "INIT") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 169mksym "ACL2" "CORRESPONDING-STATE") (mkpair (mksym "ACL2" "INIT") (mkpair ( 170mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym 171"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 172"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 173, 174 175(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 176"CORRESPONDING-STATES") (mkpair (mkpair (mksym "ACL2" "INITS") (mkpair (mksym 177"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 178"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 179mksym "ACL2" "INITS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 180"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 181"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair ( 182mkpair (mksym "ACL2" "CORRESPONDING-STATE") (mkpair (mkpair (mksym 183"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "INITS") (mksym "COMMON-LISP" 184"NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 185mkpair (mksym "ACL2" "CORRESPONDING-STATES") (mkpair (mkpair (mksym 186"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "INITS") (mksym "COMMON-LISP" 187"NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym 188"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 189"NIL"))))) 190, 191 192(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CONE-VARIABLES") ( 193mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "C") (mksym 194"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "FIND-ALL-VARIABLES") ( 195mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" 196"REMOVE-DUPLICATE-OCCURRENCES") (mkpair (mksym "ACL2" "VARS") (mksym 197"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 198mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 199"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) ( 200mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 201mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") ( 202mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" 203"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 204"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "EQUATIONS") (mksym 205"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) ( 206mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 207, 208 209(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 210"CONE-OF-INFLUENCE-REDUCTION") (mkpair (mkpair (mksym "ACL2" "C") (mkpair ( 211mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mkpair ( 212mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "VARIABLES") ( 213mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 214mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 215mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 216mksym "ACL2" "FIND-ALL-EQUATIONS") (mkpair (mksym "ACL2" "VARIABLES") (mkpair ( 217mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 218mkpair (mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 219mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 220"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 221"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 222"ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 223"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 224mksym "ACL2" "CORRESPONDING-STATES") (mkpair (mkpair (mksym "ACL2" "G") ( 225mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 226"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") ( 227mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARIABLES") (mksym 228"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair ( 229mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 230"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARIABLES") (mkpair (mkpair ( 231mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 232"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 233"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) ( 234mkpair (mkpair (mksym "ACL2" "CONE-VARIABLES") (mkpair (mksym "ACL2" "VARS") ( 235mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym 236"ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 237, 238 239(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 240"EVALUATION-EQ-MEMBERP-FROM-ALL-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" 241"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 242"ACL2" "ALL-EVALUATIONS-P") (mkpair (mksym "ACL2" "STATES-CONE") (mkpair ( 243mksym "ACL2" "VARS-CONE") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 244mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") ( 245mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "VARS-CONE") (mksym 246"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 247mkpair (mksym "ACL2" "CONSISTENT-P-EQUATIONS") (mkpair (mksym "ACL2" 248"VARS-CONE") (mkpair (mksym "ACL2" "EQN") (mkpair (mksym "ACL2" 249"EQUATIONS-CONE") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 250"ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym 251"ACL2" "PRODUCE-NEXT-STATE") (mkpair (mksym "ACL2" "VARS-CONE") (mkpair ( 252mksym "ACL2" "Q") (mkpair (mksym "ACL2" "EQN") (mksym "COMMON-LISP" "NIL"))))) ( 253mkpair (mksym "ACL2" "VARS-CONE") (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 254mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 255mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 256mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 257"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 258"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 259"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 260"ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "S") (mkpair (mkpair ( 261mksym "ACL2" "CREATE-NEXT-STATES-OF-P") (mkpair (mksym "ACL2" "Q") (mkpair ( 262mksym "ACL2" "STATES-CONE") (mkpair (mksym "ACL2" "VARS-CONE") (mkpair (mksym 263"ACL2" "EQUATIONS-CONE") (mksym "COMMON-LISP" "NIL")))))) (mkpair (mksym 264"ACL2" "VARS-CONE") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 265"NIL")))) (mksym "COMMON-LISP" "NIL")))) 266, 267 268(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 269"CONE-OF-INFLUENCE-REDUCTION-IS-CIRCUIT-P") (mkpair (mkpair (mksym "ACL2" 270"IMPLIES") (mkpair (mkpair (mksym "ACL2" "CIRCUITP") (mkpair (mksym "ACL2" 271"C") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "CIRCUITP") ( 272mkpair (mkpair (mksym "ACL2" "CONE-OF-INFLUENCE-REDUCTION") (mkpair (mksym 273"ACL2" "C") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 274mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 275"COMMON-LISP" "NIL")))) 276, 277 278(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 279"CONE-OF-INFLUENCE-IS-C-BISIMI-EQUIV") (mkpair (mkpair (mksym "ACL2" 280"IMPLIES") (mkpair (mkpair (mksym "ACL2" "CIRCUITP") (mkpair (mksym "ACL2" 281"C") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 282"C-BISIM-EQUIV") (mkpair (mkpair (mksym "ACL2" "CREATE-KRIPKE") (mkpair ( 283mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 284"CREATE-KRIPKE") (mkpair (mkpair (mksym "ACL2" "CONE-OF-INFLUENCE-REDUCTION") ( 285mkpair (mksym "ACL2" "C") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 286"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 287"CONE-VARIABLES") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "C") ( 288mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 289"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 290 291]; 292