1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
|
(M2::CONSTANT-FOLD-+)
(M2::COMMUTATIVITY2-OF-+)
(M2::COMMUTATIVITY2-OF-*
(6 4 (:REWRITE DEFAULT-*-2))
(6 4 (:REWRITE DEFAULT-*-1))
(4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
)
(M2::PLUS-RIGHT-ID
(4 4 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(3 2 (:REWRITE DEFAULT-+-2))
(3 2 (:REWRITE DEFAULT-+-1))
)
(M2::*-0)
(M2::+-CANCELLATION1)
(M2::STACKS)
(M2::STATES)
(M2::FRAMES)
(M2::STEP-OPENER
(379 379 (:REWRITE DEFAULT-CAR))
(365 67 (:DEFINITION NTH))
(350 70 (:DEFINITION ASSOC-EQUAL))
(307 307 (:REWRITE DEFAULT-CDR))
(164 41 (:REWRITE ZP-OPEN))
(143 93 (:REWRITE DEFAULT-+-2))
(115 93 (:REWRITE DEFAULT-+-1))
(82 82 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(56 8 (:DEFINITION M2::POPN))
(49 45 (:REWRITE DEFAULT-<-2))
(48 8 (:DEFINITION M2::BIND))
(45 45 (:REWRITE DEFAULT-<-1))
(20 4 (:DEFINITION LEN))
(19 19 (:TYPE-PRESCRIPTION M2::STEP))
(19 19 (:TYPE-PRESCRIPTION M2::DO-INST))
(18 6 (:DEFINITION M2::BUILD-CLASS-FIELD-BINDINGS))
(8 4 (:REWRITE DEFAULT-*-2))
(8 4 (:REWRITE DEFAULT-*-1))
(4 4 (:TYPE-PRESCRIPTION LEN))
(4 2 (:REWRITE DEFAULT-UNARY-MINUS))
(2 2 (:REWRITE DEFAULT-COERCE-2))
(2 2 (:REWRITE DEFAULT-COERCE-1))
)
(M2::C+)
(M2::C*)
(M2::C+-REVEALED
(12 10 (:REWRITE DEFAULT-+-2))
(10 10 (:REWRITE DEFAULT-<-2))
(10 10 (:REWRITE DEFAULT-<-1))
(10 10 (:REWRITE DEFAULT-+-1))
(3 3 (:REWRITE ZP-OPEN))
(2 2 (:REWRITE FOLD-CONSTS-IN-+))
)
(M2::C*-REVEALED
(10 7 (:REWRITE DEFAULT-+-2))
(9 9 (:REWRITE DEFAULT-*-2))
(9 9 (:REWRITE DEFAULT-*-1))
(7 7 (:REWRITE DEFAULT-<-2))
(7 7 (:REWRITE DEFAULT-<-1))
(7 7 (:REWRITE DEFAULT-+-1))
(3 3 (:REWRITE ZP-OPEN))
)
(M2::M2-C+
(182 14 (:REWRITE M2::STEP-OPENER))
(168 14 (:DEFINITION M2::NEXT-INST))
(126 14 (:DEFINITION NTH))
(92 29 (:REWRITE ZP-OPEN))
(38 33 (:REWRITE DEFAULT-+-2))
(33 33 (:REWRITE DEFAULT-+-1))
(30 27 (:REWRITE DEFAULT-<-2))
(28 28 (:DEFINITION M2::TOP-FRAME))
(27 27 (:REWRITE DEFAULT-<-1))
(14 14 (:REWRITE DEFAULT-CDR))
(14 14 (:REWRITE DEFAULT-CAR))
)
(M2::M2-+
(56 3 (:DEFINITION M2::M2))
(39 3 (:REWRITE M2::STEP-OPENER))
(36 3 (:DEFINITION M2::NEXT-INST))
(27 3 (:DEFINITION NTH))
(18 6 (:REWRITE ZP-OPEN))
(7 7 (:REWRITE DEFAULT-+-2))
(7 7 (:REWRITE DEFAULT-+-1))
(6 6 (:DEFINITION M2::TOP-FRAME))
(4 4 (:REWRITE DEFAULT-<-2))
(4 4 (:REWRITE DEFAULT-<-1))
(3 3 (:REWRITE DEFAULT-CDR))
(3 3 (:REWRITE DEFAULT-CAR))
(1 1 (:REWRITE FOLD-CONSTS-IN-+))
(1 1 (:REWRITE M2::CONSTANT-FOLD-+))
)
(M2::M2-OPENER
(65 5 (:REWRITE M2::STEP-OPENER))
(60 5 (:DEFINITION M2::NEXT-INST))
(45 5 (:DEFINITION NTH))
(22 7 (:REWRITE ZP-OPEN))
(10 10 (:DEFINITION M2::TOP-FRAME))
(8 8 (:REWRITE DEFAULT-+-2))
(8 8 (:REWRITE DEFAULT-+-1))
(6 6 (:REWRITE DEFAULT-<-2))
(6 6 (:REWRITE DEFAULT-<-1))
(5 5 (:REWRITE DEFAULT-CDR))
(5 5 (:REWRITE DEFAULT-CAR))
)
(M2::ASSOC-EQUAL-BIND
(229 165 (:REWRITE DEFAULT-CAR))
(81 67 (:REWRITE DEFAULT-CDR))
)
(M2::BIND-FORMALS-CONS
(3 3 (:REWRITE DEFAULT-CDR))
(3 3 (:REWRITE DEFAULT-CAR))
)
(M2::POPN-OPENER
(5 5 (:REWRITE DEFAULT-+-2))
(5 5 (:REWRITE DEFAULT-+-1))
(2 2 (:REWRITE ZP-OPEN))
(1 1 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE DEFAULT-<-1))
)
(M2::FACT)
(M2::FACT-METHOD)
(M2::MATH-CLASS)
(M2::FACT-CLOCK)
(M2::EXAMPLE1)
(M2::FACT-CLOCK-REVEALED
(29 20 (:REWRITE DEFAULT-+-2))
(23 20 (:REWRITE DEFAULT-+-1))
(5 5 (:REWRITE DEFAULT-*-2))
(5 5 (:REWRITE DEFAULT-*-1))
(3 3 (:REWRITE ZP-OPEN))
(3 3 (:REWRITE DEFAULT-<-2))
(3 3 (:REWRITE DEFAULT-<-1))
)
(M2::EXAMPLE2-HINT)
(M2::EXAMPLE2
(84 8 (:DEFINITION M2::C+))
(53 40 (:REWRITE DEFAULT-+-2))
(40 40 (:REWRITE DEFAULT-+-1))
(34 34 (:REWRITE DEFAULT-CAR))
(21 17 (:REWRITE DEFAULT-<-2))
(17 17 (:REWRITE DEFAULT-<-1))
(16 16 (:REWRITE DEFAULT-CDR))
(12 4 (:REWRITE M2::CONSTANT-FOLD-+))
(10 5 (:REWRITE DEFAULT-*-2))
(5 5 (:TYPE-PRESCRIPTION M2::FACT))
(5 5 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(5 5 (:REWRITE DEFAULT-*-1))
(3 3 (:TYPE-PRESCRIPTION M2::EXAMPLE2-HINT))
)
(M2::XINCREMENT-METHOD)
(M2::XINCREMENT-CLOCK)
(M2::INBOX-METHOD)
(M2::POINT-CLASS)
(M2::SETCOLOR-METHOD)
(M2::SETCOLOR-CLOCK)
(M2::SETCOLORBOX-METHOD)
(M2::COLOREDPOINT-CLASS)
(M2::EXAMPLE3)
(M2::INSTANCE-OF)
(M2::POINT.X)
(M2::POINT.Y)
(M2::INBOX-CLOCK)
(M2::INBOX)
(M2::SETCOLORBOX-CLOCK)
(M2::SETCOLORBOX-HEAP)
(M2::EXAMPLE4
(9032 8700 (:REWRITE DEFAULT-CAR))
(6386 6054 (:REWRITE DEFAULT-CDR))
(2046 330 (:DEFINITION NTH))
(792 198 (:REWRITE ZP-OPEN))
(780 533 (:REWRITE DEFAULT-<-2))
(780 533 (:REWRITE DEFAULT-<-1))
(743 743 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(482 387 (:REWRITE DEFAULT-+-2))
(453 387 (:REWRITE DEFAULT-+-1))
(176 88 (:REWRITE DEFAULT-UNARY-MINUS))
(40 40 (:TYPE-PRESCRIPTION M2::REVERSE))
)
(M2::HACKISH-LEMMA1
(180 36 (:DEFINITION ASSOC-EQUAL))
(120 120 (:REWRITE DEFAULT-CAR))
(84 84 (:REWRITE DEFAULT-CDR))
(13 13 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(12 6 (:REWRITE DEFAULT-<-2))
(12 6 (:REWRITE DEFAULT-<-1))
(2 1 (:REWRITE DEFAULT-+-2))
(1 1 (:REWRITE DEFAULT-+-1))
)
(M2::HACKISH-LEMMA2
(240 48 (:DEFINITION ASSOC-EQUAL))
(160 160 (:REWRITE DEFAULT-CAR))
(112 112 (:REWRITE DEFAULT-CDR))
(17 17 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(16 8 (:REWRITE DEFAULT-<-2))
(16 8 (:REWRITE DEFAULT-<-1))
(2 1 (:REWRITE DEFAULT-+-2))
(1 1 (:REWRITE DEFAULT-+-1))
)
(M2::EXAMPLE5
(1339 1339 (:REWRITE DEFAULT-CAR))
(859 859 (:REWRITE DEFAULT-CDR))
(632 134 (:DEFINITION NTH))
(316 184 (:REWRITE DEFAULT-+-2))
(216 36 (:DEFINITION M2::BIND))
(208 52 (:REWRITE ZP-OPEN))
(184 184 (:REWRITE DEFAULT-+-1))
(52 52 (:REWRITE DEFAULT-<-2))
(52 52 (:REWRITE DEFAULT-<-1))
(48 48 (:TYPE-PRESCRIPTION M2::REVERSE))
(20 20 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
)
(M2::SETCOLORBOX-HEAP-PROPERTY
(296 296 (:REWRITE DEFAULT-CAR))
(270 263 (:REWRITE DEFAULT-CDR))
(214 42 (:DEFINITION ASSOC-EQUAL))
(156 26 (:DEFINITION M2::BIND))
)
|
