% benchmark parameters -N8 -p

% Find a noncommutative ring.  To make it more difficult, assume
% the ring has a unit.

op(450, xfx, +). % sum
op(400, xfx, *). % product
op(350, fy, ~).  % minus

list(usable).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% RING AXIOMS

% <+,~,0> is an Abelian group:

0+x=x.
x+0=x.
~x+x=0.
x+ ~x=0.
(x+y)+z=x+ (y+z).
x+y=y+x.

% Product is associative:

(x*y)*z=x* (y*z).

% Left and right distributivity:

x* (y+z)=x*y+x*z.
(y+z)*x=y*x+z*x.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Ring lemmas

~ ~x=x.
~0=0.
0*x=0.
x*0=0.

% Assume the ring has a unit.

1*x=x.
x*1=x.

% There are 2 noncommuting elements.

a*b!=b*a.

% Using constants a and b as the noncommuting elements allows
% the possibility that they can be 0 or 1.
% Since 0 and 1 commute with everything, we could fix the
% noncommuting elements by using 2*3!=3*2 instead.
% In general it's a good idea to do this, but it doesn't make
% much difference in this case.
%
% 2*3!=3*2.

end_of_list.
