formulas(assumptions).

%Group (Q,*)
x * (y * z) = (x * y) * z.
x * 0 = x. 0 * x = x.
x * x' = 0. x ' * x = 0.

%uniquely 2 divisible
s(x * x) = x.
s(x) * s(x) = x.

%commutator
r(x,y) = (y * x)' * (x * y).

%class 3 (easier assumption)
r(r(r(x,y),u),z) = 0.

%metabelian (can assume if class 3 assumed)
r(r(x,y),r(u,v)) = 0.

%implied by metabelian assumption
r(s(r(x,y)),z) = s(r(r(x,y),z)).
r(r(x,y),z) * (r(r(z,x),y) * r(r(y,z),x)) = 0.

%associated loop (Q,+)
x + y = (x * y) * s(r(y,x)).
x \ y = s(x' * (y * (x' * y'))) * y.
x \ y = y * s(y' * (x' * (y * x'))).
x + (x \ y) = y.
(x + y)' = x' + y'.
x + y = y + x.
x' + (x + y) = x + (x' + y).

% new stuff
P(x,y) = x' \ (x + y).
P(x,P(y,P(x,z))) = P(P(x,y),z).

%left inner mappings
l(u,x,y) = (y + x) \ (y + (x + u)).

%Reverse Goals

%Automorphic loop
%l(u + v,x,y) = l(u,x,y) + l(v,x,y).
%l(u',x,y) = l(u,x,y)'.

%For Hints

%class 2
%r(r(x,y),z) = 0.
%2 - Engel
%r(r(x,y),y) = 0.

%Easier Goal
l(u',x,y) = l(u,x,y)'.

end_of_list.

formulas(goals).

%Main Goal Automorphic loop
l(u + v,x,y) = l(u,x,y) + l(v,x,y).

%Easier Goal
%l(u',x,y) = l(u,x,y)'.

end_of_list.