1open HolKernel Parse boolLib bossLib intSyntax pairSyntax listSyntax stringLib numLib sexp; 2 3val package = 4 implode(map chr (cons 77 (cons 49 nil))); 5 6val events = [ 7 8(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PUSH") (mkpair ( 9mkpair (mksym "M1" "X") (mkpair (mksym "M1" "Y") (mksym "COMMON-LISP" "NIL"))) ( 10mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "X") (mkpair ( 11mksym "M1" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 12, 13 14(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TOP") (mkpair ( 15mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair ( 16mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" 17"NIL"))) (mksym "COMMON-LISP" "NIL"))))) 18, 19 20(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "POP") (mkpair ( 21mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair ( 22mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" 23"NIL"))) (mksym "COMMON-LISP" "NIL"))))) 24, 25 26(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NTH") (mkpair ( 27mkpair (mksym "M1" "N") (mkpair (mksym "COMMON-LISP" "LIST") (mksym 28"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 29mkpair (mksym "ACL2" "ZP") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" 30"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym 31"COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 32"M1" "NTH") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym 33"COMMON-LISP" "QUOTE") (mkpair (mknum "-1" "1" "0" "1") (mksym "COMMON-LISP" 34"NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 35mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "COMMON-LISP" "LIST") ( 36mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 37"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 38, 39 40(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "MAKE-STATE") ( 41mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "LOCALS") (mkpair (mksym 42"M1" "STACK") (mkpair (mksym "M1" "PROGRAM") (mksym "COMMON-LISP" "NIL"))))) ( 43mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "PC") (mkpair ( 44mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "LOCALS") (mkpair ( 45mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "STACK") (mkpair ( 46mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "PROGRAM") (mkpair ( 47mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 48mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 49"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 50"NIL")))) (mksym "COMMON-LISP" "NIL"))))) 51, 52 53(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PC") (mkpair ( 54mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 55"M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" 56"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym 57"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 58, 59 60(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "LOCALS") (mkpair ( 61mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 62"M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "1" 63"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym 64"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 65, 66 67(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "STACK") (mkpair ( 68mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 69"M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" 70"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym 71"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 72, 73 74(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PROGRAM") (mkpair ( 75mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 76"M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "3" 77"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "S") (mksym 78"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 79, 80 81(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "OP-CODE") (mkpair ( 82mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair ( 83mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" 84"NIL"))) (mksym "COMMON-LISP" "NIL"))))) 85, 86 87(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ARG1") (mkpair ( 88mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair ( 89mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 90mknum "1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" 91"INST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 92, 93 94(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ARG2") (mkpair ( 95mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair ( 96mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 97mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" 98"INST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 99, 100 101(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ARG3") (mkpair ( 102mkpair (mksym "M1" "INST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair ( 103mksym "M1" "NTH") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 104mknum "3" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" 105"INST") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 106, 107 108(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "LEN") (mkpair ( 109mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 110"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 111mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 112"COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" 113"NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym 114"COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" 115"NIL"))) (mkpair (mkpair (mksym "M1" "LEN") (mkpair (mkpair (mksym 116"COMMON-LISP" "CDR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) ( 117mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 118"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 119, 120 121(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "APP") (mkpair ( 122mkpair (mksym "M1" "X") (mkpair (mksym "M1" "Y") (mksym "COMMON-LISP" "NIL"))) ( 123mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 124"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) ( 125mkpair (mksym "M1" "Y") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair ( 126mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "X") (mksym 127"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair ( 128mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" 129"NIL"))) (mkpair (mksym "M1" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym 130"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 131"NIL"))))) 132, 133 134(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "REV") (mkpair ( 135mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 136"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 137mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 138"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 139"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "APP") (mkpair (mkpair ( 140mksym "M1" "REV") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym 141"M1" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair ( 142mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" 143"CAR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 144mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 145"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 146"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 147, 148 149(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "REV1") (mkpair ( 150mkpair (mksym "M1" "X") (mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL"))) ( 151mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 152"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) ( 153mkpair (mksym "M1" "A") (mkpair (mkpair (mksym "M1" "REV1") (mkpair (mkpair ( 154mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" 155"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym 156"COMMON-LISP" "CAR") (mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL"))) ( 157mkpair (mksym "M1" "A") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 158"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 159, 160 161(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "FREV") (mkpair ( 162mkpair (mksym "M1" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 163"M1" "REV1") (mkpair (mksym "M1" "X") (mkpair (mkpair (mksym "COMMON-LISP" 164"QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) ( 165mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 166, 167 168(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "REPEAT") (mkpair ( 169mkpair (mksym "M1" "TH") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) ( 170mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") ( 171mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 172"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 173"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair ( 174mksym "M1" "TH") (mkpair (mkpair (mksym "M1" "REPEAT") (mkpair (mksym "M1" 175"TH") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym 176"COMMON-LISP" "QUOTE") (mkpair (mknum "-1" "1" "0" "1") (mksym "COMMON-LISP" 177"NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym 178"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 179"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 180, 181 182(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "POPN") (mkpair ( 183mkpair (mksym "M1" "N") (mkpair (mksym "M1" "STK") (mksym "COMMON-LISP" "NIL"))) ( 184mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") ( 185mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" 186"STK") (mkpair (mkpair (mksym "M1" "POPN") (mkpair (mkpair (mksym "ACL2" 187"BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1" 188"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym 189"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "M1" "POP") (mkpair (mksym 190"M1" "STK") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 191mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 192, 193 194(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "UPDATE-NTH") ( 195mkpair (mkpair (mksym "M1" "N") (mkpair (mksym "M1" "V") (mkpair (mksym 196"COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 197"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") (mkpair (mksym "M1" 198"N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 199"CONS") (mkpair (mksym "M1" "V") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 200mkpair (mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (mksym 201"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair ( 202mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "COMMON-LISP" "LIST") ( 203mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "UPDATE-NTH") ( 204mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" 205"QUOTE") (mkpair (mknum "-1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) ( 206mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "M1" 207"V") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "COMMON-LISP" 208"LIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 209"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 210"NIL"))))) 211, 212 213(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "MEMBER") (mkpair ( 214mkpair (mksym "M1" "E") (mkpair (mksym "COMMON-LISP" "LIST") (mksym 215"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 216mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "COMMON-LISP" "LIST") ( 217mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 218mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 219mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" 220"EQUAL") (mkpair (mksym "M1" "E") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 221mkpair (mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) (mksym 222"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 223mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 224"M1" "MEMBER") (mkpair (mksym "M1" "E") (mkpair (mkpair (mksym "COMMON-LISP" 225"CDR") (mkpair (mksym "COMMON-LISP" "LIST") (mksym "COMMON-LISP" "NIL"))) ( 226mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 227"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 228, 229 230(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "INDEX") (mkpair ( 231mkpair (mksym "M1" "E") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) ( 232mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 233"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) ( 234mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") ( 235mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 236mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "E") (mkpair ( 237mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "LST") (mksym 238"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 239"COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" 240"NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym 241"COMMON-LISP" "QUOTE") (mkpair (mknum "1" "1" "0" "1") (mksym "COMMON-LISP" 242"NIL"))) (mkpair (mkpair (mksym "M1" "INDEX") (mkpair (mksym "M1" "E") ( 243mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "LST") (mksym 244"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 245"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) ( 246mksym "COMMON-LISP" "NIL"))))) 247, 248 249(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "SUPPLIEDP") ( 250mkpair (mkpair (mksym "M1" "KEY") (mkpair (mksym "M1" "ARGS") (mksym 251"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 252mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ARGS") (mksym 253"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 254mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 255mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") ( 256mkpair (mksym "M1" "KEY") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 257mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 258mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") ( 259mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "SUPPLIEDP") (mkpair ( 260mksym "M1" "KEY") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair ( 261mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP" 262"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 263"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 264"NIL"))))) 265, 266 267(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "ACTUAL") (mkpair ( 268mkpair (mksym "M1" "KEY") (mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP" 269"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 270"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) ( 271mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 272"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 273"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "KEY") ( 274mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "ARGS") (mksym 275"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 276"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 277mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 278mkpair (mkpair (mksym "M1" "ACTUAL") (mkpair (mksym "M1" "KEY") (mkpair ( 279mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 280mkpair (mksym "M1" "ARGS") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 281"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) ( 282mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 283, 284 285(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "BOUNDP") (mkpair ( 286mkpair (mksym "M1" "VAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" 287"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 288"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) ( 289mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 290"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 291"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "VAR") ( 292mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym 293"COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) ( 294mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 295mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym 296"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "BOUNDP") (mkpair (mksym 297"M1" "VAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" 298"ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 299"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 300"NIL"))))) 301, 302 303(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "BINDING") (mkpair ( 304mkpair (mksym "M1" "VAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" 305"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 306"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) ( 307mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 308"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 309"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "VAR") ( 310mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym 311"COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) ( 312mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 313mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 314mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") ( 315mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym 316"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "BINDING") (mkpair (mksym 317"M1" "VAR") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" 318"ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 319"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 320"NIL"))))) 321, 322 323(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "BIND") (mkpair ( 324mkpair (mksym "M1" "VAR") (mkpair (mksym "M1" "VAL") (mkpair (mksym "M1" 325"ALIST") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 326"IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "M1" 327"ALIST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 328"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" 329"VAR") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "VAL") ( 330mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 331"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 332"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 333mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 334"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 335"COMMON-LISP" "EQUAL") (mkpair (mksym "M1" "VAR") (mkpair (mkpair (mksym 336"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 337mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 338mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") ( 339mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "VAR") ( 340mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "VAL") ( 341mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 342"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 343"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 344mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 345mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym 346"COMMON-LISP" "CAR") (mkpair (mksym "M1" "ALIST") (mksym "COMMON-LISP" "NIL"))) ( 347mkpair (mkpair (mksym "M1" "BIND") (mkpair (mksym "M1" "VAR") (mkpair (mksym 348"M1" "VAL") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" 349"ALIST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 350"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 351"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 352, 353 354(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "U-FIX") (mkpair ( 355mkpair (mksym "M1" "X") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) ( 356mkpair (mkpair (mksym "COMMON-LISP" "MOD") (mkpair (mksym "M1" "X") (mkpair ( 357mkpair (mksym "COMMON-LISP" "EXPT") (mkpair (mkpair (mksym "COMMON-LISP" 358"QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) ( 359mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 360"NIL")))) (mksym "COMMON-LISP" "NIL"))))) 361, 362 363(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "S-FIX") (mkpair ( 364mkpair (mksym "M1" "X") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) ( 365mkpair (mkpair (mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym 366"M1" "TEMP") (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 367mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "<") ( 368mkpair (mksym "M1" "TEMP") (mkpair (mkpair (mksym "COMMON-LISP" "EXPT") ( 369mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") ( 370mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") ( 371mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1" "1" "0" "1") ( 372mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" 373"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 374mkpair (mksym "M1" "TEMP") (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair ( 375mksym "M1" "TEMP") (mkpair (mkpair (mksym "ACL2" "UNARY--") (mkpair (mkpair ( 376mksym "COMMON-LISP" "EXPT") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 377mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 378"M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym 379"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 380"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "MOD") (mkpair (mksym "M1" "X") ( 381mkpair (mkpair (mksym "COMMON-LISP" "EXPT") (mkpair (mkpair (mksym 382"COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym "COMMON-LISP" 383"NIL"))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) (mksym 384"COMMON-LISP" "NIL")))) (mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL")))) ( 385mksym "COMMON-LISP" "NIL"))))) 386, 387 388(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "U-BIG1") (mkpair ( 389mkpair (mksym "M1" "LST") (mkpair (mksym "M1" "ACC") (mksym "COMMON-LISP" 390"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 391"COMMON-LISP" "ENDP") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) ( 392mkpair (mksym "M1" "ACC") (mkpair (mkpair (mksym "M1" "U-BIG1") (mkpair ( 393mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "M1" "LST") (mksym 394"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-+") (mkpair ( 395mkpair (mksym "M1" "U-FIX") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 396mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 397mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "8" "1" "0" "1") (mksym 398"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 399"ACL2" "BINARY-*") (mkpair (mkpair (mksym "COMMON-LISP" "EXPT") (mkpair ( 400mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "2" "1" "0" "1") (mksym 401"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 402mknum "8" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 403"NIL")))) (mkpair (mksym "M1" "ACC") (mksym "COMMON-LISP" "NIL")))) (mksym 404"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 405"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 406, 407 408(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "U-BIG") (mkpair ( 409mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 410"M1" "U-BIG1") (mkpair (mksym "M1" "LST") (mkpair (mkpair (mksym 411"COMMON-LISP" "QUOTE") (mkpair (mknum "0" "1" "0" "1") (mksym "COMMON-LISP" 412"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 413, 414 415(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "S-BIG") (mkpair ( 416mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 417"M1" "S-FIX") (mkpair (mkpair (mksym "M1" "U-BIG") (mkpair (mksym "M1" "LST") ( 418mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BINARY-*") ( 419mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "8" "1" "0" "1") ( 420mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "LEN") (mkpair ( 421mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 422mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 423, 424 425(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NEXTN") (mkpair ( 426mkpair (mksym "M1" "N") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) ( 427mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") ( 428mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 429"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 430"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair ( 431mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "LST") (mksym 432"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "NEXTN") (mkpair (mkpair ( 433mksym "ACL2" "BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 434mkpair (mknum "-1" "1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym 435"M1" "N") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 436"CDR") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym 437"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 438"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 439, 440 441(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "SKIPN") (mkpair ( 442mkpair (mksym "M1" "N") (mkpair (mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) ( 443mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ZP") ( 444mkpair (mksym "M1" "N") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" 445"LST") (mkpair (mkpair (mksym "M1" "SKIPN") (mkpair (mkpair (mksym "ACL2" 446"BINARY-+") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mknum "-1" 447"1" "0" "1") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "M1" "N") (mksym 448"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 449mksym "M1" "LST") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 450mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 451 452]; 453