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