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).

%%%%%%%%%%%%%%%%
%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_of_list.
