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.