% -------------------------------------------------------------------------
% Prove AIM + {Moufang (M1), LC} => all 7 goals
% -------------------------------------------------------------------------

assign(order, kbo).
set(lex_order_vars).

lex([LEX_1,1,a,K,L,R,T,*,\,/]).   %LOOP_1

set(para_units_only).

assign(max_megs, 8000).
assign(max_weight, 35).
assign(sos_limit,-1).

list(actions).

   % reduce the maximum weight after a while
   given =  30 -> assign(max_weight, 25).

end_of_list.

list(given_selection).
   
   % hint matchers are the highest priority
   part(H, high, weight, hint) = 1.
   
   part(Wf, low, weight, false) = 3.
   
   part(W0w, low, weight, weight <= 20) = 16.
   part(W0a, low, age,    weight <= 20) =  2.
   part(W0r, low, random, weight <= 20) =  5.
   
   part(W1w, low, weight, weight >  20 & weight <= 30) = 8.
   part(W1a, low, age,    weight >  20 & weight <= 30) = 2.
   part(W1r, low, random, weight >  20 & weight <= 30) = 5.
   
   part(W2w, low, weight, weight >  30) = 4.
   part(W2a, low, age,    weight >  30) = 2.
   part(W2r, low, random, weight >  30) = 5.
   
end_of_list.

formulas(assumptions).

   % loop axioms
   1 * x = x.
   x * 1 = x.
   x \ (x * y) = y.
   x * (x \ y) = y.
   (x * y) / y = x.
   (x / y) * y = x.
   
   % associator
   (x * (y * z)) \ ((x * y) * z) = a(x,y,z).
   
   % commutator
   (x * y) \ (y * x) = K(y,x).
   
   % inner mappings
   
   % L(u,x,y) = u L(x) L(y) L(yx)^{-1}
   (y * x) \ (y * (x * u)) = L(u,x,y).
   
   % R(u,x,y) = u R(x) R(y) R(xy)^{-1}
   ((u * x) * y) / (x * y) = R(u,x,y).
   
   % T(u,x) = u R(x) L(x)^{-1}
   x \ (u * x) = T(u,x).
   
   % obvious compatibility
   a(x,y,z) = 1 -> L(z,y,x) = z.
   L(x,y,z) = x -> a(z,y,x) = 1.
   T(x,y) = x -> T(y,x) = y.
   T(x,y) = x -> K(x,y) = 1.
   K(x,y) = 1 -> T(x,y) = x.
   
   % abelian inner mapping group
   T(T(u,x),y) = T(T(u,y),x).
   T(L(u,x,y),z) = L(T(u,z),x,y).
   T(R(u,x,y),z) = R(T(u,z),x,y).
   L(R(u,x,y),z,w) = R(L(u,z,w),x,y).
   L(L(u,x,y),z,w) = L(L(u,z,w),x,y).
   R(R(u,x,y),z,w) = R(R(u,z,w),x,y).

end_of_list.

formulas(goals).

   a(K(x,y),z,u) = 1              # label("aK1").
   a(x,K(y,z),u) = 1              # label("aK2").
   a(x,y,K(z,u)) = 1              # label("aK3").
   K(a(x,y,z),u) = 1              # label("Ka").

   a(a(x,y,z),u,w) = 1            # label("aa1").
   a(x,a(y,z,u),w) = 1            # label("aa2").
   a(x,y,a(z,u,w)) = 1            # label("aa3").

end_of_list.

% --------------------
% Current Special Case
% --------------------

formulas(assumptions).

   ((x * y) * x) * z = x * (y * (x * z)) # label("Moufang (M1)").
   (x * (x * y)) * z = x * (x * (y * z)) # label("LC").

end_of_list.
