assign(order, kbo).
formulas(assumptions).
% identity element
1 * x = x.
x * 1 = x.
% quasigroup
x * (x \ y) = y.
x \ (x * y) = y.
(x * y) / y = x.
(x / y) * y = x.
% inverse property
x' * x = 1.
x * x' = 1.
x' * (x * y) = y.
(y * x) * x' = y.
(x * y)' = y' * x'.
% T(A) is an automorphism
A' * ((u * v) * A) = (A' *
(u * A)) * (A' * (v * A)).
% R(A,x) is an
automorphism
(((u * v) * A) * y) * (A *
y)' = (((u * A) * y) * (A * y)') * (((v * A) * y) * (A * y)').
end_of_list.
formulas(goals).
% R(x,A) is an
automorphism
(((u * v) * x) * A) * (x *
A)' = (((u * x) * A) * (x * A)') * (((v * x) * A) * (x * A)').
end_of_list.
assign(order,
kbo).
formulas(assumptions).
%
identity element
1 * x =
x.
x * 1 =
x.
%
quasigroup
x * (x \
y) = y.
x \ (x *
y) = y.
(x * y)
/ y = x.
(x / y)
* y = x.
%
inverse property
x' * x =
1.
x * x' =
1.
x' * (x
* y) = y.
(y * x)
* x' = y.
(x * y)' = y' * x'.
% T(A) is an automorphism
A' * ((u * v) * A) = (A' *
(u * A)) * (A' * (v * A)).
% R(A,x) is an
automorphism
(((u * v) * A) * y) * (A *
y)' = (((u * A) * y) * (A * y)') * (((v * A) * y) * (A * y)').
% R(x,A) is an
automorphism
(((u * v) * x) * A) * (x *
A)' = (((u * x) * A) * (x * A)') * (((v * x) * A) * (x * A)').
end_of_list.
formulas(goals).
% L(A,x) is an automorphism
(y * A)' * (y * (A * (u *
v))) = ((y * A)' * (y * (A * u))) * ((y * A)' * (y * (A * v))).
end_of_list.
assign(order,
kbo).
formulas(assumptions).
%
identity element
1 * x =
x.
x * 1 =
x.
%
quasigroup
x * (x \
y) = y.
x \ (x *
y) = y.
(x * y)
/ y = x.
(x / y)
* y = x.
%
inverse property
x' * x =
1.
x * x' =
1.
x' * (x
* y) = y.
(y * x)
* x' = y.
(x * y)' = y' * x'.
% T(A) is an automorphism
A' * ((u * v) * A) = (A' *
(u * A)) * (A' * (v * A)).
% R(x,A) is an
automorphism
(((u * v) * x) * A) * (x *
A)' = (((u * x) * A) * (x * A)') * (((v * x) * A) * (x * A)').
end_of_list.
formulas(goals).
% R(A,x) is an
automorphism
(((u * v) * A) * y) * (A *
y)' = (((u * A) * y) * (A * y)') * (((v * A) * y) * (A * y)').
end_of_list.
assign(order, kbo).
formulas(assumptions).
% identity element
1 * x = x.
x * 1 = x.
% quasigroup
x * (x \ y) = y.
x \ (x * y) = y.
(x * y) / y = x.
(x / y) * y = x.
% inverse property
x' * x = 1.
x * x' = 1.
x' * (x * y) = y.
(y * x) * x' = y.
(x * y)' = y' * x'.
% T(A) is an automorphism
A' * ((u * v) * A) = (A' *
(u * A)) * (A' * (v * A)).
% L(A,x) is an
automorphism
(y * A)' * (y * (A * (u *
v))) = ((y * A)' * (y * (A * u))) * ((y * A)' * (y * (A * v))).
end_of_list.
formulas(goals).
% L(x,A) is an
automorphism
(A * x)' * (A * (x * (u *
v))) = ((A * x)' * (A * (x * u))) * ((A * x)' * (A * (x * v))).
end_of_list.
assign(order, kbo).
formulas(assumptions).
% identity element
1 * x = x.
x * 1 = x.
% quasigroup
x * (x \ y) = y.
x \ (x * y) = y.
(x * y) / y = x.
(x / y) * y = x.
% inverse property
x' * x = 1.
x * x' = 1.
x' * (x * y) = y.
(y * x) * x' = y.
(x * y)' = y' * x'.
% T(A) is an automorphism
A' * ((u * v) * A) = (A' *
(u * A)) * (A' * (v * A)).
% L(A,x) is an automorphism
(y * A)' * (y * (A * (u *
v))) = ((y * A)' * (y * (A * u))) * ((y * A)' * (y * (A * v))).
% L(x,A) is an
automorphism
(A * x)' * (A * (x * (u *
v))) = ((A * x)' * (A * (x * u))) * ((A * x)' * (A * (x * v))).
end_of_list.
formulas(goals).
% R(A,x) is an
automorphism
(((u * v) * A) * y) * (A *
y)' = (((u * A) * y) * (A * y)') * (((v * A) * y) * (A * y)').
end_of_list.
assign(order, kbo).
formulas(assumptions).
% identity element
1 * x = x.
x * 1 = x.
% quasigroup
x * (x \ y) = y.
x \ (x * y) = y.
(x * y) / y = x.
(x / y) * y = x.
% inverse property
x' * x = 1.
x * x' = 1.
x' * (x * y) = y.
(y * x) * x' = y.
(x * y)' = y' * x'.
% T(A) is an automorphism
A' * ((u * v) * A) = (A' *
(u * A)) * (A' * (v * A)).
% L(x,A) is an automorphism
(A * x)' * (A * (x * (u *
v))) = ((A * x)' * (A * (x * u))) * ((A * x)' * (A * (x * v))).
end_of_list.
formulas(goals).
% L(A,x) is an
automorphism
(y * A)' * (y * (A * (u *
v))) = ((y * A)' * (y * (A * u))) * ((y * A)' * (y * (A * v))).
end_of_list.