assign(order, kbo).

formulas(assumptions).

% id

1 * x = x.

x * 1 = x.

% quasigroup

(x * y) / y = x.

(x / y) * y = x.

x * (x \ y) = y.

x \ (x * y) = y.

% A is A2

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

% A in commutant

A * x = x * A.

% B is A2

B * ((x * y) * B) = (B * x) * (y * B).

% B in commutant

B * x = x * B.

end_of_list.

formulas(goals).

% A * B in commutant

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

end_of_list.

assign(order, kbo).

formulas(assumptions).

% id

1 * x = x.

x * 1 = x.

% quasigroup

(x * y) / y = x.

(x / y) * y = x.

x * (x \ y) = y.

x \ (x * y) = y.

% A is A2

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

% A in commutant

A * x = x * A.

% B is A2

B * ((x * y) * B) = (B * x) * (y * B).

% B in commutant

B * x = x * B.

% consequences

% A * B in commutant

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

end_of_list.

formulas(goals).

% A \ B in commutant

(A \ B) * x = x * (A \ B).

end_of_list.

assign(order, kbo).

formulas(assumptions).

% id

1 * x = x.

x * 1 = x.

% quasigroup

(x * y) / y = x.

(x / y) * y = x.

x * (x \ y) = y.

x \ (x * y) = y.

% A is A2

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

% A in commutant

A * x = x * A.

% B is A2

B * ((x * y) * B) = (B * x) * (y * B).

% B in commutant

B * x = x * B.

% consequences

% A * B in commutant

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

% A \ B in commutant

(A \ B) * x = x * (A \ B).

end_of_list.

formulas(goals).

% (A * B) is A2

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

end_of_list.

assign(order, kbo).

formulas(assumptions).

% id

1 * x = x.

x * 1 = x.

% quasigroup

(x * y) / y = x.

(x / y) * y = x.

x * (x \ y) = y.

x \ (x * y) = y.

% A is A2

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

% A in commutant

A * x = x * A.

% B is A2

B * ((x * y) * B) = (B * x) * (y * B).

% B in commutant

B * x = x * B.

% consequences

% A * B in commutant

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

% A \ B in commutant

(A \ B) * x = x * (A \ B).

% (A * B) is A2

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

end_of_list.

formulas(goals).

% (A / B) is A2

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

end_of_list.

assign(order, kbo).

formulas(assumptions).

% id

1 * x = x.

x * 1 = x.

% quasigroup

(x * y) / y = x.

(x / y) * y = x.

x * (x \ y) = y.

x \ (x * y) = y.

% A is A2

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

% A in commutant

A * x = x * A.

% B is A2

B * ((x * y) * B) = (B * x) * (y * B).

% B in commutant

B * x = x * B.

% consequences

% A * B in commutant

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

% A \ B in commutant

(A \ B) * x = x * (A \ B).

% (A * B) is A2

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

% (A / B) is A2

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

end_of_list.

formulas(goals).

% (A \ B) is A2

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

end_of_list.