1 include "logic/equality.ma".
3 (* Inclusion of: RNG025-9.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : RNG025-9 : TPTP v3.7.0. Released v1.0.0. *)
9 (* Domain : Ring Theory (Alternative) *)
11 (* Problem : Middle or Flexible Law *)
13 (* Version : [Ste87] (equality) axioms : Biased. *)
15 (* Theorem formulation : Linearized. *)
19 (* Refs : [Ste87] Stevens (1987), Some Experiments in Nonassociative Rin *)
25 (* Status : Satisfiable *)
27 (* Rating : 0.33 v3.2.0, 0.67 v3.1.0, 0.33 v2.5.0, 0.67 v2.4.0, 0.67 v2.2.1, 0.75 v2.2.0, 0.67 v2.1.0, 1.00 v2.0.0 *)
29 (* Syntax : Number of clauses : 25 ( 0 non-Horn; 25 unit; 1 RR) *)
31 (* Number of atoms : 25 ( 25 equality) *)
33 (* Maximal clause size : 1 ( 1 average) *)
35 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
37 (* Number of functors : 9 ( 4 constant; 0-3 arity) *)
39 (* Number of variables : 54 ( 2 singleton) *)
41 (* Maximal term depth : 4 ( 3 average) *)
43 (* Comments : Biased towards Otter. *)
45 (* -------------------------------------------------------------------------- *)
47 (* ----Don't Include nonassociative ring axioms. *)
49 (* ----The associator has to be replaced by its linearised form. *)
51 (* include('axioms/RNG003-0.ax'). *)
53 (* -------------------------------------------------------------------------- *)
55 (* ----The next 7 clause are extra lemmas which Stevens found useful *)
57 (* ----Commutativity for addition *)
59 (* ----Associativity for addition *)
61 (* ----There exists an additive identity element *)
63 (* ----Multiplicative zero *)
65 (* ----Existence of left additive additive_inverse *)
67 (* ----Distributive property of product over sum *)
69 (* ----Inverse of additive_inverse of X is X *)
71 (* ----Right alternative law *)
73 (* ----Left alternative law *)
77 (* input_clause(associator,axiom, *)
79 (* [++equal(associator(X,Y,Z),add(multiply(multiply(X,Y),Z), *)
81 (* additive_inverse(multiply(X,multiply(Y,Z)))))]). *)
83 (* ----Linearised for of the associator *)
86 ntheorem prove_flexible_law:
87 (∀Univ:Type.∀U:Univ.∀V:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.
89 ∀add:∀_:Univ.∀_:Univ.Univ.
90 ∀additive_identity:Univ.
91 ∀additive_inverse:∀_:Univ.Univ.
92 ∀associator:∀_:Univ.∀_:Univ.∀_:Univ.Univ.
95 ∀commutator:∀_:Univ.∀_:Univ.Univ.
96 ∀multiply:∀_:Univ.∀_:Univ.Univ.
97 ∀H0:∀X:Univ.∀Y:Univ.eq Univ (commutator X Y) (add (multiply Y X) (additive_inverse (multiply X Y))).
98 ∀H1:∀U:Univ.∀V:Univ.∀X:Univ.∀Y:Univ.eq Univ (associator (add U V) X Y) (add (associator U X Y) (associator V X Y)).
99 ∀H2:∀U:Univ.∀V:Univ.∀X:Univ.∀Y:Univ.eq Univ (associator X (add U V) Y) (add (associator X U Y) (associator X V Y)).
100 ∀H3:∀U:Univ.∀V:Univ.∀X:Univ.∀Y:Univ.eq Univ (associator X Y (add U V)) (add (associator X Y U) (associator X Y V)).
101 ∀H4:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X X) Y) (multiply X (multiply X Y)).
102 ∀H5:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X Y) Y) (multiply X (multiply Y Y)).
103 ∀H6:∀X:Univ.eq Univ (additive_inverse (additive_inverse X)) X.
104 ∀H7:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) Z) (add (multiply X Z) (multiply Y Z)).
105 ∀H8:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply X Y) (multiply X Z)).
106 ∀H9:∀X:Univ.eq Univ (add X (additive_inverse X)) additive_identity.
107 ∀H10:∀X:Univ.eq Univ (add (additive_inverse X) X) additive_identity.
108 ∀H11:∀X:Univ.eq Univ (multiply X additive_identity) additive_identity.
109 ∀H12:∀X:Univ.eq Univ (multiply additive_identity X) additive_identity.
110 ∀H13:∀X:Univ.eq Univ (add X additive_identity) X.
111 ∀H14:∀X:Univ.eq Univ (add additive_identity X) X.
112 ∀H15:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
113 ∀H16:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).
114 ∀H17:∀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))).
115 ∀H18:∀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))).
116 ∀H19:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X (additive_inverse Y)) Z) (add (multiply X Z) (additive_inverse (multiply Y Z))).
117 ∀H20:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y (additive_inverse Z))) (add (multiply X Y) (additive_inverse (multiply X Z))).
118 ∀H21:∀X:Univ.∀Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
119 ∀H22:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
120 ∀H23:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).eq Univ (add (associator a b c) (associator a c b)) additive_identity)
130 #additive_identity ##.
131 #additive_inverse ##.
161 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 ##;
162 ntry (nassumption) ##;
165 (* -------------------------------------------------------------------------- *)