1 include "logic/equality.ma".
3 (* Inclusion of: RNG010-7.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : RNG010-7 : TPTP v3.7.0. Bugfixed v2.3.0. *)
9 (* Domain : Ring Theory (Right alternative) *)
11 (* Problem : Skew symmetry of the auxilliary function *)
13 (* Version : [Ste87] (equality) axioms : Augmented. *)
15 (* English : The three Moufang identities imply the skew symmetry *)
17 (* of s(W,X,Y,Z) = (W*X,Y,Z) - X*(W,Y,Z) - (X,Y,Z)*W. *)
19 (* Recall that skew symmetry means that the function sign *)
21 (* changes when any two arguments are swapped. This problem *)
23 (* proves the case for swapping the first two arguments. *)
25 (* Refs : [Ste87] Stevens (1987), Some Experiments in Nonassociative Rin *)
31 (* Status : Unknown *)
33 (* Rating : 1.00 v2.3.0 *)
35 (* Syntax : Number of clauses : 27 ( 0 non-Horn; 27 unit; 1 RR) *)
37 (* Number of atoms : 27 ( 27 equality) *)
39 (* Maximal clause size : 1 ( 1 average) *)
41 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
43 (* Number of functors : 11 ( 5 constant; 0-4 arity) *)
45 (* Number of variables : 58 ( 2 singleton) *)
47 (* Maximal term depth : 6 ( 3 average) *)
49 (* Comments : Extra lemmas added to help the ITP prover. *)
51 (* Bugfixes : v2.3.0 - Clause prove_skew_symmetry fixed. *)
53 (* : v2.3.0 - Left alternative law added in. *)
55 (* : v2.3.0 - Clauses right_moufang and left_moufang fixed. *)
57 (* -------------------------------------------------------------------------- *)
59 (* ----Include nonassociative ring axioms. *)
61 (* Inclusion of: Axioms/RNG003-0.ax *)
63 (* -------------------------------------------------------------------------- *)
65 (* File : RNG003-0 : TPTP v3.7.0. Released v1.0.0. *)
67 (* Domain : Ring Theory (Alternative) *)
69 (* Axioms : Alternative ring theory (equality) axioms *)
71 (* Version : [Ste87] (equality) axioms. *)
75 (* Refs : [Ste87] Stevens (1987), Some Experiments in Nonassociative Rin *)
77 (* Source : [Ste87] *)
83 (* Syntax : Number of clauses : 15 ( 0 non-Horn; 15 unit; 0 RR) *)
85 (* Number of atoms : 15 ( 15 equality) *)
87 (* Maximal clause size : 1 ( 1 average) *)
89 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
91 (* Number of functors : 6 ( 1 constant; 0-3 arity) *)
93 (* Number of variables : 27 ( 2 singleton) *)
95 (* Maximal term depth : 5 ( 2 average) *)
99 (* -------------------------------------------------------------------------- *)
101 (* ----There exists an additive identity element *)
103 (* ----Multiplicative zero *)
105 (* ----Existence of left additive additive_inverse *)
107 (* ----Inverse of additive_inverse of X is X *)
109 (* ----Distributive property of product over sum *)
111 (* ----Commutativity for addition *)
113 (* ----Associativity for addition *)
115 (* ----Right alternative law *)
117 (* ----Left alternative law *)
123 (* -------------------------------------------------------------------------- *)
125 (* -------------------------------------------------------------------------- *)
127 (* ----The next 7 clauses are extra lemmas which Stevens found useful *)
129 (* ----Definition of s *)
131 (* ----Right Moufang *)
133 (* ----Left Moufang *)
134 ntheorem prove_skew_symmetry:
135 (∀Univ:Type.∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.
137 ∀add:∀_:Univ.∀_:Univ.Univ.
138 ∀additive_identity:Univ.
139 ∀additive_inverse:∀_:Univ.Univ.
140 ∀associator:∀_:Univ.∀_:Univ.∀_:Univ.Univ.
143 ∀commutator:∀_:Univ.∀_:Univ.Univ.
145 ∀multiply:∀_:Univ.∀_:Univ.Univ.
146 ∀s:∀_:Univ.∀_:Univ.∀_:Univ.∀_:Univ.Univ.
147 ∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) (multiply Z X)) (multiply (multiply X (multiply Y Z)) X).
148 ∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X (multiply Y X)) Z) (multiply X (multiply Y (multiply X Z))).
149 ∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply Z (multiply X (multiply Y X))) (multiply (multiply (multiply Z X) Y) X).
150 ∀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))).
151 ∀H4:∀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))).
152 ∀H5:∀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))).
153 ∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X (additive_inverse Y)) Z) (add (multiply X Z) (additive_inverse (multiply Y Z))).
154 ∀H7:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y (additive_inverse Z))) (add (multiply X Y) (additive_inverse (multiply X Z))).
155 ∀H8:∀X:Univ.∀Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
156 ∀H9:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
157 ∀H10:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).
158 ∀H11:∀X:Univ.∀Y:Univ.eq Univ (commutator X Y) (add (multiply Y X) (additive_inverse (multiply X Y))).
159 ∀H12:∀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)))).
160 ∀H13:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X X) Y) (multiply X (multiply X Y)).
161 ∀H14:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X Y) Y) (multiply X (multiply Y Y)).
162 ∀H15:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
163 ∀H16:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).
164 ∀H17:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) Z) (add (multiply X Z) (multiply Y Z)).
165 ∀H18:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply X Y) (multiply X Z)).
166 ∀H19:∀X:Univ.eq Univ (additive_inverse (additive_inverse X)) X.
167 ∀H20:∀X:Univ.eq Univ (add X (additive_inverse X)) additive_identity.
168 ∀H21:∀X:Univ.eq Univ (add (additive_inverse X) X) additive_identity.
169 ∀H22:∀X:Univ.eq Univ (multiply X additive_identity) additive_identity.
170 ∀H23:∀X:Univ.eq Univ (multiply additive_identity X) additive_identity.
171 ∀H24:∀X:Univ.eq Univ (add X additive_identity) X.
172 ∀H25:∀X:Univ.eq Univ (add additive_identity X) X.eq Univ (s a b c d) (additive_inverse (s b a c d)))
181 #additive_identity ##.
182 #additive_inverse ##.
216 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 ##;
217 ntry (nassumption) ##;
220 (* -------------------------------------------------------------------------- *)