% The following op commands allow us to use infix operations
% and omit some parentheses.
% * is the semigroup operation; @ is the commutator.
% x*y*z is right associated; x*y@z is (x*y)@z

op(450, infix, @).
op(400, infix_right, *).

% The lex command determines how equations are oriented and
% whether they are mode into rewrite rules.

lex([A, B, C, D, F, G, e, _@_, _*_]).

set(anl_eq).  % standard equational strategy
set(para_from_units_only).
set(para_into_units_only).

set(hyper_res).  % inference rule for use with cancellation laws

assign(max_weight, 19).
assign(pick_given_ratio, 4).

% Time and memory limits.

assign(max_seconds, 60).
assign(max_mem, 150000).

% Limit the output.

set(order_history).
clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
clear(detailed_history).

list(usable).
x = x.
end_of_list.

list(usable).
% x * y != x * z | y = z.           % left cancellation
% y * x != z * x | y = z.           % right cancellation

% The following forms of cancellation are logically equivalent
% to the preceding, but usually better in practice.

  x * y != u | x * z != u | y = z.  % left cancellation
  y * x != u | z * x != u | y = z.  % right cancellation
end_of_list.

list(sos).
(x * y) * z = x * (y * z).          % * is a semigroup
y * x * (x @ y) = x * y.            % CS admits commutator
end_of_list.

% Prove x@x is a constant which is a left and right identity.

assign(max_proofs, 3).

list(passive).
B @ B != A @ A     | $Ans(constant).
(A @ A) * B != B   | $Ans(left_identity).
B * (A @ A) != B   | $Ans(right_identity).
end_of_list.


