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