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 bool4:
 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,z:A.
 119     (add x y) = (add (add x (mult y z)) y).
 120 intros.
 121 exact (
 122   ((eq_ind A (add y (add x (mult y z)))
 123  (\lambda x_DemodGoal_193:A.(eq A (add x y) x_DemodGoal_193))
 124  (eq_ind A x
 125  (\lambda x_DemodGoal_893:A.(eq A x_DemodGoal_893 (add y (add x (mult y z)))))
 126   (eq_ind A y (\lambda x_DemodGoal_894:A.(eq A x x_DemodGoal_894))
 127   (eq_ind A (add y zero) (\lambda x_Demod_554:A.(eq A x x_Demod_554))
 128   (eq_ind_r A (add zero x) (\lambda x_SupR_809:A.(eq A x_SupR_809 (add y zero)))
 129   (eq_ind_r A (add y (mult (add zero y) zero))
 130   (\lambda x_Demod_553:A.(eq A (add zero x) x_Demod_553))
 131   (eq_ind A (add (add zero x) zero)
 132   (\lambda x_Demod_540:A.(eq A x_Demod_540 (add x (mult (add zero x) zero))))
 133   (eq_ind_r A (mult zero x))
 134   (\lambda x_Demod_526:A.(eq A (add (add zero x) x_Demod_526) (add x (mult (add zero x) zero))))
 135   (eq_ind_r A (mult (add zero x) (add (add zero x) x))
 136   (\lambda x_SupR_606:A.(eq A (add (add zero x) (mult zero x)) x_SupR_606))
 137   (eq_ind A (add (add zero x) zero)
 138   (\lambda x_SupR_296:A.(eq A (add (add zero x) (mult zero x)) (mult x_SupR_296 (add (add zero x) x))))
 139   (H2 (add zero x) zero x) (add zero x) (H4 (add zero x))) (add x (mult (add zero x) zero))
 140   (eq_ind A (add x zero)
 141   (\lambda x_SupR_357:A.(eq A (add x (mult (add zero x) zero)) (mult x_SupR_357 (add (add zero x) x))))
 142   (eq_ind A (mult (add (add zero x) x) (add x zero))
 143   (\lambda x_SupR_310:A.(eq A (add x (mult (add zero x) zero)) x_SupR_310))
 144   (eq_ind A (add x (add zero x))
 145   (\lambda x_SupR_302:A.(eq A (add x (mult (add zero x) zero)) (mult x_SupR_302 (add x zero))))
 146   (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
 147   (eq_ind A (mult zero one)
 148   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero x)))
 149   (eq_ind_r A (add x one)
 150   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero x)))
 151   (eq_ind_r A (inv zero)
 152   (\lambda x_SupR_785:A.(eq A (mult zero (add x x_SupR_785)) (mult zero x)))
 153   (eq_ind A (add (mult zero x) zero)
 154   (\lambda x_Demod_223:A.(eq A (mult zero (add x (inv zero))) x_Demod_223))
 155   (eq_ind A (mult zero (inv zero))
 156   (\lambda x_SupR_337:A.(eq A (mult zero (add x (inv zero))) (add (mult zero x) x_SupR_337)))
 157   (H3 zero x (inv zero)) zero (H7 zero)) (mult zero x) (H4 (mult zero x))) one
 158   (eq_ind A (add (inv zero) zero)
 159   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 160   (eq_ind A (add zero (inv zero))
 161   (\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
 162   (eq_ind A (add x (inv x))
 163   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add x one)))
 164   (eq_ind A (mult (inv x) one)
 165   (\lambda x_SupR_396:A.(eq A (add x x_SupR_396) (add x one)))
 166   (eq_ind_r A (mult one (add x one))
 167   (\lambda x_Demod_199:A.(eq A (add x (mult (inv x) one)) x_Demod_199))
 168   (eq_ind A (add x (inv x))
 169   (\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)
 170   (eq_ind A (mult (add x one) one)
 171   (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add x one))))
 172   (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)
 173   (eq_ind A (add zero zero)
 174   (\lambda x_Demod_543:A.(eq A (add y x_Demod_543) (add y (mult (add zero y) zero))))
 175   (eq_ind_r A (mult zero y)
 176   (\lambda x_Demod_524:A.(eq A (add y (add zero x_Demod_524)) (add y (mult (add zero y) zero))))
 177   (eq_ind_r A (mult zero (add zero y))
 178   (\lambda x_SupR_628:A.(eq A (add y x_SupR_628) (add y (mult (add zero y) zero))))
 179   (eq_ind_r A (mult (add y (add zero y)) (add y zero))
 180   (\lambda x_Demod_195:A.(eq A (add y (mult zero (add zero y))) x_Demod_195))
 181   (eq_ind_r A (mult (add y zero) (add y (add zero y)))
 182   (\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))
 183   (eq_ind A (add zero zero)
 184   (\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
 185   (eq_ind A (mult zero one)
 186   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero y)))
 187   (eq_ind_r A (add y one)
 188   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero y)))
 189   (eq_ind_r A (inv zero)
 190   (\lambda x_SupR_785:A.(eq A (mult zero (add y x_SupR_785)) (mult zero y)))
 191   (eq_ind A (add (mult zero y) zero)
 192   (\lambda x_Demod_223:A.(eq A (mult zero (add y (inv zero))) x_Demod_223))
 193   (eq_ind A (mult zero (inv zero))
 194   (\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
 195   (eq_ind A (add (inv zero) zero)
 196   (\lambda x_SupR_463:A.(eq A one x_SupR_463)) (eq_ind A (add zero (inv zero))
 197   (\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
 198   (eq_ind A (add y (inv y))
 199   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add y one)))
 200   (eq_ind A (mult (inv y) one)
 201   (\lambda x_SupR_396:A.(eq A (add y x_SupR_396) (add y one)))
 202   (eq_ind_r A (mult one (add y one))
 203   (\lambda x_Demod_199:A.(eq A (add y (mult (inv y) one)) x_Demod_199))
 204   (eq_ind A (add y (inv y))
 205   (\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)
 206   (eq_ind A (mult (add y one) one)
 207   (\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
 208   (eq_ind A (add x zero)
 209   (\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)))
 210   (sym_eq\subst[A \Assign A ; x \Assign (add y (add x (mult y z))) ; y \Assign y]
 211   (eq_ind_r A (add zero y)
 212   (\lambda x_SupR_826:A.(eq A (add y (add x (mult y z))) x_SupR_826))
 213   (eq_ind_r A (add zero (mult (add y zero) y))
 214   (\lambda x_Demod_553:A.(eq A (add y (add x (mult y z))) x_Demod_553))
 215   (eq_ind A (add (add y (add x (mult y z))) zero)
 216   (\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))))
 217   (eq_ind_r A (mult zero (add x (mult y z)))
 218   (\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))))
 219   (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))))
 220   (\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))
 221   (eq_ind A (add (add y (add x (mult y z))) zero)
 222   (\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))))))
 223   (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))
 224   (eq_ind A (add (add x (mult y z)) y)
 225   (\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))
 226   (\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))))
 227   (\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)
 228   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero (add x (mult y z)))))
 229   (eq_ind_r A (add (add x (mult y z)) one)
 230   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero (add x (mult y z)))))
 231   (eq_ind_r A (inv zero)
 232   (\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)))))
 233   (eq_ind A (add (mult zero (add x (mult y z))) zero)
 234   (\lambda x_Demod_223:A.(eq A (mult zero (add (add x (mult y z)) (inv zero))) x_Demod_223))
 235   (eq_ind A (mult zero (inv zero))
 236   (\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
 237   (eq_ind A (add (inv zero) zero)
 238   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 239   (eq_ind A (add zero (inv zero))
 240   (\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
 241   (eq_ind A (add (add x (mult y z)) (inv (add x (mult y z))))
 242   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add (add x (mult y z)) one)))
 243   (eq_ind A (mult (inv (add x (mult y z))) one)
 244   (\lambda x_SupR_396:A.(eq A (add (add x (mult y z)) x_SupR_396) (add (add x (mult y z)) one)))
 245   (eq_ind_r A (mult one (add (add x (mult y z)) one))
 246   (\lambda x_Demod_199:A.(eq A (add (add x (mult y z)) (mult (inv (add x (mult y z))) one)) x_Demod_199))
 247   (eq_ind A (add (add x (mult y z)) (inv (add x (mult y z))))
 248   (\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)
 249   (\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)
 250   (eq_ind A (add y zero)
 251   (\lambda x_Demod_543:A.(eq A (add zero x_Demod_543) (add zero (mult (add y zero) y))))
 252   (eq_ind_r A (mult zero zero)
 253   (\lambda x_Demod_524:A.(eq A (add zero (add y x_Demod_524)) (add zero (mult (add y zero) y))))
 254   (eq_ind_r A (mult y (add y zero))
 255   (\lambda x_SupR_628:A.(eq A (add zero x_SupR_628) (add zero (mult (add y zero) y))))
 256   (eq_ind_r A (mult (add zero (add y zero)) (add zero y))
 257   (\lambda x_Demod_195:A.(eq A (add zero (mult y (add y zero))) x_Demod_195))
 258   (eq_ind_r A (mult (add zero y) (add zero (add y zero)))
 259   (\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))
 260   (eq_ind A (add y zero)
 261   (\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
 262   (eq_ind A (mult zero one)
 263   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero zero)))
 264   (eq_ind_r A (add zero one)
 265   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero zero)))
 266   (eq_ind_r A (inv zero)
 267   (\lambda x_SupR_785:A.(eq A (mult zero (add zero x_SupR_785)) (mult zero zero)))
 268   (eq_ind A (add (mult zero zero) zero)
 269   (\lambda x_Demod_223:A.(eq A (mult zero (add zero (inv zero))) x_Demod_223))
 270   (eq_ind A (mult zero (inv zero))
 271   (\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
 272   (eq_ind A (add (inv zero) zero)
 273   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 274   (eq_ind A (add zero (inv zero))
 275   (\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
 276   (eq_ind A (add zero (inv zero))
 277   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add zero one)))
 278   (eq_ind A (mult (inv zero) one) (\lambda x_SupR_396:A.(eq A (add zero x_SupR_396) (add zero one)))
 279   (eq_ind_r A (mult one (add zero one))
 280   (\lambda x_Demod_199:A.(eq A (add zero (mult (inv zero) one)) x_Demod_199))
 281   (eq_ind A (add zero (inv zero))
 282   (\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)
 283   (eq_ind A (mult (add zero one) one)
 284   (\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
 285   (eq_ind A (add y zero)
 286   (\lambda x_SupR_299:A.(eq A x_SupR_299 (add zero y))) (H y zero) y (H4 y))))) (add x y)
 287   (sym_eq\subst[A \Assign A ; x \Assign (add x y) ; y \Assign x]
 288   (eq_ind_r A (add zero x)
 289   (\lambda x_SupR_826:A.(eq A (add x y) x_SupR_826))
 290   (eq_ind_r A (add zero (mult (add x zero) x))
 291   (\lambda x_Demod_553:A.(eq A (add x y) x_Demod_553))
 292   (eq_ind A (add (add x y) zero)
 293   (\lambda x_Demod_540:A.(eq A x_Demod_540 (add y (mult (add x y) x))))
 294   (eq_ind_r A (mult zero y)
 295   (\lambda x_Demod_526:A.(eq A (add (add x y) x_Demod_526) (add y (mult (add x y) x))))
 296   (eq_ind_r A (mult (add x y) (add (add x y) y))
 297   (\lambda x_SupR_606:A.(eq A (add (add x y) (mult zero y)) x_SupR_606))
 298   (eq_ind A (add (add x y) zero)
 299   (\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))
 300   (eq_ind A (add y x)
 301   (\lambda x_SupR_357:A.(eq A (add y (mult (add x y) x)) (mult x_SupR_357 (add (add x y) y))))
 302   (eq_ind A (mult (add (add x y) y) (add y x))
 303   (\lambda x_SupR_310:A.(eq A (add y (mult (add x y) x)) x_SupR_310))
 304   (eq_ind A (add y (add x y))
 305   (\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
 306   (eq_ind A (mult zero one)
 307   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero y)))
 308   (eq_ind_r A (add y one)
 309   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero y)))
 310   (eq_ind_r A (inv zero)
 311   (\lambda x_SupR_785:A.(eq A (mult zero (add y x_SupR_785)) (mult zero y)))
 312   (eq_ind A (add (mult zero y) zero)
 313   (\lambda x_Demod_223:A.(eq A (mult zero (add y (inv zero))) x_Demod_223))
 314   (eq_ind A (mult zero (inv zero))
 315   (\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
 316   (eq_ind A (add (inv zero) zero)
 317   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 318   (eq_ind A (add zero (inv zero))
 319   (\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
 320   (eq_ind A (add y (inv y))
 321   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add y one)))
 322   (eq_ind A (mult (inv y) one)
 323   (\lambda x_SupR_396:A.(eq A (add y x_SupR_396) (add y one)))
 324   (eq_ind_r A (mult one (add y one))
 325   (\lambda x_Demod_199:A.(eq A (add y (mult (inv y) one)) x_Demod_199))
 326   (eq_ind A (add y (inv y))
 327   (\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)
 328   (eq_ind A (mult (add y one) one)
 329   (\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)
 330   (eq_ind A (add x zero)
 331   (\lambda x_Demod_543:A.(eq A (add zero x_Demod_543) (add zero (mult (add x zero) x))))
 332   (eq_ind_r A (mult zero zero)
 333   (\lambda x_Demod_524:A.(eq A (add zero (add x x_Demod_524)) (add zero (mult (add x zero) x))))
 334   (eq_ind_r A (mult x (add x zero))
 335   (\lambda x_SupR_628:A.(eq A (add zero x_SupR_628) (add zero (mult (add x zero) x))))
 336   (eq_ind_r A (mult (add zero (add x zero)) (add zero x))
 337   (\lambda x_Demod_195:A.(eq A (add zero (mult x (add x zero))) x_Demod_195))
 338   (eq_ind_r A (mult (add zero x) (add zero (add x zero)))
 339   (\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))
 340   (eq_ind A (add x zero)
 341   (\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
 342   (eq_ind A (mult zero one)
 343   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero zero)))
 344   (eq_ind_r A (add zero one)
 345   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero zero)))
 346   (eq_ind_r A (inv zero)
 347   (\lambda x_SupR_785:A.(eq A (mult zero (add zero x_SupR_785)) (mult zero zero)))
 348   (eq_ind A (add (mult zero zero) zero)
 349   (\lambda x_Demod_223:A.(eq A (mult zero (add zero (inv zero))) x_Demod_223))
 350   (eq_ind A (mult zero (inv zero))
 351   (\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
 352   (eq_ind A (add (inv zero) zero)
 353   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 354   (eq_ind A (add zero (inv zero))
 355   (\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
 356   (eq_ind A (add zero (inv zero))
 357   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add zero one)))
 358   (eq_ind A (mult (inv zero) one)
 359   (\lambda x_SupR_396:A.(eq A (add zero x_SupR_396) (add zero one)))
 360   (eq_ind_r A (mult one (add zero one))
 361   (\lambda x_Demod_199:A.(eq A (add zero (mult (inv zero) one)) x_Demod_199))
 362   (eq_ind A (add zero (inv zero))
 363   (\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)
 364   (eq_ind A (mult (add zero one) one)
 365   (\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
 366   (eq_ind A (add x zero)
 367   (\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)
 368   (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)))
 369 ). qed.
 370
 371 STOP
 372
 373 auto paramodulation.
 374
 375 qed.
 376
 377 theorem bool4:
 378   \forall A:Set.
 379   \forall one:A.
 380   \forall zero:A.
 381   \forall add: A \to A \to A.
 382   \forall mult: A \to A \to A.
 383   \forall inv: A \to A.
 384   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 385   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 386   \forall d1: (\forall x,y,z:A.
 387               (add x (mult y z)) = (mult (add x y) (add x z))).
 388   \forall d2: (\forall x,y,z:A.
 389               (mult x (add y z)) = (add (mult x y) (mult x z))).
 390   \forall i1: (\forall x:A. (add x zero) = x).
 391   \forall i2: (\forall x:A. (mult x one) = x).
 392   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 393   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 394   \forall x,y,z:A.
 395     (add x y) = (add (add x (mult y z)) y).
 396 intros.
 397 exact
 398 ((eq_ind A (add y (add x (mult y z)))
 399  (\lambda x_DemodGoal_193:A.(eq A (add x y) x_DemodGoal_193))
 400  (eq_ind A x
 401  (\lambda x_DemodGoal_893:A.(eq A x_DemodGoal_893 (add y (add x (mult y z)))))
 402   (eq_ind A y (\lambda x_DemodGoal_894:A.(eq A x x_DemodGoal_894))
 403   (eq_ind A (add y zero) (\lambda x_Demod_554:A.(eq A x x_Demod_554))
 404   (eq_ind_r A (add zero x) (\lambda x_SupR_809:A.(eq A x_SupR_809 (add y zero)))
 405   (eq_ind_r A (add y (mult (add zero y) zero))
 406   (\lambda x_Demod_553:A.(eq A (add zero x) x_Demod_553))
 407   (eq_ind A (add (add zero x) zero)
 408   (\lambda x_Demod_540:A.(eq A x_Demod_540 (add x (mult (add zero x) zero))))
 409   (eq_ind_r A (mult zero x)
 410   (\lambda x_Demod_526:A.(eq A (add (add zero x) x_Demod_526) (add x (mult (add zero x) zero))))
 411   (eq_ind_r A (mult (add zero x) (add (add zero x) x))
 412   (\lambda x_SupR_606:A.(eq A (add (add zero x) (mult zero x)) x_SupR_606))
 413   (eq_ind A (add (add zero x) zero)
 414   (\lambda x_SupR_296:A.(eq A (add (add zero x) (mult zero x)) (mult x_SupR_296 (add (add zero x) x))))
 415   (H2 (add zero x) zero x) (add zero x) (H4 (add zero x))) (add x (mult (add zero x) zero))
 416   (eq_ind A (add x zero)
 417   (\lambda x_SupR_357:A.(eq A (add x (mult (add zero x) zero)) (mult x_SupR_357 (add (add zero x) x))))
 418   (eq_ind A (mult (add (add zero x) x) (add x zero))
 419   (\lambda x_SupR_310:A.(eq A (add x (mult (add zero x) zero)) x_SupR_310))
 420   (eq_ind A (add x (add zero x))
 421   (\lambda x_SupR_302:A.(eq A (add x (mult (add zero x) zero)) (mult x_SupR_302 (add x zero))))
 422   (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
 423   (eq_ind A (mult zero one)
 424   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero x)))
 425   (eq_ind_r A (add x one)
 426   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero x)))
 427   (eq_ind_r A (inv zero)
 428   (\lambda x_SupR_785:A.(eq A (mult zero (add x x_SupR_785)) (mult zero x)))
 429   (eq_ind A (add (mult zero x) zero)
 430   (\lambda x_Demod_223:A.(eq A (mult zero (add x (inv zero))) x_Demod_223))
 431   (eq_ind A (mult zero (inv zero))
 432   (\lambda x_SupR_337:A.(eq A (mult zero (add x (inv zero))) (add (mult zero x) x_SupR_337)))
 433   (H3 zero x (inv zero)) zero (H7 zero)) (mult zero x) (H4 (mult zero x))) one
 434   (eq_ind A (add (inv zero) zero)
 435   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 436   (eq_ind A (add zero (inv zero))
 437   (\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
 438   (eq_ind A (add x (inv x))
 439   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add x one)))
 440   (eq_ind A (mult (inv x) one)
 441   (\lambda x_SupR_396:A.(eq A (add x x_SupR_396) (add x one)))
 442   (eq_ind_r A (mult one (add x one))
 443   (\lambda x_Demod_199:A.(eq A (add x (mult (inv x) one)) x_Demod_199))
 444   (eq_ind A (add x (inv x))
 445   (\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)
 446   (eq_ind A (mult (add x one) one)
 447   (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add x one))))
 448   (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)
 449   (eq_ind A (add zero zero)
 450   (\lambda x_Demod_543:A.(eq A (add y x_Demod_543) (add y (mult (add zero y) zero))))
 451   (eq_ind_r A (mult zero y)
 452   (\lambda x_Demod_524:A.(eq A (add y (add zero x_Demod_524)) (add y (mult (add zero y) zero))))
 453   (eq_ind_r A (mult zero (add zero y))
 454   (\lambda x_SupR_628:A.(eq A (add y x_SupR_628) (add y (mult (add zero y) zero))))
 455   (eq_ind_r A (mult (add y (add zero y)) (add y zero))
 456   (\lambda x_Demod_195:A.(eq A (add y (mult zero (add zero y))) x_Demod_195))
 457   (eq_ind_r A (mult (add y zero) (add y (add zero y)))
 458   (\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))
 459   (eq_ind A (add zero zero)
 460   (\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
 461   (eq_ind A (mult zero one)
 462   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero y)))
 463   (eq_ind_r A (add y one)
 464   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero y)))
 465   (eq_ind_r A (inv zero)
 466   (\lambda x_SupR_785:A.(eq A (mult zero (add y x_SupR_785)) (mult zero y)))
 467   (eq_ind A (add (mult zero y) zero)
 468   (\lambda x_Demod_223:A.(eq A (mult zero (add y (inv zero))) x_Demod_223))
 469   (eq_ind A (mult zero (inv zero))
 470   (\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
 471   (eq_ind A (add (inv zero) zero)
 472   (\lambda x_SupR_463:A.(eq A one x_SupR_463)) (eq_ind A (add zero (inv zero))
 473   (\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
 474   (eq_ind A (add y (inv y))
 475   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add y one)))
 476   (eq_ind A (mult (inv y) one)
 477   (\lambda x_SupR_396:A.(eq A (add y x_SupR_396) (add y one)))
 478   (eq_ind_r A (mult one (add y one))
 479   (\lambda x_Demod_199:A.(eq A (add y (mult (inv y) one)) x_Demod_199))
 480   (eq_ind A (add y (inv y))
 481   (\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)
 482   (eq_ind A (mult (add y one) one)
 483   (\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
 484   (eq_ind A (add x zero)
 485   (\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)))
 486   (sym_eq\subst[A \Assign A ; x \Assign (add y (add x (mult y z))) ; y \Assign y]
 487   (eq_ind_r A (add zero y)
 488   (\lambda x_SupR_826:A.(eq A (add y (add x (mult y z))) x_SupR_826))
 489   (eq_ind_r A (add zero (mult (add y zero) y))
 490   (\lambda x_Demod_553:A.(eq A (add y (add x (mult y z))) x_Demod_553))
 491   (eq_ind A (add (add y (add x (mult y z))) zero)
 492   (\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))))
 493   (eq_ind_r A (mult zero (add x (mult y z)))
 494   (\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))))
 495   (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))))
 496   (\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))
 497   (eq_ind A (add (add y (add x (mult y z))) zero)
 498   (\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))))))
 499   (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))
 500   (eq_ind A (add (add x (mult y z)) y)
 501   (\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))
 502   (\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))))
 503   (\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)
 504   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero (add x (mult y z)))))
 505   (eq_ind_r A (add (add x (mult y z)) one)
 506   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero (add x (mult y z)))))
 507   (eq_ind_r A (inv zero)
 508   (\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)))))
 509   (eq_ind A (add (mult zero (add x (mult y z))) zero)
 510   (\lambda x_Demod_223:A.(eq A (mult zero (add (add x (mult y z)) (inv zero))) x_Demod_223))
 511   (eq_ind A (mult zero (inv zero))
 512   (\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
 513   (eq_ind A (add (inv zero) zero)
 514   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 515   (eq_ind A (add zero (inv zero))
 516   (\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
 517   (eq_ind A (add (add x (mult y z)) (inv (add x (mult y z))))
 518   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add (add x (mult y z)) one)))
 519   (eq_ind A (mult (inv (add x (mult y z))) one)
 520   (\lambda x_SupR_396:A.(eq A (add (add x (mult y z)) x_SupR_396) (add (add x (mult y z)) one)))
 521   (eq_ind_r A (mult one (add (add x (mult y z)) one))
 522   (\lambda x_Demod_199:A.(eq A (add (add x (mult y z)) (mult (inv (add x (mult y z))) one)) x_Demod_199))
 523   (eq_ind A (add (add x (mult y z)) (inv (add x (mult y z))))
 524   (\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)
 525   (\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)
 526   (eq_ind A (add y zero)
 527   (\lambda x_Demod_543:A.(eq A (add zero x_Demod_543) (add zero (mult (add y zero) y))))
 528   (eq_ind_r A (mult zero zero)
 529   (\lambda x_Demod_524:A.(eq A (add zero (add y x_Demod_524)) (add zero (mult (add y zero) y))))
 530   (eq_ind_r A (mult y (add y zero))
 531   (\lambda x_SupR_628:A.(eq A (add zero x_SupR_628) (add zero (mult (add y zero) y))))
 532   (eq_ind_r A (mult (add zero (add y zero)) (add zero y))
 533   (\lambda x_Demod_195:A.(eq A (add zero (mult y (add y zero))) x_Demod_195))
 534   (eq_ind_r A (mult (add zero y) (add zero (add y zero)))
 535   (\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))
 536   (eq_ind A (add y zero)
 537   (\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
 538   (eq_ind A (mult zero one)
 539   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero zero)))
 540   (eq_ind_r A (add zero one)
 541   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero zero)))
 542   (eq_ind_r A (inv zero)
 543   (\lambda x_SupR_785:A.(eq A (mult zero (add zero x_SupR_785)) (mult zero zero)))
 544   (eq_ind A (add (mult zero zero) zero)
 545   (\lambda x_Demod_223:A.(eq A (mult zero (add zero (inv zero))) x_Demod_223))
 546   (eq_ind A (mult zero (inv zero))
 547   (\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
 548   (eq_ind A (add (inv zero) zero)
 549   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 550   (eq_ind A (add zero (inv zero))
 551   (\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
 552   (eq_ind A (add zero (inv zero))
 553   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add zero one)))
 554   (eq_ind A (mult (inv zero) one) (\lambda x_SupR_396:A.(eq A (add zero x_SupR_396) (add zero one)))
 555   (eq_ind_r A (mult one (add zero one))
 556   (\lambda x_Demod_199:A.(eq A (add zero (mult (inv zero) one)) x_Demod_199))
 557   (eq_ind A (add zero (inv zero))
 558   (\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)
 559   (eq_ind A (mult (add zero one) one)
 560   (\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
 561   (eq_ind A (add y zero)
 562   (\lambda x_SupR_299:A.(eq A x_SupR_299 (add zero y))) (H y zero) y (H4 y))))) (add x y)
 563   (sym_eq\subst[A \Assign A ; x \Assign (add x y) ; y \Assign x]
 564   (eq_ind_r A (add zero x)
 565   (\lambda x_SupR_826:A.(eq A (add x y) x_SupR_826))
 566   (eq_ind_r A (add zero (mult (add x zero) x))
 567   (\lambda x_Demod_553:A.(eq A (add x y) x_Demod_553))
 568   (eq_ind A (add (add x y) zero)
 569   (\lambda x_Demod_540:A.(eq A x_Demod_540 (add y (mult (add x y) x))))
 570   (eq_ind_r A (mult zero y)
 571   (\lambda x_Demod_526:A.(eq A (add (add x y) x_Demod_526) (add y (mult (add x y) x))))
 572   (eq_ind_r A (mult (add x y) (add (add x y) y))
 573   (\lambda x_SupR_606:A.(eq A (add (add x y) (mult zero y)) x_SupR_606))
 574   (eq_ind A (add (add x y) zero)
 575   (\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))
 576   (eq_ind A (add y x)
 577   (\lambda x_SupR_357:A.(eq A (add y (mult (add x y) x)) (mult x_SupR_357 (add (add x y) y))))
 578   (eq_ind A (mult (add (add x y) y) (add y x))
 579   (\lambda x_SupR_310:A.(eq A (add y (mult (add x y) x)) x_SupR_310))
 580   (eq_ind A (add y (add x y))
 581   (\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
 582   (eq_ind A (mult zero one)
 583   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero y)))
 584   (eq_ind_r A (add y one)
 585   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero y)))
 586   (eq_ind_r A (inv zero)
 587   (\lambda x_SupR_785:A.(eq A (mult zero (add y x_SupR_785)) (mult zero y)))
 588   (eq_ind A (add (mult zero y) zero)
 589   (\lambda x_Demod_223:A.(eq A (mult zero (add y (inv zero))) x_Demod_223))
 590   (eq_ind A (mult zero (inv zero))
 591   (\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
 592   (eq_ind A (add (inv zero) zero)
 593   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 594   (eq_ind A (add zero (inv zero))
 595   (\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
 596   (eq_ind A (add y (inv y))
 597   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add y one)))
 598   (eq_ind A (mult (inv y) one)
 599   (\lambda x_SupR_396:A.(eq A (add y x_SupR_396) (add y one)))
 600   (eq_ind_r A (mult one (add y one))
 601   (\lambda x_Demod_199:A.(eq A (add y (mult (inv y) one)) x_Demod_199))
 602   (eq_ind A (add y (inv y))
 603   (\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)
 604   (eq_ind A (mult (add y one) one)
 605   (\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)
 606   (eq_ind A (add x zero)
 607   (\lambda x_Demod_543:A.(eq A (add zero x_Demod_543) (add zero (mult (add x zero) x))))
 608   (eq_ind_r A (mult zero zero)
 609   (\lambda x_Demod_524:A.(eq A (add zero (add x x_Demod_524)) (add zero (mult (add x zero) x))))
 610   (eq_ind_r A (mult x (add x zero))
 611   (\lambda x_SupR_628:A.(eq A (add zero x_SupR_628) (add zero (mult (add x zero) x))))
 612   (eq_ind_r A (mult (add zero (add x zero)) (add zero x))
 613   (\lambda x_Demod_195:A.(eq A (add zero (mult x (add x zero))) x_Demod_195))
 614   (eq_ind_r A (mult (add zero x) (add zero (add x zero)))
 615   (\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))
 616   (eq_ind A (add x zero)
 617   (\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
 618   (eq_ind A (mult zero one)
 619   (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero zero)))
 620   (eq_ind_r A (add zero one)
 621   (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero zero)))
 622   (eq_ind_r A (inv zero)
 623   (\lambda x_SupR_785:A.(eq A (mult zero (add zero x_SupR_785)) (mult zero zero)))
 624   (eq_ind A (add (mult zero zero) zero)
 625   (\lambda x_Demod_223:A.(eq A (mult zero (add zero (inv zero))) x_Demod_223))
 626   (eq_ind A (mult zero (inv zero))
 627   (\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
 628   (eq_ind A (add (inv zero) zero)
 629   (\lambda x_SupR_463:A.(eq A one x_SupR_463))
 630   (eq_ind A (add zero (inv zero))
 631   (\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
 632   (eq_ind A (add zero (inv zero))
 633   (\lambda x_Demod_268:A.(eq A x_Demod_268 (add zero one)))
 634   (eq_ind A (mult (inv zero) one)
 635   (\lambda x_SupR_396:A.(eq A (add zero x_SupR_396) (add zero one)))
 636   (eq_ind_r A (mult one (add zero one))
 637   (\lambda x_Demod_199:A.(eq A (add zero (mult (inv zero) one)) x_Demod_199))
 638   (eq_ind A (add zero (inv zero))
 639   (\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)
 640   (eq_ind A (mult (add zero one) one)
 641   (\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
 642   (eq_ind A (add x zero)
 643   (\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)
 644   (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)))
 645 ).
 646 auto paramodulation.
 647
 648 qed.
 649 theorem bool5:
 650   \forall A:Set.
 651   \forall one:A.
 652   \forall zero:A.
 653   \forall add: A \to A \to A.
 654   \forall mult: A \to A \to A.
 655   \forall inv: A \to A.
 656   \forall c1:(\forall x,y:A.(add x y) = (add y x)).
 657   \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
 658   \forall d1: (\forall x,y,z:A.
 659               (add x (mult y z)) = (mult (add x y) (add x z))).
 660   \forall d2: (\forall x,y,z:A.
 661               (mult x (add y z)) = (add (mult x y) (mult x z))).
 662   \forall i1: (\forall x:A. (add x zero) = x).
 663   \forall i2: (\forall x:A. (mult x one) = x).
 664   \forall inv1: (\forall x:A. (add x (inv x)) = one).
 665   \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
 666   \forall x,y:A.
 667     (inv (mult x y)) = (add (inv x) (inv y)).
 668 intros.auto paramodulation.
 669 qed.