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