]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/tests/bool.ma
update in basic_2
[helm.git] / matitaB / matita / tests / bool.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15
16
17 include "coq.ma".
18
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".
24
25 (* 
26
27 theorem SKK:
28   \forall A:Set.
29   \forall app: A \to A \to A.
30   \forall K:A. 
31   \forall S: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))).
35   \forall x:A.
36     (app (app (app S K) K) x) = x.
37 intros.autobatch paramodulation.
38 qed.
39
40 theorem bool1:
41   \forall A:Set.
42   \forall one:A.
43   \forall zero:A.
44   \forall add: A \to A \to A.
45   \forall mult: A \to A \to A.
46   \forall inv: 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). 
57   (inv zero) = one.
58 intros.autobatch paramodulation.
59 qed.
60   
61 theorem bool2:
62   \forall A:Set.
63   \forall one:A.
64   \forall zero:A.
65   \forall add: A \to A \to A.
66   \forall mult: A \to A \to A.
67   \forall inv: 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.autobatch paramodulation.
80 qed.
81
82 theorem bool3:
83   \forall A:Set.
84   \forall one:A.
85   \forall zero:A.
86   \forall add: A \to A \to A.
87   \forall mult: A \to A \to A.
88   \forall inv: 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.autobatch paramodulation.
101 qed.
102
103 theorem bool266:
104   \forall A:Set.
105   \forall one:A.
106   \forall zero:A.
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.autobatch paramodulation.
122 qed.
123 *)
124 theorem bool507:
125   \forall A:Set.
126   \forall one:A.
127   \forall zero:A.
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.autobatch paramodulation.
143 qed.
144 (*
145 theorem bool515:
146   \forall A:Set.
147   \forall one:A.
148   \forall zero:A.
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.autobatch paramodulation.
164 qed.
165
166 theorem bool304:
167   \forall A:Set.
168   \forall one:A.
169   \forall zero:A.
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.autobatch paramodulation.
185 qed.
186
187 theorem bool531:
188   \forall A:Set.
189   \forall one:A.
190   \forall zero:A.
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.autobatch paramodulation.
206 qed.
207
208 theorem bool253:
209   \forall A:Set.
210   \forall one:A.
211   \forall zero:A.
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.autobatch paramodulation.
227 qed.
228
229 theorem bool557:
230   \forall A:Set.
231   \forall one:A.
232   \forall zero:A.
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). 
246   \forall x,y:A. 
247     inv x =  (add (inv x) (inv (add y x))).
248 intros.autobatch paramodulation.
249 qed.
250
251 theorem bool609:
252   \forall A:Set.
253   \forall one:A.
254   \forall zero:A.
255   \forall add: A \to A \to A.
256   \forall mult: A \to A \to A.
257   \forall inv: A \to A.
258   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
259   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
260   \forall d1: (\forall x,y,z:A.
261               (add x (mult y z)) = (mult (add x y) (add x z))).
262   \forall d2: (\forall x,y,z:A.
263               (mult x (add y z)) = (add (mult x y) (mult x z))).  
264   \forall i1: (\forall x:A. (add x zero) = x).
265   \forall i2: (\forall x:A. (mult x one) = x).   
266   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
267   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
268   \forall x,y:A. 
269     inv x =  (add (inv (add y x)) (inv x)).
270 intros.autobatch paramodulation.
271 qed.
272 (*
273 theorem bool260:
274   \forall A:Set.
275   \forall one:A.
276   \forall zero:A.
277   \forall add: A \to A \to A.
278   \forall mult: A \to A \to A.
279   \forall inv: A \to A.
280   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
281   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
282   \forall d1: (\forall x,y,z:A.
283               (add x (mult y z)) = (mult (add x y) (add x z))).
284   \forall d2: (\forall x,y,z:A.
285               (mult x (add y z)) = (add (mult x y) (mult x z))).  
286   \forall i1: (\forall x:A. (add x zero) = x).
287   \forall i2: (\forall x:A. (mult x one) = x).   
288   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
289   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
290   \forall x,y,z:A. 
291     add x (mult x y) = mult x (add x y).
292 intros.autobatch paramodulation.
293 qed.
294
295 theorem bool276:
296   \forall A:Set.
297   \forall one:A.
298   \forall zero:A.
299   \forall add: A \to A \to A.
300   \forall mult: A \to A \to A.
301   \forall inv: A \to A.
302   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
303   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
304   \forall d1: (\forall x,y,z:A.
305               (add x (mult y z)) = (mult (add x y) (add x z))).
306   \forall d2: (\forall x,y,z:A.
307               (mult x (add y z)) = (add (mult x y) (mult x z))).  
308   \forall i1: (\forall x:A. (add x zero) = x).
309   \forall i2: (\forall x:A. (mult x one) = x).   
310   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
311   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
312   \forall x,y,z,u:A. 
313     (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u))).
314 intros.autobatch paramodulation.
315 qed. 
316
317 theorem bool250:
318   \forall A:Set.
319   \forall one:A.
320   \forall zero:A.
321   \forall add: A \to A \to A.
322   \forall mult: A \to A \to A.
323   \forall inv: A \to A.
324   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
325   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
326   \forall d1: (\forall x,y,z:A.
327               (add x (mult y z)) = (mult (add x y) (add x z))).
328   \forall d2: (\forall x,y,z:A.
329               (mult x (add y z)) = (add (mult x y) (mult x z))).  
330   \forall i1: (\forall x:A. (add x zero) = x).
331   \forall i2: (\forall x:A. (mult x one) = x).   
332   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
333   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
334   \forall x,y,z:A. 
335     add x (mult y z) = mult (add y x) (add x z).
336 intros.autobatch paramodulation.
337 qed. 
338
339 theorem bool756minimal:
340   \forall A:Set.
341   \forall add: A \to A \to A.
342   \forall mult: A \to A \to A.
343   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
344   \forall hint1: (\forall x,y,z,u:A. 
345     add y (add x (mult x u)) = (add (mult (add x y) z) (add x (mult y u)))).
346   \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
347   \forall x,y,z:A. 
348     add x (add y (mult y z)) = add x (add y (mult x z)).
349 intros;
350 autobatch paramodulation.
351 qed.
352
353 theorem bool756simplified:
354   \forall A:Set.
355   \forall add: A \to A \to A.
356   \forall mult: A \to A \to A.
357   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
358   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
359   \forall hint1: (\forall x,y,z,u:A. 
360     (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u)))).
361   \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
362   \forall hint3: (\forall x,y,z:A. 
363     add x (mult y z) = mult (add y x) (add x z)).
364   \forall hint4: (\forall x,y:A. 
365     add x (mult x y) = mult x (add x y)).
366   \forall x,y,z:A. 
367     add x (add y (mult y z)) = add x (add y (mult x z)).
368 intros;
369 autobatch paramodulation.
370 qed.
371
372 theorem bool756:
373   \forall A:Set.
374   \forall one:A.
375   \forall zero:A.
376   \forall add: A \to A \to A.
377   \forall mult: A \to A \to A.
378   \forall inv: A \to A.
379   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
380   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
381   \forall d1: (\forall x,y,z:A.
382               (add x (mult y z)) = (mult (add x y) (add x z))).
383   \forall d2: (\forall x,y,z:A.
384               (mult x (add y z)) = (add (mult x y) (mult x z))).  
385   \forall i1: (\forall x:A. (add x zero) = x).
386   \forall i2: (\forall x:A. (mult x one) = x).   
387   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
388   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
389   \forall hint1: (\forall x,y,z,u:A. 
390     (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u)))).
391   \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
392   \forall hint3: (\forall x,y,z:A. 
393     add x (mult y z) = mult (add y x) (add x z)).
394   \forall hint4: (\forall x,y:A. 
395     add x (mult x y) = mult x (add x y)).
396   \forall x,y,z:A. 
397     add x y = add x (add y (mult x z)).
398 intros;
399 cut (mult (add y x) (add x (add y z)) = add x (add y (mult x z)));
400 [autobatch paramodulation
401 |autobatch paramodulation]
402 qed.
403
404 theorem bool756full:
405   \forall A:Set.
406   \forall one:A.
407   \forall zero:A.
408   \forall add: A \to A \to A.
409   \forall mult: A \to A \to A.
410   \forall inv: A \to A.
411   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
412   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
413   \forall d1: (\forall x,y,z:A.
414               (add x (mult y z)) = (mult (add x y) (add x z))).
415   \forall d2: (\forall x,y,z:A.
416               (mult x (add y z)) = (add (mult x y) (mult x z))).  
417   \forall i1: (\forall x:A. (add x zero) = x).
418   \forall i2: (\forall x:A. (mult x one) = x).   
419   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
420   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
421   \forall x,y,z:A. 
422     add x y = add x (add y (mult x z)).
423 intros;autobatch paramodulation.
424 qed.
425
426 theorem bool1164:
427   \forall A:Set.
428   \forall one:A.
429   \forall zero:A.
430   \forall add: A \to A \to A.
431   \forall mult: A \to A \to A.
432   \forall inv: A \to A.
433   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
434   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
435   \forall d1: (\forall x,y,z:A.
436               (add x (mult y z)) = (mult (add x y) (add x z))).
437   \forall d2: (\forall x,y,z:A.
438               (mult x (add y z)) = (add (mult x y) (mult x z))).  
439   \forall i1: (\forall x:A. (add x zero) = x).
440   \forall i2: (\forall x:A. (mult x one) = x).   
441   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
442   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
443   \forall x,y,z:A.
444     (add x y) = (add (add x (mult y z)) y).
445 intros.autobatch paramodulation.
446 qed.
447
448 theorem bool1230:
449   \forall A:Set.
450   \forall one:A.
451   \forall zero:A.
452   \forall add: A \to A \to A.
453   \forall mult: A \to A \to A.
454   \forall inv: A \to A.
455   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
456   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
457   \forall d1: (\forall x,y,z:A.
458               (add x (mult y z)) = (mult (add x y) (add x z))).
459   \forall d2: (\forall x,y,z:A.
460               (mult x (add y z)) = (add (mult x y) (mult x z))).  
461   \forall i1: (\forall x:A. (add x zero) = x).
462   \forall i2: (\forall x:A. (mult x one) = x).   
463   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
464   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
465   \forall x,y,z:A.
466   \forall c1z: (\forall x:A.(add x z) = (add z x)). 
467     add (add x y) z = add (add x y) (add z y).
468 intros.autobatch paramodulation.
469 qed.
470
471 theorem bool1230:
472   \forall A:Set.
473   \forall one:A.
474   \forall zero:A.
475   \forall add: A \to A \to A.
476   \forall mult: A \to A \to A.
477   \forall inv: A \to A.
478   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
479   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
480   \forall d1: (\forall x,y,z:A.
481               (add x (mult y z)) = (mult (add x y) (add x z))).
482   \forall d2: (\forall x,y,z:A.
483               (mult x (add y z)) = (add (mult x y) (mult x z))).  
484   \forall i1: (\forall x:A. (add x zero) = x).
485   \forall i2: (\forall x:A. (mult x one) = x).   
486   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
487   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
488   \forall x,y,z:A.
489     add (add x y) z = add (add x y) (add z y).
490 intros.autobatch paramodulation.
491 qed.
492
493 theorem bool1372:
494   \forall A:Set.
495   \forall one:A.
496   \forall zero:A.
497   \forall add: A \to A \to A.
498   \forall mult: A \to A \to A.
499   \forall inv: A \to A.
500   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
501   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
502   \forall d1: (\forall x,y,z:A.
503               (add x (mult y z)) = (mult (add x y) (add x z))).
504   \forall d2: (\forall x,y,z:A.
505               (mult x (add y z)) = (add (mult x y) (mult x z))).  
506   \forall i1: (\forall x:A. (add x zero) = x).
507   \forall i2: (\forall x:A. (mult x one) = x).   
508   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
509   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
510   \forall x,y,z:A.
511     add x (add y z) = add (add x z) y.
512 intros.autobatch paramodulation.
513 qed.
514
515 theorem bool381:
516   \forall A:Set.
517   \forall one:A.
518   \forall zero:A.
519   \forall add: A \to A \to A.
520   \forall mult: A \to A \to A.
521   \forall inv: A \to A.
522   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
523   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
524   \forall d1: (\forall x,y,z:A.
525               (add x (mult y z)) = (mult (add x y) (add x z))).
526   \forall d2: (\forall x,y,z:A.
527               (mult x (add y z)) = (add (mult x y) (mult x z))).  
528   \forall i1: (\forall x:A. (add x zero) = x).
529   \forall i2: (\forall x:A. (mult x one) = x).   
530   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
531   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
532   \forall x,y:A.
533       add (inv x) y = add (mult x y) (inv x).
534 intros.autobatch paramodulation.
535 qed.
536
537 theorem bool5hint1:
538   \forall A:Set.
539   \forall one:A.
540   \forall zero:A.
541   \forall add: A \to A \to A.
542   \forall mult: A \to A \to A.
543   \forall inv: A \to A.
544   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
545   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
546   \forall d1: (\forall x,y,z:A.
547               (add x (mult y z)) = (mult (add x y) (add x z))).
548   \forall d2: (\forall x,y,z:A.
549               (mult x (add y z)) = (add (mult x y) (mult x z))).  
550   \forall i1: (\forall x:A. (add x zero) = x).
551   \forall i2: (\forall x:A. (mult x one) = x).   
552   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
553   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
554   \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
555   \forall hint1735:(\forall x,y:A. add (inv (add x y)) x = add x (inv y)).
556   \forall hint623:(\forall x,y:A. inv (mult x y) = add (inv x) (inv (mult x y))).
557   \forall x,y:A.
558     (inv (mult x y)) = (add (inv x) (inv y)).
559 intros.autobatch paramodulation.
560 qed.
561
562 theorem bool5hint2:
563   \forall A:Set.
564   \forall one:A.
565   \forall zero:A.
566   \forall add: A \to A \to A.
567   \forall mult: A \to A \to A.
568   \forall inv: A \to A.
569   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
570   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
571   \forall d1: (\forall x,y,z:A.
572               (add x (mult y z)) = (mult (add x y) (add x z))).
573   \forall d2: (\forall x,y,z:A.
574               (mult x (add y z)) = (add (mult x y) (mult x z))).  
575   \forall i1: (\forall x:A. (add x zero) = x).
576   \forall i2: (\forall x:A. (mult x one) = x).   
577   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
578   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
579   \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
580   \forall hint623:(\forall x,y:A. inv (mult x y) = add (inv x) (inv (mult x y))).
581   \forall x,y:A.
582     (inv (mult x y)) = (add (inv x) (inv y)).
583 intros.autobatch paramodulation.
584 qed.
585
586 theorem bool5hint3:
587   \forall A:Set.
588   \forall one:A.
589   \forall zero:A.
590   \forall add: A \to A \to A.
591   \forall mult: A \to A \to A.
592   \forall inv: A \to A.
593   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
594   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
595   \forall d1: (\forall x,y,z:A.
596               (add x (mult y z)) = (mult (add x y) (add x z))).
597   \forall d2: (\forall x,y,z:A.
598               (mult x (add y z)) = (add (mult x y) (mult x z))).  
599   \forall i1: (\forall x:A. (add x zero) = x).
600   \forall i2: (\forall x:A. (mult x one) = x).   
601   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
602   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
603   \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
604   \forall hint609:(\forall x,y:A. inv x = add (inv (add y x)) (inv x)).
605   \forall x,y:A.
606     (inv (mult x y)) = (add (inv x) (inv y)).
607 intros.autobatch paramodulation.
608 qed.
609
610 theorem bool5:
611   \forall A:Set.
612   \forall one:A.
613   \forall zero:A.
614   \forall add: A \to A \to A.
615   \forall mult: A \to A \to A.
616   \forall inv: A \to A.
617   \forall c1:(\forall x,y:A.(add x y) = (add y x)). 
618   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)). 
619   \forall d1: (\forall x,y,z:A.
620               (add x (mult y z)) = (mult (add x y) (add x z))).
621   \forall d2: (\forall x,y,z:A.
622               (mult x (add y z)) = (add (mult x y) (mult x z))).  
623   \forall i1: (\forall x:A. (add x zero) = x).
624   \forall i2: (\forall x:A. (mult x one) = x).   
625   \forall inv1: (\forall x:A. (add x (inv x)) = one).  
626   \forall inv2: (\forall x:A. (mult x (inv x)) = zero). 
627   \forall x,y:A.
628     (inv (mult x y)) = (add (inv x) (inv y)).
629 intros.autobatch paramodulation.
630 qed.
631
632 *)*)
633