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.