% *********************************************************
% AIM:  R1-distributivity => aK1
% *********************************************************

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

set(para_from_small).

clear(back_demod).
set(restrict_denials).

assign(max_weight,5).

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.

   % cancellation laws
   x * y = u & x * z = u -> y = z.
   y * x = u & z * x = u -> y = z.

      % other form
      x * y = x * z -> y = z.
      y * x = z * x -> y = z.

   % useful in demodulation free runs
   x != y | z * x = z * y.
   x != y | x * z = y * z.

   % associator (right associated * a = left associated)
   (x * (y * z)) \ ((x * y) * z) = a(x,y,z) # label("associator").

   % commutator ( (x * y) * K(y,x) = y * x )
   (x * y) \ (y * x) = K(y,x) # label("commutator").

   % inner mappings
   (y * x) \ (y * (x * u)) = L(u,x,y).
   ((u * x) * y) / (x * y) = R(u,x,y).
   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).

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

   R(x1,y,z) * R(x2,y,z) = R(x1 * x2,y,z) # label("R1dist").

end_of_list.

formulas(goals).

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

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

a(K(x,y),z,u) = 1.
1 * x = x.
x * 1 = x.
x \ (x * y) = y.
x * (x \ y) = y.
(x * y) / y = x.
(x / y) * y = x.
x * y != z | x * u != z | u = y.
x * y != z | u * y != z | u = x.
x * y != x * z | y = z.
x * y != z * y | x = z.
(x * (y * z)) \ ((x * y) * z) = a(x,y,z).
a(x,y,z) = (x * (y * z)) \ ((x * y) * z).
(x * y) \ (y * x) = K(y,x).
K(x,y) = (y * x) \ (x * y).
(x * y) \ (x * (y * z)) = L(z,y,x).
L(x,y,z) = (z * y) \ (z * (y * x)).
((x * y) * z) / (y * z) = R(x,y,z).
R(x,y,z) = ((x * y) * z) / (y * z).
x \ (y * x) = T(y,x).
T(x,y) = y \ (x * y).
L(x,y,z) != x | a(z,y,x) = 1.
T(T(x,y),z) = T(T(x,z),y).
T(L(x,y,z),u) = L(T(x,u),y,z).
L(T(x,y),z,u) = T(L(x,z,u),y).
T(R(x,y,z),u) = R(T(x,u),y,z).
R(T(x,y),z,u) = T(R(x,z,u),y).
L(R(x,y,z),u,w) = R(L(x,u,w),y,z).
R(x,y,z) * R(u,y,z) = R(x * u,y,z).
a(K(c1,c2),c3,c4) != 1.
1 \ x = x.
x \ x = 1.
x / x = 1.
x / 1 = x.
x / (y \ x) = y.
(x / y) \ x = y.
x != y * z | y \ x = z.
x * y != z | x \ z = y.
x * 1 != y | x = y.
x != y * z | x / z = y.
x * y != z | z / y = x.
(x * (y * z)) * a(x,y,z) = (x * y) * z.
(x * y) * L(z,y,x) = x * (y * z).
L(x \ y,x,z) = (z * x) \ (z * y).
L(x,y,z / y) = z \ ((z / y) * (y * x)).
x \ ((x / y) * (y * z)) = L(z,y,x / y).
R(1,x,y) = (x * y) / (x * y).
(x * y) / (x * y) = R(1,x,y).
R(x,y,1) = (x * y) / (y * 1).
(x * y) / (y * 1) = R(x,y,1).
R(x,x \ y,z) = (y * z) / ((x \ y) * z).
R(x,y,y \ z) = ((x * y) * (y \ z)) / z.
((x * y) * (y \ z)) / z = R(x,y,y \ z).
R(x,y,z) * (y * z) = (x * y) * z.
R(x / y,y,z) = (x * z) / (y * z).
R(x,y / z,z) = ((x * (y / z)) * z) / y.
((x * (y / z)) * z) / y = R(x,y / z,z).
x * T(y,x) = y * x.
T(x / y,y) = y \ x.
x * y != z | x = z / y.
R(x,y,z) = R(x * u,y,z) / R(u,y,z).
R(x * y,z,u) / R(y,z,u) = R(x,z,u).
x * y != z | y = x \ z.
R(x,y,z) = R(u,y,z) \ R(u * x,y,z).
R(x,y,z) \ R(x * u,y,z) = R(u,y,z).
(x * y) / T(x,y) = y.
R(x,y,z) \ ((x * y) * z) = y * z.
R(x,y,T(z,y)) = ((x * y) * T(z,y)) / (z * y).
((x * y) * T(z,y)) / (z * y) = R(x,y,T(z,y)).
T(x,T(y,x)) = T(y,x) \ (y * x).
T(x,y) \ (x * y) = T(y,T(x,y)).
x * T(T(y,x),z) = T(y,z) * x.
x * R(T(y,x),z,u) = R(y,z,u) * x.
R(1,x,y) = 1.
(x * y) / y = R(x,y,1).
R(x,y,1) = x.
x * T(x \ y,z) = T(y / x,z) * x.
T(x / y,z) * y = y * T(y \ x,z).
x * (y * z) != (x * y) * u | L(z,y,x) = u.
(x * y) * z != x * (y * u) | L(u,y,x) = z.
T(x,x * y) = L(y \ (x * y),y,x).
L(x \ (y * x),x,y) = T(y,y * x).
L(T(x,y) \ z,T(x,y),y) = (x * y) \ (y * z).
R(x,y / z,z) * y = (x * (y / z)) * z.
a(R(x,y,z),y,z) = ((x * y) * z) \ ((R(x,y,z) * y) * z).
((x * y) * z) \ ((R(x,y,z) * y) * z) = a(R(x,y,z),y,z).
R(1 / x,x,y) = y / (x * y).
R(x / y,y,y \ z) = (x * (y \ z)) / z.
R((x / y) / z,z,y) = x / (z * y).
R(T(x / y,z),y,u) = T((x * u) / (y * u),z).
T((x * y) / (z * y),u) = R(T(x / z,u),z,y).
R(1 / x,x,x \ y) = (x \ y) / y.
R(T(1 / x,y),x,z) = T(z / (x * z),y).
T(x / (y * x),z) = R(T(1 / y,z),y,x).
R(1 / x,x,y) \ y = x * y.
R(x,x \ 1,y) \ y = (x \ 1) * y.
L(T(x,y),y,x) = T(x,x * y).
L(T(T(x,y),z),y,x) = T(T(x,x * y),z).
R(T((x / y) / z,u),z,y) = T(x / (z * y),u).
(x / (y * z)) * R(u,y,z) = R(((x / z) / y) * u,y,z).
R(((x / y) / z) * u,z,y) = (x / (z * y)) * R(u,z,y).
R(x,x \ (y / z),z) = y / ((x \ (y / z)) * z).
R(1 / x,x,x \ 1) = x \ 1.
R(x,y,y \ 1) * (y \ 1) = R(x * (1 / y),y,y \ 1).
R(x * (1 / y),y,y \ 1) = R(x,y,y \ 1) * (y \ 1).
x * R(x \ y,z,u) = R(y / x,z,u) * x.
R(x / y,z,u) * y = y * R(y \ x,z,u).
(x * T(x \ y,z)) / x = T(y / x,z).
(x * T(y,z)) / x = T((x * y) / x,z).
R(x,y * z,a(x,y,z)) \ ((x * y) * z) = (y * z) * a(x,y,z).
L(x,y,1 / y) = (1 / y) * (y * x).
(1 / x) * (x * y) = L(y,x,1 / x).
(1 / x) * (y * x) = L(T(y,x),x,1 / x).
L(T(x,y),y,1 / y) = (1 / y) * (x * y).
(1 / x) * (R(y,z,u) * x) = L(R(T(y,x),z,u),x,1 / x).
L(R(T(x,y),z,u),y,1 / y) = (1 / y) * (R(x,z,u) * y).
R(x,y,y \ 1) = (x * y) * (y \ 1).
(x * y) * (y \ 1) = R(x,y,y \ 1).
R(x,y,y \ 1) / (y \ 1) = x * y.
R(x,y,y \ 1) != z * (y \ 1) | x * y = z.
R(x,1 / y,y) = (x * (1 / y)) * y.
(x * (1 / y)) * y = R(x,1 / y,y).
R(x,1 / y,y) / y = x * (1 / y).
R(x,y,z) / R(u,y,z) = R(x / u,y,z).
R(x,y,z) \ R(u,y,z) = R(x \ u,y,z).
T(R(x / y,y,y \ z),z) = z \ (x * (y \ z)).
T(x / ((1 / x) * x),y) / x = T(1 / (1 / x),y) * (1 / x).
(x * y) * T(T(x,x * y),z) = x * (y * T(T(x,y),z)).
L(R(T(x,y),z,u),y,1 / y) = R((1 / y) * (x * y),z,u).
1 / R(x,y,z) = R(1 / x,y,z).
R(1 / x,y,z) = 1 / R(x,y,z).
R(1 / x,y,z) \ 1 = R(x,y,z).
(x \ 1) \ 1 = R(x,x,x \ 1).
R(x,x,x \ 1) = (x \ 1) \ 1.
(x * R(x \ y,z,u)) / x = R(y / x,z,u).
(x * R(y,z,u)) / x = R((x * y) / x,z,u).
R((x * y) / x,z,u) = (x * R(y,z,u)) / x.
R((x * y) / x,y,y \ 1) = (x * ((y \ 1) \ 1)) / x.
R(x,y,T(x,y)) = T(((x * y) * x) / (x * y),y).
T(((x * y) * x) / (x * y),y) = R(x,y,T(x,y)).
L(R(T(x,y) \ z,u,w),T(x,y),y) = R((x * y) \ (y * z),u,w).
T((x * y) / (z * y),z) = R(z \ x,z,y).
T(x / (y * z),y) = R(y \ (x / z),y,z).
R(x \ (y / z),x,z) = T(y / (x * z),x).
R(T(x / y,z),y,y \ z) = z \ (x * (y \ z)).
R(T(x / y,x),y,y \ x) = y \ x.
R(T(x / (x / y),x),x / y,(x / y) \ x) = y.
R(T(x / (x / y),x),x / y,y) = y.
x * y = (T(y / (y / x),y) * (y / x)) * x.
(T(x / (x / y),x) * (x / y)) * y = y * x.
((x / y) * T((x / y) \ x,x)) * y = y * x.
((x / y) * T(y,x)) * y = y * x.
(x * y) / x = (y / x) * T(x,y).
(x / y) * T(y,x) = (y * x) / y.
((x * y) / x) / T(x,y) = y / x.
(x / y) \ ((y * x) / y) = T(y,x).
T(x,y) = (y / x) \ ((x * y) / x).
T(x / y,T(y,x)) = T(y,x) \ ((y * x) / y).
T(x,y) \ ((x * y) / x) = T(y / x,T(x,y)).
((x * y) / y) / T(y,T(x,y)) = T(x,y) / y.
T(x,y * x) = y \ ((x * (y * x)) / x).
x \ ((y * (x * y)) / y) = T(y,x * y).
R(T(x,y * x),y,x) = T((x * (y * x)) / (y * x),y).
T((x * (y * x)) / (y * x),y) = R(T(x,y * x),y,x).
x / T(y,T(x,y)) = T(x,y) / y.
T(x,y) = R(T(x,y * x),y,x).
R(T(x,y * x),y,x) = T(x,y).
T(x / (y * z),R(u,y,z)) = R(u,y,z) \ R(((x / z) / y) * u,y,z).
R(x,y,z) \ R(((u / z) / y) * x,y,z) = T(u / (y * z),R(x,y,z)).
(x * (1 / y)) * y = R(x,y,y \ 1).
R(x,y,y \ 1) = R(x,1 / y,y).
R(x,1 / y,y) = R(x,y,y \ 1).
R(x,y,y \ 1) = R(x,y \ 1,(y \ 1) \ 1).
R(x,y \ 1,(y \ 1) \ 1) = R(x,y,y \ 1).
x * (y * T(T(x,y),z)) = T(x,z) * (x * y).
x * (T(x,y) * z) = T(x,y) * (x * z).
T(x,y) * (x * z) = x * (T(x,y) * z).
T(x,y) \ (x * (T(x,y) * z)) = x * z.
T(x,y) * z = x * (T(x,y) * (x \ z)).
x * (T(x,y) * (x \ z)) = T(x,y) * z.
T(x,y) \ (x * z) = x * (T(x,y) \ z).
x \ (T(x,y) * z) = T(x,y) * (x \ z).
T(x,y) \ x = x * (T(x,y) \ 1).
x * (T(x,y) \ 1) = T(x,y) \ x.
x * (T(x,y) \ y) = T(y,T(x,y)).
(x / y) * ((y \ x) \ y) = T(y,T(x / y,y)).
x \ T(x,y) = T(x,y) * (x \ 1).
T(x,y) * (x \ 1) = x \ T(x,y).
(x / y) * ((y \ x) \ y) = T(y,y \ x).
((x * y) / x) * (y \ x) = T(x,x \ (x * y)).
((x * y) / x) * (y \ x) = T(x,y).
T(x,y) = ((x * y) / x) * (y \ x).
T(x,y) / (y \ x) = (x * y) / x.
T(x,R(y,y \ 1,x)) = ((x * R(y,y \ 1,x)) / x) * ((y \ 1) * x).
((x * R(y,y \ 1,x)) / x) * ((y \ 1) * x) = T(x,R(y,y \ 1,x)).
T(x * y,x) / y = ((x * y) * x) / (x * y).
((x * y) * x) / (x * y) = T(x * y,x) / y.
T(x,x / y) / y = (x * (x / y)) / x.
T(T(x,x / y) / y,x) = x \ (x * (x / y)).
T(T(x * y,x) / y,y) = R(x,y,T(x,y)).
R(x,y,T(x,y)) = y \ T(x * y,x).
x \ T(y * x,y) = R(y,x,T(y,x)).
x \ T(y,y / x) = R(y / x,x,T(y / x,x)).
R(x / y,y,T(x / y,y)) = y \ T(x,x / y).
T(T(x,x / y) / y,x) = x / y.
T(T(R(x,y,y \ 1),R(x,y,y \ 1) / (y \ 1)) / (y \ 1),R(x,y,y \ 1)) = x * y.
R(x / y,y,y \ x) = y \ T(x,x / y).
x \ T(y,y / x) = (y * (x \ y)) / y.
(x / y) \ T(x,x / (x / y)) = (x * y) / x.
R((1 / x) * (y * x),z,u) = (1 / x) * (R(y,z,u) * x).
T(x / 1,y) / x = T(1 / (1 / x),y) * (1 / x).
T(1 / (1 / x),y) * (1 / x) = T(x / 1,y) / x.
T(1 / (1 / x),y) * (1 / x) = T(x,y) / x.
T(x,y) / x = (1 / x) * T((1 / x) \ 1,y).
(1 / x) * T((1 / x) \ 1,y) = T(x,y) / x.
(1 / x) * T(x,y) = T(x,y) / x.
R((x * y) / x,y \ 1,x) * ((y \ 1) * x) = T(x,R(y,y \ 1,x)).
T(x,R(y,y \ 1,x)) = (((x * y) / x) * (y \ 1)) * x.
(((x * y) / x) * (y \ 1)) * x = T(x,R(y,y \ 1,x)).
T(x / (y * z),R(u,y,z)) = R(u \ (((x / z) / y) * u),y,z).
R(x \ (((y / z) / u) * x),u,z) = T(y / (u * z),R(x,u,z)).
R(T((x / y) / z,u),z,y) = T(x / (z * y),R(u,z,y)).
T(x / (y * z),R(u,y,z)) = T(x / (y * z),u).
T(x,R(y,z,u)) = T((x * (z * u)) / (z * u),y).
T((x * (y * z)) / (y * z),u) = T(x,R(u,y,z)).
T(x,y) = T(x,R(y,z,u)).
T(x,R(y,z,u)) = T(x,y).
T(x,(y \ 1) \ 1) = T(x,y).
T(x,y \ z) = T(x,T(z / y,z)).
T(x,T(y / z,y)) = T(x,z \ y).
T(x,T(y,z)) = T(x,T(y,z * y)).
T(x,T(y,z * y)) = T(x,T(y,z)).
T(T(R(x,y,y \ 1),x * y) / (y \ 1),R(x,y,y \ 1)) = x * y.
T(R(T(x,x * y),y,y \ 1) / (y \ 1),R(x,y,y \ 1)) = x * y.
T(T(x,x * y) * y,R(x,y,y \ 1)) = x * y.
x * y = T(T(x,x * y) * y,x).
T(T(x,x * y) * y,x) = x * y.
T(T(x,x * (x \ y)) * (x \ y),x) = y.
T(T(x,y) * (x \ y),x) = y.
x * y = (T(x,y) * (x \ y)) * x.
(T(x,y) * (x \ y)) * x = x * y.
T(T(R(x,x \ 1,y),y) * ((x \ 1) * y),R(x,x \ 1,y)) = y.
(T(x,y) * (x \ y)) * (y \ 1) = T(T(x,y) * (x \ y),x) \ (T(x,y) * (x \ y)).
T(T(x,y) * (x \ y),x) \ (T(x,y) * (x \ y)) = (T(x,y) * (x \ y)) * (y \ 1).
(x * y) / x = T(x,y) * (x \ y).
T(x,y) * (x \ y) = (x * y) / x.
T(x,y) \ ((x * y) / x) = x \ y.
x \ y = T(y / x,T(x,y)).
T(x / y,T(y,x)) = y \ x.
T(x,T(y,x * y)) = y \ (x * y).
T(x,y) = T(x,T(y,x * y)).
T(x,T(y,x * y)) = T(x,y).
T(x,y) = T(x,T(y,x)).
T(x,T(y,x)) = T(x,y).
x / T(y,x) = T(x,y) / y.
T(x,y) / y = x / T(y,x).
x * (T(x,y) \ y) = T(y,x).
T(x,x / y) = T(x,y \ x).
(x / T(y,x)) \ T(x,y) = y.
T(x,x / (x / y)) = T(x,y).
(x / y) \ T(x,y) = (x * y) / x.
T(R(T(x,y),x \ 1,y) * ((x \ 1) * y),R(x,x \ 1,y)) = y.
T((T(x,y) * (x \ 1)) * y,R(x,x \ 1,y)) = y.
T((x \ T(x,y)) * y,R(x,x \ 1,y)) = y.
x = T((y \ T(y,x)) * x,y).
T((x \ T(x,y)) * y,x) = y.
T(x,y) = T(x,(x \ T(x,y)) * y).
T(x,(x \ T(x,y)) * y) = T(x,y).
(x / y) \ T(x,(x \ T(x,y)) * y) = (x \ T(x,y)) * y.
(x / y) \ T(x,y) = (x \ T(x,y)) * y.
(x \ T(x,y)) * y = (x * y) / x.
((x * y) / x) / y = x \ T(x,y).
x \ (T(y,x) * (y \ x)) = (T(y,x) * (y \ x)) * (x \ 1).
(T(x,y) * (x \ y)) * (y \ 1) = y \ (T(x,y) * (x \ y)).
((x * y) / x) * (y \ 1) = y \ (T(x,y) * (x \ y)).
x \ (T(y,x) * (y \ x)) = ((y * x) / y) * (x \ 1).
x \ ((y * x) / y) = ((y * x) / y) * (x \ 1).
((x * y) / x) * (y \ 1) = y \ ((x * y) / x).
R((x * y) / x,y \ 1,(y \ 1) \ 1) / ((y \ 1) \ 1) = y \ ((x * y) / x).
(x \ ((y * x) / y)) * y = T(y,R(x,x \ 1,y)).
R(x,x \ ((y * x) / y),y) = (y * x) / T(y,R(x,x \ 1,y)).
(x * y) / T(x,R(y,y \ 1,x)) = R(y,y \ ((x * y) / x),x).
(x * y) / T(x,y) = R(y,y \ ((x * y) / x),x).
R(x,x \ ((y * x) / y),y) = (y * x) / T(y,x).
R(x,x \ ((y * x) / y),y) = x.
((x * (x \ ((y * x) / y))) * y) \ ((x * (x \ ((y * x) / y))) * y) = a(R(x,x \ ((y * x) / y),y),x \ ((y * x) / y),y).
R((x * y) / x,y,y \ 1) / ((y \ 1) \ 1) = y \ ((x * y) / x).
((x * ((y \ 1) \ 1)) / x) / ((y \ 1) \ 1) = y \ ((x * y) / x).
x \ ((y * x) / y) = y \ T(y,(x \ 1) \ 1).
x \ T(x,(y \ 1) \ 1) = y \ ((x * y) / x).
x \ T(x,y) = y \ ((x * y) / x).
x \ ((y * x) / y) = y \ T(y,x).
x * (y \ T(y,x)) = (y * x) / y.
(x * y) / x != y * z | x \ T(x,y) = z.
a(R(x,x \ ((y * x) / y),y),x \ ((y * x) / y),y) = 1.
a(x,x \ ((y * x) / y),y) = 1.
a(T(x,y),T(x,y) \ ((x * y) / y),y) = 1.
a(T(x,y),T(x,y) \ x,y) = 1.
R(T(x,y),(T(x,y) \ x) * y,1) \ ((T(x,y) * (T(x,y) \ x)) * y) = ((T(x,y) \ x) * y) * a(T(x,y),T(x,y) \ x,y).
T(x,y) \ ((T(x,y) * (T(x,y) \ x)) * y) = ((T(x,y) \ x) * y) * a(T(x,y),T(x,y) \ x,y).
((T(x,y) \ x) * y) * a(T(x,y),T(x,y) \ x,y) = T(x,y) \ ((T(x,y) * (T(x,y) \ x)) * y).
((T(x,y) \ x) * y) * a(T(x,y),T(x,y) \ x,y) = T(x,y) \ (x * y).
((T(x,y) \ x) * y) * a(T(x,y),T(x,y) \ x,y) = x * (T(x,y) \ y).
((T(x,y) \ x) * y) * a(T(x,y),T(x,y) \ x,y) = T(y,x).
((T(x,y) \ x) * y) * 1 = T(y,x).
(T(x,y) \ x) * y = T(y,x).
T(x,y) / x = T(y,x) \ y.
T(x,y) \ x = T(y,x) / y.
(R(T(x,y),z,u) \ R(x,z,u)) * y = T(y,R(x,z,u)).
R(T(x,y) \ x,y,z) \ (T(y,x) * z) = y * z.
R((1 / x) * T(x,y),z,u) = (1 / x) * (R(T(y,x) \ y,z,u) * x).
(1 / x) * (R(T(y,x) \ y,z,u) * x) = R((1 / x) * T(x,y),z,u).
R(T(x,y) \ x,z,u) * y = T(y,R(x,z,u)).
R(T(x,y) \ x,z,u) * y = T(y,x).
x * y != T(y,z) | x = T(z,y) \ z.
R(T(x,y) \ x,z,u) = T(x,y) \ x.
T(x,y) \ x = (z * u) / (((T(x,y) \ x) \ z) * u).
(x * y) / (((T(z,u) \ z) \ x) * y) = T(z,u) \ z.
(T(x,y) \ x) \ (T(y,x) * z) = y * z.
(T(x,y) \ x) \ z = y * (T(y,x) \ z).
(T(x,y) \ x) \ x = T(x,y).
(x * y) / (T(x,z) * y) = T(x,z) \ x.
x / (T(y,z) * (y \ x)) = T(y,z) \ y.
(T(x,y) \ x) \ z = T(x,y) * (x \ z).
T(x,y) * (x \ z) = y * (T(y,x) \ z).
x * (T(x,y) \ x) = (y * x) / y.
(x * y) / x = y * (T(y,x) \ y).
x \ T(x,y) = T(y,x) \ y.
T(x,y) \ x = y \ T(y,x).
L(x \ T(x,y),T(y,x),x) = (y * x) \ (x * y).
L(R(x \ T(x,y),z,u),T(y,x),x) = R((y * x) \ (x * y),z,u).
x \ T(x,y) = T(x,y) / x.
T(x,y) / x = x \ T(x,y).
(1 / x) * T(x,y) = x \ T(x,y).
K(x,y) = L(x \ T(x,y),T(y,x),x).
(1 / x) * T(x,y) = R((1 / x) * T(x,y),z,u).
R((1 / x) * T(x,y),z,u) = (1 / x) * T(x,y).
R((1 / x) * T(x,y),z,u) = x \ T(x,y).
R(x \ T(x,y),z,u) = x \ T(x,y).
L(x \ T(x,y),T(y,x),x) = R((y * x) \ (x * y),z,u).
R((x * y) \ (y * x),z,u) = L(y \ T(y,x),T(x,y),y).
K(x,y) = R((y * x) \ (x * y),z,u).
R((x * y) \ (y * x),z,u) = K(y,x).
R(K(x,y),z,u) = K(x,y).
K(x,y) * (z * u) = (K(x,y) * z) * u.
(K(x,y) * z) * u = K(x,y) * (z * u).
L(x,y,K(z,u)) = x.

end_of_list.
