1 include "logic/equality.ma".
3 (* Inclusion of: RNG032-6.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : RNG032-6 : TPTP v3.2.0. Released v1.0.0. *)
9 (* Domain : Ring Theory (Right alternative) *)
11 (* Problem : 6*assr(X,X,Y)^6 = additive identity *)
13 (* Version : [Ste87] (equality) axioms : Reduced > Complete. *)
17 (* Refs : [Ste87] Stevens (1987), Some Experiments in Nonassociative Rin *)
19 (* Source : [Ste87] *)
21 (* Names : Conjecture 3 [Ste87] *)
25 (* Rating : 1.00 v2.0.0 *)
27 (* Syntax : Number of clauses : 15 ( 0 non-Horn; 15 unit; 1 RR) *)
29 (* Number of atoms : 15 ( 15 equality) *)
31 (* Maximal clause size : 1 ( 1 average) *)
33 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
35 (* Number of functors : 8 ( 3 constant; 0-3 arity) *)
37 (* Number of variables : 25 ( 2 singleton) *)
39 (* Maximal term depth : 9 ( 2 average) *)
43 (* -------------------------------------------------------------------------- *)
45 (* ----Don't Include nonassociative ring axioms. *)
47 (* ----The left alternative law has to be omitted. *)
49 (* include('axioms/RNG003-0.ax'). *)
51 (* -------------------------------------------------------------------------- *)
53 (* ----Commutativity for addition *)
55 (* ----Associativity for addition *)
57 (* ----There exists an additive identity element *)
59 (* ----Multiplicative zero *)
61 (* ----Existence of left additive additive_inverse *)
63 (* ----Distributive property of product over sum *)
65 (* ----Inverse of additive_inverse of X is X *)
67 (* ----Right alternative law *)
69 (* ----Left alternative law *)
71 (* input_clause(left_alternative,axiom, *)
73 (* [++equal(multiply(multiply(X,X),Y),multiply(X,multiply(X,Y)))]). *)
78 ntheorem prove_conjecture_3:
79 ∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
80 ∀add:∀_:Univ.∀_:Univ.Univ.
81 ∀additive_identity:Univ.
82 ∀additive_inverse:∀_:Univ.Univ.
83 ∀associator:∀_:Univ.∀_:Univ.∀_:Univ.Univ.
84 ∀commutator:∀_:Univ.∀_:Univ.Univ.
85 ∀multiply:∀_:Univ.∀_:Univ.Univ.
88 ∀H0:∀X:Univ.∀Y:Univ.eq Univ (commutator X Y) (add (multiply Y X) (additive_inverse (multiply X Y))).
89 ∀H1:∀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)))).
90 ∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X Y) Y) (multiply X (multiply Y Y)).
91 ∀H3:∀X:Univ.eq Univ (additive_inverse (additive_inverse X)) X.
92 ∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) Z) (add (multiply X Z) (multiply Y Z)).
93 ∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply X Y) (multiply X Z)).
94 ∀H6:∀X:Univ.eq Univ (add X (additive_inverse X)) additive_identity.
95 ∀H7:∀X:Univ.eq Univ (add (additive_inverse X) X) additive_identity.
96 ∀H8:∀X:Univ.eq Univ (multiply X additive_identity) additive_identity.
97 ∀H9:∀X:Univ.eq Univ (multiply additive_identity X) additive_identity.
98 ∀H10:∀X:Univ.eq Univ (add X additive_identity) X.
99 ∀H11:∀X:Univ.eq Univ (add additive_identity X) X.
100 ∀H12:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
101 ∀H13:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (add (add (add (add (add (multiply (associator x x y) (multiply (associator x x y) (associator x x y))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) additive_identity
129 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13;
132 (* -------------------------------------------------------------------------- *)