% Problem: Mikheev's Identity in Strongly Right Alternative Rings
% Status:  Challenge Problem
%
% A nonassociative ring (R,+,*) is said to be right alternative if the
% following identity holds:  (x*y)*y = x*(y*y). A right alternative ring
% is strongly right alternative if it also satisfies the Bol identity
% ((x*y)*z)*y = x*((y*z)*y).  (If the underlying abelian group (R,+) has
% no elements of order 2, then a right alternative ring is strongly right
% alternative.)
%
% The associator A(x,y,z) is defined by
%  A(x,y,z) = -(x*(y*z)) + ((x*y)*z)
% Mikheev's identity in strongly right alternative rings is A(x,x,y)^4 = 0.
% 
% I.M. Mikheev, An identity in right alternative rings,
% Algebra i Logika, Vol. 8, No. 3, pp. 357-366, May-June, 1969. 
% (translated in Algebra & Logic.) 
%
% Mikheev also constructed a 13-dimensional example where the "4" cannot be
% replaced by "2". 
%
% Mikheev actually stated his result under the additional assumption that 
% (R,+) has no elements of order 2, i.e. x+x=0 implies x=0. However,
% I *think* that his proof never uses this assumption explicitly, but rather
% uses only the Bol identity. I am not sure of this because Mikheev's paper
% is quite difficult to read, and I have never worked through all the 
% details. In any case, the additional assumption is included below but is
% commented out.

formulas(assumptions).

% (R,+,0) is an abelian group
0 + x = x. -x + x = 0.
x + y = y + x. (x + y) + z = x + (y + z).

% no elements of order 2
% x + x = 0 -> x = 0.
% x + x = y + y -> x = y. % equivalent

% (R,*) is strongly right alternative
(x * y) * y = x * (y * y).
((x * y) * z) * y = x * ((y * z) * y).

% distributive laws
(x * y) + (x * z) = x * (y + z).
(y * x) + (z * x) = (y + z) * x.
0 * x = 0. x * 0 = 0.

% associator
-(x * (y * z)) + ((x * y) * z) = A(x,y,z).

end_of_list.

formulas(goals).
% Mikheev's identity
A(x,x,y) * (A(x,x,y) * (A(x,x,y) * A(x,x,y))) = 0.
end_of_list.
