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".
29 \forall app: A \to A \to A.
32 \forall H1: (\forall x,y:A.(app (app K x) y) = x).
33 \forall H2: (\forall x,y,z:A.
34 (app (app (app S x) y) z) = (app (app x z) (app y z))).
36 (app (app (app S K) K) x) = x.
37 intros.auto paramodulation.
44 \forall add: A \to A \to A.
45 \forall mult: A \to A \to A.
47 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
48 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
49 \forall d1: (\forall x,y,z:A.
50 (add x (mult y z)) = (mult (add x y) (add x z))).
51 \forall d2: (\forall x,y,z:A.
52 (mult x (add y z)) = (add (mult x y) (mult x z))).
53 \forall i1: (\forall x:A. (add x zero) = x).
54 \forall i2: (\forall x:A. (mult x one) = x).
55 \forall inv1: (\forall x:A. (add x (inv x)) = one).
56 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
58 intros.auto paramodulation.
65 \forall add: A \to A \to A.
66 \forall mult: A \to A \to A.
68 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
69 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
70 \forall d1: (\forall x,y,z:A.
71 (add x (mult y z)) = (mult (add x y) (add x z))).
72 \forall d2: (\forall x,y,z:A.
73 (mult x (add y z)) = (add (mult x y) (mult x z))).
74 \forall i1: (\forall x:A. (add x zero) = x).
75 \forall i2: (\forall x:A. (mult x one) = x).
76 \forall inv1: (\forall x:A. (add x (inv x)) = one).
77 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
78 \forall x:A. (mult x zero) = zero.
79 intros.auto paramodulation.
86 \forall add: A \to A \to A.
87 \forall mult: A \to A \to A.
89 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
90 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
91 \forall d1: (\forall x,y,z:A.
92 (add x (mult y z)) = (mult (add x y) (add x z))).
93 \forall d2: (\forall x,y,z:A.
94 (mult x (add y z)) = (add (mult x y) (mult x z))).
95 \forall i1: (\forall x:A. (add x zero) = x).
96 \forall i2: (\forall x:A. (mult x one) = x).
97 \forall inv1: (\forall x:A. (add x (inv x)) = one).
98 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
99 \forall x:A. (inv (inv x)) = x.
100 intros.auto paramodulation.
107 \forall add: A \to A \to A.
108 \forall mult: A \to A \to A.
109 \forall inv: A \to A.
110 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
111 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
112 \forall d1: (\forall x,y,z:A.
113 (add x (mult y z)) = (mult (add x y) (add x z))).
114 \forall d2: (\forall x,y,z:A.
115 (mult x (add y z)) = (add (mult x y) (mult x z))).
116 \forall i1: (\forall x:A. (add x zero) = x).
117 \forall i2: (\forall x:A. (mult x one) = x).
118 \forall inv1: (\forall x:A. (add x (inv x)) = one).
119 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
120 \forall x,y:A. (mult x (add (inv x) y)) = (mult x y).
121 intros.auto paramodulation.
128 \forall add: A \to A \to A.
129 \forall mult: A \to A \to A.
130 \forall inv: A \to A.
131 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
132 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
133 \forall d1: (\forall x,y,z:A.
134 (add x (mult y z)) = (mult (add x y) (add x z))).
135 \forall d2: (\forall x,y,z:A.
136 (mult x (add y z)) = (add (mult x y) (mult x z))).
137 \forall i1: (\forall x:A. (add x zero) = x).
138 \forall i2: (\forall x:A. (mult x one) = x).
139 \forall inv1: (\forall x:A. (add x (inv x)) = one).
140 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
141 \forall x,y:A. zero = (mult x (mult (inv x) y)).
142 intros.auto paramodulation.
149 \forall add: A \to A \to A.
150 \forall mult: A \to A \to A.
151 \forall inv: A \to A.
152 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
153 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
154 \forall d1: (\forall x,y,z:A.
155 (add x (mult y z)) = (mult (add x y) (add x z))).
156 \forall d2: (\forall x,y,z:A.
157 (mult x (add y z)) = (add (mult x y) (mult x z))).
158 \forall i1: (\forall x:A. (add x zero) = x).
159 \forall i2: (\forall x:A. (mult x one) = x).
160 \forall inv1: (\forall x:A. (add x (inv x)) = one).
161 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
162 \forall x,y:A. zero = mult (inv x) (mult x y).
163 intros.auto paramodulation.
170 \forall add: A \to A \to A.
171 \forall mult: A \to A \to A.
172 \forall inv: A \to A.
173 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
174 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
175 \forall d1: (\forall x,y,z:A.
176 (add x (mult y z)) = (mult (add x y) (add x z))).
177 \forall d2: (\forall x,y,z:A.
178 (mult x (add y z)) = (add (mult x y) (mult x z))).
179 \forall i1: (\forall x:A. (add x zero) = x).
180 \forall i2: (\forall x:A. (mult x one) = x).
181 \forall inv1: (\forall x:A. (add x (inv x)) = one).
182 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
183 \forall x,y:A. x = (mult (add y x) x).
184 intros.auto paramodulation.
191 \forall add: A \to A \to A.
192 \forall mult: A \to A \to A.
193 \forall inv: A \to A.
194 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
195 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
196 \forall d1: (\forall x,y,z:A.
197 (add x (mult y z)) = (mult (add x y) (add x z))).
198 \forall d2: (\forall x,y,z:A.
199 (mult x (add y z)) = (add (mult x y) (mult x z))).
200 \forall i1: (\forall x:A. (add x zero) = x).
201 \forall i2: (\forall x:A. (mult x one) = x).
202 \forall inv1: (\forall x:A. (add x (inv x)) = one).
203 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
204 \forall x,y:A. zero = (mult (inv (add x y)) y).
205 intros.auto paramodulation.
212 \forall add: A \to A \to A.
213 \forall mult: A \to A \to A.
214 \forall inv: A \to A.
215 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
216 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
217 \forall d1: (\forall x,y,z:A.
218 (add x (mult y z)) = (mult (add x y) (add x z))).
219 \forall d2: (\forall x,y,z:A.
220 (mult x (add y z)) = (add (mult x y) (mult x z))).
221 \forall i1: (\forall x:A. (add x zero) = x).
222 \forall i2: (\forall x:A. (mult x one) = x).
223 \forall inv1: (\forall x:A. (add x (inv x)) = one).
224 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
225 \forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y).
226 intros.auto paramodulation.
233 \forall add: A \to A \to A.
234 \forall mult: A \to A \to A.
235 \forall inv: A \to A.
236 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
237 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
238 \forall d1: (\forall x,y,z:A.
239 (add x (mult y z)) = (mult (add x y) (add x z))).
240 \forall d2: (\forall x,y,z:A.
241 (mult x (add y z)) = (add (mult x y) (mult x z))).
242 \forall i1: (\forall x:A. (add x zero) = x).
243 \forall i2: (\forall x:A. (mult x one) = x).
244 \forall inv1: (\forall x:A. (add x (inv x)) = one).
245 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
247 \forall hint1: (\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y)).
248 \forall hint2: \forall x,y:A.zero = (mult (inv x) (mult x y)).
249 \forall hint2: (\forall x,y:A. zero = (mult (inv (add x y)) y)).
252 inv x = (add (inv x) (inv (add y x))).
253 intros.auto paramodulation.
260 \forall add: A \to A \to A.
261 \forall mult: A \to A \to A.
262 \forall inv: A \to A.
263 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
264 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
265 \forall d1: (\forall x,y,z:A.
266 (add x (mult y z)) = (mult (add x y) (add x z))).
267 \forall d2: (\forall x,y,z:A.
268 (mult x (add y z)) = (add (mult x y) (mult x z))).
269 \forall i1: (\forall x:A. (add x zero) = x).
270 \forall i2: (\forall x:A. (mult x one) = x).
271 \forall inv1: (\forall x:A. (add x (inv x)) = one).
272 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
274 \forall hint1: (\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y)).
275 \forall hint2: \forall x,y:A.zero = (mult (inv x) (mult x y)).
276 \forall hint2: (\forall x,y:A. zero = (mult (inv (add x y)) y)).
279 inv x = (add (inv (add y x)) (inv x)).
280 intros.auto paramodulation.
287 \forall add: A \to A \to A.
288 \forall mult: A \to A \to A.
289 \forall inv: A \to A.
290 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
291 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
292 \forall d1: (\forall x,y,z:A.
293 (add x (mult y z)) = (mult (add x y) (add x z))).
294 \forall d2: (\forall x,y,z:A.
295 (mult x (add y z)) = (add (mult x y) (mult x z))).
296 \forall i1: (\forall x:A. (add x zero) = x).
297 \forall i2: (\forall x:A. (mult x one) = x).
298 \forall inv1: (\forall x:A. (add x (inv x)) = one).
299 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
301 add x (mult x y) = mult x (add x y).
302 intros.auto paramodulation.
309 \forall add: A \to A \to A.
310 \forall mult: A \to A \to A.
311 \forall inv: A \to A.
312 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
313 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
314 \forall d1: (\forall x,y,z:A.
315 (add x (mult y z)) = (mult (add x y) (add x z))).
316 \forall d2: (\forall x,y,z:A.
317 (mult x (add y z)) = (add (mult x y) (mult x z))).
318 \forall i1: (\forall x:A. (add x zero) = x).
319 \forall i2: (\forall x:A. (mult x one) = x).
320 \forall inv1: (\forall x:A. (add x (inv x)) = one).
321 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
323 (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u))).
324 intros.auto paramodulation.
331 \forall add: A \to A \to A.
332 \forall mult: A \to A \to A.
333 \forall inv: A \to A.
334 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
335 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
336 \forall d1: (\forall x,y,z:A.
337 (add x (mult y z)) = (mult (add x y) (add x z))).
338 \forall d2: (\forall x,y,z:A.
339 (mult x (add y z)) = (add (mult x y) (mult x z))).
340 \forall i1: (\forall x:A. (add x zero) = x).
341 \forall i2: (\forall x:A. (mult x one) = x).
342 \forall inv1: (\forall x:A. (add x (inv x)) = one).
343 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
345 add x (mult y z) = mult (add y x) (add x z).
346 intros.auto paramodulation.
349 theorem bool756minimal:
351 \forall add: A \to A \to A.
352 \forall mult: A \to A \to A.
353 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
354 \forall hint1: (\forall x,y,z,u:A.
355 add y (add x (mult x u)) = (add (mult (add x y) z) (add x (mult y u)))).
356 \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
358 add x (add y (mult y z)) = add x (add y (mult x z)).
363 theorem bool756simplified:
365 \forall add: A \to A \to A.
366 \forall mult: A \to A \to A.
367 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
368 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
369 \forall hint1: (\forall x,y,z,u:A.
370 (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u)))).
371 \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
372 \forall hint3: (\forall x,y,z:A.
373 add x (mult y z) = mult (add y x) (add x z)).
374 \forall hint4: (\forall x,y:A.
375 add x (mult x y) = mult x (add x y)).
377 add x (add y (mult y z)) = add x (add y (mult x z)).
387 \forall add: A \to A \to A.
388 \forall mult: A \to A \to A.
389 \forall inv: A \to A.
390 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
391 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
392 \forall d1: (\forall x,y,z:A.
393 (add x (mult y z)) = (mult (add x y) (add x z))).
394 \forall d2: (\forall x,y,z:A.
395 (mult x (add y z)) = (add (mult x y) (mult x z))).
396 \forall i1: (\forall x:A. (add x zero) = x).
397 \forall i2: (\forall x:A. (mult x one) = x).
398 \forall inv1: (\forall x:A. (add x (inv x)) = one).
399 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
400 \forall hint1: (\forall x,y,z,u:A.
401 (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u)))).
402 \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
403 \forall hint3: (\forall x,y,z:A.
404 add x (mult y z) = mult (add y x) (add x z)).
405 \forall hint4: (\forall x,y:A.
406 add x (mult x y) = mult x (add x y)).
408 add x y = add x (add y (mult x z)).
410 cut (mult (add y x) (add x (add y z)) = add x (add y (mult x z)));
412 |auto paramodulation]
420 \forall add: A \to A \to A.
421 \forall mult: A \to A \to A.
422 \forall inv: A \to A.
423 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
424 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
425 \forall d1: (\forall x,y,z:A.
426 (add x (mult y z)) = (mult (add x y) (add x z))).
427 \forall d2: (\forall x,y,z:A.
428 (mult x (add y z)) = (add (mult x y) (mult x z))).
429 \forall i1: (\forall x:A. (add x zero) = x).
430 \forall i2: (\forall x:A. (mult x one) = x).
431 \forall inv1: (\forall x:A. (add x (inv x)) = one).
432 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
434 add x y = add x (add y (mult x z)).
435 intros;auto paramodulation.
437 (* war=5; active 225, maxmeta 172568 *)
438 (* war=4; active 249, maxmeta 223220 *)
444 \forall add: A \to A \to A.
445 \forall mult: A \to A \to A.
446 \forall inv: A \to A.
447 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
448 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
449 \forall d1: (\forall x,y,z:A.
450 (add x (mult y z)) = (mult (add x y) (add x z))).
451 \forall d2: (\forall x,y,z:A.
452 (mult x (add y z)) = (add (mult x y) (mult x z))).
453 \forall i1: (\forall x:A. (add x zero) = x).
454 \forall i2: (\forall x:A. (mult x one) = x).
455 \forall inv1: (\forall x:A. (add x (inv x)) = one).
456 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
458 (add x y) = (add (add x (mult y z)) y).
459 intros.auto paramodulation.
466 \forall add: A \to A \to A.
467 \forall mult: A \to A \to A.
468 \forall inv: A \to A.
469 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
470 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
471 \forall d1: (\forall x,y,z:A.
472 (add x (mult y z)) = (mult (add x y) (add x z))).
473 \forall d2: (\forall x,y,z:A.
474 (mult x (add y z)) = (add (mult x y) (mult x z))).
475 \forall i1: (\forall x:A. (add x zero) = x).
476 \forall i2: (\forall x:A. (mult x one) = x).
477 \forall inv1: (\forall x:A. (add x (inv x)) = one).
478 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
480 \forall c1z: (\forall x:A.(add x z) = (add z x)).
481 add (add x y) z = add (add x y) (add z y).
482 intros.auto paramodulation.
489 \forall add: A \to A \to A.
490 \forall mult: A \to A \to A.
491 \forall inv: A \to A.
492 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
493 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
494 \forall d1: (\forall x,y,z:A.
495 (add x (mult y z)) = (mult (add x y) (add x z))).
496 \forall d2: (\forall x,y,z:A.
497 (mult x (add y z)) = (add (mult x y) (mult x z))).
498 \forall i1: (\forall x:A. (add x zero) = x).
499 \forall i2: (\forall x:A. (mult x one) = x).
500 \forall inv1: (\forall x:A. (add x (inv x)) = one).
501 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
503 add (add x y) z = add (add x y) (add z y).
504 intros.auto paramodulation.
511 \forall add: A \to A \to A.
512 \forall mult: A \to A \to A.
513 \forall inv: A \to A.
514 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
515 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
516 \forall d1: (\forall x,y,z:A.
517 (add x (mult y z)) = (mult (add x y) (add x z))).
518 \forall d2: (\forall x,y,z:A.
519 (mult x (add y z)) = (add (mult x y) (mult x z))).
520 \forall i1: (\forall x:A. (add x zero) = x).
521 \forall i2: (\forall x:A. (mult x one) = x).
522 \forall inv1: (\forall x:A. (add x (inv x)) = one).
523 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
525 add x (add y z) = add (add x z) y.
526 intros.auto paramodulation.
533 \forall add: A \to A \to A.
534 \forall mult: A \to A \to A.
535 \forall inv: A \to A.
536 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
537 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
538 \forall d1: (\forall x,y,z:A.
539 (add x (mult y z)) = (mult (add x y) (add x z))).
540 \forall d2: (\forall x,y,z:A.
541 (mult x (add y z)) = (add (mult x y) (mult x z))).
542 \forall i1: (\forall x:A. (add x zero) = x).
543 \forall i2: (\forall x:A. (mult x one) = x).
544 \forall inv1: (\forall x:A. (add x (inv x)) = one).
545 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
547 add (inv x) y = add (mult x y) (inv x).
548 intros.auto paramodulation.
555 \forall add: A \to A \to A.
556 \forall mult: A \to A \to A.
557 \forall inv: A \to A.
558 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
559 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
560 \forall d1: (\forall x,y,z:A.
561 (add x (mult y z)) = (mult (add x y) (add x z))).
562 \forall d2: (\forall x,y,z:A.
563 (mult x (add y z)) = (add (mult x y) (mult x z))).
564 \forall i1: (\forall x:A. (add x zero) = x).
565 \forall i2: (\forall x:A. (mult x one) = x).
566 \forall inv1: (\forall x:A. (add x (inv x)) = one).
567 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
568 \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
569 \forall hint1735:(\forall x,y:A. add (inv (add x y)) x = add x (inv y)).
570 \forall hint623:(\forall x,y:A. inv (mult x y) = add (inv x) (inv (mult x y))).
572 (inv (mult x y)) = (add (inv x) (inv y)).
573 intros.auto paramodulation.
581 \forall add: A \to A \to A.
582 \forall mult: A \to A \to A.
583 \forall inv: A \to A.
584 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
585 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
586 \forall d1: (\forall x,y,z:A.
587 (add x (mult y z)) = (mult (add x y) (add x z))).
588 \forall d2: (\forall x,y,z:A.
589 (mult x (add y z)) = (add (mult x y) (mult x z))).
590 \forall i1: (\forall x:A. (add x zero) = x).
591 \forall i2: (\forall x:A. (mult x one) = x).
592 \forall inv1: (\forall x:A. (add x (inv x)) = one).
593 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
594 \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
595 \forall hint623:(\forall x,y:A. inv (mult x y) = add (inv x) (inv (mult x y))).
597 (inv (mult x y)) = (add (inv x) (inv y)).
598 intros.auto paramodulation.
606 \forall add: A \to A \to A.
607 \forall mult: A \to A \to A.
608 \forall inv: A \to A.
609 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
610 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
611 \forall d1: (\forall x,y,z:A.
612 (add x (mult y z)) = (mult (add x y) (add x z))).
613 \forall d2: (\forall x,y,z:A.
614 (mult x (add y z)) = (add (mult x y) (mult x z))).
615 \forall i1: (\forall x:A. (add x zero) = x).
616 \forall i2: (\forall x:A. (mult x one) = x).
617 \forall inv1: (\forall x:A. (add x (inv x)) = one).
618 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
619 \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
620 \forall hint609:(\forall x,y:A. inv x = add (inv (add y x)) (inv x)).
622 (inv (mult x y)) = (add (inv x) (inv y)).
623 intros.auto paramodulation.
631 \forall add: A \to A \to A.
632 \forall mult: A \to A \to A.
633 \forall inv: A \to A.
634 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
635 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
636 \forall d1: (\forall x,y,z:A.
637 (add x (mult y z)) = (mult (add x y) (add x z))).
638 \forall d2: (\forall x,y,z:A.
639 (mult x (add y z)) = (add (mult x y) (mult x z))).
640 \forall i1: (\forall x:A. (add x zero) = x).
641 \forall i2: (\forall x:A. (mult x one) = x).
642 \forall inv1: (\forall x:A. (add x (inv x)) = one).
643 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
645 (inv (mult x y)) = (add (inv x) (inv y)).
646 intros.auto paramodulation.