% Problem: Units in Strongly Right Alternative Rings
% Status:  Open Problem
%
% In a strongly right alternative ring with unity 1, an element c is a
% unit if there exists d such that c*d = d*c = 1. 
% 
% Problem: Let R be a strongly right alternative ring, and let U(R) be the
% set of all units. Is U(R) a Bol loop?
%
% It is sufficient to check: Is U(R) closed under * ?
% In fact, if a*b = b*a = 1 and c*d = d*c = 1, then a*c has a complicated
% looking right inverse: (a*c) * ((d*((b*(c*a))*b))*d) = 1.
% If a*c has a left inverse at all, then it must be this thing, which
% explains the form of the denial below.
%
% The associator is included below since many proofs in nonassociative
% rings are easier when it is used.
%
% One can certainly load up the input with various facts about right
% alternative rings, such as Mikheev's identity. 
%
% Below the main input file are special cases in which result is is known.

formulas(assumptions).

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

% (R,*,1) strongly right alternative with unity
1 * x = x. x * 1 = x.
(x * y) * y = x * (y * y).
((x * y) * z) * y = x * ((y * z) * y).

% distributive
(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).

% a, c in U(R) with inverses b, d
a * b = 1. b * a = 1.
c * d = 1. d * c = 1.

% goal
((d * ((b * (c * a)) * b)) * d) * (a * c) != 1.

end_of_list.

%%
%% Extra Assumptions
%% 

% left alternative
% (x * x) * y = x * (x * y).

% (-1,1)-ring
% A(x,y,z) + (A(y,z,x) + A(z,x,y)) = 0.

% Join of alternative rings and (-1,1)-rings
%A(x * y,z,x) + (A(z,x,x * y) + A(x,x * y,z)) = (A(x,y,z) + (A(y,z,x) + A(z,x,y))) * x.
%A(x,y,z * x) + (A(y,z * x,x) + A(z * x,x,y)) = x * (A(x,y,z) + (A(y,z,x) + A(z,x,y))).
%A(A(x,y,z) + (A(y,z,x) + A(z,x,y)),u,w) = -A(u,A(x,y,z) + (A(y,z,x) + A(z,x,y)),w).

