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" "<<") (mkpair ( 9mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" 10"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 11"ACL2" "LEXORDER") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") ( 12mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") ( 13mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mksym "ACL2" "X") ( 14mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 15"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 16"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 17mksym "COMMON-LISP" "NIL"))))) 18, 19 20(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "<<-IRREFLEXIVE") ( 21mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "<<") ( 22mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 23"NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) 24, 25 26(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "<<-TRANSITIVE") ( 27mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" 28"IF") (mkpair (mkpair (mksym "ACL2" "<<") (mkpair (mksym "ACL2" "X") (mkpair ( 29mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 30"ACL2" "<<") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "Z") (mksym 31"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 32mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 33"NIL"))))) (mkpair (mkpair (mksym "ACL2" "<<") (mkpair (mksym "ACL2" "X") ( 34mkpair (mksym "ACL2" "Z") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 35"NIL")))) (mksym "COMMON-LISP" "NIL")))) 36, 37 38(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "<<-ASYMMETRIC") ( 39mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "<<") ( 40mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" 41"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym 42"ACL2" "<<") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "X") (mksym 43"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 44"NIL")))) (mksym "COMMON-LISP" "NIL")))) 45, 46 47(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "<<-TRICHOTOMY") ( 48mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" 49"IF") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym 50"ACL2" "<<") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "X") (mksym 51"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 52"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair ( 53mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) ( 54mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 55mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 56"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "<<") (mkpair (mksym 57"ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym 58"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 59, 60 61(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "<<-IMPLIES-LEXORDER") ( 62mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "ACL2" "<<") ( 63mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" 64"NIL")))) (mkpair (mkpair (mksym "ACL2" "LEXORDER") (mkpair (mksym "ACL2" "X") ( 65mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 66"NIL")))) (mksym "COMMON-LISP" "NIL")))) 67 68]; 69