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