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" "FOO") (mkpair ( 9mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym 10"COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "X") ( 11mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) 12, 13 14(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "FOO-PROP") (mkpair ( 15mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "COMMON-LISP" 16"CAR") (mkpair (mkpair (mksym "ACL2" "FOO") (mkpair (mksym "ACL2" "X") (mksym 17"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 18"X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 19, 20 21(mkpair (mksym "ACL2" "MUTUAL-RECURSION") (mkpair (mkpair (mksym 22"COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "BAR") (mkpair (mkpair (mksym 23"ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP" 24"IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "X") ( 25mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BAR") (mkpair ( 26mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 27"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 28"X") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 29mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "H") (mkpair ( 30mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mksym "ACL2" 31"X") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL")))) 32 33]; 34