1 include "logic/equality.ma".
3 (* Inclusion of: RNG032-7.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : RNG032-7 : 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 : Augmented. *)
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 : 22 ( 0 non-Horn; 22 unit; 1 RR) *)
29 (* Number of atoms : 22 ( 22 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 : 43 ( 2 singleton) *)
39 (* Maximal term depth : 9 ( 3 average) *)
41 (* Comments : Extra lemmas added to help the ITP prover. *)
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 (* ----The next 7 clause are extra lemmas which Stevens found useful *)
55 (* ----Commutativity for addition *)
57 (* ----Associativity for addition *)
59 (* ----There exists an additive identity element *)
61 (* ----Multiplicative zero *)
63 (* ----Existence of left additive additive_inverse *)
65 (* ----Distributive property of product over sum *)
67 (* ----Inverse of additive_inverse of X is X *)
69 (* ----Right alternative law *)
71 (* ----Left alternative law *)
73 (* input_clause(left_alternative,axiom, *)
75 (* [++equal(multiply(multiply(X,X),Y),multiply(X,multiply(X,Y)))]). *)
80 ntheorem prove_conjecture_3:
81 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
82 ∀add:∀_:Univ.∀_:Univ.Univ.
83 ∀additive_identity:Univ.
84 ∀additive_inverse:∀_:Univ.Univ.
85 ∀associator:∀_:Univ.∀_:Univ.∀_:Univ.Univ.
86 ∀commutator:∀_:Univ.∀_:Univ.Univ.
87 ∀multiply:∀_:Univ.∀_:Univ.Univ.
90 ∀H0:∀X:Univ.∀Y:Univ.eq Univ (commutator X Y) (add (multiply Y X) (additive_inverse (multiply X Y))).
91 ∀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)))).
92 ∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X Y) Y) (multiply X (multiply Y Y)).
93 ∀H3:∀X:Univ.eq Univ (additive_inverse (additive_inverse X)) X.
94 ∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) Z) (add (multiply X Z) (multiply Y Z)).
95 ∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply X Y) (multiply X Z)).
96 ∀H6:∀X:Univ.eq Univ (add X (additive_inverse X)) additive_identity.
97 ∀H7:∀X:Univ.eq Univ (add (additive_inverse X) X) additive_identity.
98 ∀H8:∀X:Univ.eq Univ (multiply X additive_identity) additive_identity.
99 ∀H9:∀X:Univ.eq Univ (multiply additive_identity X) additive_identity.
100 ∀H10:∀X:Univ.eq Univ (add X additive_identity) X.
101 ∀H11:∀X:Univ.eq Univ (add additive_identity X) X.
102 ∀H12:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
103 ∀H13:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).
104 ∀H14:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) (additive_inverse Z)) (add (additive_inverse (multiply X Z)) (additive_inverse (multiply Y Z))).
105 ∀H15:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (additive_inverse X) (add Y Z)) (add (additive_inverse (multiply X Y)) (additive_inverse (multiply X Z))).
106 ∀H16:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X (additive_inverse Y)) Z) (add (multiply X Z) (additive_inverse (multiply Y Z))).
107 ∀H17:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y (additive_inverse Z))) (add (multiply X Y) (additive_inverse (multiply X Z))).
108 ∀H18:∀X:Univ.∀Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
109 ∀H19:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
110 ∀H20:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).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)
117 #additive_identity ##.
118 #additive_inverse ##.
145 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17,H18,H19,H20 ##;
148 (* -------------------------------------------------------------------------- *)