1 include "logic/equality.ma".
3 (* Inclusion of: RNG010-5.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : RNG010-5 : TPTP v3.7.0. Bugfixed v2.3.0. *)
9 (* Domain : Ring Theory (Right alternative) *)
11 (* Problem : Skew symmetry of the auxilliary function *)
13 (* Version : [Ove90] (equality) axioms : *)
15 (* Incomplete > Augmented > Incomplete. *)
17 (* English : The three Moufang identities imply the skew symmetry *)
19 (* of s(W,X,Y,Z) = (W*X,Y,Z) - X*(W,Y,Z) - (X,Y,Z)*W. *)
21 (* Recall that skew symmetry means that the function sign *)
23 (* changes when any two arguments are swapped. This problem *)
25 (* proves the case for swapping the first two arguments. *)
27 (* Refs : [Ove90] Overbeek (1990), ATP competition announced at CADE-10 *)
29 (* : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal *)
31 (* : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11 *)
33 (* : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in *)
35 (* Source : [Ove90] *)
37 (* Names : CADE-11 Competition Eq-9 [Ove90] *)
39 (* : THEOREM EQ-9 [LM93] *)
41 (* : PROBLEM 9 [Zha93] *)
43 (* Status : Unknown *)
45 (* Rating : 1.00 v2.3.0 *)
47 (* Syntax : Number of clauses : 27 ( 0 non-Horn; 27 unit; 2 RR) *)
49 (* Number of atoms : 27 ( 27 equality) *)
51 (* Maximal clause size : 1 ( 1 average) *)
53 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
55 (* Number of functors : 11 ( 5 constant; 0-4 arity) *)
57 (* Number of variables : 52 ( 2 singleton) *)
59 (* Maximal term depth : 6 ( 3 average) *)
61 (* Comments : I copied this directly. I think the Moufang identities may *)
63 (* be wrong. At least they're in another form. *)
65 (* : Yes, now they known to be wrong, and bugfixed in v2.3.0. *)
67 (* Bugfixes : v2.3.0 - Clauses right_moufang and left_moufang fixed. *)
69 (* -------------------------------------------------------------------------- *)
71 (* ----Commutativity of addition *)
73 (* ----Associativity of addition *)
75 (* ----Additive identity *)
77 (* ----Additive inverse *)
79 (* ----Inverse of identity is identity, stupid *)
81 (* ----Axiom of Overbeek *)
83 (* ----Inverse of (x + y) is additive_inverse(x) + additive_inverse(y), *)
85 (* ----Inverse of additive_inverse of X is X *)
87 (* ----Behavior of 0 and the multiplication operation *)
89 (* ----Axiom of Overbeek *)
91 (* ----x * additive_inverse(y) = additive_inverse (x * y), *)
93 (* ----Distributive property of product over sum *)
95 (* ----Right alternative law *)
101 (* ----Middle associator identity *)
103 (* ----Left alternative law *)
105 (* ----Definition of s *)
107 (* ----Right Moufang *)
109 (* ----Left Moufang *)
111 (* ----Middle Moufang *)
112 ntheorem prove_skew_symmetry:
113 (∀Univ:Type.∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.
115 ∀add:∀_:Univ.∀_:Univ.Univ.
116 ∀additive_identity:Univ.
117 ∀additive_inverse:∀_:Univ.Univ.
118 ∀associator:∀_:Univ.∀_:Univ.∀_:Univ.Univ.
121 ∀commutator:∀_:Univ.∀_:Univ.Univ.
123 ∀multiply:∀_:Univ.∀_:Univ.Univ.
124 ∀s:∀_:Univ.∀_:Univ.∀_:Univ.∀_:Univ.Univ.
125 ∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) (multiply Z X)) (multiply (multiply X (multiply Y Z)) X).
126 ∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X (multiply Y X)) Z) (multiply X (multiply Y (multiply X Z))).
127 ∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply Z (multiply X (multiply Y X))) (multiply (multiply (multiply Z X) Y) X).
128 ∀H3:∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (s W X Y Z) (add (add (associator (multiply W X) Y Z) (additive_inverse (multiply X (associator W Y Z)))) (additive_inverse (multiply (associator X Y Z) W))).
129 ∀H4:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X X) Y) (multiply X (multiply X Y)).
130 ∀H5:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply (associator X X Y) X) (associator X X Y)) additive_identity.
131 ∀H6:∀X:Univ.∀Y:Univ.eq Univ (commutator X Y) (add (multiply Y X) (additive_inverse (multiply X Y))).
132 ∀H7:∀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)))).
133 ∀H8:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X Y) Y) (multiply X (multiply Y Y)).
134 ∀H9:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) Z) (add (multiply X Z) (multiply Y Z)).
135 ∀H10:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply X Y) (multiply X Z)).
136 ∀H11:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
137 ∀H12:∀X:Univ.∀Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
138 ∀H13:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).
139 ∀H14:∀X:Univ.eq Univ (multiply additive_identity X) additive_identity.
140 ∀H15:∀X:Univ.eq Univ (multiply X additive_identity) additive_identity.
141 ∀H16:∀X:Univ.eq Univ (additive_inverse (additive_inverse X)) X.
142 ∀H17:∀X:Univ.∀Y:Univ.eq Univ (additive_inverse (add X Y)) (add (additive_inverse X) (additive_inverse Y)).
143 ∀H18:∀X:Univ.∀Y:Univ.eq Univ (add X (add (additive_inverse X) Y)) Y.
144 ∀H19:eq Univ (additive_inverse additive_identity) additive_identity.
145 ∀H20:∀X:Univ.eq Univ (add (additive_inverse X) X) additive_identity.
146 ∀H21:∀X:Univ.eq Univ (add X (additive_inverse X)) additive_identity.
147 ∀H22:∀X:Univ.eq Univ (add additive_identity X) X.
148 ∀H23:∀X:Univ.eq Univ (add X additive_identity) X.
149 ∀H24:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add (add X Y) Z) (add X (add Y Z)).
150 ∀H25:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (s a b c d) (additive_inverse (s b a c d)))
159 #additive_identity ##.
160 #additive_inverse ##.
194 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17,H18,H19,H20,H21,H22,H23,H24,H25 ##;
195 ntry (nassumption) ##;
198 (* -------------------------------------------------------------------------- *)