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") (mksym "COMMON-LISP" "NIL")) (mkpair ( 10mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 11mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "EQUATION") ( 12mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") ( 13mkpair (mkpair (mksym "ACL2" "BOOLEANP") (mkpair (mksym "ACL2" "EQUATION") ( 14mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 15mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 16"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 17"COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "EQUATION") (mkpair (mkpair ( 18mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 19"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 20"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 21mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") ( 22mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 23mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym 24"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 25"ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair ( 26mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym 27"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 28"COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym "ACL2" "&") (mkpair (mksym 29"COMMON-LISP" "+") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 30mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 31mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 32"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "SET-UNION") (mkpair ( 33mkpair (mksym "ACL2" "FIND-VARIABLES") (mkpair (mkpair (mksym "COMMON-LISP" 34"CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym 35"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "FIND-VARIABLES") ( 36mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym 37"COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 38mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 39"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym 40"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 41mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 42"EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" 43"EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 44"COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" 45"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 46"EQUAL") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" 47"EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 48"COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "~") (mksym "COMMON-LISP" "NIL"))) ( 49mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 50mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 51"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "FIND-VARIABLES") ( 52mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym 53"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 54"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair ( 55mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 56mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 57"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 58"NIL"))))) 59, 60 61(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" 62"CONSISTENT-EQUATION-RECORD-P") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair ( 63mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 64mksym "ACL2" "FORALL") (mkpair (mkpair (mksym "ACL2" "V") (mkpair (mksym 65"ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 66"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair ( 67mksym "ACL2" "UNIQUEP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 68"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 69"ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "VARS") ( 70mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 71mkpair (mksym "ACL2" "EQUATION") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 72mksym "ACL2" "V") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" 73"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 74"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 75mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 76mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 77"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 78mkpair (mksym "ACL2" "FIND-VARIABLES") (mkpair (mksym "ACL2" "EQUATION") ( 79mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym 80"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 81"NIL")))) (mksym "COMMON-LISP" "NIL"))))) 82, 83 84(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CONS-LIST-P") ( 85mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "EQUATIONS") ( 86mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 87mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") ( 88mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 89mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 90mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 91"CONSP") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 92"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) ( 93mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) (mksym 94"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "CONS-LIST-P") (mkpair ( 95mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym 96"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQUATIONS") (mksym 97"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 98mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 99"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 100, 101 102(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CIRCUITP") ( 103mkpair (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")) (mkpair ( 104mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 105"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 106mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") ( 107mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" 108"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 109"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 110"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) ( 111mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 112mkpair (mkpair (mksym "ACL2" "STRICT-EVALUATION-LIST-P") (mkpair (mkpair ( 113mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 114mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 115"ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 116mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 117"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") ( 118mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 119mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "UNIQUEP") (mkpair ( 120mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 121mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 122mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) ( 123mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 124"CONS-LIST-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 125"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 126"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) ( 127mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 128"QUOTE") (mkpair (mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) ( 129mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 130"NIL")))) (mkpair (mkpair (mksym "ACL2" "CONSISTENT-EQUATION-RECORD-P") ( 131mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 132"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) ( 133mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 134mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 135mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 136"ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 137mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 138"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 139mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 140mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 141mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 142"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 143"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 144"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 145"NIL"))))) 146, 147 148(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSIGN-T") ( 149mkpair (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "STATES") (mksym 150"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 151mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym 152"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 153mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 154mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym 155"ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 156"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 157"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 158"NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 159"ASSIGN-T") (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" 160"CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mksym 161"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 162"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 163, 164 165(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSIGN-NIL") ( 166mkpair (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "STATES") (mksym 167"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 168mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym 169"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 170mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 171mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym 172"ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 173"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 174"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 175"NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 176"ASSIGN-NIL") (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" 177"CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mksym 178"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 179"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 180, 181 182(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 183"CREATE-ALL-EVALUATIONS") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair ( 184mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 185"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 186mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 187"STATES") (mkpair (mkpair (mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair ( 188mkpair (mksym "ACL2" "REC-STATES") (mkpair (mksym "ACL2" "VARS") (mksym 189"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-APPEND") (mkpair ( 190mkpair (mksym "ACL2" "ASSIGN-T") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 191mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 192"ACL2" "REC-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 193"ACL2" "ASSIGN-NIL") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 194mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 195"REC-STATES") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 196mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 197"CREATE-ALL-EVALUATIONS") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 198mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 199"STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mksym 200"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 201"NIL"))))) 202, 203 204(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LABEL-FN-OF-ST") ( 205mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym 206"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 207mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym 208"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 209mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 210mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") ( 211mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 212mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 213"ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 214"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 215"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 216"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" 217"VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 218"LABEL-FN-OF-ST") (mkpair (mksym "ACL2" "ST") (mkpair (mkpair (mksym 219"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) ( 220mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 221mksym "ACL2" "LABEL-FN-OF-ST") (mkpair (mksym "ACL2" "ST") (mkpair (mkpair ( 222mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 223"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) ( 224mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 225, 226 227(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CREATE-LABEL-FN") ( 228mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mkpair ( 229mksym "ACL2" "LABEL") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 230"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 231mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 232"LABEL") (mkpair (mkpair (mksym "ACL2" "CREATE-LABEL-FN") (mkpair (mkpair ( 233mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym 234"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair (mkpair (mksym 235"ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" 236"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 237"LABEL-FN-OF-ST") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 238"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") ( 239mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "LABEL") (mksym 240"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 241"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 242, 243 244(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "APPLY-EQUATION") ( 245mkpair (mkpair (mksym "ACL2" "EQUATION") (mkpair (mksym "ACL2" "ST") (mksym 246"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 247mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "EQUATION") (mksym 248"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 249mkpair (mksym "ACL2" "BOOLEANP") (mkpair (mksym "ACL2" "EQUATION") (mksym 250"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQUATION") (mkpair (mkpair ( 251mksym "ACL2" "G") (mkpair (mksym "ACL2" "EQUATION") (mkpair (mksym "ACL2" 252"ST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 253mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 254"EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" 255"EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 256"COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" 257"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mkpair (mksym 258"COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" 259"CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mksym "ACL2" "ST") (mkpair (mksym 260"ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 261"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair ( 262mksym "ACL2" "CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mkpair (mksym 263"COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "~") (mksym "COMMON-LISP" "NIL"))) ( 264mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") ( 265mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym 266"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 267mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 268"NIL"))) (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mksym 269"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 270mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 271"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 272"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 273"NIL"))) (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "EQUATION") (mksym 274"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 275mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") ( 276mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 277mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym 278"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mkpair ( 279mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" 280"CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mksym "ACL2" "ST") (mkpair (mksym 281"ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 282"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair ( 283mksym "ACL2" "CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mkpair (mksym 284"COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "&") (mksym "COMMON-LISP" "NIL"))) ( 285mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 286mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym 287"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 288"NIL"))) (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 289mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym "COMMON-LISP" 290"CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym 291"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 292"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair ( 293mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 294"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 295"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 296"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair ( 297mksym "ACL2" "CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mkpair (mksym 298"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "+") (mksym "COMMON-LISP" 299"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 300"IF") (mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym 301"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 302"NIL"))) (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 303mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym "COMMON-LISP" 304"CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) ( 305mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 306mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 307mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym 308"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 309"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair ( 310mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) ( 311mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 312"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 313"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 314mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 315mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym 316"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" 317"EQUATION") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 318"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 319"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 320"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 321, 322 323(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 324"PRODUCE-NEXT-STATE") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym 325"ACL2" "ST") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) ( 326mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 327"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 328"NIL"))) (mkpair (mksym "ACL2" "ST") (mkpair (mkpair (mksym "ACL2" "S") ( 329mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") ( 330mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") ( 331mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 332mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 333"ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "ST") ( 334mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 335"PRODUCE-NEXT-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 336mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "ST") ( 337mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) (mksym 338"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 339"NIL"))))) 340, 341 342(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 343"CONSISTENT-P-EQUATIONS") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair ( 344mksym "ACL2" "EQN") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" 345"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 346"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 347"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 348"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 349"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair ( 350mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 351"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQN") ( 352mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 353mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym 354"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQUATIONS") (mksym 355"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 356"ACL2" "CONSISTENT-P-EQUATIONS") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 357mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 358"ACL2" "EQN") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) ( 359mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 360"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 361"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 362, 363 364(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" "NEXT-STATE-IS-OK") ( 365mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym 366"ACL2" "VARS") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) ( 367mkpair (mkpair (mksym "ACL2" "EXISTS") (mkpair (mkpair (mksym "ACL2" "EQN") ( 368mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 369mkpair (mkpair (mksym "ACL2" "CONSISTENT-P-EQUATIONS") (mkpair (mksym "ACL2" 370"VARS") (mkpair (mksym "ACL2" "EQN") (mkpair (mksym "ACL2" "EQUATIONS") ( 371mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") ( 372mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "PRODUCE-NEXT-STATE") ( 373mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" 374"EQN") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mksym "ACL2" "VARS") (mksym 375"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 376mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 377"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 378"NIL"))))) 379, 380 381(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 382"CREATE-NEXT-STATES-OF-P") (mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym 383"ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 384"EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 385"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 386mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 387"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 388"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 389mkpair (mksym "ACL2" "NEXT-STATE-IS-OK") (mkpair (mksym "ACL2" "P") (mkpair ( 390mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym 391"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 392"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym 393"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 394mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 395"ACL2" "CREATE-NEXT-STATES-OF-P") (mkpair (mksym "ACL2" "P") (mkpair (mkpair ( 396mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym 397"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 398"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) ( 399mkpair (mkpair (mksym "ACL2" "CREATE-NEXT-STATES-OF-P") (mkpair (mksym "ACL2" 400"P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" 401"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair ( 402mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mksym 403"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 404"NIL"))))) 405, 406 407(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 408"CREATE-NEXT-STATES") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 409"ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 410"EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 411"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 412mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 413"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 414"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair ( 415mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym 416"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 417"CREATE-NEXT-STATES-OF-P") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 418mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 419"ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 420"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "ACL2" 421"CREATE-NEXT-STATES") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 422mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 423"STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 424"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL"))))) ( 425mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 426, 427 428(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CREATE-KRIPKE") ( 429mkpair (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")) (mkpair ( 430mkpair (mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" 431"VARS") (mkpair (mksym "ACL2" "EQUATIONS") (mkpair (mksym "ACL2" 432"INITIAL-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mkpair ( 433mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair ( 434mksym "ACL2" "EQUATIONS") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 435"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mkpair ( 436mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "LABEL-FN") ( 437mkpair (mksym "ACL2" "EQUATIONS") (mkpair (mksym "ACL2" "VARS") (mkpair ( 438mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "INITIAL-STATES") (mksym 439"COMMON-LISP" "NIL")))))) (mkpair (mkpair (mkpair (mksym "COMMON-LISP" 440"LAMBDA") (mkpair (mkpair (mksym "ACL2" "TRANSITION") (mkpair (mksym "ACL2" 441"STATES") (mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" 442"LABEL-FN") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))))) ( 443mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" 444"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) ( 445mkpair (mksym "ACL2" "VARS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair ( 446mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") ( 447mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "TRANSITION") (mkpair ( 448mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 449mkpair (mksym "KEYWORD" "LABEL-FN") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 450mksym "ACL2" "LABEL-FN") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair ( 451mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") ( 452mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair ( 453mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 454mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 455mkpair (mksym "ACL2" "SET-UNION") (mkpair (mksym "ACL2" "INITIAL-STATES") ( 456mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 457mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 458"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 459"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) ( 460mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 461mksym "ACL2" "CREATE-NEXT-STATES") (mkpair (mkpair (mksym "ACL2" "SET-UNION") ( 462mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym 463"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "SET-UNION") (mkpair ( 464mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym 465"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 466"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mkpair (mksym "ACL2" "STATES") ( 467mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "LABEL-FN") ( 468mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mksym 469"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "CREATE-LABEL-FN") ( 470mkpair (mkpair (mksym "ACL2" "SET-UNION") (mkpair (mksym "ACL2" 471"INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) ( 472mkpair (mksym "ACL2" "VARS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 473mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 474"COMMON-LISP" "NIL"))))) (mkpair (mksym "ACL2" "EQUATIONS") (mkpair (mksym 475"ACL2" "VARS") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" 476"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP" 477"NIL")))) (mkpair (mkpair (mksym "ACL2" "CREATE-ALL-EVALUATIONS") (mkpair ( 478mksym "ACL2" "VARS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair ( 479mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 480mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 481mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 482"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" 483"EQUATIONS") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 484"INITIAL-STATES") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) ( 485mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 486"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) ( 487mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 488mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 489mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 490"ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 491mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 492"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") ( 493mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 494"COMMON-LISP" "NIL"))))) 495, 496 497(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 498"CREATE-KRIPKE-PRODUCES-CIRCUIT-MODEL") (mkpair (mkpair (mksym "ACL2" 499"IMPLIES") (mkpair (mkpair (mksym "ACL2" "CIRCUITP") (mkpair (mksym "ACL2" 500"C") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 501"CIRCUIT-MODELP") (mkpair (mkpair (mksym "ACL2" "CREATE-KRIPKE") (mkpair ( 502mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 503mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 504 505]; 506