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
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
|
(ADE::1-BIT-<*)
(ADE::1-BIT-<*$DESTRUCTURE)
(ADE::NOT-PRIMP-1-BIT-<)
(ADE::1-BIT-<$NETLIST)
(ADE::1-BIT-<&)
(ADE::CHECK-1-BIT-<$NETLIST)
(ADE::1-BIT-<$VALUE
(75 33 (:REWRITE ADE::F-GATES=B-GATES))
(45 45 (:REWRITE DEFAULT-CAR))
(32 32 (:REWRITE DEFAULT-CDR))
(30 6 (:DEFINITION ADE::DELETE-TO-EQ))
(24 24 (:TYPE-PRESCRIPTION BOOLEANP))
(9 9 (:TYPE-PRESCRIPTION ADE::F-XNOR))
(9 9 (:TYPE-PRESCRIPTION ADE::F-AND3))
)
(ADE::FV-<
(1 1 (:TYPE-PRESCRIPTION ADE::F-XNOR))
)
(ADE::3V-FIX-FV-<
(114 30 (:REWRITE ADE::F-GATES=B-GATES))
(48 48 (:TYPE-PRESCRIPTION BOOLEANP))
(24 24 (:REWRITE DEFAULT-CAR))
(22 11 (:TYPE-PRESCRIPTION ADE::3V-FIX))
(18 18 (:TYPE-PRESCRIPTION ADE::F-XNOR))
(18 18 (:TYPE-PRESCRIPTION ADE::F-AND3))
(12 12 (:REWRITE DEFAULT-CDR))
)
(ADE::FV-<-OF-F-BUF-CANCELED
(378 109 (:REWRITE ADE::F-GATES=B-GATES))
(176 176 (:TYPE-PRESCRIPTION BOOLEANP))
(68 68 (:REWRITE DEFAULT-CAR))
(48 48 (:TYPE-PRESCRIPTION ADE::F-XNOR))
(48 48 (:TYPE-PRESCRIPTION ADE::F-AND3))
(36 12 (:REWRITE ADE::F-BUF-OF-NOT-BOOLEANP))
(34 34 (:REWRITE DEFAULT-CDR))
(9 9 (:TYPE-PRESCRIPTION ADE::F-AND))
(8 4 (:REWRITE ADE::BOOLEANP-OF-F-BUF))
(3 3 (:REWRITE ADE::3VP-F-OR))
)
(ADE::FV-<-OF-V-THREEFIX-CANCELED-1
(4527 1986 (:REWRITE ADE::F-GATES=B-GATES))
(1367 1349 (:REWRITE DEFAULT-CAR))
(971 962 (:REWRITE DEFAULT-CDR))
(642 214 (:REWRITE ADE::V-THREEFIX-BVP))
(428 428 (:TYPE-PRESCRIPTION ADE::BVP))
(2 2 (:REWRITE ADE::3VP-F-OR))
)
(ADE::FV-<-OF-V-THREEFIX-CANCELED-2
(8881 3095 (:REWRITE ADE::F-GATES=B-GATES))
(894 298 (:REWRITE ADE::V-THREEFIX-BVP))
(659 659 (:TYPE-PRESCRIPTION ADE::V-THREEFIX))
(596 596 (:TYPE-PRESCRIPTION ADE::BVP))
(424 106 (:REWRITE ADE::CAR-V-THREEFIX))
(240 240 (:TYPE-PRESCRIPTION ADE::3V-FIX))
(37 37 (:TYPE-PRESCRIPTION ADE::F-AND))
(22 2 (:REWRITE ADE::F-BUF-DELETE-LEMMAS-1))
(4 4 (:REWRITE ADE::3VP-F-OR))
)
(ADE::V-<)
(ADE::BOOLEANP-V-<)
(ADE::FV-<=V-<
(342 342 (:REWRITE DEFAULT-CAR))
(174 174 (:REWRITE DEFAULT-CDR))
(159 159 (:TYPE-PRESCRIPTION ADE::F-NOT))
(99 99 (:TYPE-PRESCRIPTION ADE::F-AND3))
(30 30 (:TYPE-PRESCRIPTION ADE::F-XNOR))
(30 10 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
(13 13 (:REWRITE ADE::F-AND-REWRITE))
(4 4 (:TYPE-PRESCRIPTION BOOLEANP-OF-BOOL-FIX))
(1 1 (:REWRITE ADE::F-OR-REWRITE))
(1 1 (:REWRITE ADE::3VP-F-OR))
)
(ADE::V-<-LEMMA
(160 160 (:REWRITE DEFAULT-CAR))
(92 32 (:REWRITE BOOL-FIX-WHEN-BOOLEANP))
(72 72 (:REWRITE DEFAULT-CDR))
(56 56 (:TYPE-PRESCRIPTION BOOLEANP))
(24 8 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
)
(ADE::V-<-APPEND
(1492 1030 (:REWRITE DEFAULT-CDR))
(1487 1319 (:REWRITE DEFAULT-CAR))
(488 245 (:REWRITE DEFAULT-+-2))
(486 243 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(324 108 (:REWRITE CAR-OF-APPEND))
(285 95 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
(245 245 (:REWRITE DEFAULT-+-1))
(243 243 (:TYPE-PRESCRIPTION TRUE-LISTP))
(243 243 (:TYPE-PRESCRIPTION BINARY-APPEND))
(81 81 (:REWRITE CONSP-OF-APPEND))
(80 80 (:LINEAR LEN-WHEN-PREFIXP))
(54 54 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
(40 40 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
)
(ADE::V-<-CORRECT-INDUCT)
(ADE::V-<-CORRECT-1
(875 527 (:REWRITE DEFAULT-CDR))
(776 404 (:REWRITE DEFAULT-CAR))
(652 202 (:REWRITE ADE::V-<-LEMMA))
(539 272 (:REWRITE DEFAULT-+-2))
(340 172 (:REWRITE DEFAULT-*-2))
(300 50 (:REWRITE BOOL-FIX-WHEN-BOOLEANP))
(272 272 (:REWRITE DEFAULT-+-1))
(240 16 (:DEFINITION BINARY-APPEND))
(172 172 (:REWRITE DEFAULT-*-1))
(132 44 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
(128 32 (:REWRITE APPEND-WHEN-NOT-CONSP))
(112 16 (:REWRITE CAR-OF-APPEND))
(101 101 (:REWRITE REV-WHEN-NOT-CONSP))
(100 100 (:LINEAR LEN-WHEN-PREFIXP))
(51 24 (:REWRITE DEFAULT-<-1))
(50 50 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(49 24 (:REWRITE DEFAULT-<-2))
(32 8 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
(20 10 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(10 10 (:TYPE-PRESCRIPTION BINARY-APPEND))
)
(ADE::V-<-CORRECT-2
(1102 691 (:REWRITE DEFAULT-CDR))
(968 527 (:REWRITE DEFAULT-CAR))
(745 250 (:REWRITE ADE::V-<-LEMMA))
(697 349 (:REWRITE DEFAULT-+-2))
(464 232 (:REWRITE DEFAULT-*-2))
(427 7 (:REWRITE ADE::V-<-CORRECT-1))
(349 349 (:REWRITE DEFAULT-+-1))
(330 55 (:REWRITE BOOL-FIX-WHEN-BOOLEANP))
(300 20 (:DEFINITION BINARY-APPEND))
(232 232 (:REWRITE DEFAULT-*-1))
(157 40 (:REWRITE APPEND-WHEN-NOT-CONSP))
(147 49 (:REWRITE ADE::BOOL-FIX-CAR-X=X))
(140 20 (:REWRITE CAR-OF-APPEND))
(132 132 (:LINEAR LEN-WHEN-PREFIXP))
(125 125 (:REWRITE REV-WHEN-NOT-CONSP))
(90 90 (:LINEAR ADE::V-<-CORRECT-1))
(79 38 (:REWRITE DEFAULT-<-2))
(75 38 (:REWRITE DEFAULT-<-1))
(66 66 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(40 10 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
(28 14 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
(14 14 (:TYPE-PRESCRIPTION BINARY-APPEND))
)
(ADE::V-<-BODY)
(ADE::V-<*
(10 5 (:TYPE-PRESCRIPTION ADE::CONSP-SIS))
(5 5 (:TYPE-PRESCRIPTION POSP))
)
(ADE::V-<*$DESTRUCTURE
(120 60 (:TYPE-PRESCRIPTION ADE::CONSP-SIS))
(66 12 (:REWRITE APPEND-WHEN-NOT-CONSP))
(60 60 (:TYPE-PRESCRIPTION POSP))
(60 6 (:DEFINITION BINARY-APPEND))
(24 6 (:DEFINITION ADE::V-<-BODY))
(16 16 (:REWRITE DEFAULT-CDR))
(11 11 (:REWRITE DEFAULT-CAR))
(6 6 (:REWRITE ZP-OPEN))
(6 6 (:REWRITE DEFAULT-+-2))
(6 6 (:REWRITE DEFAULT-+-1))
)
(ADE::NOT-PRIMP-V-<)
(ADE::V-<$NETLIST)
(ADE::V-<&)
(ADE::CHECK-V-<$NETLIST-64)
(ADE::V-<-BODY-INDUCT)
(ADE::V-<-BODY$VALUE
(236 222 (:REWRITE DEFAULT-+-2))
(222 222 (:REWRITE DEFAULT-+-1))
(211 95 (:REWRITE ADE::F-GATES=B-GATES))
(185 137 (:REWRITE DEFAULT-CDR))
(165 112 (:REWRITE DEFAULT-CAR))
(70 70 (:TYPE-PRESCRIPTION BOOLEANP))
(61 16 (:REWRITE ZP-OPEN))
(56 28 (:TYPE-PRESCRIPTION ADE::CONSP-SIS))
(40 10 (:REWRITE ADE::CONSP-ASSOC-EQ-VALUES))
(36 7 (:REWRITE ADE::FV-<=V-<))
(28 28 (:TYPE-PRESCRIPTION ADE::SIS))
(28 28 (:TYPE-PRESCRIPTION POSP))
(27 21 (:TYPE-PRESCRIPTION ADE::F-XNOR))
(26 2 (:DEFINITION MEMBER-EQUAL))
(21 21 (:TYPE-PRESCRIPTION ADE::F-AND3))
(18 18 (:REWRITE DEFAULT-<-2))
(18 18 (:REWRITE DEFAULT-<-1))
(14 2 (:REWRITE ADE::UNBOUND-IN-BODY-SE-OCC))
(12 12 (:TYPE-PRESCRIPTION ADE::SE))
(12 6 (:REWRITE ADE::LEN-SIS))
(12 2 (:DEFINITION BINARY-APPEND))
(10 10 (:TYPE-PRESCRIPTION PAIRLIS$))
(8 8 (:LINEAR LEN-WHEN-PREFIXP))
(8 2 (:REWRITE ADE::UNBOUND-IN-BODY-ATOM))
(8 2 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
(6 6 (:REWRITE ADE::NFIX-OF-NAT))
(4 4 (:TYPE-PRESCRIPTION ADE::UNBOUND-IN-BODY))
(4 4 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
(4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(2 2 (:REWRITE DEFAULT-SYMBOL-NAME))
)
(ADE::V-<-BODY$VALUE-M=0
(45 1 (:DEFINITION ADE::SE-OCC))
(28 5 (:REWRITE ADE::SINGLETON-ASSOC-EQ-VALUES))
(25 25 (:TYPE-PRESCRIPTION ADE::FV-<))
(23 5 (:REWRITE ADE::ASSOC-EQ-VALUES-ATOM))
(12 6 (:TYPE-PRESCRIPTION ADE::CONSP-SIS))
(11 1 (:DEFINITION PAIRLIS$))
(9 9 (:TYPE-PRESCRIPTION LEN))
(8 5 (:REWRITE DEFAULT-CDR))
(7 4 (:REWRITE DEFAULT-CAR))
(6 6 (:TYPE-PRESCRIPTION ADE::SIS))
(6 6 (:TYPE-PRESCRIPTION ADE::SE))
(6 6 (:TYPE-PRESCRIPTION POSP))
(6 1 (:DEFINITION BINARY-APPEND))
(5 5 (:TYPE-PRESCRIPTION PAIRLIS$))
(5 2 (:REWRITE APPEND-WHEN-NOT-CONSP))
(5 1 (:DEFINITION LEN))
(4 4 (:LINEAR LEN-WHEN-PREFIXP))
(4 3 (:REWRITE DEFAULT-+-2))
(4 2 (:REWRITE ADE::LEN-SIS))
(4 2 (:REWRITE ADE::FV-<=V-<))
(4 1 (:DEFINITION ADE::V-<-BODY))
(3 3 (:REWRITE DEFAULT-+-1))
(2 2 (:TYPE-PRESCRIPTION ADE::V-<-BODY))
(2 2 (:TYPE-PRESCRIPTION BOOLEANP))
(2 2 (:REWRITE ADE::NFIX-OF-NAT))
(2 2 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(1 1 (:REWRITE ZP-OPEN))
(1 1 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE DEFAULT-<-1))
)
(ADE::V-<$VALUE
(63 33 (:REWRITE DEFAULT-+-2))
(42 3 (:DEFINITION ADE::V-<-BODY))
(33 33 (:REWRITE DEFAULT-+-1))
(30 6 (:DEFINITION BINARY-APPEND))
(30 4 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-2))
(30 4 (:REWRITE ADE::DISJOINT-SIS-SAME-SYM-1))
(30 2 (:DEFINITION ATOM))
(24 3 (:REWRITE ZP-OPEN))
(15 8 (:REWRITE DEFAULT-<-2))
(14 14 (:TYPE-PRESCRIPTION PAIRLIS$))
(14 1 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-SE-OCC))
(13 3 (:REWRITE PREFIXP-WHEN-PREFIXP))
(12 4 (:REWRITE ADE::BV-IS-TRUE-LIST))
(12 3 (:REWRITE ADE::NOT-EQUAL-WITH-SI-OF-DIFF-SYMBOL . 2))
(11 1 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-CONS))
(11 1 (:DEFINITION MEMBER-EQUAL))
(10 10 (:TYPE-PRESCRIPTION ADE::BVP))
(9 8 (:REWRITE DEFAULT-<-1))
(8 8 (:LINEAR LEN-WHEN-PREFIXP))
(8 2 (:DEFINITION TRUE-LISTP))
(6 6 (:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE))
(5 2 (:REWRITE ADE::UNBOUND-IN-BODY-ATOM))
(4 4 (:TYPE-PRESCRIPTION ADE::UNBOUND-IN-BODY))
(4 4 (:LINEAR ADE::A-HELPFUL-LEMMA-FOR-TREE-INDUCTIONS))
(4 2 (:REWRITE ADE::FV-<=V-<))
(3 3 (:REWRITE PREFIXP-TRANSITIVE . 2))
(3 3 (:REWRITE PREFIXP-TRANSITIVE . 1))
(3 3 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 2))
(3 3 (:REWRITE PREFIXP-ONE-WAY-OR-ANOTHER . 1))
(3 3 (:REWRITE DEFAULT-SYMBOL-NAME))
(2 2 (:REWRITE TAKE-WHEN-ATOM))
(2 2 (:REWRITE PREFIXP-WHEN-NOT-CONSP-RIGHT))
(2 2 (:REWRITE PREFIXP-WHEN-NOT-CONSP-LEFT))
(2 2 (:REWRITE ADE::NTHCDR-OF-POS-CONST-IDX))
(2 2 (:REWRITE ADE::ALL-UNBOUND-IN-BODY-ATOM-NAMES))
(1 1 (:TYPE-PRESCRIPTION ADE::ALL-UNBOUND-IN-BODY))
)
|
