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" "EVALUATION-EQ") ( 9mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym 10"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 11"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 12mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 13"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 14"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 15"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 16mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 17"NIL"))) (mkpair (mksym "ACL2" "P") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 18mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 19mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Q") ( 20mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 21mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (mksym 22"ACL2" "Q") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" 23"VARS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 24mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 25mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 26"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 27, 28 29(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 30"EVALUATION-EQ-IS-SYMMETRIC") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") ( 31mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") ( 32mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 33"NIL"))))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym 34"ACL2" "Q") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "VARS") (mksym 35"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 36"NIL")))) 37, 38 39(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 40"EVALUATION-EQ-MEMBER-P") (mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym 41"ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 42mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 43"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 44"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 45"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 46"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair ( 47mksym "ACL2" "ST") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 48"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") ( 49mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 50mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 51mkpair (mksym "ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "ST") ( 52mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") ( 53mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym 54"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 55"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 56, 57 58(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 59"EVALUATION-EQ-MEMBER") (mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym 60"ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 61mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 62"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 63"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 64"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 65"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair ( 66mksym "ACL2" "ST") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 67"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") ( 68mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 69mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 70mksym "ACL2" "EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "ST") (mkpair ( 71mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym 72"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 73"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) ( 74mksym "COMMON-LISP" "NIL"))))) 75, 76 77(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBER-IS-MEMBERP") ( 78mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" 79"EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" 80"STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 81mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "ACL2" 82"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" 83"STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 84mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mksym 85"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 86, 87 88(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 89"MEMBER-IS-EVALUATION-EQ") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 90mkpair (mksym "ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "P") ( 91mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym 92"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") ( 93mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" 94"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" 95"STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 96mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mksym 97"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 98, 99 100(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" "STRICT-EVALUATION-P") ( 101mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym 102"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "FORALL") (mkpair ( 103mkpair (mksym "ACL2" "V") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 104"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair ( 105mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" 106"VARS") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair ( 107mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 108mksym "ACL2" "V") (mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")))) ( 109mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 110"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 111, 112 113(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 114"STRICT-EVALUATION-P-EXPANDED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 115mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 116"STRICT-EVALUATION-P") (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" 117"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 118"NOT") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") ( 119mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym 120"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 121mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 122"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym 123"ACL2" "G") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "ST") (mksym 124"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 125"NIL")))) (mksym "COMMON-LISP" "NIL")))) 126, 127 128(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 129"STRICT-EVALUATION-LIST-P") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair ( 130mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 131"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 132mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 133"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 134"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 135"ACL2" "STRICT-EVALUATION-P") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 136mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 137"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 138"STRICT-EVALUATION-LIST-P") (mkpair (mksym "ACL2" "VARS") (mkpair (mkpair ( 139mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym 140"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 141"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 142"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 143"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 144, 145 146(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "EVALUATION-P") ( 147mkpair (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym 148"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 149mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym 150"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 151mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 152"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "BOOLEANP") (mkpair (mkpair ( 153mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 154"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "ST") ( 155mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 156mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" "ST") (mkpair (mkpair ( 157mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 158"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 159"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 160mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym 161"COMMON-LISP" "NIL"))))) 162, 163 164(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 165"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 166"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 167"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 168mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 169"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 170"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 171"ACL2" "EVALUATION-P") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 172mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 173"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 174"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 175mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 176"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 177"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 178mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym 179"COMMON-LISP" "NIL"))))) 180, 181 182(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" "ALL-EVALUATIONS-P") ( 183mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym 184"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "FORALL") (mkpair ( 185mkpair (mksym "ACL2" "ST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair ( 186mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (mkpair ( 187mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 188mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" 189"ST") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym 190"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 191"NIL")))) (mksym "COMMON-LISP" "NIL"))))) 192, 193 194(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 195"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "M-STATES") (mkpair ( 196mksym "ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 197"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 198"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "M-STATES") (mksym "COMMON-LISP" 199"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 200"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 201"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ-MEMBER-P") ( 202mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "M-STATES") ( 203mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N-STATES") (mkpair (mksym 204"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 205"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 206mksym "ACL2" "M-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 207"N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 208mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 209"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 210"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 211, 212 213(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 214"EVALUATION-EQ-SUBSET-TO-MEMBER") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 215mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 216"EVALUATION-EQ-SUBSET-P") (mkpair (mksym "ACL2" "M-STATES") (mkpair (mksym 217"ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 218mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair ( 219mksym "ACL2" "M-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 220mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 221"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 222"ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "P") (mkpair (mksym 223"ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 224mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 225, 226 227(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "TRUTHP-LABEL") ( 228mkpair (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "S") (mksym 229"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 230mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "LABEL") (mksym 231"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 232mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 233"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair ( 234mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 235mksym "ACL2" "LABEL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "S") ( 236mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 237mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mksym 238"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair ( 239mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "LABEL") (mksym 240"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "S") (mksym "COMMON-LISP" "NIL")))) ( 241mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 242"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 243"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 244, 245 246(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ONLY-TRUTH-P") ( 247mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "M") (mksym 248"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 249mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym 250"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 251mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 252"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair ( 253mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 254mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 255"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 256"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 257"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 258"ONLY-TRUTH-P") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym 259"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 260mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 261mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 262"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 263"NIL"))))) 264, 265 266(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 267"ALL-TRUTHSP-LABEL") (mkpair (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym 268"ACL2" "S") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 269mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 270"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 271"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 272"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 273"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair ( 274mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 275mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "VARS") (mksym 276"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "S") (mksym "COMMON-LISP" "NIL")))) ( 277mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") ( 278mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 279mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 280mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 281"LABEL") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 282mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" 283"LABEL") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP" 284"CDR") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))) (mksym 285"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 286mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 287"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 288"NIL"))))) 289, 290 291(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 292"ALL-TRUTHSP-LABEL-EXPANDED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 293mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 294"ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "S") ( 295mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 296mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 297mksym "ACL2" "V") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 298mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" 299"G") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "S") (mksym 300"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 301mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 302"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 303"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 304mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 305"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 306mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym 307"ACL2" "LABEL") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 308mksym "COMMON-LISP" "NIL")))) 309, 310 311(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 312"ONLY-ALL-TRUTHS-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 313"ACL2" "M") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 314mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 315"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 316"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 317"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 318"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") ( 319mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" 320"CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 321mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 322"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 323"NIL"))) (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 324mkpair (mkpair (mksym "ACL2" "ONLY-ALL-TRUTHS-P") (mkpair (mkpair (mksym 325"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 326"NIL"))) (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "VARS") (mksym 327"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 328mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 329"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 330"NIL"))))) 331, 332 333(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 334"LABEL-SUBSET-VARS") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 335"ACL2" "M") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 336mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 337"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 338"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 339"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 340"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mkpair ( 341mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 342mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 343"M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mksym 344"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "LABEL-SUBSET-VARS") ( 345mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") ( 346mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" 347"VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" 348"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 349mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym 350"COMMON-LISP" "NIL"))))) 351, 352 353(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 354"LABEL-SUBSET-SUBSET-REDUCTION") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 355mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 356"LABEL-SUBSET-VARS") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" 357"M") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 358mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym 359"ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 360"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 361"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 362"ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym 363"ACL2" "P") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 364mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 365"NIL")))) (mksym "COMMON-LISP" "NIL")))) 366, 367 368(mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" 369"WELL-FORMED-TRANSITION-P") (mkpair (mkpair (mksym "ACL2" "STATES-M") (mkpair ( 370mksym "ACL2" "TRANS-M") (mkpair (mksym "ACL2" "STATES-N") (mkpair (mksym 371"ACL2" "TRANS-N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))))) ( 372mkpair (mkpair (mksym "ACL2" "FORALL") (mkpair (mkpair (mksym "ACL2" "P") ( 373mkpair (mksym "ACL2" "Q") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 374mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 375mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair ( 376mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 377mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 378"EVALUATION-P") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "VARS") ( 379mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 380mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair ( 381mksym "ACL2" "STATES-M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 382mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 383mksym "ACL2" "Q") (mkpair (mksym "ACL2" "STATES-N") (mksym "COMMON-LISP" 384"NIL")))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" 385"Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 386mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 387mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 388mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 389"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 390"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 391"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 392"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 393"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 394"ACL2" "EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 395mksym "ACL2" "P") (mkpair (mksym "ACL2" "TRANS-M") (mksym "COMMON-LISP" "NIL")))) ( 396mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "Q") (mkpair (mksym 397"ACL2" "TRANS-N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") ( 398mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym 399"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 400, 401 402(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 403"WELL-FORMED-TRANSITION-P-EXPANDED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 404mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 405"WELL-FORMED-TRANSITION-P") (mkpair (mksym "ACL2" "STATES-M") (mkpair (mksym 406"ACL2" "TRANS-M") (mkpair (mksym "ACL2" "STATES-N") (mkpair (mksym "ACL2" 407"TRANS-N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) ( 408mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 409"EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") ( 410mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 411mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") ( 412mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 413"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 414"ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "STATES-M") ( 415mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 416mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "Q") (mkpair ( 417mksym "ACL2" "STATES-N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 418mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" 419"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 420"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 421mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 422mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 423"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 424mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 425"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 426mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 427"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 428mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 429"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 430"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym 431"ACL2" "P") (mkpair (mksym "ACL2" "TRANS-M") (mksym "COMMON-LISP" "NIL")))) ( 432mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "Q") (mkpair (mksym 433"ACL2" "TRANS-N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") ( 434mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym 435"COMMON-LISP" "NIL")))) 436, 437 438(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 439"TRANSITION-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 440"ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "TRANS") (mksym "COMMON-LISP" 441"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 442"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 443"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 444"COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 445"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mkpair ( 446mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 447"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "TRANS") ( 448mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "STATES-PRIME") (mksym 449"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "TRANSITION-SUBSET-P") ( 450mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") ( 451mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "STATES-PRIME") (mkpair ( 452mksym "ACL2" "TRANS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 453"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 454"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 455"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 456, 457 458(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 459"TRANSITION-SUBSET-P-EXPANDED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 460mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 461"TRANSITION-SUBSET-P") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" 462"STATES-PRIME") (mkpair (mksym "ACL2" "TRANS") (mksym "COMMON-LISP" "NIL"))))) ( 463mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 464"MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "STATES") (mksym 465"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 466mksym "ACL2" "R") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" 467"P") (mkpair (mksym "ACL2" "TRANS") (mksym "COMMON-LISP" "NIL")))) (mksym 468"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 469mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 470"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 471"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 472mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "R") (mkpair ( 473mksym "ACL2" "STATES-PRIME") (mksym "COMMON-LISP" "NIL")))) (mksym 474"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 475, 476 477(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CIRCUIT-MODELP") ( 478mkpair (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")) (mkpair ( 479mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 480"ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 481mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 482"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 483mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 484"QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) ( 485mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 486"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 487"ACL2" "ALL-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 488mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 489mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 490"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 491"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 492"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 493mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 494mkpair (mkpair (mksym "ACL2" "STRICT-EVALUATION-LIST-P") (mkpair (mkpair ( 495mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 496mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 497"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 498mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 499"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym 500"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 501"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ONLY-ALL-TRUTHS-P") ( 502mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 503"QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) ( 504mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym 505"ACL2" "M") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 506"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 507"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 508mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 509mkpair (mkpair (mksym "ACL2" "ONLY-TRUTH-P") (mkpair (mkpair (mksym "ACL2" 510"G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 511"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym 512"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 513mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 514"LABEL-SUBSET-VARS") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 515mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 516"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 517mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 518mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 519"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 520mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 521mkpair (mkpair (mksym "ACL2" "TRANSITION-SUBSET-P") (mkpair (mkpair (mksym 522"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 523"KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 524mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 525mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 526mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 527"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 528"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym 529"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 530mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 531mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "G") ( 532mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 533"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 534mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 535mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 536mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 537"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 538"IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mkpair (mksym 539"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 540"KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 541mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 542mksym "ACL2" "NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair ( 543mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 544mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 545mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 546mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 547"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 548mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 549mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 550mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 551"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 552"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 553"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 554"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 555"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 556"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 557"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 558"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 559"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 560"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 561"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 562"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 563"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 564"NIL"))))) 565, 566 567(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "C-BISIM-EQUIV") ( 568mkpair (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym 569"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 570"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair ( 571mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 572"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair ( 573mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 574"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym 575"ACL2" "VARS") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 576"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 577"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 578mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 579mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair ( 580mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 581mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 582mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 583mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 584"WELL-FORMED-TRANSITION-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 585mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 586mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 587"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 588"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym 589"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 590mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 591"QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) ( 592mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 593mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 594mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 595"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") ( 596mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 597mkpair (mkpair (mksym "ACL2" "WELL-FORMED-TRANSITION-P") (mkpair (mkpair ( 598mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 599mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 600"N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 601mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 602"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym 603"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 604mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 605"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 606mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 607"QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) ( 608mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym 609"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 610"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ-SUBSET-P") ( 611mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 612"QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" 613"NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 614mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 615mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) ( 616mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym 617"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 618"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 619mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") ( 620mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" 621"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 622"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym 623"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 624mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 625mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 626"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 627"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 628"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 629"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 630"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 631"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 632"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 633"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 634"COMMON-LISP" "NIL"))) (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"))))) (mkpair (mkpair (mksym 637"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 638"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 639"NIL"))))) 640, 641 642(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "CIRCUIT-BISIM") ( 643mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (mkpair (mksym 644"ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 645"COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 646mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair (mksym "ACL2" "M") (mksym 647"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 648mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair (mksym "ACL2" "N") (mksym 649"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 650mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mkpair ( 651mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 652mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 653"M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair ( 654mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 655mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 656mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 657"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) ( 658mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 659mkpair (mkpair (mksym "ACL2" "WELL-FORMED-TRANSITION-P") (mkpair (mkpair ( 660mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 661mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 662"M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 663mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 664"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym 665"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 666mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 667"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) ( 668mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 669"QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) ( 670mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym 671"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 672"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "WELL-FORMED-TRANSITION-P") ( 673mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" 674"QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) ( 675mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 676mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 677mksym "KEYWORD" "TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 678"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 679mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 680"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym 681"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 682mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym 683"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 684mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair ( 685mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 686"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 687mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") ( 688mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 689"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 690"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym 691"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) ( 692mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 693mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 694"EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 695mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") ( 696mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" 697"NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 698"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym 699"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 700mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 701mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 702mksym "ACL2" "VARS") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 703mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "VARIABLES") (mksym 704"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 705mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 706mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair ( 707mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 708mkpair (mksym "KEYWORD" "VARIABLES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 709mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 710mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") ( 711mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 712"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 713"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 714mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 715"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 716mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 717mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 718mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 719"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 720"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 721"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 722"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 723"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 724"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 725"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 726"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 727"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 728"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 729"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 730"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 731"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 732"NIL"))))) 733, 734 735(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 736"C-BISIMILAR-INITIAL-STATE-WITNESS-M->N") (mkpair (mkpair (mksym "ACL2" "S") ( 737mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 738"VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 739"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym 740"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 741"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 742"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") ( 743mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 744, 745 746(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 747"C-BISIMILAR-INITIAL-STATE-WITNESS-N->M") (mkpair (mkpair (mksym "ACL2" "M") ( 748mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 749"VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 750"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym 751"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 752"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 753"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") ( 754mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 755, 756 757(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 758"ALL-EVALUATIONS-CONSIDERS-AN-EVALUATION-A-MEMBER") (mkpair (mkpair (mksym 759"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair ( 760mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" "ST") (mkpair (mksym 761"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 762"ALL-EVALUATIONS-P") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" 763"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 764"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 765mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" 766"EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" 767"STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 768mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 769, 770 771(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 772"TRUTHP-LABEL-FROM-ONLY-TRUTHP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 773mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 774"ONLY-TRUTH-P") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "M") ( 775mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 776mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "STATES") (mksym 777"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 778mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 779"NIL"))))) (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (mkpair ( 780mksym "ACL2" "LABEL-OF") (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "M") ( 781mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "S") (mksym "COMMON-LISP" 782"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 783, 784 785(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 786"ALL-TRUTHS-P-FROM-ONLY-ALL-TRUTHS-P") (mkpair (mkpair (mksym "ACL2" 787"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 788"ACL2" "ONLY-ALL-TRUTHS-P") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 789"ACL2" "M") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 790mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair ( 791mksym "ACL2" "STATES") (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"ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair ( 795mksym "ACL2" "S") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 796mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 797"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 798, 799 800(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 801"MEMBERP-TO-INTERSECT-REDUCTION") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 802mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair ( 803mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mksym "ACL2" "X") (mkpair ( 804mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 805mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 806"MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "X") (mksym 807"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 808mksym "ACL2" "V") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) ( 809mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 810"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 811"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 812, 813 814(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 815"EVALUATION-EQ-VARS-REDUCTION") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 816mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 817"EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") ( 818mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 819mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" 820"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 821"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 822mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") ( 823mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "V") (mkpair (mksym 824"ACL2" "P") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") ( 825mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "Q") (mksym "COMMON-LISP" 826"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 827mksym "COMMON-LISP" "NIL")))) 828, 829 830(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 831"VARIABLES-IN-LABEL-ARE-T-IN-Q") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 832mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 833"MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2" 834"SET-INTERSECT") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "VARS") ( 835mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 836mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") ( 837mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "P") (mksym "COMMON-LISP" 838"NIL")))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym 839"ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym 840"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 841mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 842"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 843mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 844"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") ( 845mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "V") (mkpair (mksym 846"ACL2" "Q") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 847"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 848"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 849"COMMON-LISP" "NIL")))) 850, 851 852(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 853"ONLY-TRUTHSP-AND-SUBSET-TO-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 854mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 855"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym 856"ACL2" "V") (mkpair (mksym "ACL2" "Q") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 857mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym 858"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 859"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym 860"ACL2" "V") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 861mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 862"SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "VARIABLES") ( 863mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 864"ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "Q") ( 865mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 866mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 867mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 868mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 869"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 870"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 871"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 872"ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "LABEL") ( 873mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 874"COMMON-LISP" "NIL")))) 875, 876 877(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 878"TRUTHP-LABEL-TO-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 879mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 880mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") ( 881mkpair (mksym "ACL2" "LP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 882"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 883"IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (mksym "ACL2" 884"LP") (mkpair (mksym "ACL2" "P") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 885mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 886"EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") ( 887mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 888mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 889mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" 890"NIL")))) (mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mksym 891"ACL2" "LQ") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARIABLES") ( 892mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 893mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 894"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 895mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 896"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 897mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 898"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 899mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 900"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 901mksym "ACL2" "V") (mkpair (mksym "ACL2" "LQ") (mksym "COMMON-LISP" "NIL")))) ( 902mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 903, 904 905(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 906"TRUTHP-LABEL-IS-A-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 907mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 908"TRUTHP-LABEL") (mkpair (mksym "ACL2" "LP") (mkpair (mksym "ACL2" "P") (mksym 909"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 910mkpair (mksym "ACL2" "EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair ( 911mksym "ACL2" "Q") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 912mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 913"SUBSET") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "VARIABLES") ( 914mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 915"ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LQ") (mkpair (mksym "ACL2" "Q") ( 916mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 917mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 918mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 919mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 920"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 921"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 922"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 923"ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair ( 924mksym "ACL2" "LP") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 925mkpair (mksym "ACL2" "LQ") (mksym "COMMON-LISP" "NIL")))) (mksym 926"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 927, 928 929(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 930"C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair (mkpair (mksym "ACL2" "P") ( 931mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" 932"Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 933"COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2" 934"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym 935"ACL2" "G") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "G") ( 936mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 937"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym 938"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" 939"VARS") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 940, 941 942(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 943"C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mkpair (mksym "ACL2" "P") ( 944mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" 945"R") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 946"COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2" 947"EVALUATION-EQ-MEMBER") (mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym 948"ACL2" "G") (mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") ( 949mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 950"TRANSITION") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym 951"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" 952"VARS") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 953, 954 955(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 956"EVALUATIONP-FOR-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 957mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 958"EVALUATION-P") (mkpair (mksym "ACL2" "ST") (mkpair (mksym "ACL2" "VARIABLES") ( 959mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 960mksym "ACL2" "VARS") (mkpair (mksym "ACL2" "VARIABLES") (mksym "COMMON-LISP" 961"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 962"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 963mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" "ST") ( 964mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym 965"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 966, 967 968(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 969"EVALUATION-P-ONLY-EVALUATIONS-REDUCTION") (mkpair (mkpair (mksym "ACL2" 970"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 971"ACL2" "ONLY-EVALUATIONS-P") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym 972"ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 973"MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "STATES") (mksym 974"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 975mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 976"NIL"))))) (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") (mkpair (mksym 977"ACL2" "P") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) ( 978mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 979, 980 981(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 982"R-IS-EVALUATION-EQ-MEMBER-P") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 983mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 984"EVALUATION-EQ") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") ( 985mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 986mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 987"WELL-FORMED-TRANSITION-P") (mkpair (mksym "ACL2" "STATES-M") (mkpair (mksym 988"ACL2" "TRANS-M") (mkpair (mksym "ACL2" "STATES-N") (mkpair (mksym "ACL2" 989"TRANS-N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) ( 990mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 991"MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "STATES-M") ( 992mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 993mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "Q") (mkpair ( 994mksym "ACL2" "STATES-N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 995mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "EVALUATION-P") ( 996mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 997"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 998"ACL2" "EVALUATION-P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" 999"VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 1000"MEMBERP") (mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym "ACL2" "G") ( 1001mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "TRANS-M") (mksym 1002"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1003"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1004"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1005"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1006"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1007"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1008"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1009"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1010"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1011"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1012"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1013"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1014"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1015"ACL2" "EVALUATION-EQ-MEMBER-P") (mkpair (mksym "ACL2" "R") (mkpair (mkpair ( 1016mksym "ACL2" "G") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "TRANS-N") ( 1017mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mksym 1018"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1019"NIL")))) 1020, 1021 1022(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1023"C-BISIMILAR-EQUIV-IMPLIES-INIT->INIT-M->N") (mkpair (mkpair (mksym "ACL2" 1024"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1025"ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") ( 1026mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 1027mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym 1028"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1029"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1030"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 1031mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 1032"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 1033mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "ACL2" 1034"C-BISIMILAR-INITIAL-STATE-WITNESS-M->N") (mkpair (mksym "ACL2" "S") (mkpair ( 1035mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1036mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 1037mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 1038"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") ( 1039mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 1040"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1041, 1042 1043(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1044"C-BISIMILAR-EQUIV-IMPLIES-INIT->INIT-N->M") (mkpair (mkpair (mksym "ACL2" 1045"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1046"ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") ( 1047mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 1048mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym 1049"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1050"KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 1051"ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 1052mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 1053"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 1054mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "ACL2" 1055"C-BISIMILAR-INITIAL-STATE-WITNESS-N->M") (mkpair (mksym "ACL2" "M") (mkpair ( 1056mksym "ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1057mksym "COMMON-LISP" "NIL")))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 1058mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 1059"INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 1060mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 1061"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1062, 1063 1064(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1065"C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-M->N") (mkpair (mkpair ( 1066mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1067mkpair (mksym "ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair ( 1068mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 1069mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair ( 1070mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1071mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) ( 1072mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1073"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1074"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 1075mkpair (mkpair (mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "S") ( 1076mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym "ACL2" 1077"C-BISIMILAR-INITIAL-STATE-WITNESS-M->N") (mkpair (mksym "ACL2" "S") (mkpair ( 1078mksym "ACL2" "M") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1079mksym "COMMON-LISP" "NIL")))))) (mkpair (mksym "ACL2" "N") (mkpair (mksym 1080"ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP" "NIL")))) ( 1081mksym "COMMON-LISP" "NIL")))) 1082, 1083 1084(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1085"C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-N->M") (mkpair (mkpair ( 1086mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 1087mkpair (mksym "ACL2" "C-BISIM-EQUIV") (mkpair (mksym "ACL2" "M") (mkpair ( 1088mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) ( 1089mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S") (mkpair ( 1090mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1091mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) ( 1092mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1093"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 1094"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 1095mkpair (mkpair (mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mkpair (mksym "ACL2" 1096"C-BISIMILAR-INITIAL-STATE-WITNESS-N->M") (mkpair (mksym "ACL2" "M") (mkpair ( 1097mksym "ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1098mksym "COMMON-LISP" "NIL")))))) (mkpair (mksym "ACL2" "M") (mkpair (mksym 1099"ACL2" "S") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 1100"COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP" "NIL")))) (mksym 1101"COMMON-LISP" "NIL")))) 1102, 1103 1104(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1105"C-BISIMILAR-STATES-HAVE-LABELS-EQUAL") (mkpair (mkpair (mksym "ACL2" 1106"IMPLIES") (mkpair (mkpair (mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym 1107"ACL2" "P") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair ( 1108mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) ( 1109mkpair (mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mkpair (mksym "ACL2" 1110"SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym 1111"ACL2" "Q") (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 1112mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 1113"ACL2" "SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair ( 1114mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 1115mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym 1116"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 1117"NIL")))) 1118, 1119 1120(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1121"C-BISIMILAR-WITNESS-MEMBER-OF-STATES-M->N") (mkpair (mkpair (mksym "ACL2" 1122"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1123"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") ( 1124mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1125"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 1126"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair ( 1127mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") ( 1128mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 1129mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 1130mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 1131"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 1132mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1133mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 1134"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1135mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 1136"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 1137mkpair (mksym "ACL2" "C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair (mksym 1138"ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (mkpair ( 1139mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1140mksym "COMMON-LISP" "NIL")))))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 1141mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 1142mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" 1143"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 1144mksym "COMMON-LISP" "NIL")))) 1145, 1146 1147(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1148"C-BISIMILAR-WITNESS-MEMBER-OF-STATES-N->M") (mkpair (mkpair (mksym "ACL2" 1149"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1150"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") ( 1151mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1152"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 1153"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair ( 1154mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "N") ( 1155mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 1156mkpair (mksym "ACL2" "R") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 1157mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 1158"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) ( 1159mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1160mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 1161"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 1162mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 1163"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 1164mkpair (mksym "ACL2" "C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mksym 1165"ACL2" "P") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair ( 1166mksym "ACL2" "R") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") ( 1167mksym "COMMON-LISP" "NIL")))))))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 1168mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 1169mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 1170"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 1171mksym "COMMON-LISP" "NIL")))) 1172, 1173 1174(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1175"C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-M->N") (mkpair (mkpair (mksym 1176"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair ( 1177mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym 1178"ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair ( 1179mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 1180"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") ( 1181mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 1182mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1183"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1184"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") ( 1185mkpair (mkpair (mksym "ACL2" "C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair ( 1186mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") ( 1187mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1188"VARS") (mksym "COMMON-LISP" "NIL")))))))) (mkpair (mksym "ACL2" "N") (mkpair ( 1189mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP" 1190"NIL")))) (mksym "COMMON-LISP" "NIL")))) 1191, 1192 1193(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1194"C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-N->M") (mkpair (mkpair (mksym 1195"ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair ( 1196mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym 1197"ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair ( 1198mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 1199"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") ( 1200mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 1201mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1202"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1203"ACL2" "CIRCUIT-BISIM") (mkpair (mkpair (mksym "ACL2" 1204"C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mksym "ACL2" "P") (mkpair ( 1205mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") ( 1206mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" 1207"NIL")))))))) (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "R") (mkpair ( 1208mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) ( 1209mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1210, 1211 1212(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1213"C-BISIMILAR-WITNESS-MATCHES-TRANSITION-M->N") (mkpair (mkpair (mksym "ACL2" 1214"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1215"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") ( 1216mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1217"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2" 1218"NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair ( 1219mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1220"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1221"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1222"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym 1223"ACL2" "C-BISIMILAR-TRANSITION-WITNESS-M->N") (mkpair (mksym "ACL2" "P") ( 1224mkpair (mksym "ACL2" "R") (mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" 1225"Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 1226"COMMON-LISP" "NIL")))))))) (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" 1227"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1228, 1229 1230(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 1231"C-BISIMILAR-WITNESS-MATCHES-TRANSITION-N->M") (mkpair (mkpair (mksym "ACL2" 1232"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 1233"ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") ( 1234mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 1235"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym "ACL2" 1236"NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") (mkpair ( 1237mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1238"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 1239"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 1240"ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym 1241"ACL2" "C-BISIMILAR-TRANSITION-WITNESS-N->M") (mkpair (mksym "ACL2" "P") ( 1242mkpair (mksym "ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" 1243"R") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" "VARS") (mksym 1244"COMMON-LISP" "NIL")))))))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 1245"NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 1246 1247]; 1248