1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/SK/".
17 include "legacy/coq.ma".
19 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
20 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
21 alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
22 alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
23 alias id "sym_eq" = "cic:/Coq/Init/Logic/sym_eq.con".
27 \forall app: A \to A \to A.
30 \forall H1: (\forall x,y:A.(app (app K x) y) = x).
31 \forall H2: (\forall x,y,z:A.
32 (app (app (app S x) y) z) = (app (app x z) (app y z))).
34 (app (app (app S K) K) x) = x.
35 intros.auto paramodulation.
42 \forall add: A \to A \to A.
43 \forall mult: A \to A \to A.
45 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
46 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
47 \forall d1: (\forall x,y,z:A.
48 (add x (mult y z)) = (mult (add x y) (add x z))).
49 \forall d2: (\forall x,y,z:A.
50 (mult x (add y z)) = (add (mult x y) (mult x z))).
51 \forall i1: (\forall x:A. (add x zero) = x).
52 \forall i2: (\forall x:A. (mult x one) = x).
53 \forall inv1: (\forall x:A. (add x (inv x)) = one).
54 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
56 intros.auto paramodulation.
63 \forall add: A \to A \to A.
64 \forall mult: A \to A \to A.
66 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
67 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
68 \forall d1: (\forall x,y,z:A.
69 (add x (mult y z)) = (mult (add x y) (add x z))).
70 \forall d2: (\forall x,y,z:A.
71 (mult x (add y z)) = (add (mult x y) (mult x z))).
72 \forall i1: (\forall x:A. (add x zero) = x).
73 \forall i2: (\forall x:A. (mult x one) = x).
74 \forall inv1: (\forall x:A. (add x (inv x)) = one).
75 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
76 \forall x:A. (mult x zero) = zero.
77 intros.auto paramodulation.
84 \forall add: A \to A \to A.
85 \forall mult: A \to A \to A.
87 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
88 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
89 \forall d1: (\forall x,y,z:A.
90 (add x (mult y z)) = (mult (add x y) (add x z))).
91 \forall d2: (\forall x,y,z:A.
92 (mult x (add y z)) = (add (mult x y) (mult x z))).
93 \forall i1: (\forall x:A. (add x zero) = x).
94 \forall i2: (\forall x:A. (mult x one) = x).
95 \forall inv1: (\forall x:A. (add x (inv x)) = one).
96 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
97 \forall x:A. (inv (inv x)) = x.
98 intros.auto paramodulation.
105 \forall add: A \to A \to A.
106 \forall mult: A \to A \to A.
107 \forall inv: A \to A.
108 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
109 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
110 \forall d1: (\forall x,y,z:A.
111 (add x (mult y z)) = (mult (add x y) (add x z))).
112 \forall d2: (\forall x,y,z:A.
113 (mult x (add y z)) = (add (mult x y) (mult x z))).
114 \forall i1: (\forall x:A. (add x zero) = x).
115 \forall i2: (\forall x:A. (mult x one) = x).
116 \forall inv1: (\forall x:A. (add x (inv x)) = one).
117 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
118 \forall x,y:A. (mult x (add (inv x) y)) = (mult x y).
119 intros.auto paramodulation.
126 \forall add: A \to A \to A.
127 \forall mult: A \to A \to A.
128 \forall inv: A \to A.
129 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
130 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
131 \forall d1: (\forall x,y,z:A.
132 (add x (mult y z)) = (mult (add x y) (add x z))).
133 \forall d2: (\forall x,y,z:A.
134 (mult x (add y z)) = (add (mult x y) (mult x z))).
135 \forall i1: (\forall x:A. (add x zero) = x).
136 \forall i2: (\forall x:A. (mult x one) = x).
137 \forall inv1: (\forall x:A. (add x (inv x)) = one).
138 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
139 \forall x,y:A. zero = (mult x (mult (inv x) y)).
140 intros.auto paramodulation.
147 \forall add: A \to A \to A.
148 \forall mult: A \to A \to A.
149 \forall inv: A \to A.
150 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
151 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
152 \forall d1: (\forall x,y,z:A.
153 (add x (mult y z)) = (mult (add x y) (add x z))).
154 \forall d2: (\forall x,y,z:A.
155 (mult x (add y z)) = (add (mult x y) (mult x z))).
156 \forall i1: (\forall x:A. (add x zero) = x).
157 \forall i2: (\forall x:A. (mult x one) = x).
158 \forall inv1: (\forall x:A. (add x (inv x)) = one).
159 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
160 \forall x,y:A. zero = mult (inv x) (mult x y).
161 intros.auto paramodulation.
168 \forall add: A \to A \to A.
169 \forall mult: A \to A \to A.
170 \forall inv: A \to A.
171 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
172 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
173 \forall d1: (\forall x,y,z:A.
174 (add x (mult y z)) = (mult (add x y) (add x z))).
175 \forall d2: (\forall x,y,z:A.
176 (mult x (add y z)) = (add (mult x y) (mult x z))).
177 \forall i1: (\forall x:A. (add x zero) = x).
178 \forall i2: (\forall x:A. (mult x one) = x).
179 \forall inv1: (\forall x:A. (add x (inv x)) = one).
180 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
181 \forall x,y:A. x = (mult (add y x) x).
182 intros.auto paramodulation.
189 \forall add: A \to A \to A.
190 \forall mult: A \to A \to A.
191 \forall inv: A \to A.
192 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
193 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
194 \forall d1: (\forall x,y,z:A.
195 (add x (mult y z)) = (mult (add x y) (add x z))).
196 \forall d2: (\forall x,y,z:A.
197 (mult x (add y z)) = (add (mult x y) (mult x z))).
198 \forall i1: (\forall x:A. (add x zero) = x).
199 \forall i2: (\forall x:A. (mult x one) = x).
200 \forall inv1: (\forall x:A. (add x (inv x)) = one).
201 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
202 \forall x,y:A. zero = (mult (inv (add x y)) y).
203 intros.auto paramodulation.
210 \forall add: A \to A \to A.
211 \forall mult: A \to A \to A.
212 \forall inv: A \to A.
213 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
214 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
215 \forall d1: (\forall x,y,z:A.
216 (add x (mult y z)) = (mult (add x y) (add x z))).
217 \forall d2: (\forall x,y,z:A.
218 (mult x (add y z)) = (add (mult x y) (mult x z))).
219 \forall i1: (\forall x:A. (add x zero) = x).
220 \forall i2: (\forall x:A. (mult x one) = x).
221 \forall inv1: (\forall x:A. (add x (inv x)) = one).
222 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
223 \forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y).
224 intros.auto paramodulation.
231 \forall add: A \to A \to A.
232 \forall mult: A \to A \to A.
233 \forall inv: A \to A.
234 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
235 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
236 \forall d1: (\forall x,y,z:A.
237 (add x (mult y z)) = (mult (add x y) (add x z))).
238 \forall d2: (\forall x,y,z:A.
239 (mult x (add y z)) = (add (mult x y) (mult x z))).
240 \forall i1: (\forall x:A. (add x zero) = x).
241 \forall i2: (\forall x:A. (mult x one) = x).
242 \forall inv1: (\forall x:A. (add x (inv x)) = one).
243 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
245 \forall hint1: (\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y)).
246 \forall hint2: \forall x,y:A.zero = (mult (inv x) (mult x y)).
247 \forall hint2: (\forall x,y:A. zero = (mult (inv (add x y)) y)).
250 inv x = (add (inv x) (inv (add y x))).
251 intros.auto paramodulation.
258 \forall add: A \to A \to A.
259 \forall mult: A \to A \to A.
260 \forall inv: A \to A.
261 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
262 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
263 \forall d1: (\forall x,y,z:A.
264 (add x (mult y z)) = (mult (add x y) (add x z))).
265 \forall d2: (\forall x,y,z:A.
266 (mult x (add y z)) = (add (mult x y) (mult x z))).
267 \forall i1: (\forall x:A. (add x zero) = x).
268 \forall i2: (\forall x:A. (mult x one) = x).
269 \forall inv1: (\forall x:A. (add x (inv x)) = one).
270 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
272 \forall hint1: (\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y)).
273 \forall hint2: \forall x,y:A.zero = (mult (inv x) (mult x y)).
274 \forall hint2: (\forall x,y:A. zero = (mult (inv (add x y)) y)).
277 inv x = (add (inv (add y x)) (inv x)).
278 intros.auto paramodulation.
285 \forall add: A \to A \to A.
286 \forall mult: A \to A \to A.
287 \forall inv: A \to A.
288 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
289 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
290 \forall d1: (\forall x,y,z:A.
291 (add x (mult y z)) = (mult (add x y) (add x z))).
292 \forall d2: (\forall x,y,z:A.
293 (mult x (add y z)) = (add (mult x y) (mult x z))).
294 \forall i1: (\forall x:A. (add x zero) = x).
295 \forall i2: (\forall x:A. (mult x one) = x).
296 \forall inv1: (\forall x:A. (add x (inv x)) = one).
297 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
299 add x (mult x y) = mult x (add x y).
300 intros.auto paramodulation.
307 \forall add: A \to A \to A.
308 \forall mult: A \to A \to A.
309 \forall inv: A \to A.
310 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
311 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
312 \forall d1: (\forall x,y,z:A.
313 (add x (mult y z)) = (mult (add x y) (add x z))).
314 \forall d2: (\forall x,y,z:A.
315 (mult x (add y z)) = (add (mult x y) (mult x z))).
316 \forall i1: (\forall x:A. (add x zero) = x).
317 \forall i2: (\forall x:A. (mult x one) = x).
318 \forall inv1: (\forall x:A. (add x (inv x)) = one).
319 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
321 (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u))).
322 intros.auto paramodulation.
329 \forall add: A \to A \to A.
330 \forall mult: A \to A \to A.
331 \forall inv: A \to A.
332 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
333 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
334 \forall d1: (\forall x,y,z:A.
335 (add x (mult y z)) = (mult (add x y) (add x z))).
336 \forall d2: (\forall x,y,z:A.
337 (mult x (add y z)) = (add (mult x y) (mult x z))).
338 \forall i1: (\forall x:A. (add x zero) = x).
339 \forall i2: (\forall x:A. (mult x one) = x).
340 \forall inv1: (\forall x:A. (add x (inv x)) = one).
341 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
343 add x (mult y z) = mult (add y x) (add x z).
344 intros.auto paramodulation.
347 theorem bool756minimal:
349 \forall add: A \to A \to A.
350 \forall mult: A \to A \to A.
351 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
352 \forall hint1: (\forall x,y,z,u:A.
353 add y (add x (mult x u)) = (add (mult (add x y) z) (add x (mult y u)))).
354 \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
356 add x (add y (mult y z)) = add x (add y (mult x z)).
361 theorem bool756simplified:
363 \forall add: A \to A \to A.
364 \forall mult: A \to A \to A.
365 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
366 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
367 \forall hint1: (\forall x,y,z,u:A.
368 (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u)))).
369 \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
370 \forall hint3: (\forall x,y,z:A.
371 add x (mult y z) = mult (add y x) (add x z)).
372 \forall hint4: (\forall x,y:A.
373 add x (mult x y) = mult x (add x y)).
375 add x (add y (mult y z)) = add x (add y (mult x z)).
385 \forall add: A \to A \to A.
386 \forall mult: A \to A \to A.
387 \forall inv: A \to A.
388 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
389 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
390 \forall d1: (\forall x,y,z:A.
391 (add x (mult y z)) = (mult (add x y) (add x z))).
392 \forall d2: (\forall x,y,z:A.
393 (mult x (add y z)) = (add (mult x y) (mult x z))).
394 \forall i1: (\forall x:A. (add x zero) = x).
395 \forall i2: (\forall x:A. (mult x one) = x).
396 \forall inv1: (\forall x:A. (add x (inv x)) = one).
397 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
398 \forall hint1: (\forall x,y,z,u:A.
399 (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u)))).
400 \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
401 \forall hint3: (\forall x,y,z:A.
402 add x (mult y z) = mult (add y x) (add x z)).
403 \forall hint4: (\forall x,y:A.
404 add x (mult x y) = mult x (add x y)).
406 add x y = add x (add y (mult x z)).
408 cut (mult (add y x) (add x (add y z)) = add x (add y (mult x z)));
410 |auto paramodulation]
418 \forall add: A \to A \to A.
419 \forall mult: A \to A \to A.
420 \forall inv: A \to A.
421 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
422 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
423 \forall d1: (\forall x,y,z:A.
424 (add x (mult y z)) = (mult (add x y) (add x z))).
425 \forall d2: (\forall x,y,z:A.
426 (mult x (add y z)) = (add (mult x y) (mult x z))).
427 \forall i1: (\forall x:A. (add x zero) = x).
428 \forall i2: (\forall x:A. (mult x one) = x).
429 \forall inv1: (\forall x:A. (add x (inv x)) = one).
430 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
432 add x y = add x (add y (mult x z)).
433 intros;auto paramodulation.
435 (* war=5; active 225, maxmeta 172568 *)
436 (* war=4; active 249, maxmeta 223220 *)
442 \forall add: A \to A \to A.
443 \forall mult: A \to A \to A.
444 \forall inv: A \to A.
445 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
446 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
447 \forall d1: (\forall x,y,z:A.
448 (add x (mult y z)) = (mult (add x y) (add x z))).
449 \forall d2: (\forall x,y,z:A.
450 (mult x (add y z)) = (add (mult x y) (mult x z))).
451 \forall i1: (\forall x:A. (add x zero) = x).
452 \forall i2: (\forall x:A. (mult x one) = x).
453 \forall inv1: (\forall x:A. (add x (inv x)) = one).
454 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
456 (add x y) = (add (add x (mult y z)) y).
457 intros.auto paramodulation.
464 \forall add: A \to A \to A.
465 \forall mult: A \to A \to A.
466 \forall inv: A \to A.
467 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
468 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
469 \forall d1: (\forall x,y,z:A.
470 (add x (mult y z)) = (mult (add x y) (add x z))).
471 \forall d2: (\forall x,y,z:A.
472 (mult x (add y z)) = (add (mult x y) (mult x z))).
473 \forall i1: (\forall x:A. (add x zero) = x).
474 \forall i2: (\forall x:A. (mult x one) = x).
475 \forall inv1: (\forall x:A. (add x (inv x)) = one).
476 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
478 \forall c1z: (\forall x:A.(add x z) = (add z x)).
479 add (add x y) z = add (add x y) (add z y).
480 intros.auto paramodulation.
487 \forall add: A \to A \to A.
488 \forall mult: A \to A \to A.
489 \forall inv: A \to A.
490 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
491 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
492 \forall d1: (\forall x,y,z:A.
493 (add x (mult y z)) = (mult (add x y) (add x z))).
494 \forall d2: (\forall x,y,z:A.
495 (mult x (add y z)) = (add (mult x y) (mult x z))).
496 \forall i1: (\forall x:A. (add x zero) = x).
497 \forall i2: (\forall x:A. (mult x one) = x).
498 \forall inv1: (\forall x:A. (add x (inv x)) = one).
499 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
501 add (add x y) z = add (add x y) (add z y).
502 intros.auto paramodulation.
509 \forall add: A \to A \to A.
510 \forall mult: A \to A \to A.
511 \forall inv: A \to A.
512 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
513 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
514 \forall d1: (\forall x,y,z:A.
515 (add x (mult y z)) = (mult (add x y) (add x z))).
516 \forall d2: (\forall x,y,z:A.
517 (mult x (add y z)) = (add (mult x y) (mult x z))).
518 \forall i1: (\forall x:A. (add x zero) = x).
519 \forall i2: (\forall x:A. (mult x one) = x).
520 \forall inv1: (\forall x:A. (add x (inv x)) = one).
521 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
523 add x (add y z) = add (add x z) y.
524 intros.auto paramodulation.
531 \forall add: A \to A \to A.
532 \forall mult: A \to A \to A.
533 \forall inv: A \to A.
534 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
535 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
536 \forall d1: (\forall x,y,z:A.
537 (add x (mult y z)) = (mult (add x y) (add x z))).
538 \forall d2: (\forall x,y,z:A.
539 (mult x (add y z)) = (add (mult x y) (mult x z))).
540 \forall i1: (\forall x:A. (add x zero) = x).
541 \forall i2: (\forall x:A. (mult x one) = x).
542 \forall inv1: (\forall x:A. (add x (inv x)) = one).
543 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
545 add (inv x) y = add (mult x y) (inv x).
546 intros.auto paramodulation.
553 \forall add: A \to A \to A.
554 \forall mult: A \to A \to A.
555 \forall inv: A \to A.
556 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
557 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
558 \forall d1: (\forall x,y,z:A.
559 (add x (mult y z)) = (mult (add x y) (add x z))).
560 \forall d2: (\forall x,y,z:A.
561 (mult x (add y z)) = (add (mult x y) (mult x z))).
562 \forall i1: (\forall x:A. (add x zero) = x).
563 \forall i2: (\forall x:A. (mult x one) = x).
564 \forall inv1: (\forall x:A. (add x (inv x)) = one).
565 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
566 \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
567 \forall hint1735:(\forall x,y:A. add (inv (add x y)) x = add x (inv y)).
568 \forall hint623:(\forall x,y:A. inv (mult x y) = add (inv x) (inv (mult x y))).
570 (inv (mult x y)) = (add (inv x) (inv y)).
571 intros.auto paramodulation.
579 \forall add: A \to A \to A.
580 \forall mult: A \to A \to A.
581 \forall inv: A \to A.
582 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
583 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
584 \forall d1: (\forall x,y,z:A.
585 (add x (mult y z)) = (mult (add x y) (add x z))).
586 \forall d2: (\forall x,y,z:A.
587 (mult x (add y z)) = (add (mult x y) (mult x z))).
588 \forall i1: (\forall x:A. (add x zero) = x).
589 \forall i2: (\forall x:A. (mult x one) = x).
590 \forall inv1: (\forall x:A. (add x (inv x)) = one).
591 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
592 \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
593 \forall hint623:(\forall x,y:A. inv (mult x y) = add (inv x) (inv (mult x y))).
595 (inv (mult x y)) = (add (inv x) (inv y)).
596 intros.auto paramodulation.
604 \forall add: A \to A \to A.
605 \forall mult: A \to A \to A.
606 \forall inv: A \to A.
607 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
608 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
609 \forall d1: (\forall x,y,z:A.
610 (add x (mult y z)) = (mult (add x y) (add x z))).
611 \forall d2: (\forall x,y,z:A.
612 (mult x (add y z)) = (add (mult x y) (mult x z))).
613 \forall i1: (\forall x:A. (add x zero) = x).
614 \forall i2: (\forall x:A. (mult x one) = x).
615 \forall inv1: (\forall x:A. (add x (inv x)) = one).
616 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
617 \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
618 \forall hint609:(\forall x,y:A. inv x = add (inv (add y x)) (inv x)).
620 (inv (mult x y)) = (add (inv x) (inv y)).
621 intros.auto paramodulation.
629 \forall add: A \to A \to A.
630 \forall mult: A \to A \to A.
631 \forall inv: A \to A.
632 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
633 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
634 \forall d1: (\forall x,y,z:A.
635 (add x (mult y z)) = (mult (add x y) (add x z))).
636 \forall d2: (\forall x,y,z:A.
637 (mult x (add y z)) = (add (mult x y) (mult x z))).
638 \forall i1: (\forall x:A. (add x zero) = x).
639 \forall i2: (\forall x:A. (mult x one) = x).
640 \forall inv1: (\forall x:A. (add x (inv x)) = one).
641 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
643 (inv (mult x y)) = (add (inv x) (inv y)).
644 intros.auto paramodulation.