assign(eq_defs, fold).

formulas(sos).

% Nonassociative Ring

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

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

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

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

(x * y) * x = x * (y * x).       % flexible

(B * A) * A != B * (A * A).      % denial of right

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

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

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

end_of_list.