assign(order, kbo).

formulas(assumptions).

% L(A) bijects

A * (A \ y) = y.

A \ (A * y) = y.

% R(A) one-to-one

(x * A) / A = x.

% A is an (A) element

% A2

A * ((x * y) * A) = (A * x) * (y * A).

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

end_of_list.

formulas(goals).

% A / A is a left identity element

(A / A) * x = x.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% L(A) bijects

A * (A \ y) = y.

A \ (A * y) = y.

% R(A) one-to-one

(x * A) / A = x.

% A is an (A) element

% A2

A * ((x * y) * A) = (A * x) * (y * A).

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

end_of_list.

formulas(goals).

% A / A is a right identity element

x * (A / A) = x.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% L(A) bijects

A * (A \ y) = y.

A \ (A * y) = y.

% R(A) onto

(x / A) * A = x.

% A is an (A) element

% A2

A * ((x * y) * A) = (A * x) * (y * A).

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

end_of_list.

formulas(goals).

% A / A is a left identity element

(A / A) * x = x.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% L(A) bijects

A * (A \ y) = y.

A \ (A * y) = y.

% R(A) onto

(x / A) * A = x.

% A is an (A) element

% A2

A * ((x * y) * A) = (A * x) * (y * A).

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

end_of_list.

formulas(goals).

% A / A is a left identity element

x * (A / A) = x.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% L(A) onto

A * (A \ y) = y.

% R(A) onto

(x / A) * A = x.

% A is left alternative element

A * (A * x) = (A * A) * x.

% A is an (C) element

% C2

A * (x * (A * y)) = ((A * x) * A) * y.

% C1x

z * (A * (z * y)) = ((z * A) * z) * y.

% C1y

z * (x * (z * A)) = ((z * x) * z) * A.

end_of_list.

formulas(goals).

% A / A is a left identity element

x * (A / A) = x.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% L(A) onto

A * (A \ y) = y.

% R(A) onto

(x / A) * A = x.

% A is left alternative element

A * (A * x) = (A * A) * x.

% A is an (C) element

% C2

A * (x * (A * y)) = ((A * x) * A) * y.

% C1x

z * (A * (z * y)) = ((z * A) * z) * y.

% C1y

z * (x * (z * A)) = ((z * x) * z) * A.

end_of_list.

formulas(goals).

% A / A is a left identity element

(A / A) * x = x.

end_of_list.