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" "UPDATE-MACRO") ( 9mkpair (mkpair (mksym "ACL2" "UPDS") (mkpair (mksym "ACL2" "RESULT") (mksym 10"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 11mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "UPDS") (mksym 12"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "RESULT") (mkpair (mkpair (mksym 13"ACL2" "UPDATE-MACRO") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 14mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "UPDS") (mksym 15"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 16"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 17mksym "ACL2" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 18"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 19mksym "ACL2" "UPDS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 20"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 21mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "UPDS") (mksym 22"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 23"COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "RESULT") (mkpair (mkpair (mksym 24"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 25"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 26"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 27mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 28"COMMON-LISP" "NIL"))))) 29, 30 31(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "MEMBERP") ( 32mkpair (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym 33"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 34mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "X") (mksym 35"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 36mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (mkpair ( 37mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 38"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 39"COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym 40"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 41mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 42mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 43mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 44mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 45mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 46"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 47, 48 49(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 50mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" 51"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 52"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 53mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") ( 54mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 55mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP" 56"CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 57mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 58"ACL2" "SUBSET") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym 59"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym 60"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 61mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 62"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 63, 64 65(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SET-INTERSECT") ( 66mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym 67"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 68mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym 69"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 70mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 71mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 72mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 73"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) ( 74mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym 75"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 76mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mkpair (mksym 77"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 78mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 79"NIL")))) (mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mkpair ( 80mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 81"NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym 82"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 83"NIL"))))) 84, 85 86(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SET-UNION") ( 87mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym 88"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 89mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym 90"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mkpair (mkpair (mksym 91"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair ( 92mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 93"NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 94mkpair (mksym "ACL2" "SET-UNION") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 95mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 96"Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 97"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") ( 98mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "SET-UNION") ( 99mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 100"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) ( 101mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 102"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 103, 104 105(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SET-EQUAL") ( 106mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym 107"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 108mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (mkpair (mksym 109"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 110"SUBSET") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "X") (mksym 111"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 112mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 113"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 114, 115 116(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LTL-CONSTANTP") ( 117mkpair (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL")) (mkpair ( 118mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 119"EQUAL") (mkpair (mksym "ACL2" "F") (mkpair (mkpair (mksym "COMMON-LISP" 120"QUOTE") (mkpair (mksym "ACL2" "TRUE") (mksym "COMMON-LISP" "NIL"))) (mksym 121"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair ( 122mksym "ACL2" "F") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 123mksym "ACL2" "TRUE") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 124mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "F") ( 125mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "FALSE") ( 126mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 127"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 128, 129 130(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LTL-VARIABLEP") ( 131mkpair (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL")) (mkpair ( 132mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 133"SYMBOLP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 134mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 135mkpair (mksym "ACL2" "F") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 136mkpair (mkpair (mksym "COMMON-LISP" "+") (mkpair (mksym "ACL2" "&") (mkpair ( 137mksym "ACL2" "U") (mkpair (mksym "ACL2" "W") (mkpair (mksym "ACL2" "X") ( 138mkpair (mksym "ACL2" "F") (mkpair (mksym "ACL2" "G") (mksym "COMMON-LISP" 139"NIL")))))))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 140mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 141mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 142"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 143, 144 145(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LTL-FORMULAP") ( 146mkpair (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL")) (mkpair ( 147mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") ( 148mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 149mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "LTL-CONSTANTP") ( 150mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 151mksym "ACL2" "LTL-CONSTANTP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" 152"NIL"))) (mkpair (mkpair (mksym "ACL2" "LTL-VARIABLEP") (mkpair (mksym "ACL2" 153"F") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 154mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 155"EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" "F") ( 156mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 157mkpair (mknum "3" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym 158"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 159mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 160mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym 161"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 162"COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym "COMMON-LISP" "+") (mkpair ( 163mksym "ACL2" "&") (mkpair (mksym "ACL2" "U") (mkpair (mksym "ACL2" "W") ( 164mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))) (mksym 165"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 166mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP" 167"CAR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mksym 168"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair ( 169mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 170mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym 171"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 172"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 173"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 174mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 175mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 176"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 177mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") ( 178mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 179mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym 180"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 181"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair ( 182mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" 183"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym 184"ACL2" "~") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "F") (mkpair ( 185mksym "ACL2" "G") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))) ( 186mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") ( 187mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym 188"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) ( 189mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 190mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 191"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 192"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 193"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 194"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 195, 196 197(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 198"RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "ACL2" "F") (mkpair (mksym 199"ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 200"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (mkpair ( 201mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 202"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "LTL-CONSTANTP") (mkpair ( 203mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 204"LTL-CONSTANTP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) ( 205mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 206"LTL-VARIABLEP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) ( 207mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "F") (mkpair ( 208mksym "ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 209"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 210"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 211"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 212"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym 213"ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 214"COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym "COMMON-LISP" 215"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 216"IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym 217"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 218mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 219mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym "ACL2" 220"&") (mkpair (mksym "COMMON-LISP" "+") (mkpair (mksym "ACL2" "U") (mkpair ( 221mksym "ACL2" "W") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))) ( 222mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 223mkpair (mkpair (mksym "ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym 224"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) ( 225mkpair (mksym "ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 226mksym "ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP" 227"CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym 228"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) ( 229mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 230"ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 231"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 232"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 233"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 234"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 235"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair ( 236mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" 237"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" 238"0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair ( 239mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 240mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "F") (mksym 241"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 242mkpair (mksym "ACL2" "~") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" 243"F") (mkpair (mksym "ACL2" "G") (mksym "COMMON-LISP" "NIL"))))) (mksym 244"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 245"ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 246mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym 247"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 248"V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 249"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 250mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 251mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 252"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 253"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 254, 255 256(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "NEXT-STATEP") ( 257mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym 258"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 259"MEMBERP") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "G") ( 260mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 261mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym 262"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 263mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 264"COMMON-LISP" "NIL"))))) 265, 266 267(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "INITIAL-STATEP") ( 268mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (mksym 269"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 270mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 271"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym 272"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 273mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 274, 275 276(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LABEL-OF") ( 277mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "M") (mksym 278"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym 279"ACL2" "S") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 280"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "LABEL-FN") (mksym 281"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 282mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 283, 284 285(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 286"NEXT-STATES-IN-STATES") (mkpair (mkpair (mksym "ACL2" "M") (mkpair (mksym 287"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 288"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 289mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 290"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 291"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 292"ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 293"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 294"NIL"))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 295"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym 296"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 297mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 298mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 299mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 300"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 301"NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym 302"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 303"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 304"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 305mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym 306"COMMON-LISP" "NIL"))))) 307, 308 309(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "EVALUATION-EQ") ( 310mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym 311"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 312"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 313mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 314"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 315"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 316"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 317mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 318"NIL"))) (mkpair (mksym "ACL2" "P") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 319mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 320mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Q") ( 321mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 322mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (mksym 323"ACL2" "Q") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" 324"VARS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 325mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 326mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 327"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 328, 329 330(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 331"EVALUATION-EQ-MEMBER-P") (mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym 332"ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 333mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 334"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 335"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 336"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 337"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair ( 338mksym "ACL2" "ST") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 339"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") ( 340mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 341mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 342mkpair (mksym "ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "ST") ( 343mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") ( 344mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym 345"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 346"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 347, 348 349(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 350"EVALUATION-EQ-MEMBER") (mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym 351"ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 352mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 353"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 354"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 355"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 356"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair ( 357mksym "ACL2" "ST") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 358"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") ( 359mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 360mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 361mksym "ACL2" "EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "ST") (mkpair ( 362mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym 363"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 364"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) ( 365mksym "COMMON-LISP" "NIL"))))) 366, 367 368(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" "STRICT-EVALUATION-P") ( 369mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym 370"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "FORALL") (mkpair ( 371mkpair (mksym "ACL2" "V") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 372"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair ( 373mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" 374"VARS") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair ( 375mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 376mksym "ACL2" "V") (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) ( 377mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 378"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 379, 380 381(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 382"STRICT-EVALUATION-LIST-P") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair ( 383mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 384"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 385mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 386"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 387"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 388"ACL2" "STRICT-EVALUATION-P") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 389mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 390"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 391"STRICT-EVALUATION-LIST-P") (mkpair (mksym "ACL2" "VARS") (mkpair (mkpair ( 392mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym 393"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 394"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 395"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 396"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 397, 398 399(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "EVALUATION-P") ( 400mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym 401"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 402mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym 403"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 404mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 405"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "BOOLEANP") (mkpair (mkpair ( 406mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 407"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "ST") ( 408mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 409mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" "ST") (mkpair (mkpair ( 410mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 411"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 412"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 413mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym 414"COMMON-LISP" "NIL"))))) 415, 416 417(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 418"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 419"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 420"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 421mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 422"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 423"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 424"ACL2" "EVALUATION-P") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 425mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 426"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 427"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 428mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 429"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 430"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 431mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym 432"COMMON-LISP" "NIL"))))) 433, 434 435(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" "ALL-EVALUATIONS-P") ( 436mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym 437"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "FORALL") (mkpair ( 438mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair ( 439mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (mkpair ( 440mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 441mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" 442"ST") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym 443"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 444"NIL")))) (mksym "COMMON-LISP" "NIL"))))) 445, 446 447(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 448"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "M-STATES") (mkpair ( 449mksym "ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 450"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 451"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "M-STATES") (mksym "COMMON-LISP" 452"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 453"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 454"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ-MEMBER-P") ( 455mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "M-STATES") ( 456mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N-STATES") (mkpair (mksym 457"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 458"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 459mksym "ACL2" "M-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 460"N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 461mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 462"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 463"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 464, 465 466(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 467"EVALUATION-EQ-SUBSET-TO-MEMBER") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 468mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 469"EVALUATION-EQ-SUBSET-P") (mkpair (mksym "ACL2" "M-STATES") (mkpair (mksym 470"ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 471mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair ( 472mksym "ACL2" "M-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 473mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 474"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 475"ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "P") (mkpair (mksym 476"ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 477mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 478, 479 480(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "TRUTHP-LABEL") ( 481mkpair (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "S") (mksym 482"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 483mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "LABEL") (mksym 484"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 485mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 486"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair ( 487mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 488mksym "ACL2" "LABEL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "S") ( 489mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 490mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mksym 491"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair ( 492mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "LABEL") (mksym 493"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "S") (mksym "COMMON-LISP" "NIL")))) ( 494mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 495"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 496"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 497, 498 499(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ONLY-TRUTH-P") ( 500mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "M") (mksym 501"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 502mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym 503"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 504mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 505"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair ( 506mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 507mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 508"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 509"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 510"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 511"ONLY-TRUTH-P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym 512"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 513mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 514mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 515"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 516"NIL"))))) 517, 518 519(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 520"ALL-TRUTHSP-LABEL") (mkpair (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym 521"ACL2" "S") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 522mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 523"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 524"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 525"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 526"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair ( 527mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 528mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym 529"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "S") (mksym "COMMON-LISP" "NIL")))) ( 530mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") ( 531mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 532mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 533mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 534"LABEL") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 535mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" 536"LABEL") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" 537"CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mksym 538"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 539mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 540"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 541"NIL"))))) 542, 543 544(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 545"ONLY-ALL-TRUTHS-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 546"ACL2" "M") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 547mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 548"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 549"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 550"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 551"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") ( 552mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" 553"CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 554mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 555"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 556"NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 557mkpair (mkpair (mksym "ACL2" "ONLY-ALL-TRUTHS-P") (mkpair (mkpair (mksym 558"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 559"NIL"))) (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "VARS") (mksym 560"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 561mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 562"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 563"NIL"))))) 564, 565 566(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 567"LABEL-SUBSET-VARS") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 568"ACL2" "M") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 569mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 570"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 571"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 572"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 573"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mkpair ( 574mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 575mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 576"M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mksym 577"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "LABEL-SUBSET-VARS") ( 578mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") ( 579mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" 580"VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" 581"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 582mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym 583"COMMON-LISP" "NIL"))))) 584, 585 586(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" 587"WELL-FORMED-TRANSITION-P") (mkpair (mkpair (mksym "ACL2" "STATES-M") (mkpair ( 588mksym "ACL2" "TRANS-M") (mkpair (mksym "ACL2" "STATES-N") (mkpair (mksym 589"ACL2" "TRANS-N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))))) ( 590mkpair (mkpair (mksym "ACL2" "FORALL") (mkpair (mkpair (mksym "ACL2" "P") ( 591mkpair (mksym "ACL2" "Q") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 592mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 593mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair ( 594mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 595mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 596"EVALUATION-P") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "VARS") ( 597mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 598mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair ( 599mksym "ACL2" "STATES-M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 600mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 601mksym "ACL2" "Q") (mkpair (mksym "ACL2" "STATES-N") (mksym "COMMON-LISP" 602"NIL")))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" 603"Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 604mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 605mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 606mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 607"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 608"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 609"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 610"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 611"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 612"ACL2" "EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 613mksym "ACL2" "P") (mkpair (mksym "ACL2" "TRANS-M") (mksym "COMMON-LISP" "NIL")))) ( 614mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "Q") (mkpair (mksym 615"ACL2" "TRANS-N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") ( 616mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym 617"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 618, 619 620(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 621"TRANSITION-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 622"ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "TRANS") (mksym "COMMON-LISP" 623"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 624"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 625"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 626"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 627"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mkpair ( 628mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 629"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "TRANS") ( 630mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "STATES-PRIME") (mksym 631"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "TRANSITION-SUBSET-P") ( 632mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") ( 633mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "STATES-PRIME") (mkpair ( 634mksym "ACL2" "TRANS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 635"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 636"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 637"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 638, 639 640(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CIRCUIT-MODELP") ( 641mkpair (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")) (mkpair ( 642mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 643"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 644mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 645"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 646mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 647"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) ( 648mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 649"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 650"ACL2" "ALL-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 651mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 652mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 653"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 654"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 655"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 656mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 657mkpair (mkpair (mksym "ACL2" "STRICT-EVALUATION-LIST-P") (mkpair (mkpair ( 658mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 659mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 660"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 661mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 662"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym 663"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 664"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ONLY-ALL-TRUTHS-P") ( 665mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 666"QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) ( 667mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym 668"ACL2" "M") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 669"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 670"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 671mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 672mkpair (mkpair (mksym "ACL2" "ONLY-TRUTH-P") (mkpair (mkpair (mksym "ACL2" 673"G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 674"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym 675"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 676mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 677"LABEL-SUBSET-VARS") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 678mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 679"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 680mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 681mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 682"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 683mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 684mkpair (mkpair (mksym "ACL2" "TRANSITION-SUBSET-P") (mkpair (mkpair (mksym 685"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 686"KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 687mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 688mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 689mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 690"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 691"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym 692"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 693mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 694mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "G") ( 695mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 696"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 697mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 698mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 699mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 700"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 701"IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mkpair (mksym 702"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 703"KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 704mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 705mksym "ACL2" "NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair ( 706mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 707mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 708mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 709mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 710"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 711mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 712mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 713mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 714"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 715"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 716"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 717"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 718"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 719"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 720"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 721"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 722"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 723"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 724"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 725"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 726"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 727"NIL"))))) 728, 729 730(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "C-BISIM-EQUIV") ( 731mkpair (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym 732"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 733"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair ( 734mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 735"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair ( 736mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 737"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym 738"ACL2" "VARS") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 739"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 740"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 741mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 742mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair ( 743mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 744mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 745mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 746mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 747"WELL-FORMED-TRANSITION-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 748mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 749mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 750"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 751"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym 752"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 753mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 754"QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) ( 755mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 756mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 757mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 758"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") ( 759mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 760mkpair (mkpair (mksym "ACL2" "WELL-FORMED-TRANSITION-P") (mkpair (mkpair ( 761mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 762mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 763"N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 764mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 765"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym 766"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 767mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 768"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 769mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 770"QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) ( 771mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym 772"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 773"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ-SUBSET-P") ( 774mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 775"QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" 776"NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 777mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 778mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) ( 779mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym 780"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 781"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 782mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") ( 783mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" 784"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 785"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym 786"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 787mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 788mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 789"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 790"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 791"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 792"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 793"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 794"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 795"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 796"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 797"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 798"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 799"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 800"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 801"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 802"NIL"))))) 803, 804 805(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CIRCUIT-BISIM") ( 806mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (mkpair (mksym 807"ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 808"COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 809mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair (mksym "ACL2" "M") (mksym 810"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 811mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair (mksym "ACL2" "N") (mksym 812"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 813mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mkpair ( 814mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 815mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 816"M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair ( 817mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 818mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 819mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 820"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) ( 821mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 822mkpair (mkpair (mksym "ACL2" "WELL-FORMED-TRANSITION-P") (mkpair (mkpair ( 823mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 824mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 825"M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 826mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 827"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym 828"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 829mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 830"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) ( 831mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 832"QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) ( 833mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym 834"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 835"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "WELL-FORMED-TRANSITION-P") ( 836mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 837"QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) ( 838mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 839mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 840mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 841"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 842mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 843"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym 844"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 845mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym 846"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 847mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair ( 848mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 849"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 850mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") ( 851mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 852"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 853"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym 854"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) ( 855mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 856mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 857"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 858mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") ( 859mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" 860"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 861"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym 862"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 863mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 864mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 865mksym "ACL2" "VARS") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 866mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 867"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 868mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 869mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair ( 870mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 871mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 872mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 873mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") ( 874mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 875"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 876"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 877mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 878"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 879mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 880mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 881mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 882"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 883"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 884"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 885"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 886"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 887"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 888"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 889"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 890"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 891"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 892"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 893"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 894"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 895"NIL"))))) 896, 897 898(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "FIND-VARIABLES") ( 899mkpair (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL")) (mkpair ( 900mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 901mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "EQUATION") ( 902mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") ( 903mkpair (mkpair (mksym "ACL2" "BOOLEANP") (mkpair (mksym "ACL2" "EQUATION") ( 904mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 905mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 906"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 907"COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "EQUATION") (mkpair (mkpair ( 908mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 909"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 910"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 911mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") ( 912mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 913mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym 914"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 915"ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair ( 916mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym 917"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 918"COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym "ACL2" "&") (mkpair (mksym 919"COMMON-LISP" "+") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 920mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 921mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 922"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "SET-UNION") (mkpair ( 923mkpair (mksym "ACL2" "FIND-VARIABLES") (mkpair (mkpair (mksym "COMMON-LISP" 924"CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym 925"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "FIND-VARIABLES") ( 926mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym 927"COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 928mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 929"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym 930"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 931mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 932"EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" 933"EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 934"COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" 935"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 936"EQUAL") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" 937"EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 938"COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "~") (mksym "COMMON-LISP" "NIL"))) ( 939mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 940mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 941"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "FIND-VARIABLES") ( 942mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym 943"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 944"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair ( 945mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 946mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 947"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 948"NIL"))))) 949, 950 951(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" 952"CONSISTENT-EQUATION-RECORD-P") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair ( 953mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 954mksym "ACL2" "FORALL") (mkpair (mkpair (mksym "ACL2" "V") (mkpair (mksym 955"ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 956"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair ( 957mksym "ACL2" "UNIQUEP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 958"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 959"ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "VARS") ( 960mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 961mkpair (mksym "ACL2" "EQUATION") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 962mksym "ACL2" "V") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" 963"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 964"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 965mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 966mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 967"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 968mkpair (mksym "ACL2" "FIND-VARIABLES") (mkpair (mksym "ACL2" "EQUATION") ( 969mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym 970"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 971"NIL")))) (mksym "COMMON-LISP" "NIL"))))) 972, 973 974(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CONS-LIST-P") ( 975mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "EQUATIONS") ( 976mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 977mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") ( 978mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 979mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 980mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 981"CONSP") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 982"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) ( 983mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) (mksym 984"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "CONS-LIST-P") (mkpair ( 985mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym 986"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQUATIONS") (mksym 987"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 988mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 989"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 990, 991 992(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CIRCUITP") ( 993mkpair (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")) (mkpair ( 994mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 995"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 996mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") ( 997mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" 998"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 999"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 1000"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) ( 1001mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 1002mkpair (mkpair (mksym "ACL2" "STRICT-EVALUATION-LIST-P") (mkpair (mkpair ( 1003mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 1004mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1005"ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 1006mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 1007"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") ( 1008mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 1009mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "UNIQUEP") (mkpair ( 1010mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1011mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 1012mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) ( 1013mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 1014"CONS-LIST-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 1015"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 1016"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) ( 1017mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 1018"QUOTE") (mkpair (mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) ( 1019mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1020"NIL")))) (mkpair (mkpair (mksym "ACL2" "CONSISTENT-EQUATION-RECORD-P") ( 1021mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 1022"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) ( 1023mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 1024mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 1025mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1026"ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 1027mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 1028"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 1029mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 1030mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 1031mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1032"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1033"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1034"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 1035"NIL"))))) 1036, 1037 1038(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSIGN-T") ( 1039mkpair (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "STATES") (mksym 1040"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1041mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym 1042"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 1043mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 1044mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym 1045"ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1046"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1047"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 1048"NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 1049"ASSIGN-T") (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" 1050"CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mksym 1051"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1052"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1053, 1054 1055(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSIGN-NIL") ( 1056mkpair (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "STATES") (mksym 1057"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1058mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym 1059"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 1060mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 1061mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym 1062"ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1063"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1064"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 1065"NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 1066"ASSIGN-NIL") (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" 1067"CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mksym 1068"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1069"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1070, 1071 1072(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1073"CREATE-ALL-EVALUATIONS") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair ( 1074mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1075"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 1076mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 1077"STATES") (mkpair (mkpair (mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair ( 1078mkpair (mksym "ACL2" "REC-STATES") (mkpair (mksym "ACL2" "VARS") (mksym 1079"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-APPEND") (mkpair ( 1080mkpair (mksym "ACL2" "ASSIGN-T") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 1081mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1082"ACL2" "REC-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1083"ACL2" "ASSIGN-NIL") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 1084mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 1085"REC-STATES") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 1086mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 1087"CREATE-ALL-EVALUATIONS") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 1088mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 1089"STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mksym 1090"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 1091"NIL"))))) 1092, 1093 1094(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LABEL-FN-OF-ST") ( 1095mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym 1096"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1097mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym 1098"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 1099mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 1100mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") ( 1101mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 1102mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1103"ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1104"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 1105"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 1106"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" 1107"VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 1108"LABEL-FN-OF-ST") (mkpair (mksym "ACL2" "ST") (mkpair (mkpair (mksym 1109"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) ( 1110mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 1111mksym "ACL2" "LABEL-FN-OF-ST") (mkpair (mksym "ACL2" "ST") (mkpair (mkpair ( 1112mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 1113"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) ( 1114mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1115, 1116 1117(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CREATE-LABEL-FN") ( 1118mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mkpair ( 1119mksym "ACL2" "LABEL") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1120"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 1121mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 1122"LABEL") (mkpair (mkpair (mksym "ACL2" "CREATE-LABEL-FN") (mkpair (mkpair ( 1123mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym 1124"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair (mkpair (mksym 1125"ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" 1126"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 1127"LABEL-FN-OF-ST") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 1128"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") ( 1129mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "LABEL") (mksym 1130"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 1131"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1132, 1133 1134(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "APPLY-EQUATION") ( 1135mkpair (mkpair (mksym "ACL2" "EQUATION") (mkpair (mksym "ACL2" "ST") (mksym 1136"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1137mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "EQUATION") (mksym 1138"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1139mkpair (mksym "ACL2" "BOOLEANP") (mkpair (mksym "ACL2" "EQUATION") (mksym 1140"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQUATION") (mkpair (mkpair ( 1141mksym "ACL2" "G") (mkpair (mksym "ACL2" "EQUATION") (mkpair (mksym "ACL2" 1142"ST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 1143mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 1144"EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" 1145"EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1146"COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" 1147"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mkpair (mksym 1148"COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" 1149"CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mksym "ACL2" "ST") (mkpair (mksym 1150"ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1151"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair ( 1152mksym "ACL2" "CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mkpair (mksym 1153"COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "~") (mksym "COMMON-LISP" "NIL"))) ( 1154mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") ( 1155mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym 1156"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 1157mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 1158"NIL"))) (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mksym 1159"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 1160mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 1161"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1162"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 1163"NIL"))) (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "EQUATION") (mksym 1164"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1165mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") ( 1166mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 1167mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym 1168"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mkpair ( 1169mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" 1170"CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mksym "ACL2" "ST") (mkpair (mksym 1171"ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1172"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair ( 1173mksym "ACL2" "CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mkpair (mksym 1174"COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "&") (mksym "COMMON-LISP" "NIL"))) ( 1175mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 1176mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym 1177"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 1178"NIL"))) (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 1179mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym "COMMON-LISP" 1180"CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym 1181"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 1182"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair ( 1183mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1184"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1185"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1186"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQL") (mkpair ( 1187mksym "ACL2" "CASE-DO-NOT-USE-ELSEWHERE") (mkpair (mkpair (mksym 1188"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "+") (mksym "COMMON-LISP" 1189"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 1190"IF") (mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym 1191"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 1192"NIL"))) (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 1193mkpair (mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym "COMMON-LISP" 1194"CAR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) ( 1195mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 1196mksym "ACL2" "APPLY-EQUATION") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 1197mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym 1198"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" 1199"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair ( 1200mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) ( 1201mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 1202"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 1203"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 1204mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 1205mkpair (mksym "ACL2" "EQUATION") (mksym "COMMON-LISP" "NIL"))) (mksym 1206"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" 1207"EQUATION") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1208"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1209"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 1210"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1211, 1212 1213(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1214"PRODUCE-NEXT-STATE") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym 1215"ACL2" "ST") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) ( 1216mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1217"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 1218"NIL"))) (mkpair (mksym "ACL2" "ST") (mkpair (mkpair (mksym "ACL2" "S") ( 1219mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") ( 1220mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "APPLY-EQUATION") ( 1221mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 1222mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1223"ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "ST") ( 1224mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 1225"PRODUCE-NEXT-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 1226mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "ST") ( 1227mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) (mksym 1228"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 1229"NIL"))))) 1230, 1231 1232(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1233"CONSISTENT-P-EQUATIONS") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair ( 1234mksym "ACL2" "EQN") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" 1235"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1236"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 1237"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1238"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1239"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair ( 1240mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 1241"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQN") ( 1242mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 1243mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym 1244"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQUATIONS") (mksym 1245"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1246"ACL2" "CONSISTENT-P-EQUATIONS") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 1247mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1248"ACL2" "EQN") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) ( 1249mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 1250"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 1251"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1252, 1253 1254(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" "NEXT-STATE-IS-OK") ( 1255mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym 1256"ACL2" "VARS") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) ( 1257mkpair (mkpair (mksym "ACL2" "EXISTS") (mkpair (mkpair (mksym "ACL2" "EQN") ( 1258mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 1259mkpair (mkpair (mksym "ACL2" "CONSISTENT-P-EQUATIONS") (mkpair (mksym "ACL2" 1260"VARS") (mkpair (mksym "ACL2" "EQN") (mkpair (mksym "ACL2" "EQUATIONS") ( 1261mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") ( 1262mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "PRODUCE-NEXT-STATE") ( 1263mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" 1264"EQN") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mksym "ACL2" "VARS") (mksym 1265"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1266mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 1267"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1268"NIL"))))) 1269, 1270 1271(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1272"CREATE-NEXT-STATES-OF-P") (mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym 1273"ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 1274"EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1275"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 1276mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1277"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1278"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1279mkpair (mksym "ACL2" "NEXT-STATE-IS-OK") (mkpair (mksym "ACL2" "P") (mkpair ( 1280mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym 1281"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 1282"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym 1283"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 1284mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1285"ACL2" "CREATE-NEXT-STATES-OF-P") (mkpair (mksym "ACL2" "P") (mkpair (mkpair ( 1286mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym 1287"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 1288"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) ( 1289mkpair (mkpair (mksym "ACL2" "CREATE-NEXT-STATES-OF-P") (mkpair (mksym "ACL2" 1290"P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" 1291"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair ( 1292mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mksym 1293"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 1294"NIL"))))) 1295, 1296 1297(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1298"CREATE-NEXT-STATES") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 1299"ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 1300"EQUATIONS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1301"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 1302mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1303"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1304"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair ( 1305mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym 1306"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 1307"CREATE-NEXT-STATES-OF-P") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 1308mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1309"ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 1310"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "ACL2" 1311"CREATE-NEXT-STATES") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 1312mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 1313"STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 1314"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL"))))) ( 1315mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1316, 1317 1318(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CREATE-KRIPKE") ( 1319mkpair (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")) (mkpair ( 1320mkpair (mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" 1321"VARS") (mkpair (mksym "ACL2" "EQUATIONS") (mkpair (mksym "ACL2" 1322"INITIAL-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mkpair ( 1323mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair ( 1324mksym "ACL2" "EQUATIONS") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 1325"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mkpair ( 1326mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "LABEL-FN") ( 1327mkpair (mksym "ACL2" "EQUATIONS") (mkpair (mksym "ACL2" "VARS") (mkpair ( 1328mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "INITIAL-STATES") (mksym 1329"COMMON-LISP" "NIL")))))) (mkpair (mkpair (mkpair (mksym "COMMON-LISP" 1330"LAMBDA") (mkpair (mkpair (mksym "ACL2" "TRANSITION") (mkpair (mksym "ACL2" 1331"STATES") (mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" 1332"LABEL-FN") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))))) ( 1333mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" 1334"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) ( 1335mkpair (mksym "ACL2" "VARS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair ( 1336mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") ( 1337mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "TRANSITION") (mkpair ( 1338mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1339mkpair (mksym "KEYWORD" "LABEL-FN") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 1340mksym "ACL2" "LABEL-FN") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair ( 1341mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") ( 1342mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair ( 1343mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1344mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 1345mkpair (mksym "ACL2" "SET-UNION") (mkpair (mksym "ACL2" "INITIAL-STATES") ( 1346mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 1347mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1348"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 1349"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) ( 1350mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 1351mksym "ACL2" "CREATE-NEXT-STATES") (mkpair (mkpair (mksym "ACL2" "SET-UNION") ( 1352mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym 1353"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "SET-UNION") (mkpair ( 1354mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym 1355"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 1356"EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mkpair (mksym "ACL2" "STATES") ( 1357mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "LABEL-FN") ( 1358mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mksym 1359"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "CREATE-LABEL-FN") ( 1360mkpair (mkpair (mksym "ACL2" "SET-UNION") (mkpair (mksym "ACL2" 1361"INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) ( 1362mkpair (mksym "ACL2" "VARS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1363mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 1364"COMMON-LISP" "NIL"))))) (mkpair (mksym "ACL2" "EQUATIONS") (mkpair (mksym 1365"ACL2" "VARS") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" 1366"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP" 1367"NIL")))) (mkpair (mkpair (mksym "ACL2" "CREATE-ALL-EVALUATIONS") (mkpair ( 1368mksym "ACL2" "VARS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair ( 1369mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 1370mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1371mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 1372"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" 1373"EQUATIONS") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" 1374"INITIAL-STATES") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) ( 1375mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 1376"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) ( 1377mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 1378mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 1379mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1380"ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 1381mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 1382"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") ( 1383mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 1384"COMMON-LISP" "NIL"))))) 1385, 1386 1387(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "FIND-VARIABLES*") ( 1388mkpair (mkpair (mksym "ACL2" "EQUATION-LIST") (mksym "COMMON-LISP" "NIL")) ( 1389mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1390"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "EQUATION-LIST") (mksym 1391"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 1392mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 1393mksym "ACL2" "SET-UNION") (mkpair (mkpair (mksym "ACL2" "FIND-VARIABLES") ( 1394mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" 1395"EQUATION-LIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 1396mkpair (mkpair (mksym "ACL2" "FIND-VARIABLES*") (mkpair (mkpair (mksym 1397"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "EQUATION-LIST") (mksym 1398"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 1399"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1400, 1401 1402(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1403"FIND-ALL-VARIABLES-1-PASS") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair ( 1404mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 1405mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") ( 1406mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 1407mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1408"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "SET-UNION") (mkpair ( 1409mkpair (mksym "ACL2" "FIND-VARIABLES*") (mkpair (mkpair (mksym "ACL2" "G") ( 1410mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") ( 1411mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "EQUATIONS") (mksym 1412"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1413"ACL2" "FIND-ALL-VARIABLES-1-PASS") (mkpair (mkpair (mksym "COMMON-LISP" 1414"CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 1415mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1416"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1417, 1418 1419(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1420"FIND-ALL-VARIABLES") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym 1421"ACL2" "VARIABLES") (mkpair (mksym "ACL2" "EQUATIONS") (mksym "COMMON-LISP" 1422"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1423"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair ( 1424mkpair (mksym "ACL2" "UNIQUEP") (mkpair (mksym "ACL2" "VARIABLES") (mksym 1425"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1426"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "UNIQUEP") (mkpair (mksym 1427"ACL2" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 1428mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1429"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "UNIQUEP") (mkpair (mksym 1430"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 1431mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" 1432"UNIQUEP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mksym 1433"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair ( 1434mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym 1435"ACL2" "VARIABLES") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) ( 1436mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mksym 1437"ACL2" "VARS") (mkpair (mkpair (mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair ( 1438mkpair (mksym "ACL2" "NEW-VARS") (mkpair (mksym "ACL2" "EQUATIONS") (mkpair ( 1439mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" 1440"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1441"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym 1442"ACL2" "NEW-VARS") (mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" 1443"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 1444"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 1445mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 1446"SET-EQUAL") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "NEW-VARS") ( 1447mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mkpair (mkpair ( 1448mksym "ACL2" "FIND-ALL-VARIABLES") (mkpair (mksym "ACL2" "NEW-VARS") (mkpair ( 1449mksym "ACL2" "VARIABLES") (mkpair (mksym "ACL2" "EQUATIONS") (mksym 1450"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 1451"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 1452"SET-UNION") (mkpair (mkpair (mksym "ACL2" "FIND-ALL-VARIABLES-1-PASS") ( 1453mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "EQUATIONS") (mksym 1454"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 1455"NIL")))) (mkpair (mksym "ACL2" "EQUATIONS") (mkpair (mksym "ACL2" "VARS") ( 1456mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" "NIL")))))) (mksym 1457"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1458, 1459 1460(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1461"FIND-ALL-EQUATIONS") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym 1462"ACL2" "EQUATIONS") (mkpair (mksym "ACL2" "EQ-REC") (mksym "COMMON-LISP" 1463"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1464"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 1465"NIL"))) (mkpair (mksym "ACL2" "EQ-REC") (mkpair (mkpair (mksym "ACL2" 1466"FIND-ALL-EQUATIONS") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 1467mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 1468"EQUATIONS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym 1469"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) ( 1470mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 1471mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1472"ACL2" "EQUATIONS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" 1473"EQ-REC") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) ( 1474mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1475, 1476 1477(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1478"REMOVE-DUPLICATE-OCCURRENCES") (mkpair (mkpair (mksym "ACL2" "X") (mksym 1479"COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1480mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym 1481"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym 1482"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair ( 1483mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 1484"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" 1485"X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair ( 1486mkpair (mksym "ACL2" "REMOVE-DUPLICATE-OCCURRENCES") (mkpair (mkpair (mksym 1487"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 1488mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") ( 1489mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 1490"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 1491"REMOVE-DUPLICATE-OCCURRENCES") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 1492mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 1493"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) ( 1494mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1495, 1496 1497(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1498"CORRESPONDING-STATE") (mkpair (mkpair (mksym "ACL2" "INIT") (mkpair (mksym 1499"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1500"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 1501mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1502"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1503"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair ( 1504mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 1505"NIL"))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 1506"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) ( 1507mkpair (mksym "ACL2" "INIT") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 1508mksym "ACL2" "CORRESPONDING-STATE") (mkpair (mksym "ACL2" "INIT") (mkpair ( 1509mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym 1510"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1511"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1512, 1513 1514(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1515"CORRESPONDING-STATES") (mkpair (mkpair (mksym "ACL2" "INITS") (mkpair (mksym 1516"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1517"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 1518mksym "ACL2" "INITS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 1519"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1520"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair ( 1521mkpair (mksym "ACL2" "CORRESPONDING-STATE") (mkpair (mkpair (mksym 1522"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "INITS") (mksym "COMMON-LISP" 1523"NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 1524mkpair (mksym "ACL2" "CORRESPONDING-STATES") (mkpair (mkpair (mksym 1525"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "INITS") (mksym "COMMON-LISP" 1526"NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym 1527"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 1528"NIL"))))) 1529, 1530 1531(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CONE-VARIABLES") ( 1532mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "C") (mksym 1533"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "FIND-ALL-VARIABLES") ( 1534mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" 1535"REMOVE-DUPLICATE-OCCURRENCES") (mkpair (mksym "ACL2" "VARS") (mksym 1536"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 1537mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 1538"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) ( 1539mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 1540mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") ( 1541mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" 1542"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 1543"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "EQUATIONS") (mksym 1544"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) ( 1545mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1546, 1547 1548(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1549"CONE-OF-INFLUENCE-REDUCTION") (mkpair (mkpair (mksym "ACL2" "C") (mkpair ( 1550mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mkpair ( 1551mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "VARIABLES") ( 1552mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 1553mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 1554mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 1555mksym "ACL2" "FIND-ALL-EQUATIONS") (mkpair (mksym "ACL2" "VARIABLES") (mkpair ( 1556mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1557mkpair (mksym "KEYWORD" "EQUATIONS") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 1558mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1559"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1560"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1561"ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1562"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 1563mksym "ACL2" "CORRESPONDING-STATES") (mkpair (mkpair (mksym "ACL2" "G") ( 1564mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 1565"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") ( 1566mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARIABLES") (mksym 1567"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mkpair ( 1568mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 1569"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARIABLES") (mkpair (mkpair ( 1570mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1571"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 1572"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) ( 1573mkpair (mkpair (mksym "ACL2" "CONE-VARIABLES") (mkpair (mksym "ACL2" "VARS") ( 1574mkpair (mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym 1575"ACL2" "C") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 1576, 1577 1578(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1579"CONE-OF-INFLUENCE-REDUCTION-IS-CIRCUIT-P") (mkpair (mkpair (mksym "ACL2" 1580"IMPLIES") (mkpair (mkpair (mksym "ACL2" "CIRCUITP") (mkpair (mksym "ACL2" 1581"C") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "CIRCUITP") ( 1582mkpair (mkpair (mksym "ACL2" "CONE-OF-INFLUENCE-REDUCTION") (mkpair (mksym 1583"ACL2" "C") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 1584mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 1585"COMMON-LISP" "NIL")))) 1586, 1587 1588(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1589"CONE-OF-INFLUENCE-IS-C-BISIMI-EQUIV") (mkpair (mkpair (mksym "ACL2" 1590"IMPLIES") (mkpair (mkpair (mksym "ACL2" "CIRCUITP") (mkpair (mksym "ACL2" 1591"C") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 1592"C-BISIM-EQUIV") (mkpair (mkpair (mksym "ACL2" "CREATE-KRIPKE") (mkpair ( 1593mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 1594"CREATE-KRIPKE") (mkpair (mkpair (mksym "ACL2" "CONE-OF-INFLUENCE-REDUCTION") ( 1595mkpair (mksym "ACL2" "C") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 1596"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 1597"CONE-VARIABLES") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "C") ( 1598mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 1599"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1600, 1601 1602(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1603"CREATE-KRIPKE-PRODUCES-CIRCUIT-MODEL") (mkpair (mkpair (mksym "ACL2" 1604"IMPLIES") (mkpair (mkpair (mksym "ACL2" "CIRCUITP") (mkpair (mksym "ACL2" 1605"C") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 1606"CIRCUIT-MODELP") (mkpair (mkpair (mksym "ACL2" "CREATE-KRIPKE") (mkpair ( 1607mksym "ACL2" "C") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 1608mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1609, 1610 1611(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1612"C-BISIMILAR-INITIAL-STATE-WITNESS-M->N") (mkpair (mkpair (mksym "ACL2" "S") ( 1613mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1614"VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 1615"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym 1616"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1617"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1618"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") ( 1619mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1620, 1621 1622(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1623"C-BISIMILAR-INITIAL-STATE-WITNESS-N->M") (mkpair (mkpair (mksym "ACL2" "M") ( 1624mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1625"VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 1626"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym 1627"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1628"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1629"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") ( 1630mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1631, 1632 1633(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1634"C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair (mkpair (mksym "ACL2" "P") ( 1635mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" 1636"Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 1637"COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2" 1638"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym 1639"ACL2" "G") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "G") ( 1640mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 1641"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym 1642"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" 1643"VARS") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1644, 1645 1646(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 1647"C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mkpair (mksym "ACL2" "P") ( 1648mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" 1649"R") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 1650"COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2" 1651"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym 1652"ACL2" "G") (mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") ( 1653mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 1654"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym 1655"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" 1656"VARS") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 1657, 1658 1659(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1660"C-BISIMILAR-EQUIV-IMPLIES-INIT->INIT-M->N") (mkpair (mkpair (mksym "ACL2" 1661"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1662"ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") ( 1663mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 1664mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym 1665"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1666"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1667"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 1668mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 1669"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 1670mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "ACL2" 1671"C-BISIMILAR-INITIAL-STATE-WITNESS-M->N") (mkpair (mksym "ACL2" "S") (mkpair ( 1672mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1673mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 1674mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 1675"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") ( 1676mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 1677"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1678, 1679 1680(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1681"C-BISIMILAR-EQUIV-IMPLIES-INIT->INIT-N->M") (mkpair (mkpair (mksym "ACL2" 1682"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1683"ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") ( 1684mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 1685mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym 1686"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1687"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1688"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 1689mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 1690"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 1691mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "ACL2" 1692"C-BISIMILAR-INITIAL-STATE-WITNESS-N->M") (mkpair (mksym "ACL2" "M") (mkpair ( 1693mksym "ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1694mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 1695mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 1696"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 1697mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 1698"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1699, 1700 1701(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1702"C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-M->N") (mkpair (mkpair ( 1703mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1704mkpair (mksym "ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair ( 1705mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 1706mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair ( 1707mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1708mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) ( 1709mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1710"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1711"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 1712mkpair (mkpair (mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "S") ( 1713mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym "ACL2" 1714"C-BISIMILAR-INITIAL-STATE-WITNESS-M->N") (mkpair (mksym "ACL2" "S") (mkpair ( 1715mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1716mksym "COMMON-LISP" "NIL")))))) (mkpair (mksym "ACL2" "N") (mkpair (mksym 1717"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP" "NIL")))) ( 1718mksym "COMMON-LISP" "NIL")))) 1719, 1720 1721(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1722"C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-N->M") (mkpair (mkpair ( 1723mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1724mkpair (mksym "ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair ( 1725mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 1726mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair ( 1727mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1728mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) ( 1729mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1730"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1731"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 1732mkpair (mkpair (mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mkpair (mksym "ACL2" 1733"C-BISIMILAR-INITIAL-STATE-WITNESS-N->M") (mkpair (mksym "ACL2" "M") (mkpair ( 1734mksym "ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1735mksym "COMMON-LISP" "NIL")))))) (mkpair (mksym "ACL2" "M") (mkpair (mksym 1736"ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 1737"COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP" "NIL")))) (mksym 1738"COMMON-LISP" "NIL")))) 1739, 1740 1741(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1742"C-BISIMILAR-STATES-HAVE-LABELS-EQUAL") (mkpair (mkpair (mksym "ACL2" 1743"IMPLIES") (mkpair (mkpair (mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym 1744"ACL2" "P") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair ( 1745mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) ( 1746mkpair (mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mkpair (mksym "ACL2" 1747"SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym 1748"ACL2" "Q") (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 1749mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1750"ACL2" "SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair ( 1751mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 1752mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym 1753"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1754"NIL")))) 1755, 1756 1757(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1758"C-BISIMILAR-WITNESS-MEMBER-OF-STATES-M->N") (mkpair (mkpair (mksym "ACL2" 1759"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1760"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") ( 1761mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1762"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 1763"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair ( 1764mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") ( 1765mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 1766mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 1767mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 1768"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 1769mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1770mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 1771"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1772mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 1773"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 1774mkpair (mksym "ACL2" "C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair (mksym 1775"ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (mkpair ( 1776mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1777mksym "COMMON-LISP" "NIL")))))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 1778mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 1779mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" 1780"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 1781mksym "COMMON-LISP" "NIL")))) 1782, 1783 1784(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1785"C-BISIMILAR-WITNESS-MEMBER-OF-STATES-N->M") (mkpair (mkpair (mksym "ACL2" 1786"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1787"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") ( 1788mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1789"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 1790"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair ( 1791mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "N") ( 1792mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 1793mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 1794mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 1795"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) ( 1796mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1797mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 1798"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1799mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 1800"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 1801mkpair (mksym "ACL2" "C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mksym 1802"ACL2" "P") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair ( 1803mksym "ACL2" "R") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1804mksym "COMMON-LISP" "NIL")))))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 1805mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 1806mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 1807"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 1808mksym "COMMON-LISP" "NIL")))) 1809, 1810 1811(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1812"C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-M->N") (mkpair (mkpair (mksym 1813"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair ( 1814mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym 1815"ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair ( 1816mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 1817"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") ( 1818mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 1819mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1820"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1821"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") ( 1822mkpair (mkpair (mksym "ACL2" "C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair ( 1823mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") ( 1824mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1825"VARS") (mksym "COMMON-LISP" "NIL")))))))) (mkpair (mksym "ACL2" "N") (mkpair ( 1826mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP" 1827"NIL")))) (mksym "COMMON-LISP" "NIL")))) 1828, 1829 1830(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1831"C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-N->M") (mkpair (mkpair (mksym 1832"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair ( 1833mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym 1834"ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair ( 1835mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 1836"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") ( 1837mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 1838mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1839"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1840"ACL2" "CIRCUIT-BISIM") (mkpair (mkpair (mksym "ACL2" 1841"C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mksym "ACL2" "P") (mkpair ( 1842mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") ( 1843mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 1844"NIL")))))))) (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "R") (mkpair ( 1845mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) ( 1846mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1847, 1848 1849(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1850"C-BISIMILAR-WITNESS-MATCHES-TRANSITION-M->N") (mkpair (mkpair (mksym "ACL2" 1851"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1852"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") ( 1853mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1854"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2" 1855"NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair ( 1856mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1857"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1858"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1859"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym 1860"ACL2" "C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair (mksym "ACL2" "P") ( 1861mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" 1862"Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 1863"COMMON-LISP" "NIL")))))))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" 1864"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1865, 1866 1867(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1868"C-BISIMILAR-WITNESS-MATCHES-TRANSITION-N->M") (mkpair (mkpair (mksym "ACL2" 1869"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1870"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") ( 1871mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1872"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2" 1873"NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") (mkpair ( 1874mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1875"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1876"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1877"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym 1878"ACL2" "C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mksym "ACL2" "P") ( 1879mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" 1880"R") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 1881"COMMON-LISP" "NIL")))))))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 1882"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1883 1884]; 1885