matita/tests/SK.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 theorem SKK:
  26   \forall A:Set.
  27   \forall app: A \to A \to A.
  28   \forall K:A.
  29   \forall S:A.
  30   \forall H1: (\forall x,y:A.(app (app K x) y) = x).
  31   \forall H2: (\forall x,y,z:A.
  32     (app (app (app S x) y) z) = (app (app x z) (app y z))).
  33   \forall x:A.
  34     (app (app (app S K) K) x) = x.
  35 intros.auto paramodulation.
  36 qed.
  37
  38 theorem bool1:
  39   \forall A:Set.
  40   \forall one:A.
  41   \forall zero:A.
  42   \forall add: A \to A \to A.
  43   \forall mult: A \to A \to A.
  44   \forall inv: A \to A.
  45   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
  46   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
  47   \forall d1: (\forall x,y,z:A.
  48               (add x (mult y z)) = (mult (add x y) (add x z))).
  49   \forall d2: (\forall x,y,z:A.
  50               (mult x (add y z)) = (add (mult x y) (mult x z))).
  51   \forall i1: (\forall x:A. (add x zero) = x).
  52   \forall i2: (\forall x:A. (mult x one) = x).
  53   \forall inv1: (\forall x:A. (add x (inv x)) = one).
  54   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
  55   (inv zero) = one.
  56 intros.auto paramodulation.
  57 qed.
  58
  59 theorem bool2:
  60   \forall A:Set.
  61   \forall one:A.
  62   \forall zero:A.
  63   \forall add: A \to A \to A.
  64   \forall mult: A \to A \to A.
  65   \forall inv: A \to A.
  66   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
  67   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
  68   \forall d1: (\forall x,y,z:A.
  69               (add x (mult y z)) = (mult (add x y) (add x z))).
  70   \forall d2: (\forall x,y,z:A.
  71               (mult x (add y z)) = (add (mult x y) (mult x z))).
  72   \forall i1: (\forall x:A. (add x zero) = x).
  73   \forall i2: (\forall x:A. (mult x one) = x).
  74   \forall inv1: (\forall x:A. (add x (inv x)) = one).
  75   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
  76   \forall x:A. (mult x zero) = zero.
  77 intros.auto paramodulation.
  78 qed.
  79
  80 theorem bool3:
  81   \forall A:Set.
  82   \forall one:A.
  83   \forall zero:A.
  84   \forall add: A \to A \to A.
  85   \forall mult: A \to A \to A.
  86   \forall inv: A \to A.
  87   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
  88   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
  89   \forall d1: (\forall x,y,z:A.
  90               (add x (mult y z)) = (mult (add x y) (add x z))).
  91   \forall d2: (\forall x,y,z:A.
  92               (mult x (add y z)) = (add (mult x y) (mult x z))).
  93   \forall i1: (\forall x:A. (add x zero) = x).
  94   \forall i2: (\forall x:A. (mult x one) = x).
  95   \forall inv1: (\forall x:A. (add x (inv x)) = one).
  96   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
  97   \forall x:A. (inv (inv x)) = x.
  98 intros.auto paramodulation.
  99 qed.
 100
 101 theorem bool266:
 102   \forall A:Set.
 103   \forall one:A.
 104   \forall zero:A.
 105   \forall add: A \to A \to A.
 106   \forall mult: A \to A \to A.
 107   \forall inv: A \to A.
 108   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 109   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 110   \forall d1: (\forall x,y,z:A.
 111               (add x (mult y z)) = (mult (add x y) (add x z))).
 112   \forall d2: (\forall x,y,z:A.
 113               (mult x (add y z)) = (add (mult x y) (mult x z))).
 114   \forall i1: (\forall x:A. (add x zero) = x).
 115   \forall i2: (\forall x:A. (mult x one) = x).
 116   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 117   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 118   \forall x,y:A. (mult x (add (inv x) y)) = (mult x y).
 119 intros.auto paramodulation.
 120 qed.
 121
 122 theorem bool507:
 123   \forall A:Set.
 124   \forall one:A.
 125   \forall zero:A.
 126   \forall add: A \to A \to A.
 127   \forall mult: A \to A \to A.
 128   \forall inv: A \to A.
 129   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 130   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 131   \forall d1: (\forall x,y,z:A.
 132               (add x (mult y z)) = (mult (add x y) (add x z))).
 133   \forall d2: (\forall x,y,z:A.
 134               (mult x (add y z)) = (add (mult x y) (mult x z))).
 135   \forall i1: (\forall x:A. (add x zero) = x).
 136   \forall i2: (\forall x:A. (mult x one) = x).
 137   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 138   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 139   \forall x,y:A. zero = (mult x (mult (inv x) y)).
 140 intros.auto paramodulation.
 141 qed.
 142
 143 theorem bool515:
 144   \forall A:Set.
 145   \forall one:A.
 146   \forall zero:A.
 147   \forall add: A \to A \to A.
 148   \forall mult: A \to A \to A.
 149   \forall inv: A \to A.
 150   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 151   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 152   \forall d1: (\forall x,y,z:A.
 153               (add x (mult y z)) = (mult (add x y) (add x z))).
 154   \forall d2: (\forall x,y,z:A.
 155               (mult x (add y z)) = (add (mult x y) (mult x z))).
 156   \forall i1: (\forall x:A. (add x zero) = x).
 157   \forall i2: (\forall x:A. (mult x one) = x).
 158   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 159   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 160   \forall x,y:A. zero = mult (inv x) (mult x y).
 161 intros.auto paramodulation.
 162 qed.
 163
 164 theorem bool304:
 165   \forall A:Set.
 166   \forall one:A.
 167   \forall zero:A.
 168   \forall add: A \to A \to A.
 169   \forall mult: A \to A \to A.
 170   \forall inv: A \to A.
 171   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 172   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 173   \forall d1: (\forall x,y,z:A.
 174               (add x (mult y z)) = (mult (add x y) (add x z))).
 175   \forall d2: (\forall x,y,z:A.
 176               (mult x (add y z)) = (add (mult x y) (mult x z))).
 177   \forall i1: (\forall x:A. (add x zero) = x).
 178   \forall i2: (\forall x:A. (mult x one) = x).
 179   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 180   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 181   \forall x,y:A. x = (mult (add y x) x).
 182 intros.auto paramodulation.
 183 qed.
 184
 185 theorem bool531:
 186   \forall A:Set.
 187   \forall one:A.
 188   \forall zero:A.
 189   \forall add: A \to A \to A.
 190   \forall mult: A \to A \to A.
 191   \forall inv: A \to A.
 192   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 193   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 194   \forall d1: (\forall x,y,z:A.
 195               (add x (mult y z)) = (mult (add x y) (add x z))).
 196   \forall d2: (\forall x,y,z:A.
 197               (mult x (add y z)) = (add (mult x y) (mult x z))).
 198   \forall i1: (\forall x:A. (add x zero) = x).
 199   \forall i2: (\forall x:A. (mult x one) = x).
 200   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 201   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 202   \forall x,y:A. zero = (mult (inv (add x y)) y).
 203 intros.auto paramodulation.
 204 qed.
 205
 206 theorem bool253:
 207   \forall A:Set.
 208   \forall one:A.
 209   \forall zero:A.
 210   \forall add: A \to A \to A.
 211   \forall mult: A \to A \to A.
 212   \forall inv: A \to A.
 213   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 214   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 215   \forall d1: (\forall x,y,z:A.
 216               (add x (mult y z)) = (mult (add x y) (add x z))).
 217   \forall d2: (\forall x,y,z:A.
 218               (mult x (add y z)) = (add (mult x y) (mult x z))).
 219   \forall i1: (\forall x:A. (add x zero) = x).
 220   \forall i2: (\forall x:A. (mult x one) = x).
 221   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 222   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 223   \forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y).
 224 intros.auto paramodulation.
 225 qed.
 226
 227 theorem bool557:
 228   \forall A:Set.
 229   \forall one:A.
 230   \forall zero:A.
 231   \forall add: A \to A \to A.
 232   \forall mult: A \to A \to A.
 233   \forall inv: A \to A.
 234   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 235   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 236   \forall d1: (\forall x,y,z:A.
 237               (add x (mult y z)) = (mult (add x y) (add x z))).
 238   \forall d2: (\forall x,y,z:A.
 239               (mult x (add y z)) = (add (mult x y) (mult x z))).
 240   \forall i1: (\forall x:A. (add x zero) = x).
 241   \forall i2: (\forall x:A. (mult x one) = x).
 242   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 243   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 244   (*
 245   \forall hint1: (\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y)).
 246   \forall hint2: \forall x,y:A.zero = (mult (inv x) (mult x y)).
 247   \forall hint2: (\forall x,y:A. zero = (mult (inv (add x y)) y)).
 248   *)
 249   \forall x,y:A.
 250     inv x =  (add (inv x) (inv (add y x))).
 251 intros.auto paramodulation.
 252 qed.
 253
 254 theorem bool609:
 255   \forall A:Set.
 256   \forall one:A.
 257   \forall zero:A.
 258   \forall add: A \to A \to A.
 259   \forall mult: A \to A \to A.
 260   \forall inv: A \to A.
 261   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 262   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 263   \forall d1: (\forall x,y,z:A.
 264               (add x (mult y z)) = (mult (add x y) (add x z))).
 265   \forall d2: (\forall x,y,z:A.
 266               (mult x (add y z)) = (add (mult x y) (mult x z))).
 267   \forall i1: (\forall x:A. (add x zero) = x).
 268   \forall i2: (\forall x:A. (mult x one) = x).
 269   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 270   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 271   (*
 272   \forall hint1: (\forall x,y:A. (add (inv x) (mult y x)) = (add (inv x) y)).
 273   \forall hint2: \forall x,y:A.zero = (mult (inv x) (mult x y)).
 274   \forall hint2: (\forall x,y:A. zero = (mult (inv (add x y)) y)).
 275   *)
 276   \forall x,y:A.
 277     inv x =  (add (inv (add y x)) (inv x)).
 278 intros.auto paramodulation.
 279 qed.
 280 (*
 281 theorem bool260:
 282   \forall A:Set.
 283   \forall one:A.
 284   \forall zero:A.
 285   \forall add: A \to A \to A.
 286   \forall mult: A \to A \to A.
 287   \forall inv: A \to A.
 288   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 289   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 290   \forall d1: (\forall x,y,z:A.
 291               (add x (mult y z)) = (mult (add x y) (add x z))).
 292   \forall d2: (\forall x,y,z:A.
 293               (mult x (add y z)) = (add (mult x y) (mult x z))).
 294   \forall i1: (\forall x:A. (add x zero) = x).
 295   \forall i2: (\forall x:A. (mult x one) = x).
 296   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 297   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 298   \forall x,y,z:A.
 299     add x (mult x y) = mult x (add x y).
 300 intros.auto paramodulation.
 301 qed.
 302
 303 theorem bool276:
 304   \forall A:Set.
 305   \forall one:A.
 306   \forall zero:A.
 307   \forall add: A \to A \to A.
 308   \forall mult: A \to A \to A.
 309   \forall inv: A \to A.
 310   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 311   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 312   \forall d1: (\forall x,y,z:A.
 313               (add x (mult y z)) = (mult (add x y) (add x z))).
 314   \forall d2: (\forall x,y,z:A.
 315               (mult x (add y z)) = (add (mult x y) (mult x z))).
 316   \forall i1: (\forall x:A. (add x zero) = x).
 317   \forall i2: (\forall x:A. (mult x one) = x).
 318   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 319   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 320   \forall x,y,z,u:A.
 321     (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u))).
 322 intros.auto paramodulation.
 323 qed.
 324
 325 theorem bool250:
 326   \forall A:Set.
 327   \forall one:A.
 328   \forall zero:A.
 329   \forall add: A \to A \to A.
 330   \forall mult: A \to A \to A.
 331   \forall inv: A \to A.
 332   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 333   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 334   \forall d1: (\forall x,y,z:A.
 335               (add x (mult y z)) = (mult (add x y) (add x z))).
 336   \forall d2: (\forall x,y,z:A.
 337               (mult x (add y z)) = (add (mult x y) (mult x z))).
 338   \forall i1: (\forall x:A. (add x zero) = x).
 339   \forall i2: (\forall x:A. (mult x one) = x).
 340   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 341   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 342   \forall x,y,z:A.
 343     add x (mult y z) = mult (add y x) (add x z).
 344 intros.auto paramodulation.
 345 qed.
 346
 347 theorem bool756minimal:
 348   \forall A:Set.
 349   \forall add: A \to A \to A.
 350   \forall mult: A \to A \to A.
 351   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 352   \forall hint1: (\forall x,y,z,u:A.
 353     add y (add x (mult x u)) = (add (mult (add x y) z) (add x (mult y u)))).
 354   \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
 355   \forall x,y,z:A.
 356     add x (add y (mult y z)) = add x (add y (mult x z)).
 357 intros;
 358 auto paramodulation.
 359 qed.
 360
 361 theorem bool756simplified:
 362   \forall A:Set.
 363   \forall add: A \to A \to A.
 364   \forall mult: A \to A \to A.
 365   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 366   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 367   \forall hint1: (\forall x,y,z,u:A.
 368     (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u)))).
 369   \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
 370   \forall hint3: (\forall x,y,z:A.
 371     add x (mult y z) = mult (add y x) (add x z)).
 372   \forall hint4: (\forall x,y:A.
 373     add x (mult x y) = mult x (add x y)).
 374   \forall x,y,z:A.
 375     add x (add y (mult y z)) = add x (add y (mult x z)).
 376 intros;
 377 auto paramodulation.
 378 qed.
 379 (* 46 sec. *)
 380
 381 theorem bool756:
 382   \forall A:Set.
 383   \forall one:A.
 384   \forall zero:A.
 385   \forall add: A \to A \to A.
 386   \forall mult: A \to A \to A.
 387   \forall inv: A \to A.
 388   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 389   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 390   \forall d1: (\forall x,y,z:A.
 391               (add x (mult y z)) = (mult (add x y) (add x z))).
 392   \forall d2: (\forall x,y,z:A.
 393               (mult x (add y z)) = (add (mult x y) (mult x z))).
 394   \forall i1: (\forall x:A. (add x zero) = x).
 395   \forall i2: (\forall x:A. (mult x one) = x).
 396   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 397   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 398   \forall hint1: (\forall x,y,z,u:A.
 399     (mult (add x y) (add z (add x u))) = (add (mult (add x y) z) (add x (mult y u)))).
 400   \forall hint2: (\forall x,y:A. x = (mult (add y x) x)).
 401   \forall hint3: (\forall x,y,z:A.
 402     add x (mult y z) = mult (add y x) (add x z)).
 403   \forall hint4: (\forall x,y:A.
 404     add x (mult x y) = mult x (add x y)).
 405   \forall x,y,z:A.
 406     add x y = add x (add y (mult x z)).
 407 intros;
 408 cut (mult (add y x) (add x (add y z)) = add x (add y (mult x z)));
 409 [auto paramodulation
 410 |auto paramodulation]
 411 qed.
 412 (*  186 sec *)
 413 *)
 414 theorem bool756full:
 415   \forall A:Set.
 416   \forall one:A.
 417   \forall zero:A.
 418   \forall add: A \to A \to A.
 419   \forall mult: A \to A \to A.
 420   \forall inv: A \to A.
 421   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 422   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 423   \forall d1: (\forall x,y,z:A.
 424               (add x (mult y z)) = (mult (add x y) (add x z))).
 425   \forall d2: (\forall x,y,z:A.
 426               (mult x (add y z)) = (add (mult x y) (mult x z))).
 427   \forall i1: (\forall x:A. (add x zero) = x).
 428   \forall i2: (\forall x:A. (mult x one) = x).
 429   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 430   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 431   \forall x,y,z:A.
 432     add x y = add x (add y (mult x z)).
 433 intros;auto paramodulation.
 434 qed.
 435 (* war=5; active 225, maxmeta 172568 *)
 436 (* war=4; active 249, maxmeta 223220 *)
 437 (*
 438 theorem bool1164:
 439   \forall A:Set.
 440   \forall one:A.
 441   \forall zero:A.
 442   \forall add: A \to A \to A.
 443   \forall mult: A \to A \to A.
 444   \forall inv: A \to A.
 445   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 446   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 447   \forall d1: (\forall x,y,z:A.
 448               (add x (mult y z)) = (mult (add x y) (add x z))).
 449   \forall d2: (\forall x,y,z:A.
 450               (mult x (add y z)) = (add (mult x y) (mult x z))).
 451   \forall i1: (\forall x:A. (add x zero) = x).
 452   \forall i2: (\forall x:A. (mult x one) = x).
 453   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 454   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 455   \forall x,y,z:A.
 456     (add x y) = (add (add x (mult y z)) y).
 457 intros.auto paramodulation.
 458 qed.
 459
 460 theorem bool1230:
 461   \forall A:Set.
 462   \forall one:A.
 463   \forall zero:A.
 464   \forall add: A \to A \to A.
 465   \forall mult: A \to A \to A.
 466   \forall inv: A \to A.
 467   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 468   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 469   \forall d1: (\forall x,y,z:A.
 470               (add x (mult y z)) = (mult (add x y) (add x z))).
 471   \forall d2: (\forall x,y,z:A.
 472               (mult x (add y z)) = (add (mult x y) (mult x z))).
 473   \forall i1: (\forall x:A. (add x zero) = x).
 474   \forall i2: (\forall x:A. (mult x one) = x).
 475   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 476   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 477   \forall x,y,z:A.
 478   \forall c1z: (\forall x:A.(add x z) = (add z x)).
 479     add (add x y) z = add (add x y) (add z y).
 480 intros.auto paramodulation.
 481 qed.
 482
 483 theorem bool1230:
 484   \forall A:Set.
 485   \forall one:A.
 486   \forall zero:A.
 487   \forall add: A \to A \to A.
 488   \forall mult: A \to A \to A.
 489   \forall inv: A \to A.
 490   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 491   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 492   \forall d1: (\forall x,y,z:A.
 493               (add x (mult y z)) = (mult (add x y) (add x z))).
 494   \forall d2: (\forall x,y,z:A.
 495               (mult x (add y z)) = (add (mult x y) (mult x z))).
 496   \forall i1: (\forall x:A. (add x zero) = x).
 497   \forall i2: (\forall x:A. (mult x one) = x).
 498   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 499   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 500   \forall x,y,z:A.
 501     add (add x y) z = add (add x y) (add z y).
 502 intros.auto paramodulation.
 503 qed.
 504
 505 theorem bool1372:
 506   \forall A:Set.
 507   \forall one:A.
 508   \forall zero:A.
 509   \forall add: A \to A \to A.
 510   \forall mult: A \to A \to A.
 511   \forall inv: A \to A.
 512   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 513   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 514   \forall d1: (\forall x,y,z:A.
 515               (add x (mult y z)) = (mult (add x y) (add x z))).
 516   \forall d2: (\forall x,y,z:A.
 517               (mult x (add y z)) = (add (mult x y) (mult x z))).
 518   \forall i1: (\forall x:A. (add x zero) = x).
 519   \forall i2: (\forall x:A. (mult x one) = x).
 520   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 521   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 522   \forall x,y,z:A.
 523     add x (add y z) = add (add x z) y.
 524 intros.auto paramodulation.
 525 qed.*)
 526
 527 theorem bool381:
 528   \forall A:Set.
 529   \forall one:A.
 530   \forall zero:A.
 531   \forall add: A \to A \to A.
 532   \forall mult: A \to A \to A.
 533   \forall inv: A \to A.
 534   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 535   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 536   \forall d1: (\forall x,y,z:A.
 537               (add x (mult y z)) = (mult (add x y) (add x z))).
 538   \forall d2: (\forall x,y,z:A.
 539               (mult x (add y z)) = (add (mult x y) (mult x z))).
 540   \forall i1: (\forall x:A. (add x zero) = x).
 541   \forall i2: (\forall x:A. (mult x one) = x).
 542   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 543   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 544   \forall x,y:A.
 545       add (inv x) y = add (mult x y) (inv x).
 546 intros.auto paramodulation.
 547 qed.
 548
 549 theorem bool5hint1:
 550   \forall A:Set.
 551   \forall one:A.
 552   \forall zero:A.
 553   \forall add: A \to A \to A.
 554   \forall mult: A \to A \to A.
 555   \forall inv: A \to A.
 556   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 557   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 558   \forall d1: (\forall x,y,z:A.
 559               (add x (mult y z)) = (mult (add x y) (add x z))).
 560   \forall d2: (\forall x,y,z:A.
 561               (mult x (add y z)) = (add (mult x y) (mult x z))).
 562   \forall i1: (\forall x:A. (add x zero) = x).
 563   \forall i2: (\forall x:A. (mult x one) = x).
 564   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 565   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 566   \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
 567   \forall hint1735:(\forall x,y:A. add (inv (add x y)) x = add x (inv y)).
 568   \forall hint623:(\forall x,y:A. inv (mult x y) = add (inv x) (inv (mult x y))).
 569   \forall x,y:A.
 570     (inv (mult x y)) = (add (inv x) (inv y)).
 571 intros.auto paramodulation.
 572 qed.
 573 (* 90 *)
 574
 575 theorem bool5hint2:
 576   \forall A:Set.
 577   \forall one:A.
 578   \forall zero:A.
 579   \forall add: A \to A \to A.
 580   \forall mult: A \to A \to A.
 581   \forall inv: A \to A.
 582   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 583   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 584   \forall d1: (\forall x,y,z:A.
 585               (add x (mult y z)) = (mult (add x y) (add x z))).
 586   \forall d2: (\forall x,y,z:A.
 587               (mult x (add y z)) = (add (mult x y) (mult x z))).
 588   \forall i1: (\forall x:A. (add x zero) = x).
 589   \forall i2: (\forall x:A. (mult x one) = x).
 590   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 591   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 592   \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
 593   \forall hint623:(\forall x,y:A. inv (mult x y) = add (inv x) (inv (mult x y))).
 594   \forall x,y:A.
 595     (inv (mult x y)) = (add (inv x) (inv y)).
 596 intros.auto paramodulation.
 597 qed.
 598 (* 41 *)
 599
 600 theorem bool5hint3:
 601   \forall A:Set.
 602   \forall one:A.
 603   \forall zero:A.
 604   \forall add: A \to A \to A.
 605   \forall mult: A \to A \to A.
 606   \forall inv: A \to A.
 607   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 608   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 609   \forall d1: (\forall x,y,z:A.
 610               (add x (mult y z)) = (mult (add x y) (add x z))).
 611   \forall d2: (\forall x,y,z:A.
 612               (mult x (add y z)) = (add (mult x y) (mult x z))).
 613   \forall i1: (\forall x:A. (add x zero) = x).
 614   \forall i2: (\forall x:A. (mult x one) = x).
 615   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 616   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 617   \forall hint1731:(\forall x,y:A. add (inv (add x y)) y = add y (inv x)).
 618   \forall hint609:(\forall x,y:A. inv x = add (inv (add y x)) (inv x)).
 619   \forall x,y:A.
 620     (inv (mult x y)) = (add (inv x) (inv y)).
 621 intros.auto paramodulation.
 622 qed.
 623 (* 41 *)
 624
 625 theorem bool5:
 626   \forall A:Set.
 627   \forall one:A.
 628   \forall zero:A.
 629   \forall add: A \to A \to A.
 630   \forall mult: A \to A \to A.
 631   \forall inv: A \to A.
 632   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 633   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 634   \forall d1: (\forall x,y,z:A.
 635               (add x (mult y z)) = (mult (add x y) (add x z))).
 636   \forall d2: (\forall x,y,z:A.
 637               (mult x (add y z)) = (add (mult x y) (mult x z))).
 638   \forall i1: (\forall x:A. (add x zero) = x).
 639   \forall i2: (\forall x:A. (mult x one) = x).
 640   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 641   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 642   \forall x,y:A.
 643     (inv (mult x y)) = (add (inv x) (inv y)).
 644 intros.auto paramodulation.
 645 qed.