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
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
|
(|16P|)
(|16_0|)
(16_+)
(16_-)
(S16_*)
(16_*)
(|16_1|)
(16_NORM)
(16_DOT)
(16_CONJUGATE)
(16-VECTOR-CLOSURE
(301 301 (:REWRITE DEFAULT-CDR))
(301 301 (:REWRITE DEFAULT-CAR))
(16 16 (:REWRITE DEFAULT-UNARY-MINUS))
(16 16 (:REWRITE DEFAULT-+-2))
(16 16 (:REWRITE DEFAULT-+-1))
(16 16 (:REWRITE DEFAULT-*-2))
(16 16 (:REWRITE DEFAULT-*-1))
)
(ASSOCIATIVITY-OF-16_+
(267 267 (:REWRITE DEFAULT-CDR))
(267 267 (:REWRITE DEFAULT-CAR))
(128 128 (:REWRITE DEFAULT-+-2))
(128 128 (:REWRITE DEFAULT-+-1))
(48 48 (:REWRITE FOLD-CONSTS-IN-+))
)
(COMMUTATIVITY-OF-16_+
(158 158 (:REWRITE DEFAULT-CDR))
(158 158 (:REWRITE DEFAULT-CAR))
(48 48 (:REWRITE DEFAULT-+-2))
(48 48 (:REWRITE DEFAULT-+-1))
)
(UNICITY-OF-16_0
(64 64 (:REWRITE DEFAULT-CDR))
(64 64 (:REWRITE DEFAULT-CAR))
(16 16 (:REWRITE DEFAULT-+-2))
(16 16 (:REWRITE DEFAULT-+-1))
)
(INVERSE-OF-16_+
(94 94 (:REWRITE DEFAULT-CDR))
(94 94 (:REWRITE DEFAULT-CAR))
(16 16 (:REWRITE DEFAULT-UNARY-MINUS))
(16 16 (:REWRITE DEFAULT-+-2))
(16 16 (:REWRITE DEFAULT-+-1))
)
(ASSOCIATIVITY-OF-S16_*
(97 97 (:REWRITE DEFAULT-*-2))
(97 97 (:REWRITE DEFAULT-*-1))
(94 94 (:REWRITE DEFAULT-CDR))
(94 94 (:REWRITE DEFAULT-CAR))
(48 48 (:REWRITE FOLD-CONSTS-IN-*))
)
(UNICITY-OF-SCALAR16-1
(64 64 (:REWRITE DEFAULT-CDR))
(64 64 (:REWRITE DEFAULT-CAR))
(16 16 (:REWRITE DEFAULT-*-2))
(16 16 (:REWRITE DEFAULT-*-1))
)
(DISTRIBUTIVITY-S16_*-SCALAR-+
(128 128 (:REWRITE DEFAULT-*-2))
(128 128 (:REWRITE DEFAULT-*-1))
(124 124 (:REWRITE DEFAULT-CDR))
(124 124 (:REWRITE DEFAULT-CAR))
(33 33 (:REWRITE DEFAULT-+-2))
(33 33 (:REWRITE DEFAULT-+-1))
)
(DISTRIBUTIVITY-S16_*-16_+
(203 203 (:REWRITE DEFAULT-CDR))
(203 203 (:REWRITE DEFAULT-CAR))
(80 80 (:REWRITE DEFAULT-*-2))
(80 80 (:REWRITE DEFAULT-*-1))
(48 48 (:REWRITE DEFAULT-+-2))
(48 48 (:REWRITE DEFAULT-+-1))
)
(16_1&16_*-CLOSURE
(10659 3101 (:REWRITE DEFAULT-+-2))
(3865 3101 (:REWRITE DEFAULT-+-1))
(2527 2527 (:REWRITE FOLD-CONSTS-IN-+))
(1109 698 (:REWRITE DEFAULT-CDR))
(1109 698 (:REWRITE DEFAULT-CAR))
(683 464 (:REWRITE DEFAULT-UNARY-MINUS))
(448 448 (:REWRITE DEFAULT-*-2))
(448 448 (:REWRITE DEFAULT-*-1))
)
(NOT-16_1=16_0)
(LEFT-DISTRIBUTIVITY-16_*_16_+
(164776 26393 (:REWRITE DEFAULT-+-2))
(150439 139262 (:TYPE-PRESCRIPTION |x < y => 0 < -x+y|))
(33117 26393 (:REWRITE DEFAULT-+-1))
(23973 23973 (:REWRITE FOLD-CONSTS-IN-+))
(13594 13594 (:TYPE-PRESCRIPTION |x < y => 0 < y-x|))
(6038 3568 (:REWRITE DEFAULT-*-2))
(3862 2022 (:REWRITE DEFAULT-CDR))
(3862 2022 (:REWRITE DEFAULT-CAR))
(3771 2298 (:REWRITE DEFAULT-UNARY-MINUS))
(3694 3568 (:REWRITE DEFAULT-*-1))
(1536 1536 (:REWRITE FOLD-CONSTS-IN-*))
)
(RIGHT-DISTRIBUTIVITY-16_*_16_+
(164810 26427 (:REWRITE DEFAULT-+-2))
(150284 139107 (:TYPE-PRESCRIPTION |x < y => 0 < -x+y|))
(33151 26427 (:REWRITE DEFAULT-+-1))
(23973 23973 (:REWRITE FOLD-CONSTS-IN-+))
(13439 13439 (:TYPE-PRESCRIPTION |x < y => 0 < y-x|))
(5974 3600 (:REWRITE DEFAULT-*-2))
(3786 2022 (:REWRITE DEFAULT-CDR))
(3786 2022 (:REWRITE DEFAULT-CAR))
(3781 2328 (:REWRITE DEFAULT-UNARY-MINUS))
(3684 3600 (:REWRITE DEFAULT-*-1))
(1536 1536 (:REWRITE FOLD-CONSTS-IN-*))
)
(UNICITY-OF-16_1
(527 527 (:REWRITE DEFAULT-CDR))
(527 527 (:REWRITE DEFAULT-CAR))
(288 288 (:REWRITE DEFAULT-*-2))
(288 288 (:REWRITE DEFAULT-*-1))
(207 207 (:REWRITE DEFAULT-+-2))
(207 207 (:REWRITE DEFAULT-+-1))
(52 52 (:REWRITE DEFAULT-UNARY-MINUS))
)
(REALP>=0-16_NORM
(2266 370 (:REWRITE DEFAULT-+-2))
(916 370 (:REWRITE DEFAULT-+-1))
(312 312 (:REWRITE FOLD-CONSTS-IN-+))
(79 79 (:REWRITE DEFAULT-CDR))
(79 79 (:REWRITE DEFAULT-CAR))
(32 32 (:REWRITE DEFAULT-*-2))
(32 32 (:REWRITE DEFAULT-*-1))
(17 1 (:REWRITE DEFAULT-<-1))
(1 1 (:REWRITE DEFAULT-<-2))
)
(16_NORM=0
(2014 318 (:REWRITE DEFAULT-+-2))
(985 985 (:REWRITE DEFAULT-CDR))
(883 883 (:REWRITE DEFAULT-CAR))
(724 318 (:REWRITE DEFAULT-+-1))
(324 108 (:LINEAR X*Y>1-POSITIVE))
(278 278 (:REWRITE FOLD-CONSTS-IN-+))
(119 119 (:REWRITE DEFAULT-*-2))
(119 119 (:REWRITE DEFAULT-*-1))
(108 108 (:REWRITE DEFAULT-<-2))
(108 108 (:REWRITE DEFAULT-<-1))
(9 9 (:REWRITE EQUAL-CONSTANT-+))
)
(16_DOT-DEF
(73214 5897 (:REWRITE DEFAULT-+-2))
(68417 68417 (:TYPE-PRESCRIPTION NONNEGATIVE-PRODUCT))
(17238 5385 (:TYPE-PRESCRIPTION |x < y => 0 < -x+y|))
(12473 5897 (:REWRITE DEFAULT-+-1))
(5642 5642 (:REWRITE FOLD-CONSTS-IN-+))
(364 62 (:REWRITE DEFAULT-UNARY-MINUS))
(351 271 (:REWRITE DEFAULT-*-2))
(351 271 (:REWRITE DEFAULT-*-1))
(192 192 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(105 105 (:REWRITE DEFAULT-CDR))
(105 105 (:REWRITE DEFAULT-CAR))
(32 32 (:REWRITE FOLD-CONSTS-IN-*))
(1 1 (:REWRITE EQUAL-CONSTANT-+))
)
(DISTRIBUTIVITY-16_DOT-16_+
(1632 1632 (:REWRITE DEFAULT-+-2))
(1632 1632 (:REWRITE DEFAULT-+-1))
(1491 1491 (:REWRITE FOLD-CONSTS-IN-+))
(297 297 (:REWRITE DEFAULT-CDR))
(297 297 (:REWRITE DEFAULT-CAR))
(254 254 (:REWRITE DEFAULT-*-2))
(254 254 (:REWRITE DEFAULT-*-1))
(96 96 (:REWRITE FOLD-CONSTS-IN-*))
)
(FORALL-U-16_DOT-U-X=0)
(FORALL-U-16_DOT-U-X=0-NECC)
(FORALL-U-16_DOT-U-X=0-DEF
(900 3 (:REWRITE FORALL-U-16_DOT-U-X=0-NECC))
(555 555 (:REWRITE DEFAULT-+-2))
(555 555 (:REWRITE DEFAULT-+-1))
(468 468 (:REWRITE FOLD-CONSTS-IN-+))
(144 96 (:REWRITE DEFAULT-*-2))
(144 96 (:REWRITE DEFAULT-*-1))
(135 135 (:REWRITE DEFAULT-CDR))
(135 135 (:REWRITE DEFAULT-CAR))
(98 98 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(8 2 (:LINEAR X*Y>1-POSITIVE))
(4 4 (:REWRITE EQUAL-CONSTANT-+))
(4 2 (:REWRITE DEFAULT-<-2))
(2 2 (:REWRITE DEFAULT-<-1))
)
(16_DOT=0
(2199 503 (:REWRITE DEFAULT-+-2))
(1045 1045 (:REWRITE DEFAULT-CDR))
(943 943 (:REWRITE DEFAULT-CAR))
(909 503 (:REWRITE DEFAULT-+-1))
(862 2 (:REWRITE FORALL-U-16_DOT-U-X=0-NECC))
(860 1 (:DEFINITION FORALL-U-16_DOT-U-X=0))
(434 434 (:REWRITE FOLD-CONSTS-IN-+))
(330 110 (:LINEAR X*Y>1-POSITIVE))
(151 151 (:REWRITE DEFAULT-*-2))
(151 151 (:REWRITE DEFAULT-*-1))
(110 110 (:REWRITE DEFAULT-<-2))
(110 110 (:REWRITE DEFAULT-<-1))
(48 16 (:REWRITE COMMUTATIVITY-OF-*))
(10 10 (:REWRITE EQUAL-CONSTANT-+))
(2 2 (:TYPE-PRESCRIPTION FORALL-U-16_DOT-U-X=0))
)
(FORALL-U-16_DOT-U-X=0->X=8_0
(30 30 (:REWRITE DEFAULT-CDR))
(30 30 (:REWRITE DEFAULT-CAR))
)
(16_CONJUGATE-DEF-REWRITE
(133 133 (:REWRITE DEFAULT-CDR))
(133 133 (:REWRITE DEFAULT-CAR))
(35 35 (:REWRITE DEFAULT-*-2))
(35 35 (:REWRITE DEFAULT-*-1))
(31 31 (:REWRITE DEFAULT-UNARY-MINUS))
(25 25 (:REWRITE DEFAULT-+-2))
(25 25 (:REWRITE DEFAULT-+-1))
(5 5 (:REWRITE EQUAL-CONSTANT-+))
)
(16_NORM=8_NORM
(775 199 (:REWRITE DEFAULT-+-2))
(467 199 (:REWRITE DEFAULT-+-1))
(146 146 (:REWRITE FOLD-CONSTS-IN-+))
(47 47 (:REWRITE DEFAULT-CDR))
(47 47 (:REWRITE DEFAULT-CAR))
(32 32 (:REWRITE DEFAULT-*-2))
(32 32 (:REWRITE DEFAULT-*-1))
)
(8P-8_0-ORTHOGONAL-8_0-8P
(50 50 (:REWRITE DEFAULT-CDR))
(50 50 (:REWRITE DEFAULT-CAR))
(8 8 (:REWRITE DEFAULT-*-2))
(8 8 (:REWRITE DEFAULT-*-1))
)
(16_1-DEF)
(16_*-CONS=CONS-8_*
(1914 854 (:REWRITE DEFAULT-+-2))
(1018 854 (:REWRITE DEFAULT-+-1))
(590 590 (:REWRITE FOLD-CONSTS-IN-+))
(523 422 (:REWRITE DEFAULT-CDR))
(523 422 (:REWRITE DEFAULT-CAR))
(288 288 (:REWRITE DEFAULT-*-2))
(288 288 (:REWRITE DEFAULT-*-1))
(229 189 (:REWRITE DEFAULT-UNARY-MINUS))
)
(8P*I=CONS-8_0-8P
(134 134 (:REWRITE DEFAULT-CDR))
(134 134 (:REWRITE DEFAULT-CAR))
(72 72 (:REWRITE DEFAULT-*-2))
(72 72 (:REWRITE DEFAULT-*-1))
(59 59 (:REWRITE DEFAULT-+-2))
(59 59 (:REWRITE DEFAULT-+-1))
(12 12 (:REWRITE DEFAULT-UNARY-MINUS))
)
(|16_/|)
(|16P-16_/|
(1133 185 (:REWRITE DEFAULT-+-2))
(458 185 (:REWRITE DEFAULT-+-1))
(364 124 (:REWRITE DEFAULT-CDR))
(364 124 (:REWRITE DEFAULT-CAR))
(304 48 (:REWRITE DEFAULT-*-2))
(304 48 (:REWRITE DEFAULT-*-1))
(270 30 (:REWRITE DEFAULT-UNARY-MINUS))
(180 2 (:REWRITE /R-WHEN-ABS-NUMERATOR=1))
(156 156 (:REWRITE FOLD-CONSTS-IN-+))
(118 1 (:REWRITE DEFAULT-UNARY-/))
(49 1 (:REWRITE NUMERATOR-WHEN-INTEGERP))
(17 1 (:REWRITE DEFAULT-NUMERATOR))
(3 1 (:LINEAR X*Y>1-POSITIVE))
(1 1 (:REWRITE EQUAL-CONSTANT-+))
(1 1 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE DEFAULT-<-1))
)
(16_*-16_CONJUGATE-RIGHT
(6576 2198 (:REWRITE DEFAULT-+-2))
(3451 2198 (:REWRITE DEFAULT-+-1))
(3169 2381 (:TYPE-PRESCRIPTION |x < y => 0 < -x+y|))
(1444 1444 (:REWRITE FOLD-CONSTS-IN-+))
(1188 870 (:REWRITE DEFAULT-*-2))
(1126 870 (:REWRITE DEFAULT-*-1))
(1019 845 (:TYPE-PRESCRIPTION |x < y => 0 < y-x|))
(869 661 (:REWRITE DEFAULT-CDR))
(869 661 (:REWRITE DEFAULT-CAR))
(611 373 (:REWRITE DEFAULT-UNARY-MINUS))
(544 544 (:REWRITE FOLD-CONSTS-IN-*))
(8 4 (:REWRITE /R-WHEN-ABS-NUMERATOR=1))
(2 2 (:REWRITE NUMERATOR-WHEN-INTEGERP))
(2 2 (:REWRITE DEFAULT-UNARY-/))
(2 2 (:REWRITE DEFAULT-NUMERATOR))
)
(16_*-16_CONJUGATE-LEFT
(6544 2211 (:REWRITE DEFAULT-+-2))
(3380 2211 (:REWRITE DEFAULT-+-1))
(3048 2252 (:TYPE-PRESCRIPTION |x < y => 0 < -x+y|))
(1444 1444 (:REWRITE FOLD-CONSTS-IN-+))
(1188 870 (:REWRITE DEFAULT-*-2))
(1126 870 (:REWRITE DEFAULT-*-1))
(1019 845 (:TYPE-PRESCRIPTION |x < y => 0 < y-x|))
(869 661 (:REWRITE DEFAULT-CDR))
(869 661 (:REWRITE DEFAULT-CAR))
(658 415 (:REWRITE DEFAULT-UNARY-MINUS))
(544 544 (:REWRITE FOLD-CONSTS-IN-*))
(8 4 (:REWRITE /R-WHEN-ABS-NUMERATOR=1))
(2 2 (:REWRITE NUMERATOR-WHEN-INTEGERP))
(2 2 (:REWRITE DEFAULT-UNARY-/))
(2 2 (:REWRITE DEFAULT-NUMERATOR))
)
(16_/=16_*-INVERSE-RIGHT
(35 14 (:REWRITE /R-WHEN-ABS-NUMERATOR=1))
(24 12 (:REWRITE DEFAULT-CDR))
(24 12 (:REWRITE DEFAULT-CAR))
(11 5 (:REWRITE NUMERATOR-WHEN-INTEGERP))
(7 7 (:REWRITE DEFAULT-UNARY-/))
(5 5 (:REWRITE DEFAULT-NUMERATOR))
(4 4 (:REWRITE DEFAULT-*-2))
(4 4 (:REWRITE DEFAULT-*-1))
(2 2 (:REWRITE DEFAULT-<-2))
(2 2 (:REWRITE DEFAULT-<-1))
)
(16_/=16_*-INVERSE-LEFT
(35 14 (:REWRITE /R-WHEN-ABS-NUMERATOR=1))
(24 12 (:REWRITE DEFAULT-CDR))
(24 12 (:REWRITE DEFAULT-CAR))
(11 5 (:REWRITE NUMERATOR-WHEN-INTEGERP))
(7 7 (:REWRITE DEFAULT-UNARY-/))
(5 5 (:REWRITE DEFAULT-NUMERATOR))
(4 4 (:REWRITE DEFAULT-*-2))
(4 4 (:REWRITE DEFAULT-*-1))
(2 2 (:REWRITE DEFAULT-<-2))
(2 2 (:REWRITE DEFAULT-<-1))
)
(16_CONJUGATE-IS-NOT-TRIVIAL)
(16_*-IS-NOT-COMMUTATIVE)
(16_*-IS-NOT-ASSOCIATIVE)
(16_*-ZERO-DIVISORS)
|
