1 include "logic/equality.ma".
3 (* Inclusion of: RNG009-5.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : RNG009-5 : TPTP v3.7.0. Released v1.0.0. *)
9 (* Domain : Ring Theory *)
11 (* Problem : If X*X*X = X then the ring is commutative *)
13 (* Version : [Peterson & Stickel, 1981] (equality) axioms : *)
15 (* Reduced > Incomplete. *)
17 (* English : Given a ring in which for all x, x * x * x = x, prove that *)
19 (* for all x and y, x * y = y * x. *)
21 (* Refs : [PS81] Peterson & Stickel (1981), Complete Sets of Reductions *)
23 (* : [Ove90] Overbeek (1990), ATP competition announced at CADE-10 *)
25 (* : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal *)
27 (* : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11 *)
29 (* : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in *)
31 (* Source : [Ove90] *)
33 (* Names : CADE-11 Competition Eq-7 [Ove90] *)
35 (* : THEOREM EQ-7 [LM93] *)
37 (* : PROBLEM 7 [Zha93] *)
39 (* Status : Unsatisfiable *)
41 (* Rating : 0.56 v3.4.0, 0.62 v3.3.0, 0.50 v3.1.0, 0.44 v2.7.0, 0.36 v2.6.0, 0.17 v2.5.0, 0.25 v2.4.0, 0.00 v2.2.1, 0.67 v2.2.0, 0.71 v2.1.0, 1.00 v2.0.0 *)
43 (* Syntax : Number of clauses : 9 ( 0 non-Horn; 9 unit; 1 RR) *)
45 (* Number of atoms : 9 ( 9 equality) *)
47 (* Maximal clause size : 1 ( 1 average) *)
49 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
51 (* Number of functors : 6 ( 3 constant; 0-2 arity) *)
53 (* Number of variables : 17 ( 0 singleton) *)
55 (* Maximal term depth : 3 ( 2 average) *)
59 (* -------------------------------------------------------------------------- *)
61 (* ----Right identity and inverse *)
63 (* ----Distributive property of product over sum *)
65 (* ----Associativity of addition *)
67 (* ----Commutativity of addition *)
69 (* ----Associativity of product *)
70 ntheorem prove_commutativity:
71 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
73 ∀add:∀_:Univ.∀_:Univ.Univ.
74 ∀additive_identity:Univ.
75 ∀additive_inverse:∀_:Univ.Univ.
77 ∀multiply:∀_:Univ.∀_:Univ.Univ.
78 ∀H0:∀X:Univ.eq Univ (multiply X (multiply X X)) X.
79 ∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).
80 ∀H2:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).
81 ∀H3:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add (add X Y) Z) (add X (add Y Z)).
82 ∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) Z) (add (multiply X Z) (multiply Y Z)).
83 ∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply X Y) (multiply X Z)).
84 ∀H6:∀X:Univ.eq Univ (add X (additive_inverse X)) additive_identity.
85 ∀H7:∀X:Univ.eq Univ (add X additive_identity) X.eq Univ (multiply a b) (multiply b a))
93 #additive_identity ##.
105 nauto by H0,H1,H2,H3,H4,H5,H6,H7 ##;
106 ntry (nassumption) ##;
109 (* -------------------------------------------------------------------------- *)