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