formulas(assumptions).
%%%%%%%%%%%%%%%%%%%%%
%Cancellative semigroup without unit:
%%%%%%%%%%%%%%%%%%%%%
(x * y) * z = x * (y * z).
(x * y = x * z) -> y = z.
(x * y = z * y) -> x = z.
x * y != x.
x * y != y.
%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%Equidivisibility:
%%%%%%%%%%%%%%%%%%%%%
(x * y = u * v)
-> (x = u
| (exists w1 (x * w1 = u))
| (exists w2 (w2 * y = v))
) # label("EQD").
%%%%%%%%%%%%%%%%%%%%%
%Power relation:
%
% Power(x,y): x = y^n for some n >= 1
%%%%%%%%%%%%%%%%%%%%%
Power(x,x).
Power(x,y) & Power(y,z) -> Power(x,z).
%%%%%%%%%%%%%compatibility with *
Power(y,x) & Power(z,x) -> Power(y * z,x).
Power(y,x) & Power(z,x)
-> (y = z
| (exists u
(Power(u,x)
& ((y = z * u & y = u * z ) | (z = y * u & z = u * y ))))
).
%%%%%%%%%(breaking the power)
Power(y * z,x) ->
(
(Power(y,x) & Power(z,x)) |
(exists u exists v (
u * v = x
& (y = u | (exists y1 (y = y1 * u & Power(y1,x))))
& (z = v | (exists z1 (z = v * z1 & Power(z1,x))))
))
).
%%%%%%%%%%%%%%(no nontrivial shift)
(Power(y,x) & Power(u * (y * v), x))
-> (exists z (Power(y,z) & Power(u,z) & Power(v,z))).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Partial (non-reflexive, i.e. strict) order of lengths. Shorter(x,y) reads "x is shorter than y"):
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-Shorter(x,x).
Shorter(x,y) -> -Shorter(y,x).
Shorter(x,y) & Shorter(y,z) -> Shorter(x,z).
%%%%%%%%%%(compatible with *):
Shorter(x,x * y).
Shorter(x,y * x).
%%%%%%%%%%%%%(cancellation of length)
Shorter(x,y) <-> Shorter(x * z,y * z).
Shorter(x,y) <-> Shorter(z * x,z * y).
Shorter(x,y) <-> Shorter(x * z,z * y).
Shorter(x,y) <-> Shorter(z * x,y * z).
%%%%%%%%%
%Prefix relation
%%%%%%%%%%%
Prefix(x,y) <-> (exists z (x * z) = y).
%BEGIN
%%%%%%%%%%%%%%%%
%Suffix relation
%%%%%%%%%%%%%%%%%
Suffix(x,y) <-> (exists z (z * x) = y).
%%%%%%%%%%%%%%
%Period relation. Period(x,y) reads "x is a period of y"
%%%%%%%%%%%%%%%
Period(x,y) <-> (exists z (Power(z,x) & Prefix(y,z))).
END%
end_of_list.