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 alias symbol "eq" = "Coq's leibnitz's equality".
  19
  20 theorem SKK:
  21   \forall A:Set.
  22   \forall app: A \to A \to A.
  23   \forall K:A.
  24   \forall S:A.
  25   \forall H1: (\forall x,y:A.(app (app K x) y) = x).
  26   \forall H2: (\forall x,y,z:A.
  27     (app (app (app S x) y) z) = (app (app x z) (app y z))).
  28   \forall x:A.
  29     (app (app (app S K) K) x) = x.
  30 intros.auto paramodulation.
  31 qed.
  32
  33 theorem bool1:
  34   \forall A:Set.
  35   \forall one:A.
  36   \forall zero:A.
  37   \forall add: A \to A \to A.
  38   \forall mult: A \to A \to A.
  39   \forall inv: A \to A.
  40   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
  41   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
  42   \forall d1: (\forall x,y,z:A.
  43               (add x (mult y z)) = (mult (add x y) (add x z))).
  44   \forall d2: (\forall x,y,z:A.
  45               (mult x (add y z)) = (add (mult x y) (mult x z))).
  46   \forall i1: (\forall x:A. (add x zero) = x).
  47   \forall i2: (\forall x:A. (mult x one) = x).
  48   \forall inv1: (\forall x:A. (add x (inv x)) = one).
  49   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
  50   (inv zero) = one.
  51 intros.auto paramodulation.
  52 qed.
  53
  54 theorem bool2:
  55   \forall A:Set.
  56   \forall one:A.
  57   \forall zero:A.
  58   \forall add: A \to A \to A.
  59   \forall mult: A \to A \to A.
  60   \forall inv: A \to A.
  61   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
  62   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
  63   \forall d1: (\forall x,y,z:A.
  64               (add x (mult y z)) = (mult (add x y) (add x z))).
  65   \forall d2: (\forall x,y,z:A.
  66               (mult x (add y z)) = (add (mult x y) (mult x z))).
  67   \forall i1: (\forall x:A. (add x zero) = x).
  68   \forall i2: (\forall x:A. (mult x one) = x).
  69   \forall inv1: (\forall x:A. (add x (inv x)) = one).
  70   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
  71   \forall x:A. (mult x zero) = zero.
  72 intros.auto paramodulation.
  73 qed.
  74
  75 theorem bool3:
  76   \forall A:Set.
  77   \forall one:A.
  78   \forall zero:A.
  79   \forall add: A \to A \to A.
  80   \forall mult: A \to A \to A.
  81   \forall inv: A \to A.
  82   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
  83   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
  84   \forall d1: (\forall x,y,z:A.
  85               (add x (mult y z)) = (mult (add x y) (add x z))).
  86   \forall d2: (\forall x,y,z:A.
  87               (mult x (add y z)) = (add (mult x y) (mult x z))).
  88   \forall i1: (\forall x:A. (add x zero) = x).
  89   \forall i2: (\forall x:A. (mult x one) = x).
  90   \forall inv1: (\forall x:A. (add x (inv x)) = one).
  91   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
  92   \forall x:A. (inv (inv x)) = x.
  93 intros.auto paramodulation.
  94 qed.
  95
  96 theorem bool4:
  97   \forall A:Set.
  98   \forall one:A.
  99   \forall zero:A.
 100   \forall add: A \to A \to A.
 101   \forall mult: A \to A \to A.
 102   \forall inv: A \to A.
 103   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 104   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 105   \forall d1: (\forall x,y,z:A.
 106               (add x (mult y z)) = (mult (add x y) (add x z))).
 107   \forall d2: (\forall x,y,z:A.
 108               (mult x (add y z)) = (add (mult x y) (mult x z))).
 109   \forall i1: (\forall x:A. (add x zero) = x).
 110   \forall i2: (\forall x:A. (mult x one) = x).
 111   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 112   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 113   \forall x,y,z:A.
 114     (add x y) = (add (add x (mult y z)) y).
 115 intros.
 116 exact
 117 ((eq_ind A (add y (add x (mult y z)))
 118  (\lambda x_DemodGoal_193:A.(eq A (add x y) x_DemodGoal_193))
 119  (eq_ind A x
 120  (\lambda x_DemodGoal_893:A.(eq A x_DemodGoal_893 (add y (add x (mult y z)))))
 121   (eq_ind A y (\lambda x_DemodGoal_894:A.(eq A x x_DemodGoal_894))
 122   (eq_ind A (add y zero) (\lambda x_Demod_554:A.(eq A x x_Demod_554))
 123   (eq_ind_r A (add zero x) (\lambda x_SupR_809:A.(eq A x_SupR_809 (add y zero)))
 124   (eq_ind_r A (add y (mult (add zero y) zero))
 125   (\lambda x_Demod_553:A.(eq A (add zero x) x_Demod_553))
 126   (eq_ind A (add (add zero x) zero)
 127   (\lambda x_Demod_540:A.(eq A x_Demod_540 (add x (mult (add zero x) zero))))
 128   (eq_ind_r A (mult zero x)
 129   (\lambda x_Demod_526:A.(eq A (add (add zero x) x_Demod_526) (add x (mult (add zero x) zero))))
 130   (eq_ind_r A (mult (add zero x) (add (add zero x) x))
 131   (\lambda x_SupR_606:A.(eq A (add (add zero x) (mult zero x)) x_SupR_606))
 132   (eq_ind A (add (add zero x) zero)
 133   (\lambda x_SupR_296:A.(eq A (add (add zero x) (mult zero x)) (mult x_SupR_296 (add (add zero x) x))))
 134   (H2 (add zero x) zero x) (add zero x) (H4 (add zero x))) (add x (mult (add zero x) zero))
 135   (eq_ind A (add x zero)
 136   (\lambda x_SupR_357:A.(eq A (add x (mult (add zero x) zero)) (mult x_SupR_357 (add (add zero x) x))))
 137   (eq_ind A (mult (add (add zero x) x) (add x zero))
 138   (\lambda x_SupR_310:A.(eq A (add x (mult (add zero x) zero)) x_SupR_310))
 139   (eq_ind A (add x (add zero x))
 140   (\lambda x_SupR_302:A.(eq A (add x (mult (add zero x) zero)) (mult x_SupR_302 (add x zero))))
 141   (H2 x (add zero x) zero) (add (add zero x) x) (H x (add zero x))) (mult (add x zero) (add (add zero x) x)) (H1 (add (add zero x) x) (add x zero))) (add zero x) (H x zero))) zero
 142   (eq_ind A (mult zero one)
 143   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero x)))
 144   (eq_ind_r A (add x one)
 145   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero x)))
 146   (eq_ind_r A (inv zero)
 147   (\lambda x_SupR_785:A.(eq A (mult zero (add x x_SupR_785)) (mult zero x)))
 148   (eq_ind A (add (mult zero x) zero)
 149   (\lambda x_Demod_223:A.(eq A (mult zero (add x (inv zero))) x_Demod_223))
 150   (eq_ind A (mult zero (inv zero))
 151   (\lambda x_SupR_337:A.(eq A (mult zero (add x (inv zero))) (add (mult zero x) x_SupR_337)))
 152   (H3 zero x (inv zero)) zero (H7 zero)) (mult zero x) (H4 (mult zero x))) one
 153   (eq_ind A (add (inv zero) zero)
 154   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 155   (eq_ind A (add zero (inv zero))
 156   (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
 157   (eq_ind A (add x (inv x))
 158   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add x one)))
 159   (eq_ind A (mult (inv x) one)
 160   (\lambda x_SupR_396:A.(eq A (add x x_SupR_396) (add x one)))
 161   (eq_ind_r A (mult one (add x one))
 162   (\lambda x_Demod_199:A.(eq A (add x (mult (inv x) one)) x_Demod_199))
 163   (eq_ind A (add x (inv x))
 164   (\lambda x_SupR_268:A.(eq A (add x (mult (inv x) one)) (mult x_SupR_268 (add x one)))) (H2 x (inv x) one) one (H6 x)) (add x one)
 165   (eq_ind A (mult (add x one) one)
 166   (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add x one))))
 167   (H1 (add x one) one) (add x one) (H5 (add x one)))) (inv x) (H5 (inv x))) one (H6 x))) zero (H5 zero))) (add zero x) (H4 (add zero x))) (add y zero)
 168   (eq_ind A (add zero zero)
 169   (\lambda x_Demod_543:A.(eq A (add y x_Demod_543) (add y (mult (add zero y) zero))))
 170   (eq_ind_r A (mult zero y)
 171   (\lambda x_Demod_524:A.(eq A (add y (add zero x_Demod_524)) (add y (mult (add zero y) zero))))
 172   (eq_ind_r A (mult zero (add zero y))
 173   (\lambda x_SupR_628:A.(eq A (add y x_SupR_628) (add y (mult (add zero y) zero))))
 174   (eq_ind_r A (mult (add y (add zero y)) (add y zero))
 175   (\lambda x_Demod_195:A.(eq A (add y (mult zero (add zero y))) x_Demod_195))
 176   (eq_ind_r A (mult (add y zero) (add y (add zero y)))
 177   (\lambda x_SupR_272:A.(eq A x_SupR_272 (mult (add y (add zero y)) (add y zero)))) (H1 (add y zero) (add y (add zero y))) (add y (mult zero (add zero y))) (H2 y zero (add zero y))) (add y (mult (add zero y) zero)) (H2 y (add zero y) zero)) (add zero (mult zero y))
 178   (eq_ind A (add zero zero)
 179   (\lambda x_SupR_296:A.(eq A (add zero (mult zero y)) (mult x_SupR_296 (add zero y)))) (H2 zero zero y) zero (H4 zero))) zero
 180   (eq_ind A (mult zero one)
 181   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero y)))
 182   (eq_ind_r A (add y one)
 183   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero y)))
 184   (eq_ind_r A (inv zero)
 185   (\lambda x_SupR_785:A.(eq A (mult zero (add y x_SupR_785)) (mult zero y)))
 186   (eq_ind A (add (mult zero y) zero)
 187   (\lambda x_Demod_223:A.(eq A (mult zero (add y (inv zero))) x_Demod_223))
 188   (eq_ind A (mult zero (inv zero))
 189   (\lambda x_SupR_337:A.(eq A (mult zero (add y (inv zero))) (add (mult zero y) x_SupR_337))) (H3 zero y (inv zero)) zero (H7 zero)) (mult zero y) (H4 (mult zero y))) one
 190   (eq_ind A (add (inv zero) zero)
 191   (\lambda x_SupR_463:A.(eq A one x_SupR_463)) (eq_ind A (add zero (inv zero))
 192   (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
 193   (eq_ind A (add y (inv y))
 194   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add y one)))
 195   (eq_ind A (mult (inv y) one)
 196   (\lambda x_SupR_396:A.(eq A (add y x_SupR_396) (add y one)))
 197   (eq_ind_r A (mult one (add y one))
 198   (\lambda x_Demod_199:A.(eq A (add y (mult (inv y) one)) x_Demod_199))
 199   (eq_ind A (add y (inv y))
 200   (\lambda x_SupR_268:A.(eq A (add y (mult (inv y) one)) (mult x_SupR_268 (add y one)))) (H2 y (inv y) one) one (H6 y)) (add y one)
 201   (eq_ind A (mult (add y one) one)
 202   (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add y one)))) (H1 (add y one) one) (add y one) (H5 (add y one)))) (inv y) (H5 (inv y))) one (H6 y))) zero (H5 zero))) zero (H4 zero))) x
 203   (eq_ind A (add x zero)
 204   (\lambda x_SupR_299:A.(eq A x_SupR_299 (add zero x))) (H x zero) x (H4 x))) y (H4 y)) (add y (add x (mult y z)))
 205   (sym_eq\subst[A \Assign A ; x \Assign (add y (add x (mult y z))) ; y \Assign y]
 206   (eq_ind_r A (add zero y)
 207   (\lambda x_SupR_826:A.(eq A (add y (add x (mult y z))) x_SupR_826))
 208   (eq_ind_r A (add zero (mult (add y zero) y))
 209   (\lambda x_Demod_553:A.(eq A (add y (add x (mult y z))) x_Demod_553))
 210   (eq_ind A (add (add y (add x (mult y z))) zero)
 211   (\lambda x_Demod_540:A.(eq A x_Demod_540 (add (add x (mult y z)) (mult (add y (add x (mult y z))) y))))
 212   (eq_ind_r A (mult zero (add x (mult y z)))
 213   (\lambda x_Demod_526:A.(eq A (add (add y (add x (mult y z))) x_Demod_526) (add (add x (mult y z)) (mult (add y (add x (mult y z))) y))))
 214   (eq_ind_r A (mult (add y (add x (mult y z))) (add (add y (add x (mult y z))) (add x (mult y z))))
 215   (\lambda x_SupR_606:A.(eq A (add (add y (add x (mult y z))) (mult zero (add x (mult y z)))) x_SupR_606))
 216   (eq_ind A (add (add y (add x (mult y z))) zero)
 217   (\lambda x_SupR_296:A.(eq A (add (add y (add x (mult y z))) (mult zero (add x (mult y z)))) (mult x_SupR_296 (add (add y (add x (mult y z))) (add x (mult y z))))))
 218   (H2 (add y (add x (mult y z))) zero (add x (mult y z))) (add y (add x (mult y z))) (H4 (add y (add x (mult y z))))) (add (add x (mult y z)) (mult (add y (add x (mult y z))) y))
 219   (eq_ind A (add (add x (mult y z)) y)
 220   (\lambda x_SupR_357:A.(eq A (add (add x (mult y z)) (mult (add y (add x (mult y z))) y)) (mult x_SupR_357 (add (add y (add x (mult y z))) (add x (mult y z)))))) (eq_ind A (mult (add (add y (add x (mult y z))) (add x (mult y z))) (add (add x (mult y z)) y))
 221   (\lambda x_SupR_310:A.(eq A (add (add x (mult y z)) (mult (add y (add x (mult y z))) y)) x_SupR_310)) (eq_ind A (add (add x (mult y z)) (add y (add x (mult y z))))
 222   (\lambda x_SupR_302:A.(eq A (add (add x (mult y z)) (mult (add y (add x (mult y z))) y)) (mult x_SupR_302 (add (add x (mult y z)) y)))) (H2 (add x (mult y z)) (add y (add x (mult y z))) y) (add (add y (add x (mult y z))) (add x (mult y z))) (H (add x (mult y z)) (add y (add x (mult y z))))) (mult (add (add x (mult y z)) y) (add (add y (add x (mult y z))) (add x (mult y z)))) (H1 (add (add y (add x (mult y z))) (add x (mult y z))) (add (add x (mult y z)) y))) (add y (add x (mult y z))) (H (add x (mult y z)) y))) zero (eq_ind A (mult zero one)
 223   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero (add x (mult y z)))))
 224   (eq_ind_r A (add (add x (mult y z)) one)
 225   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero (add x (mult y z)))))
 226   (eq_ind_r A (inv zero)
 227   (\lambda x_SupR_785:A.(eq A (mult zero (add (add x (mult y z)) x_SupR_785)) (mult zero (add x (mult y z)))))
 228   (eq_ind A (add (mult zero (add x (mult y z))) zero)
 229   (\lambda x_Demod_223:A.(eq A (mult zero (add (add x (mult y z)) (inv zero))) x_Demod_223))
 230   (eq_ind A (mult zero (inv zero))
 231   (\lambda x_SupR_337:A.(eq A (mult zero (add (add x (mult y z)) (inv zero))) (add (mult zero (add x (mult y z))) x_SupR_337))) (H3 zero (add x (mult y z)) (inv zero)) zero (H7 zero)) (mult zero (add x (mult y z))) (H4 (mult zero (add x (mult y z))))) one
 232   (eq_ind A (add (inv zero) zero)
 233   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 234   (eq_ind A (add zero (inv zero))
 235   (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
 236   (eq_ind A (add (add x (mult y z)) (inv (add x (mult y z))))
 237   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add (add x (mult y z)) one)))
 238   (eq_ind A (mult (inv (add x (mult y z))) one)
 239   (\lambda x_SupR_396:A.(eq A (add (add x (mult y z)) x_SupR_396) (add (add x (mult y z)) one)))
 240   (eq_ind_r A (mult one (add (add x (mult y z)) one))
 241   (\lambda x_Demod_199:A.(eq A (add (add x (mult y z)) (mult (inv (add x (mult y z))) one)) x_Demod_199))
 242   (eq_ind A (add (add x (mult y z)) (inv (add x (mult y z))))
 243   (\lambda x_SupR_268:A.(eq A (add (add x (mult y z)) (mult (inv (add x (mult y z))) one)) (mult x_SupR_268 (add (add x (mult y z)) one)))) (H2 (add x (mult y z)) (inv (add x (mult y z))) one) one (H6 (add x (mult y z)))) (add (add x (mult y z)) one) (eq_ind A (mult (add (add x (mult y z)) one) one)
 244   (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add (add x (mult y z)) one)))) (H1 (add (add x (mult y z)) one) one) (add (add x (mult y z)) one) (H5 (add (add x (mult y z)) one)))) (inv (add x (mult y z))) (H5 (inv (add x (mult y z))))) one (H6 (add x (mult y z))))) zero (H5 zero))) (add y (add x (mult y z))) (H4 (add y (add x (mult y z))))) (add zero y)
 245   (eq_ind A (add y zero)
 246   (\lambda x_Demod_543:A.(eq A (add zero x_Demod_543) (add zero (mult (add y zero) y))))
 247   (eq_ind_r A (mult zero zero)
 248   (\lambda x_Demod_524:A.(eq A (add zero (add y x_Demod_524)) (add zero (mult (add y zero) y))))
 249   (eq_ind_r A (mult y (add y zero))
 250   (\lambda x_SupR_628:A.(eq A (add zero x_SupR_628) (add zero (mult (add y zero) y))))
 251   (eq_ind_r A (mult (add zero (add y zero)) (add zero y))
 252   (\lambda x_Demod_195:A.(eq A (add zero (mult y (add y zero))) x_Demod_195))
 253   (eq_ind_r A (mult (add zero y) (add zero (add y zero)))
 254   (\lambda x_SupR_272:A.(eq A x_SupR_272 (mult (add zero (add y zero)) (add zero y)))) (H1 (add zero y) (add zero (add y zero))) (add zero (mult y (add y zero))) (H2 zero y (add y zero))) (add zero (mult (add y zero) y)) (H2 zero (add y zero) y)) (add y (mult zero zero))
 255   (eq_ind A (add y zero)
 256   (\lambda x_SupR_296:A.(eq A (add y (mult zero zero)) (mult x_SupR_296 (add y zero)))) (H2 y zero zero) y (H4 y))) zero
 257   (eq_ind A (mult zero one)
 258   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero zero)))
 259   (eq_ind_r A (add zero one)
 260   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero zero)))
 261   (eq_ind_r A (inv zero)
 262   (\lambda x_SupR_785:A.(eq A (mult zero (add zero x_SupR_785)) (mult zero zero)))
 263   (eq_ind A (add (mult zero zero) zero)
 264   (\lambda x_Demod_223:A.(eq A (mult zero (add zero (inv zero))) x_Demod_223))
 265   (eq_ind A (mult zero (inv zero))
 266   (\lambda x_SupR_337:A.(eq A (mult zero (add zero (inv zero))) (add (mult zero zero) x_SupR_337))) (H3 zero zero (inv zero)) zero (H7 zero)) (mult zero zero) (H4 (mult zero zero))) one
 267   (eq_ind A (add (inv zero) zero)
 268   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 269   (eq_ind A (add zero (inv zero))
 270   (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
 271   (eq_ind A (add zero (inv zero))
 272   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add zero one)))
 273   (eq_ind A (mult (inv zero) one) (\lambda x_SupR_396:A.(eq A (add zero x_SupR_396) (add zero one)))
 274   (eq_ind_r A (mult one (add zero one))
 275   (\lambda x_Demod_199:A.(eq A (add zero (mult (inv zero) one)) x_Demod_199))
 276   (eq_ind A (add zero (inv zero))
 277   (\lambda x_SupR_268:A.(eq A (add zero (mult (inv zero) one)) (mult x_SupR_268 (add zero one)))) (H2 zero (inv zero) one) one (H6 zero)) (add zero one)
 278   (eq_ind A (mult (add zero one) one)
 279   (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add zero one)))) (H1 (add zero one) one) (add zero one) (H5 (add zero one)))) (inv zero) (H5 (inv zero))) one (H6 zero))) zero (H5 zero))) y (H4 y))) y
 280   (eq_ind A (add y zero)
 281   (\lambda x_SupR_299:A.(eq A x_SupR_299 (add zero y))) (H y zero) y (H4 y))))) (add x y)
 282   (sym_eq\subst[A \Assign A ; x \Assign (add x y) ; y \Assign x]
 283   (eq_ind_r A (add zero x)
 284   (\lambda x_SupR_826:A.(eq A (add x y) x_SupR_826))
 285   (eq_ind_r A (add zero (mult (add x zero) x))
 286   (\lambda x_Demod_553:A.(eq A (add x y) x_Demod_553))
 287   (eq_ind A (add (add x y) zero)
 288   (\lambda x_Demod_540:A.(eq A x_Demod_540 (add y (mult (add x y) x))))
 289   (eq_ind_r A (mult zero y)
 290   (\lambda x_Demod_526:A.(eq A (add (add x y) x_Demod_526) (add y (mult (add x y) x))))
 291   (eq_ind_r A (mult (add x y) (add (add x y) y))
 292   (\lambda x_SupR_606:A.(eq A (add (add x y) (mult zero y)) x_SupR_606))
 293   (eq_ind A (add (add x y) zero)
 294   (\lambda x_SupR_296:A.(eq A (add (add x y) (mult zero y)) (mult x_SupR_296 (add (add x y) y)))) (H2 (add x y) zero y) (add x y) (H4 (add x y))) (add y (mult (add x y) x))
 295   (eq_ind A (add y x)
 296   (\lambda x_SupR_357:A.(eq A (add y (mult (add x y) x)) (mult x_SupR_357 (add (add x y) y))))
 297   (eq_ind A (mult (add (add x y) y) (add y x))
 298   (\lambda x_SupR_310:A.(eq A (add y (mult (add x y) x)) x_SupR_310))
 299   (eq_ind A (add y (add x y))
 300   (\lambda x_SupR_302:A.(eq A (add y (mult (add x y) x)) (mult x_SupR_302 (add y x)))) (H2 y (add x y) x) (add (add x y) y) (H y (add x y))) (mult (add y x) (add (add x y) y)) (H1 (add (add x y) y) (add y x))) (add x y) (H y x))) zero
 301   (eq_ind A (mult zero one)
 302   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero y)))
 303   (eq_ind_r A (add y one)
 304   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero y)))
 305   (eq_ind_r A (inv zero)
 306   (\lambda x_SupR_785:A.(eq A (mult zero (add y x_SupR_785)) (mult zero y)))
 307   (eq_ind A (add (mult zero y) zero)
 308   (\lambda x_Demod_223:A.(eq A (mult zero (add y (inv zero))) x_Demod_223))
 309   (eq_ind A (mult zero (inv zero))
 310   (\lambda x_SupR_337:A.(eq A (mult zero (add y (inv zero))) (add (mult zero y) x_SupR_337))) (H3 zero y (inv zero)) zero (H7 zero)) (mult zero y) (H4 (mult zero y))) one
 311   (eq_ind A (add (inv zero) zero)
 312   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 313   (eq_ind A (add zero (inv zero))
 314   (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
 315   (eq_ind A (add y (inv y))
 316   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add y one)))
 317   (eq_ind A (mult (inv y) one)
 318   (\lambda x_SupR_396:A.(eq A (add y x_SupR_396) (add y one)))
 319   (eq_ind_r A (mult one (add y one))
 320   (\lambda x_Demod_199:A.(eq A (add y (mult (inv y) one)) x_Demod_199))
 321   (eq_ind A (add y (inv y))
 322   (\lambda x_SupR_268:A.(eq A (add y (mult (inv y) one)) (mult x_SupR_268 (add y one)))) (H2 y (inv y) one) one (H6 y)) (add y one)
 323   (eq_ind A (mult (add y one) one)
 324   (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add y one)))) (H1 (add y one) one) (add y one) (H5 (add y one)))) (inv y) (H5 (inv y))) one (H6 y))) zero (H5 zero))) (add x y) (H4 (add x y))) (add zero x)
 325   (eq_ind A (add x zero)
 326   (\lambda x_Demod_543:A.(eq A (add zero x_Demod_543) (add zero (mult (add x zero) x))))
 327   (eq_ind_r A (mult zero zero)
 328   (\lambda x_Demod_524:A.(eq A (add zero (add x x_Demod_524)) (add zero (mult (add x zero) x))))
 329   (eq_ind_r A (mult x (add x zero))
 330   (\lambda x_SupR_628:A.(eq A (add zero x_SupR_628) (add zero (mult (add x zero) x))))
 331   (eq_ind_r A (mult (add zero (add x zero)) (add zero x))
 332   (\lambda x_Demod_195:A.(eq A (add zero (mult x (add x zero))) x_Demod_195))
 333   (eq_ind_r A (mult (add zero x) (add zero (add x zero)))
 334   (\lambda x_SupR_272:A.(eq A x_SupR_272 (mult (add zero (add x zero)) (add zero x)))) (H1 (add zero x) (add zero (add x zero))) (add zero (mult x (add x zero))) (H2 zero x (add x zero))) (add zero (mult (add x zero) x)) (H2 zero (add x zero) x)) (add x (mult zero zero))
 335   (eq_ind A (add x zero)
 336   (\lambda x_SupR_296:A.(eq A (add x (mult zero zero)) (mult x_SupR_296 (add x zero)))) (H2 x zero zero) x (H4 x))) zero
 337   (eq_ind A (mult zero one)
 338   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero zero)))
 339   (eq_ind_r A (add zero one)
 340   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero zero)))
 341   (eq_ind_r A (inv zero)
 342   (\lambda x_SupR_785:A.(eq A (mult zero (add zero x_SupR_785)) (mult zero zero)))
 343   (eq_ind A (add (mult zero zero) zero)
 344   (\lambda x_Demod_223:A.(eq A (mult zero (add zero (inv zero))) x_Demod_223))
 345   (eq_ind A (mult zero (inv zero))
 346   (\lambda x_SupR_337:A.(eq A (mult zero (add zero (inv zero))) (add (mult zero zero) x_SupR_337))) (H3 zero zero (inv zero)) zero (H7 zero)) (mult zero zero) (H4 (mult zero zero))) one
 347   (eq_ind A (add (inv zero) zero)
 348   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 349   (eq_ind A (add zero (inv zero))
 350   (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
 351   (eq_ind A (add zero (inv zero))
 352   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add zero one)))
 353   (eq_ind A (mult (inv zero) one)
 354   (\lambda x_SupR_396:A.(eq A (add zero x_SupR_396) (add zero one)))
 355   (eq_ind_r A (mult one (add zero one))
 356   (\lambda x_Demod_199:A.(eq A (add zero (mult (inv zero) one)) x_Demod_199))
 357   (eq_ind A (add zero (inv zero))
 358   (\lambda x_SupR_268:A.(eq A (add zero (mult (inv zero) one)) (mult x_SupR_268 (add zero one)))) (H2 zero (inv zero) one) one (H6 zero)) (add zero one)
 359   (eq_ind A (mult (add zero one) one)
 360   (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add zero one)))) (H1 (add zero one) one) (add zero one) (H5 (add zero one)))) (inv zero) (H5 (inv zero))) one (H6 zero))) zero (H5 zero))) x (H4 x))) x
 361   (eq_ind A (add x zero)
 362   (\lambda x_SupR_299:A.(eq A x_SupR_299 (add zero x))) (H x zero) x (H4 x))))) (add (add x (mult y z)) y)
 363   (sym_eq\subst[A \Assign A ; x \Assign (add (add x (mult y z)) y) ; y \Assign (add y (add x (mult y z)))] (H (add x (mult y z)) y)))
 364 ).
 365 auto paramodulation.
 366
 367 qed.
 368
 369 theorem bool5:
 370   \forall A:Set.
 371   \forall one:A.
 372   \forall zero:A.
 373   \forall add: A \to A \to A.
 374   \forall mult: A \to A \to A.
 375   \forall inv: A \to A.
 376   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 377   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 378   \forall d1: (\forall x,y,z:A.
 379               (add x (mult y z)) = (mult (add x y) (add x z))).
 380   \forall d2: (\forall x,y,z:A.
 381               (mult x (add y z)) = (add (mult x y) (mult x z))).
 382   \forall i1: (\forall x:A. (add x zero) = x).
 383   \forall i2: (\forall x:A. (mult x one) = x).
 384   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 385   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 386   \forall x,y:A.
 387     (inv (mult x y)) = (add (inv x) (inv y)).
 388 intros.auto paramodulation.
 389 qed.