helm/software/matita/contribs/ng_TPTP/RNG011-5.ma

   1 include "logic/equality.ma".
   2
   3 (* Inclusion of: RNG011-5.p *)
   4
   5 (* -------------------------------------------------------------------------- *)
   6
   7 (*  File     : RNG011-5 : TPTP v3.7.0. Released v1.0.0. *)
   8
   9 (*  Domain   : Ring Theory *)
  10
  11 (*  Problem  : In a right alternative ring (((X,X,Y)*X)*(X,X,Y)) = Add Id *)
  12
  13 (*  Version  : [Ove90] (equality) axioms : *)
  14
  15 (*             Incomplete > Augmented > Incomplete. *)
  16
  17 (*  English  :  *)
  18
  19 (*  Refs     : [Ove90] Overbeek (1990), ATP competition announced at CADE-10 *)
  20
  21 (*           : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal  *)
  22
  23 (*           : [LM93]  Lusk & McCune (1993), Uniform Strategies: The CADE-11  *)
  24
  25 (*           : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in *)
  26
  27 (*  Source   : [Ove90] *)
  28
  29 (*  Names    : CADE-11 Competition Eq-10 [Ove90] *)
  30
  31 (*           : THEOREM EQ-10 [LM93] *)
  32
  33 (*           : PROBLEM 10 [Zha93] *)
  34
  35 (*  Status   : Unsatisfiable *)
  36
  37 (*  Rating   : 0.00 v2.0.0 *)
  38
  39 (*  Syntax   : Number of clauses     :   22 (   0 non-Horn;  22 unit;   2 RR) *)
  40
  41 (*             Number of atoms       :   22 (  22 equality) *)
  42
  43 (*             Maximal clause size   :    1 (   1 average) *)
  44
  45 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
  46
  47 (*             Number of functors    :    8 (   3 constant; 0-3 arity) *)
  48
  49 (*             Number of variables   :   37 (   2 singleton) *)
  50
  51 (*             Maximal term depth    :    5 (   2 average) *)
  52
  53 (*  Comments :  *)
  54
  55 (* -------------------------------------------------------------------------- *)
  56
  57 (* ----Commutativity of addition  *)
  58
  59 (* ----Associativity of addition  *)
  60
  61 (* ----Additive identity  *)
  62
  63 (* ----Additive inverse  *)
  64
  65 (* ----Inverse of identity is identity, stupid  *)
  66
  67 (* ----Axiom of Overbeek  *)
  68
  69 (* ----Inverse of (x + y) is additive_inverse(x) + additive_inverse(y),  *)
  70
  71 (* ----Inverse of additive_inverse of X is X  *)
  72
  73 (* ----Behavior of 0 and the multiplication operation  *)
  74
  75 (* ----Axiom of Overbeek  *)
  76
  77 (* ----x * additive_inverse(y) = additive_inverse (x * y),  *)
  78
  79 (* ----Distributive property of product over sum  *)
  80
  81 (* ----Right alternative law  *)
  82
  83 (* ----Associator  *)
  84
  85 (* ----Commutator  *)
  86
  87 (* ----Middle associator identity  *)
  88 ntheorem prove_equality:
  89  (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
  90 ∀a:Univ.
  91 ∀add:∀_:Univ.∀_:Univ.Univ.
  92 ∀additive_identity:Univ.
  93 ∀additive_inverse:∀_:Univ.Univ.
  94 ∀associator:∀_:Univ.∀_:Univ.∀_:Univ.Univ.
  95 ∀b:Univ.
  96 ∀commutator:∀_:Univ.∀_:Univ.Univ.
  97 ∀multiply:∀_:Univ.∀_:Univ.Univ.
  98 ∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply (associator X X Y) X) (associator X X Y)) additive_identity.
  99 ∀H1:∀X:Univ.∀Y:Univ.eq Univ (commutator X Y) (add (multiply Y X) (additive_inverse (multiply X Y))).
 100 ∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (associator X Y Z) (add (multiply (multiply X Y) Z) (additive_inverse (multiply X (multiply Y Z)))).
 101 ∀H3:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X Y) Y) (multiply X (multiply Y Y)).
 102 ∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) Z) (add (multiply X Z) (multiply Y Z)).
 103 ∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply X Y) (multiply X Z)).
 104 ∀H6:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
 105 ∀H7:∀X:Univ.∀Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
 106 ∀H8:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).
 107 ∀H9:∀X:Univ.eq Univ (multiply additive_identity X) additive_identity.
 108 ∀H10:∀X:Univ.eq Univ (multiply X additive_identity) additive_identity.
 109 ∀H11:∀X:Univ.eq Univ (additive_inverse (additive_inverse X)) X.
 110 ∀H12:∀X:Univ.∀Y:Univ.eq Univ (additive_inverse (add X Y)) (add (additive_inverse X) (additive_inverse Y)).
 111 ∀H13:∀X:Univ.∀Y:Univ.eq Univ (add X (add (additive_inverse X) Y)) Y.
 112 ∀H14:eq Univ (additive_inverse additive_identity) additive_identity.
 113 ∀H15:∀X:Univ.eq Univ (add (additive_inverse X) X) additive_identity.
 114 ∀H16:∀X:Univ.eq Univ (add X (additive_inverse X)) additive_identity.
 115 ∀H17:∀X:Univ.eq Univ (add additive_identity X) X.
 116 ∀H18:∀X:Univ.eq Univ (add X additive_identity) X.
 117 ∀H19:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add (add X Y) Z) (add X (add Y Z)).
 118 ∀H20:∀X:Univ.∀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)
 119 .
 120 #Univ ##.
 121 #X ##.
 122 #Y ##.
 123 #Z ##.
 124 #a ##.
 125 #add ##.
 126 #additive_identity ##.
 127 #additive_inverse ##.
 128 #associator ##.
 129 #b ##.
 130 #commutator ##.
 131 #multiply ##.
 132 #H0 ##.
 133 #H1 ##.
 134 #H2 ##.
 135 #H3 ##.
 136 #H4 ##.
 137 #H5 ##.
 138 #H6 ##.
 139 #H7 ##.
 140 #H8 ##.
 141 #H9 ##.
 142 #H10 ##.
 143 #H11 ##.
 144 #H12 ##.
 145 #H13 ##.
 146 #H14 ##.
 147 #H15 ##.
 148 #H16 ##.
 149 #H17 ##.
 150 #H18 ##.
 151 #H19 ##.
 152 #H20 ##.
 153 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17,H18,H19,H20 ##;
 154 ntry (nassumption) ##;
 155 nqed.
 156
 157 (* -------------------------------------------------------------------------- *)