1open HolKernel Parse boolLib bossLib intSyntax pairSyntax listSyntax stringLib numLib sexp; 2 3val package = 4 implode(map chr (cons 65 (cons 67 (cons 76 (cons 50 nil))))); 5 6val events = [ 7 8(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "RCDP") (mkpair ( 9mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 10"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NULL") (mkpair ( 11mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 12"COMMON-LISP" "NULL") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 13mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 14"COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 15mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 16"COMMON-LISP" "CONSP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 17mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 18mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 19"RCDP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") ( 20mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 21mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 22mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 23"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 24"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NULL") (mkpair ( 25mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 26"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 27"COMMON-LISP" "NULL") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 28mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 29mkpair (mkpair (mksym "ACL2" "<<") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 30mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 31"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 32"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 33mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 34"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 35"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) ( 36mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 37"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 38mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") ( 39mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair ( 40mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 41"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 42"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 43"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 44"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 45, 46 47(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "IFRP") (mkpair ( 48mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 49"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair ( 50mkpair (mksym "ACL2" "RCDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 51"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 52"NOT") (mkpair (mkpair (mksym "ACL2" "RCDP") (mkpair (mksym "ACL2" "X") ( 53mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 54mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") ( 55mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 56mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NULL") ( 57mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 58"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 59"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair ( 60mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 61"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 62"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NULL") (mkpair ( 63mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 64mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 65"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "IFRP") ( 66mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym 67"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 68mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 69mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 70"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 71"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 72"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 73"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 74"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 75"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 76"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 77"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 78, 79 80(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ACL2->RCD") ( 81mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair ( 82mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "IFRP") ( 83mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 84mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") ( 85mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 86"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "X") (mksym 87"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 88mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 89"NIL")))) (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))))) (mksym 90"COMMON-LISP" "NIL"))))) 91, 92 93(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "RCD->ACL2") ( 94mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair ( 95mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "IFRP") ( 96mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 97mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 98mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 99"NIL"))) (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))))) (mksym 100"COMMON-LISP" "NIL"))))) 101, 102 103(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "G-AUX") (mkpair ( 104mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 105"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 106"COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair ( 107mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 108"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 109mkpair (mkpair (mksym "ACL2" "<<") (mkpair (mksym "ACL2" "A") (mkpair (mkpair ( 110mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 111mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 112"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) ( 113mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 114"NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" 115"IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") ( 116mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym 117"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 118mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 119mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 120mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 121"NIL"))) (mkpair (mkpair (mksym "ACL2" "G-AUX") (mkpair (mksym "ACL2" "A") ( 122mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 123"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 124"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 125, 126 127(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "G") (mkpair ( 128mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 129"NIL"))) (mkpair (mkpair (mksym "ACL2" "G-AUX") (mkpair (mksym "ACL2" "A") ( 130mkpair (mkpair (mksym "ACL2" "ACL2->RCD") (mkpair (mksym "ACL2" "X") (mksym 131"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 132"NIL"))))) 133, 134 135(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "S-AUX") (mkpair ( 136mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" 137"R") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 138mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 139"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) ( 140mkpair (mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "R") (mksym 141"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "<<") (mkpair (mksym 142"ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair ( 143mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" 144"NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 145"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 146mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair ( 147mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "A") (mkpair (mksym 148"ACL2" "V") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "R") (mksym 149"COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) ( 150mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 151"COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym 152"COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 153mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 154mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 155mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") ( 156mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "A") ( 157mkpair (mksym "ACL2" "V") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 158mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" 159"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 160"CDR") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (mksym 161"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair ( 162mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "R") (mksym 163"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "S-AUX") (mkpair (mksym 164"ACL2" "A") (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "COMMON-LISP" 165"CDR") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (mksym 166"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 167"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 168, 169 170(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "S") (mkpair ( 171mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" 172"X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "RCD->ACL2") ( 173mkpair (mkpair (mksym "ACL2" "S-AUX") (mkpair (mksym "ACL2" "A") (mkpair ( 174mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2" "ACL2->RCD") (mkpair (mksym 175"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 176mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) 177, 178 179(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "KEYS-AUX") ( 180mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair ( 181mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ENDP") ( 182mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 183mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 184"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair ( 185mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") ( 186mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 187"NIL"))) (mkpair (mkpair (mksym "ACL2" "KEYS-AUX") (mkpair (mkpair (mksym 188"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 189mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 190"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 191, 192 193(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "KEYS") (mkpair ( 194mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 195"ACL2" "KEYS-AUX") (mkpair (mkpair (mksym "ACL2" "ACL2->RCD") (mkpair (mksym 196"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) ( 197mksym "COMMON-LISP" "NIL"))))) 198, 199 200(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "G-SAME-S") (mkpair ( 201mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") ( 202mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym 203"ACL2" "A") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "R") (mksym 204"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" 205"V") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 206, 207 208(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "G-DIFF-S") (mkpair ( 209mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") ( 210mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") ( 211mkpair (mksym "ACL2" "B") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 212"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym 213"ACL2" "G") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "S") ( 214mkpair (mksym "ACL2" "B") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" 215"R") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair ( 216mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" 217"R") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 218"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 219, 220 221(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "G-OF-S-REDUX") (mkpair ( 222mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "G") ( 223mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym 224"ACL2" "B") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "R") (mksym 225"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 226mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") ( 227mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "B") (mksym "COMMON-LISP" 228"NIL")))) (mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2" "G") ( 229mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" 230"NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) ( 231mksym "COMMON-LISP" "NIL")))) 232, 233 234(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "S-SAME-G") (mkpair ( 235mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "S") ( 236mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym 237"ACL2" "A") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 238mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mksym "ACL2" "R") ( 239mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 240, 241 242(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "S-SAME-S") (mkpair ( 243mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "S") ( 244mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "Y") (mkpair (mkpair (mksym 245"ACL2" "S") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "X") (mkpair ( 246mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) ( 247mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "A") (mkpair (mksym 248"ACL2" "Y") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) (mksym 249"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 250, 251 252(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "S-DIFF-S") (mkpair ( 253mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") ( 254mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "A") ( 255mkpair (mksym "ACL2" "B") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 256"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym 257"ACL2" "S") (mkpair (mksym "ACL2" "B") (mkpair (mksym "ACL2" "Y") (mkpair ( 258mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" 259"X") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) (mksym 260"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym 261"ACL2" "A") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "ACL2" "S") ( 262mkpair (mksym "ACL2" "B") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" 263"R") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym 264"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 265"NIL")))) 266, 267 268(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "G-KEYS-RELATIONSHIP") ( 269mkpair (mkpair (mksym "ACL2" "IFF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 270mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "KEYS") (mkpair ( 271mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) ( 272mkpair (mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "A") (mkpair (mksym 273"ACL2" "R") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 274mksym "COMMON-LISP" "NIL")))) 275, 276 277(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "S-KEYS-REDUCTION") ( 278mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" 279"KEYS") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "A") (mkpair ( 280mksym "ACL2" "V") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))))) ( 281mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 282mkpair (mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2" "INSERT") (mkpair ( 283mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "KEYS") (mkpair (mksym "ACL2" 284"R") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mkpair ( 285mkpair (mksym "ACL2" "DROP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair ( 286mksym "ACL2" "KEYS") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) ( 287mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 288"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 289, 290 291(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "KEYS-ARE-ORDERED") ( 292mkpair (mkpair (mksym "ACL2" "ORDEREDP") (mkpair (mkpair (mksym "ACL2" "KEYS") ( 293mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 294"NIL"))) (mksym "COMMON-LISP" "NIL")))) 295, 296 297(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "G-OF-NIL-IS-NIL") ( 298mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "G") ( 299mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 300mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 301"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 302"NIL")))) 303, 304 305(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 306"S-NON-NIL-CANNOT-BE-NIL") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 307mksym "ACL2" "V") (mkpair (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" 308"A") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "R") (mksym 309"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 310"NIL")))) 311, 312 313(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "NON-NIL-IF-G-NON-NIL") ( 314mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "G") ( 315mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" 316"NIL")))) (mkpair (mksym "ACL2" "R") (mksym "COMMON-LISP" "NIL")))) (mksym 317"COMMON-LISP" "NIL")))) 318, 319 320(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 321"S-SAME-G-BACK-CHAINING") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 322mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "V") (mkpair ( 323mkpair (mksym "ACL2" "G") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" 324"R") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair ( 325mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "S") ( 326mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" 327"R") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mksym "ACL2" "R") (mksym 328"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 329"NIL")))) 330, 331 332(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "UPDATE-MACRO") ( 333mkpair (mkpair (mksym "ACL2" "UPDS") (mkpair (mksym "ACL2" "RESULT") (mksym 334"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 335mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "UPDS") (mksym 336"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "RESULT") (mkpair (mkpair (mksym 337"ACL2" "UPDATE-MACRO") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair ( 338mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "UPDS") (mksym 339"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 340"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 341mksym "ACL2" "S") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 342"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 343mksym "ACL2" "UPDS") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 344"COMMON-LISP" "CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair ( 345mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "UPDS") (mksym 346"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 347"COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "RESULT") (mkpair (mkpair (mksym 348"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 349"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 350"NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 351mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 352"COMMON-LISP" "NIL"))))) 353 354]; 355