helm/software/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 set "baseuri" "cic:/matita/SK/".
  16
  17 include "legacy/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.auto 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.auto 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.auto 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.auto 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.auto 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.auto 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.auto 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.auto 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.auto 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.auto 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   (*
 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)).
 250   *)
 251   \forall x,y:A.
 252     inv x =  (add (inv x) (inv (add y x))).
 253 intros.auto paramodulation.
 254 qed.
 255
 256 theorem bool609:
 257   \forall A:Set.
 258   \forall one:A.
 259   \forall zero:A.
 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).
 273   (*
 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)).
 277   *)
 278   \forall x,y:A.
 279     inv x =  (add (inv (add y x)) (inv x)).
 280 intros.auto paramodulation.
 281 qed.
 282 (*
 283 theorem bool260:
 284   \forall A:Set.
 285   \forall one:A.
 286   \forall zero:A.
 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).
 300   \forall x,y,z:A.
 301     add x (mult x y) = mult x (add x y).
 302 intros.auto paramodulation.
 303 qed.
 304
 305 theorem bool276:
 306   \forall A:Set.
 307   \forall one:A.
 308   \forall zero:A.
 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).
 322   \forall x,y,z,u:A.
 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.
 325 qed.
 326
 327 theorem bool250:
 328   \forall A:Set.
 329   \forall one:A.
 330   \forall zero:A.
 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).
 344   \forall x,y,z:A.
 345     add x (mult y z) = mult (add y x) (add x z).
 346 intros.auto paramodulation.
 347 qed.
 348
 349 theorem bool756minimal:
 350   \forall A:Set.
 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)).
 357   \forall x,y,z:A.
 358     add x (add y (mult y z)) = add x (add y (mult x z)).
 359 intros;
 360 auto paramodulation.
 361 qed.
 362
 363 theorem bool756simplified:
 364   \forall A:Set.
 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)).
 376   \forall x,y,z:A.
 377     add x (add y (mult y z)) = add x (add y (mult x z)).
 378 intros;
 379 auto paramodulation.
 380 qed.
 381 (* 46 sec. *)
 382
 383 theorem bool756:
 384   \forall A:Set.
 385   \forall one:A.
 386   \forall zero:A.
 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)).
 407   \forall x,y,z:A.
 408     add x y = add x (add y (mult x z)).
 409 intros;
 410 cut (mult (add y x) (add x (add y z)) = add x (add y (mult x z)));
 411 [auto paramodulation
 412 |auto paramodulation]
 413 qed.
 414 (*  186 sec *)
 415 *)
 416 theorem bool756full:
 417   \forall A:Set.
 418   \forall one:A.
 419   \forall zero:A.
 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).
 433   \forall x,y,z:A.
 434     add x y = add x (add y (mult x z)).
 435 intros;auto paramodulation.
 436 qed.
 437 (* war=5; active 225, maxmeta 172568 *)
 438 (* war=4; active 249, maxmeta 223220 *)
 439 (*
 440 theorem bool1164:
 441   \forall A:Set.
 442   \forall one:A.
 443   \forall zero:A.
 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).
 457   \forall x,y,z:A.
 458     (add x y) = (add (add x (mult y z)) y).
 459 intros.auto paramodulation.
 460 qed.
 461
 462 theorem bool1230:
 463   \forall A:Set.
 464   \forall one:A.
 465   \forall zero:A.
 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).
 479   \forall x,y,z:A.
 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.
 483 qed.
 484
 485 theorem bool1230:
 486   \forall A:Set.
 487   \forall one:A.
 488   \forall zero:A.
 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).
 502   \forall x,y,z:A.
 503     add (add x y) z = add (add x y) (add z y).
 504 intros.auto paramodulation.
 505 qed.
 506
 507 theorem bool1372:
 508   \forall A:Set.
 509   \forall one:A.
 510   \forall zero:A.
 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).
 524   \forall x,y,z:A.
 525     add x (add y z) = add (add x z) y.
 526 intros.auto paramodulation.
 527 qed.*)
 528
 529 theorem bool381:
 530   \forall A:Set.
 531   \forall one:A.
 532   \forall zero:A.
 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).
 546   \forall x,y:A.
 547       add (inv x) y = add (mult x y) (inv x).
 548 intros.auto paramodulation.
 549 qed.
 550
 551 theorem bool5hint1:
 552   \forall A:Set.
 553   \forall one:A.
 554   \forall zero:A.
 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))).
 571   \forall x,y:A.
 572     (inv (mult x y)) = (add (inv x) (inv y)).
 573 intros.auto paramodulation.
 574 qed.
 575 (* 90 *)
 576
 577 theorem bool5hint2:
 578   \forall A:Set.
 579   \forall one:A.
 580   \forall zero:A.
 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))).
 596   \forall x,y:A.
 597     (inv (mult x y)) = (add (inv x) (inv y)).
 598 intros.auto paramodulation.
 599 qed.
 600 (* 41 *)
 601
 602 theorem bool5hint3:
 603   \forall A:Set.
 604   \forall one:A.
 605   \forall zero:A.
 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)).
 621   \forall x,y:A.
 622     (inv (mult x y)) = (add (inv x) (inv y)).
 623 intros.auto paramodulation.
 624 qed.
 625 (* 41 *)
 626
 627 theorem bool5:
 628   \forall A:Set.
 629   \forall one:A.
 630   \forall zero:A.
 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).
 644   \forall x,y:A.
 645     (inv (mult x y)) = (add (inv x) (inv y)).
 646 intros.auto paramodulation.
 647 qed.
 648
 649 *)