matita/tests/TPTP/Veloci/RNG011-5.p.ma

   1
   2 include "logic/equality.ma".
   3 (* Inclusion of: RNG011-5.p *)
   4 (* -------------------------------------------------------------------------- *)
   5 (*  File     : RNG011-5 : TPTP v3.1.1. Released v1.0.0. *)
   6 (*  Domain   : Ring Theory *)
   7 (*  Problem  : In a right alternative ring (((X,X,Y)*X)*(X,X,Y)) = Add Id *)
   8 (*  Version  : [Ove90] (equality) axioms : *)
   9 (*             Incomplete > Augmented > Incomplete. *)
  10 (*  English  :  *)
  11 (*  Refs     : [Ove90] Overbeek (1990), ATP competition announced at CADE-10 *)
  12 (*           : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal  *)
  13 (*           : [LM93]  Lusk & McCune (1993), Uniform Strategies: The CADE-11  *)
  14 (*           : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in *)
  15 (*  Source   : [Ove90] *)
  16 (*  Names    : CADE-11 Competition Eq-10 [Ove90] *)
  17 (*           : THEOREM EQ-10 [LM93] *)
  18 (*           : PROBLEM 10 [Zha93] *)
  19 (*  Status   : Unsatisfiable *)
  20 (*  Rating   : 0.00 v2.0.0 *)
  21 (*  Syntax   : Number of clauses     :   22 (   0 non-Horn;  22 unit;   2 RR) *)
  22 (*             Number of atoms       :   22 (  22 equality) *)
  23 (*             Maximal clause size   :    1 (   1 average) *)
  24 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
  25 (*             Number of functors    :    8 (   3 constant; 0-3 arity) *)
  26 (*             Number of variables   :   37 (   2 singleton) *)
  27 (*             Maximal term depth    :    5 (   2 average) *)
  28 (*  Comments :  *)
  29 (* -------------------------------------------------------------------------- *)
  30 (* ----Commutativity of addition  *)
  31 (* ----Associativity of addition  *)
  32 (* ----Additive identity  *)
  33 (* ----Additive inverse  *)
  34 (* ----Inverse of identity is identity, stupid  *)
  35 (* ----Axiom of Overbeek  *)
  36 (* ----Inverse of (x + y) is additive_inverse(x) + additive_inverse(y),  *)
  37 (* ----Inverse of additive_inverse of X is X  *)
  38 (* ----Behavior of 0 and the multiplication operation  *)
  39 (* ----Axiom of Overbeek  *)
  40 (* ----x * additive_inverse(y) = additive_inverse (x * y),  *)
  41 (* ----Distributive property of product over sum  *)
  42 (* ----Right alternative law  *)
  43 (* ----Associator  *)
  44 (* ----Commutator  *)
  45 (* ----Middle associator identity  *)
  46 theorem prove_equality:
  47  \forall Univ:Set.
  48 \forall a:Univ.
  49 \forall add:\forall _:Univ.\forall _:Univ.Univ.
  50 \forall additive_identity:Univ.
  51 \forall additive_inverse:\forall _:Univ.Univ.
  52 \forall associator:\forall _:Univ.\forall _:Univ.\forall _:Univ.Univ.
  53 \forall b:Univ.
  54 \forall commutator:\forall _:Univ.\forall _:Univ.Univ.
  55 \forall multiply:\forall _:Univ.\forall _:Univ.Univ.
  56 \forall H0:\forall X:Univ.\forall Y:Univ.eq Univ (multiply (multiply (associator X X Y) X) (associator X X Y)) additive_identity.
  57 \forall H1:\forall X:Univ.\forall Y:Univ.eq Univ (commutator X Y) (add (multiply Y X) (additive_inverse (multiply X Y))).
  58 \forall H2:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (associator X Y Z) (add (multiply (multiply X Y) Z) (additive_inverse (multiply X (multiply Y Z)))).
  59 \forall H3:\forall X:Univ.\forall Y:Univ.eq Univ (multiply (multiply X Y) Y) (multiply X (multiply Y Y)).
  60 \forall H4:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (multiply (add X Y) Z) (add (multiply X Z) (multiply Y Z)).
  61 \forall H5:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply X Y) (multiply X Z)).
  62 \forall H6:\forall X:Univ.\forall Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
  63 \forall H7:\forall X:Univ.\forall Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
  64 \forall H8:\forall X:Univ.\forall Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).
  65 \forall H9:\forall X:Univ.eq Univ (multiply additive_identity X) additive_identity.
  66 \forall H10:\forall X:Univ.eq Univ (multiply X additive_identity) additive_identity.
  67 \forall H11:\forall X:Univ.eq Univ (additive_inverse (additive_inverse X)) X.
  68 \forall H12:\forall X:Univ.\forall Y:Univ.eq Univ (additive_inverse (add X Y)) (add (additive_inverse X) (additive_inverse Y)).
  69 \forall H13:\forall X:Univ.\forall Y:Univ.eq Univ (add X (add (additive_inverse X) Y)) Y.
  70 \forall H14:eq Univ (additive_inverse additive_identity) additive_identity.
  71 \forall H15:\forall X:Univ.eq Univ (add (additive_inverse X) X) additive_identity.
  72 \forall H16:\forall X:Univ.eq Univ (add X (additive_inverse X)) additive_identity.
  73 \forall H17:\forall X:Univ.eq Univ (add additive_identity X) X.
  74 \forall H18:\forall X:Univ.eq Univ (add X additive_identity) X.
  75 \forall H19:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (add (add X Y) Z) (add X (add Y Z)).
  76 \forall H20:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (multiply (multiply (associator a a b) a) (associator a a b)) additive_identity
  77 .
  78 intros.
  79 autobatch paramodulation timeout=100;
  80 try assumption.
  81 print proofterm.
  82 qed.
  83 (* -------------------------------------------------------------------------- *)