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" "LTL-CONSTANTP") ( 9mkpair (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL")) (mkpair ( 10mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 11"EQUAL") (mkpair (mksym "ACL2" "F") (mkpair (mkpair (mksym "COMMON-LISP" 12"QUOTE") (mkpair (mksym "ACL2" "TRUE") (mksym "COMMON-LISP" "NIL"))) (mksym 13"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair ( 14mksym "ACL2" "F") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 15mksym "ACL2" "TRUE") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 16mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "F") ( 17mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2" "FALSE") ( 18mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 19"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 20, 21 22(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LTL-VARIABLEP") ( 23mkpair (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL")) (mkpair ( 24mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 25"SYMBOLP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 26mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 27mkpair (mksym "ACL2" "F") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 28mkpair (mkpair (mksym "COMMON-LISP" "+") (mkpair (mksym "ACL2" "&") (mkpair ( 29mksym "ACL2" "U") (mkpair (mksym "ACL2" "W") (mkpair (mksym "ACL2" "X") ( 30mkpair (mksym "ACL2" "F") (mkpair (mksym "ACL2" "G") (mksym "COMMON-LISP" 31"NIL")))))))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 32mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 33mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 34"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 35, 36 37(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LTL-FORMULAP") ( 38mkpair (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL")) (mkpair ( 39mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") ( 40mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 41mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "LTL-CONSTANTP") ( 42mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 43mksym "ACL2" "LTL-CONSTANTP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" 44"NIL"))) (mkpair (mkpair (mksym "ACL2" "LTL-VARIABLEP") (mkpair (mksym "ACL2" 45"F") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 46mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 47"EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" "F") ( 48mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 49mkpair (mknum "3" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym 50"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 51mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 52mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym 53"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 54"COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym "COMMON-LISP" "+") (mkpair ( 55mksym "ACL2" "&") (mkpair (mksym "ACL2" "U") (mkpair (mksym "ACL2" "W") ( 56mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))) (mksym 57"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 58mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP" 59"CAR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mksym 60"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair ( 61mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 62mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym 63"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 64"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 65"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 66mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 67mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 68"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 69mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") ( 70mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 71mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym 72"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 73"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair ( 74mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" 75"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym 76"ACL2" "~") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "F") (mkpair ( 77mksym "ACL2" "G") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))) ( 78mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") ( 79mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym 80"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) ( 81mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 82mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 83"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 84"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 85"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 86"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 87, 88 89(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 90"RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "ACL2" "F") (mkpair (mksym 91"ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 92"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ATOM") (mkpair ( 93mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 94"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "LTL-CONSTANTP") (mkpair ( 95mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 96"LTL-CONSTANTP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) ( 97mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 98"LTL-VARIABLEP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) ( 99mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "F") (mkpair ( 100mksym "ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 101"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 102"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 103"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 104"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym 105"ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 106"COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym "COMMON-LISP" 107"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 108"IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym 109"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 110mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 111mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mkpair (mksym "ACL2" 112"&") (mkpair (mksym "COMMON-LISP" "+") (mkpair (mksym "ACL2" "U") (mkpair ( 113mksym "ACL2" "W") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))) ( 114mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 115mkpair (mkpair (mksym "ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym 116"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) ( 117mkpair (mksym "ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 118mksym "ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP" 119"CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym 120"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) ( 121mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 122"ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 123"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 124"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 125"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 126"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 127"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair ( 128mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" 129"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" 130"0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair ( 131mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 132mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "F") (mksym 133"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 134mkpair (mksym "ACL2" "~") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" 135"F") (mkpair (mksym "ACL2" "G") (mksym "COMMON-LISP" "NIL"))))) (mksym 136"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 137"ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 138mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym 139"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 140"V-LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 141"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 142mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 143mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 144"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 145"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 146, 147 148(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 149"RESTRICTED-FORMULA-IS-AN-LTL-FORMULA") (mkpair (mkpair (mksym "ACL2" 150"IMPLIES") (mkpair (mkpair (mksym "ACL2" "RESTRICTED-FORMULAP") (mkpair ( 151mksym "ACL2" "F") (mkpair (mksym "ACL2" "V-LIST") (mksym "COMMON-LISP" "NIL")))) ( 152mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (mksym "ACL2" "F") ( 153mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 154"COMMON-LISP" "NIL")))) 155, 156 157(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 158"CREATE-RESTRICTED-VAR-SET") (mkpair (mkpair (mksym "ACL2" "F") (mksym 159"COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 160mkpair (mksym "COMMON-LISP" "ATOM") (mkpair (mksym "ACL2" "F") (mksym 161"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 162mkpair (mksym "ACL2" "LTL-CONSTANTP") (mkpair (mksym "ACL2" "F") (mksym 163"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 164mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 165mksym "COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "F") (mkpair (mkpair (mksym 166"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 167"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 168"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 169"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "LEN") (mkpair (mksym 170"ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 171"COMMON-LISP" "QUOTE") (mkpair (mknum "3" "1" "0" "1") (mksym "COMMON-LISP" 172"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 173"SET-UNION") (mkpair (mkpair (mksym "ACL2" "CREATE-RESTRICTED-VAR-SET") ( 174mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "F") (mksym 175"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 176"ACL2" "CREATE-RESTRICTED-VAR-SET") (mkpair (mkpair (mksym "COMMON-LISP" 177"CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym 178"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) ( 179mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym 180"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 181"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair ( 182mkpair (mksym "ACL2" "LEN") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" 183"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" 184"0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair ( 185mkpair (mksym "ACL2" "CREATE-RESTRICTED-VAR-SET") (mkpair (mkpair (mksym 186"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 187mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 188mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 189mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 190"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 191"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 192, 193 194(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 195"LTL-FORMULA-IS-A-RESTRICTED-FORMULA") (mkpair (mkpair (mksym "ACL2" 196"IMPLIES") (mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (mksym 197"ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" 198"RESTRICTED-FORMULAP") (mkpair (mksym "ACL2" "F") (mkpair (mkpair (mksym 199"ACL2" "CREATE-RESTRICTED-VAR-SET") (mkpair (mksym "ACL2" "F") (mksym 200"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 201"NIL")))) (mksym "COMMON-LISP" "NIL")))) 202, 203 204(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "NEXT-STATEP") ( 205mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym 206"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 207"MEMBERP") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "G") ( 208mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 209mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym 210"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 211mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 212"COMMON-LISP" "NIL"))))) 213, 214 215(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "INITIAL-STATEP") ( 216mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") (mksym 217"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 218mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 219"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym 220"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 221mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 222, 223 224(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LABEL-OF") ( 225mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "M") (mksym 226"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym 227"ACL2" "S") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 228"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "LABEL-FN") (mksym 229"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 230mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 231, 232 233(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" 234"NEXT-STATES-IN-STATES") (mkpair (mkpair (mksym "ACL2" "M") (mkpair (mksym 235"ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 236"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 237mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 238"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 239"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 240"ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 241"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 242"NIL"))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 243"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "TRANSITION") (mksym 244"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 245mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "G") (mkpair ( 246mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") ( 247mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 248"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 249"NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym 250"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" 251"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 252"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 253mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym 254"COMMON-LISP" "NIL"))))) 255, 256 257(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 258"NEXT-STATES-IN-STATES-CLARIFIED-AUX") (mkpair (mkpair (mksym "ACL2" 259"IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 260"ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "STATES") ( 261mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 262mkpair (mkpair (mksym "ACL2" "NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" 263"M") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 264mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mksym 265"ACL2" "Q") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))))) ( 266mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 267"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 268mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 269mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 270mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym 271"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 272"KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 273mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 274"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 275, 276 277(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 278"NEXT-STATES-IN-STATES-CLARIFIED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 279mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 280"NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym 281"ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 282"KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") ( 283mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 284mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 285mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 286"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 287"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 288mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") ( 289mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" 290"M") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" 291"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 292mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 293mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 294"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 295mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym 296"COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 297"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 298mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 299"COMMON-LISP" "NIL")))) 300 301]; 302