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