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 "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 9"RANGE-TRANSITION-RELATION") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 10mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") ( 11mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair ( 12mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym 13"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) ( 14mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 15mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") ( 16mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" 17"NIL"))))) (mkpair (mkpair (mksym "ACL2" "CIRCUIT-MODELP") (mkpair (mksym 18"ACL2" "M") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 19"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 20"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 21"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 22"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 23"ACL2" "MEMBERP") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" 24"G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" 25"STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym 26"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 27"NIL")))) (mksym "COMMON-LISP" "NIL")))) 28, 29 30(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 31"SUBSET-IMPLIES-MEMBERP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 32mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") ( 33mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" 34"NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") ( 35mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 36mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 37"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 38"ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "Y") ( 39mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 40"COMMON-LISP" "NIL")))) 41, 42 43(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 44"INITIAL-STATE-IS-STATE") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 45mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 46"CIRCUIT-MODELP") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL"))) ( 47mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S0") (mkpair ( 48mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 49mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) ( 50mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 51"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 52"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 53mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "S0") (mkpair ( 54mkpair (mksym "ACL2" "G") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 55mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 56mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 57mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 58, 59 60(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBERP-SET-UNION") ( 61mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" 62"MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" 63"SET-UNION") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym 64"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 65"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym 66"ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 67mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym 68"ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 69"MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "Y") (mksym 70"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 71"NIL")))) (mksym "COMMON-LISP" "NIL")))) 72, 73 74(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "MEMBERP-SET-INTERSECT") ( 75mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" 76"MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" 77"SET-INTERSECT") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym 78"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 79"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym 80"ACL2" "A") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 81mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym 82"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 83"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 84"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 85"NIL")))) (mksym "COMMON-LISP" "NIL")))) 86, 87 88(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 89"SUBSET-PRESERVES-MEMBERP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 90mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") ( 91mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" 92"NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") ( 93mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 94mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 95"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 96"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 97mksym "ACL2" "A") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) ( 98mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") ( 99mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym 100"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 101, 102 103(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 104"SET-EQUAL-IMPLIES-EQUAL-MEMBERP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 105mkpair (mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair ( 106mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 107"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair ( 108mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym 109"ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 110"MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mksym "ACL2" "Y") (mksym 111"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 112"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") (mksym "COMMON-LISP" 113"NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 114"COMMON-LISP" "NIL")))) 115, 116 117(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "BISIM-LEMMA-1-LEMMA") ( 118mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" 119"CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "M") ( 120mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair (mksym "ACL2" 121"VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 122"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 123mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair ( 124mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym "ACL2" "P") (mkpair (mksym 125"ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") ( 126mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 127mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") (mkpair (mkpair (mksym 128"ACL2" "SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair ( 129mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) ( 130mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mksym 131"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 132"NIL")))) (mksym "COMMON-LISP" "NIL")))) 133, 134 135(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "BISIM-LEMMA-1") ( 136mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" 137"IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "A") ( 138mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 139mksym "ACL2" "CIRCUIT-BISIM") (mkpair (mksym "ACL2" "P") (mkpair (mksym 140"ACL2" "M") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "N") (mkpair ( 141mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))))) (mkpair (mkpair (mksym 142"COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 143"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 144"COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 145mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym 146"ACL2" "P") (mkpair (mksym "ACL2" "M") (mksym "COMMON-LISP" "NIL")))) (mksym 147"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 148mksym "ACL2" "A") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym 149"ACL2" "Q") (mkpair (mksym "ACL2" "N") (mksym "COMMON-LISP" "NIL")))) (mksym 150"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 151"NIL")))) (mksym "COMMON-LISP" "NIL")))) 152 153]; 154