% Problem: The Circle Operation in Strongly Right Alternative Rings
% Status:  Open Problem
%
% In a strongly right alternative ring R, the "circle" operation is defined
% by x o y = x + y - x*y (just as in associative rings). The magma (R,o) is
% has 0 as its identity element and also satisfies the Bol identity 
% ((xoy)oz)oy = xo((yoz)oy). 
% An element of R is quasi-invertible if it has an inverse in (R,o). 
%
% Problem: Let R be a strongly right alternative ring, and let Q(R) be the
% set of all quasi-invertible elements. Is Q(R) a Bol loop?
%
% It is sufficient to check: Is Q(R) closed under o ?
% In fact, if aob = boa = 0 and cod = doc = o, then aoc has a complicated
% looking right inverse: (aoc) o ((do((bo(coa))ob))od) = o.
% If aoc 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.

op(450,infix,"o").

formulas(assumptions).

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

% (R,*) strongly right alternative
(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).

% circle operation 
x o y = x + (y + (-(x * y))).

% a, c in Q(R) with inverses b, d
a o b = 0. b o a = 0.
c o d = 0. d o c = 0.

% goal
((d o ((b o (c o a)) o b)) o d) o (a o c) != 0.

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).

