% --------------------------------------------------------------------------
% Gagola:  Prove the 24 lemmas on Lemma List 0.
% --------------------------------------------------------------------------

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

set(para_from_small).

clear(back_demod).
set(restrict_denials).

assign(max_weight, 5).

formulas(assumptions).

% two-sided identity
1 * x = x.
x * 1 = x.

% inverses (and IP and AAIP)
x * x' = 1.
x' * x = 1.
x' * (x * y) = y.
(y * x) * x' = y.
(x * y)' = y' * x'.

% alternative
(x * x) * y = x * (x * y).
(y * x) * x = y * (x * x).

% flexible
x * (y * x) = (x * y) * x.

% Moufang
((x * y) * x) * z = x * (y * (x * z)).
((z * x) * y) * x = z * (x * (y * x)).
(x * y) * (z * x) = x * ((y * z) * x).
(x * y) * (z * x) = (x * (y * z)) * x.

% R(u,x,y) = u R(x) R(y) R(xy)^{-1}
R(u,x,y) = ((u * x) * y) * (x * y)'.

% C in commutant
C * x = x * C.

% ***********
% Definitions
% ***********

% associator (for Normality Condition 4)

   (x * y) * z = (x * (y * z)) * a(x,y,z) # label("associator").

end_of_list.

% --------------------------------------------------------------------------
% Lemma List 0:  Associator lemmas for C (C versions of Lemmas 2-13 to 2-37.
% --------------------------------------------------------------------------

formulas(goals).

% R(C,y) and R(y,C) are automorphisms
R(u * v,C,y) = R(u,C,y) * R(v,C,y) # label("Lemma 0-13").
R(u * v,y,C) = R(u,y,C) * R(v,y,C) # label("Lemma 0-14").

% associator identities involving C
a(C,x',y) = a(x',y,C) # label("Lemma 0-15").
a(C,x',y) = a(C',y,x') # label("Lemma 0-16").
a(C,x',y) = a(y,C,x') # label("Lemma 0-17").
a(C,x',y) = a(x',C,y') # label("Lemma 0-18").
a(C,x',y) = a(C',x,y) # label("Lemma 0-19").
a(C,x',y) = a(C',x',y') # label("Lemma 0-20").
a(C,x',y) = a(y',x',C) # label("Lemma 0-21").
a(C,x',y) = a(C,y',x') # label("Lemma 0-22").
a(C,x',y) = a(C,x,y') # label("Lemma 0-23").
a(C,x',y) = a(x,y',C) # label("Lemma 0-24").
a(C,x',y) = a(C',y',x) # label("Lemma 0-25").
a(C,x',y) = a(y',C,x) # label("Lemma 0-26").
a(C,x',y) = a(y,C',x) # label("Lemma 0-27").
a(C,x',y) = a(x,C',y') # label("Lemma 0-28,0-36").
a(C,x',y) = a(y',C',x') # label("Lemma 0-29").
a(C,x',y) = a(x',C',y) # label("Lemma 0-30").
a(C,x',y) = a(x,y,C') # label("Lemma 0-31").
a(C,x',y) = a(y,x',C') # label("Lemma 0-32").
a(C,x',y) = a(y',x,C') # label("Lemma 0-33").
a(C,x',y) = a(x',y',C') # label("Lemma 0-34").
a(C,x',y) = a(C,y',x') # label("Lemma 0-35").
% a(C,x',y) = a(x,C',y') # label("Lemma 0-36").  % same as 0-28
a(C,x',y) = a(C',y,x') # label("Lemma 0-37").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

formulas(hints).

a(C,x',y) = a(C,y',x').
x * 1 = x.
x' * x = 1.
x' * (x * y) = y.
(x * y) * y' = x.
(x * y)' = y' * x'.
x' * y' = (y * x)'.
x * (y * x) = (x * y) * x.
(x * y) * x = x * (y * x).
((x * y) * x) * z = x * (y * (x * z)).
((x * y) * z) * y = x * (y * (z * y)).
(x * y) * (z * x) = x * ((y * z) * x).
R(x,y,z) = ((x * y) * z) * (y * z)'.
((x * y) * z) * (y * z)' = R(x,y,z).
C * x = x * C.
(x * y) * z = (x * (y * z)) * a(x,y,z).
(x * (y * z)) * a(x,y,z) = (x * y) * z.
x'' * 1 = x.
(x * y)' * x = y'.
x * (y * x)' = y'.
x * y' = y' * ((y * x) * y').
x' * ((x * y) * x') = y * x'.
(x * (y * x)) * z = x * (y * (x * z)).
(x * (y * (z * y))) * y' = (x * y) * z.
(x' * y) * z = x' * ((y * (z * x)) * x').
x' * ((y * (z * x)) * x') = (x' * y) * z.
R(x,y,z) * z = (x * y) * (z * ((y * z)' * z)).
(x * y) * (z * ((y * z)' * z)) = R(x,y,z) * z.
(x * (y * (z * y))) * (z * y)' = R(x * y,z,y).
R(x,y,z) * (z * (y * z)')' = R(x * y,z,(y * z)').
x' * (C * x) = C.
x = x''.
x'' = x.
x * (x' * y) = y.
(x * y') * y = x.
x * y' = (y * x')'.
(x * y')' = y * x'.
x' * y = (y' * x)'.
(x' * y)' = y' * x.
((x * y) * x) * (x' * z) = x * (y * z).
((x * y) * (y' * z)) * z' = R(x,y,y' * z).
(x * (y' * z')) * (z * y) = x.
(x * y) * (z * y)' = R(x * z',z,y).
R(x * y',y,z) = (x * z) * (y * z)'.
R(x,y,z) * (y * z) = (x * y) * z.
((x * y) * z)' * (x * (y * z)) = a(x,y,z)'.
x' * y = y * ((x * y)' * y).
x * ((y * x)' * x) = y' * x.
(x * (y * x)')' = y.
(x * y') * z' = (z * (y * x'))'.
((x * y) * z') * (z * y') = R(x,y,z').
(x' * y)' = x * ((y * x)' * x).
x * ((y * x)' * x) = (x' * y)'.
x * (y * x') = (x * y) * x'.
(x * y) * x' = x * (y * x').
(x * (y * (x * z))) * z' = x * (y * x).
C * (x * (y * x)) = x * (y * (x * C)).
(x * y) * z = x * ((y * x') * (x * z)).
x * ((y * x') * (x * z)) = (x * y) * z.
(x * (((x * y) * z)' * x)) * (y * z) = x * a(x,y,z)'.
((x * y') * z') * (z * y) = R(x,y',z').
(x * (y * (x * C))) * x' = (C * x) * y.
(x * y) * (y' * z) = R(x,y,z) * z.
R(x,y,z) * z = (x * y) * (y' * z).
(x * y) * (z' * y)' = R(x,y,z) * z.
R(x,y,z) * z = (x * y) * (z' * y)'.
((x * y) * (y' * z)) * z' = R(x,y,z).
R(x * y,x,z) * z = x * (y * z).
R(x,y',z) * z = y' * ((y * x) * z).
(x * (y * z)) * z' = R(x * y,x,z).
R(x * y,x,z) = (x * (y * z)) * z'.
R(x,y,z) * z = y * ((y' * x) * z).
R(x,y,z) = (y * ((y' * x) * z)) * z'.
(x * ((x' * y) * z)) * z' = R(y,x,z).
x' * R(y * z,y,x) = (x' * y) * z.
(x * y') * z' = x * (((x * z) * y)' * x).
x * (((x * y) * z)' * x) = (x * z') * y'.
x * R(y,z,x') = (x * (y * z)) * z'.
(x * (y * z)) * z' = x * R(y,z,x').
R(x,y,z) * y = R(x * y,z,(y * z)').
R(x * y,z,(y * z)') = R(x,y,z) * y.
(C * x) * y = x * ((y * (x * C)) * x').
x * ((y * (x * C)) * x') = (C * x) * y.
R(x * y'',y',z) = R(x,z,y) * y.
x * ((x' * y) * z) = R(y * z,y,x).
R(x * y,x,z) = z * ((z' * x) * y).
R(x,y,z) = z * ((z' * y) * (y' * x)).
x * ((x' * y) * (y' * z)) = R(z,y,x).
R(x,y,z) * z = R(x * z,x,y).
R(x * y,x,z) = R(x,z,y) * y.
R(x * y,x,z) * y' = R(x,z,y).
(R(x,y,z) * z) * y = x * (z * y).
((R(x,y,z) * z) * y) * (z * y)' = x.
R(x,y,y' * z) = R(x,y,z).
R(x,y,z) = R(x,y,y * z).
R(x,y,y * z) = R(x,y,z).
R(x,y,(z * y)') = R(x,y,z').
R(x,y * z,z') = R(x,y * z,y).
R(x,y',C) = R(x,y',C * y).
R(x,y',C * y) = R(x,y',C).
R(x * y,x,z) * y' = R(x,x * z,y).
x = R(R(x,y,z),z,y).
R(R(x,y,z),z,y) = x.
(x * (y * C)) * y' = x * R(C,y,x').
x * R(y,z * y,x') = R(x * y,z,y).
R(x * y,x,z) = x * R(y,z,x').
x * R(y,z,x') = R(x * y,x,z).
x' * R(x * y,x,z) = R(y,z,x').
C' * R(x * C,C,y) = R(x,y,C').
R(x,y,z) * y = R(x * y,z,y').
R(x * y,z,y') = R(x,y,z) * y.
R(x * C,y,x') = R(C,x,y) * x.
x * ((y * (x * C)) * x') = (x * C) * y.
R(x * y,y',z) = R(x,z,y) * y.
R(x * y,x,z) = R(x * y,y',z).
R(x * y,y',z) = R(x * y,x,z).
x * (R(x',y,z) * z) = R(z,y,x).
R(x,x * y,z) = R(x,y,z).
R(x',y,z) = R(x',x * y,z).
R(x',x * y,z) = R(x',y,z).
R(C,x * C,y) = R(C,x,y).
x * (R(x',x * y,z) * z) = R(z,y,x).
x * R(C,y,x') = R(x * C,y,C).
R(x * C,y,C) = R(x * C,x,y).
(x * (y * C)) * y' = R(x * C,y,C).
R(x * C,C',y) = R(x * C,y,C).
R(x,C',y) = R((x * C') * C,y,C).
R((x * C') * C,y,C) = R(x,C',y).
R(x,y,C) = R(x,C',y).
R(x,C',y) = R(x,y,C).
x * R(y * C,x,C) = (x * C) * y.
x' * ((x * C) * y) = R(y * C,x,C).
R(C,x',y) * y = R(y * C,x,C).
R(x * C,y,C) * x' = R(C,y',x).
R(x,y,z) = R(x,z * y,z).
R(x,y * z,y) = R(x,z,y).
R(x,y * z,z') = R(x,z,y).
R(x,y,z') = R(x,z,y * z').
R(x,y,z * y') = R(x,z,y').
R(R(x,y',z * y),y,z) = x.
R(x,y,z) = R(x,z',y * z).
R(x,y',z * y) = R(x,z,y).
R(x,C,y) = R(x,y',C).
R(x,y',C) = R(x,C,y).
R(x,y,C) = R(x,C,y').
R(x,C,y') = R(x,y,C).
R(x,y * z',C) = R(x,C,z * y').
R(x,C',y') = R(x,C,y).
R(R(x,y',C'),C,y) = x.
R(x,y,C) = R(x,y',C').
R(x,y',C') = R(x,y,C).
R(x,y,C') = R(x,y',C).
R(x,y',C) = R(x,y,C').
R(x,y,C') = R(x,C,y).
C' * R(x * C,C,y) = R(x,C,y).
R(x,C,x * y) = R(x,y,C').
R(x,C,x * y) = R(x,C,y).
R(x * C,y * x',C) = R(x * C,y,x').
C * R(x,C,y) = R(x * C,C,y).
C * R(x,C,y) = R(x * C,C,x * y).
R(x * C,C,x * y) = C * R(x,C,y).
(x * (y * z'))' * (x * y) = R(z,y',x').
R(x * C,C,x * y) = R(x * C,C,y).
x * (((x * y) * z)' * x) = (y * (z * x'))'.
R(x * C,y,x') = R(x * C,C,x * y').
R(x * C,C,x * y') = R(x * C,y,x').
R(x * C,y,x') = R(x * C,C,y').
R(x * C,C,y') = R(x * C,y,x').
R(x * C,y,x') = R(x * C,y,C).
R(x * C,y,C) = R(C,x,y) * x.
R(x * C,y,C) * x' = R(C,x,y).
R(C,x,y) = R(C,y',x).
R(C,x',y) = R(C,y,x).
R(C,x,y) = R(C,y,x').
R(C,x,y') = R(C,y,x).
(x * (y * z'))' * (x * y) = z * a(z,x,y)'.
x * a(x,y,z)' = R(x,z',y').
x' * R(x,y',z') = a(x,z,y)'.
x' * R(x,y,z') = a(x,z,y')'.
x' * R(x,y,z) = a(x,z',y')'.
a(x,y',z')' = x' * R(x,z,y).
x * a(x,y',z')' = R(x,z,y).
R(x,y,z) * a(x,z',y') = x.
R(x,y,z)' * x = a(x,z',y').
R(x,y,z')' * x = a(x,z,y').
R(C,x,y)' * C = a(C,x,y').
R(C,x,y')' * C = a(C,x,y).
a(C,x,y) = a(C,y,x').
a(C,x,y') = a(C,y,x).
a(C,x,y) = a(C,y',x).
a(C,x',y) = a(C,y,x).
a(C,x',y) = a(C,x,y').
a(C,x',y) = a(x',y,C).
C' * (x * C) = x.
(x * (y * z))' * ((x * y) * z) = a(x,y,z).
C * (C * x)' = x'.
C * (x * C') = x.
(x * (y * (x * z)))' * ((x * y) * (x * z)) = a(x * y,x,z)'.
(x * (y * (z * y)))' * ((x * y) * (z * y)) = a(x * y,z,y)'.
R(x,C,y) = R(x,C,y * C).
R(x,C,y * C) = R(x,C,y).
R(R(x,C,y),y * C,C) = x.
R(x,y * C,C) = R(x,y,C).
R(x,y',z) = R(x,(y * x)',z).
R(x,(y * x)',z) = R(x,y',z).
a(x * y,x,z)' = a(x,y,x * z).
a(x,y,x * z)' = a(x * y,x,z).
a(x * y,z,y)' = a(x,y,z * y).
a(C,x,y * C)' = a(C * x,C,y).
a(x,y,z)' = a(x * y,x,x' * z).
a(x * y,x,x' * z) = a(x,y,z)'.
a(C,x,y * C)' = a(x * C,C,y).
a(C,x,y)' = a(x * C,C,y * C').
a(x * C,C,y * C') = a(C,x,y)'.
a(x,y,y' * z) = a(y,y' * x,z)'.
a(x,x' * y,z)' = a(y,x,x' * z).
R(x,y',z')' * x = a(x,z,y).
R(x,y,z)' * x = a(x,y,(z * y)').
a(x,y,(z * y)') = R(x,y,z)' * x.
a(C,x,C * (C * y)') = a(C,y,x).
R(x,y',z')' * x = a(x,z,y * x).
R(x,y,C)' * x = a(x,C,y).
R(x,y,C)' * x = a(x,C,y * C).
a(x,C,y * C) = a(x,C,y).
a(x,C,y) = a(x,C,y * C').
a(x,C,y * C') = a(x,C,y).
a(x * C,C,y) = a(C,x,y)'.
a(x,C,y) = a(C,x * C',y)'.
a(C,x * C',y)' = a(x,C,y).
a(x,y,(z * y)') = a(x,z',y').
a(x,y,y' * z) = a(x,z'',y').
a(x,y'',z') = a(x,z,z' * y).
a(x,y,z') = a(x,z,z' * y).
a(x,y,y' * z) = a(x,z,y').
a(x,y,z) = a(x,y * z,y').
a(x,y * z,y') = a(x,y,z).
a(x * y,z,x') = a(x,y,z)'.
a(x,y,z * x) = a(x,y,z).
a(C,x,y' * C) = a(C,y,x).
a(x * y,z * x,x') = a(x,y,z)'.
a(C,x,C * y') = a(C,y,x).
a(C,C * x,y) = a(C,x,y).
a(C,x,y) = a(C,x * C',y).
a(C,x * C',y) = a(C,x,y).
a(C,x,y)' = a(x,C,y).
a(x,C,y)' = a(C,x,y).
a(x,y * z,z') = a(z,z' * x,y)'.
a(x,x' * y,z)' = a(y,z * x,x').
a(x,y * z,z') = a(x,z,z' * y).
a(x,(y * z) * y,y') = a(x,y,z).
a(x,y * z,z') = a(x,y,z').
a(x,y * z',z) = a(x,y,z'').
a(x,y * (z * y),y') = a(x,y,z).
a(x,y * z',z) = a(x,y,z).
a(x,y,z) = a(x,y * z,z).
a(x,y * z,z) = a(x,y,z).
a(x,y,z) = a(x,y,z * y).
a(x,y,z * y) = a(x,y,z).
a(x * y,z,y)' = a(x,y,z).
a(x,y,C) = a(C,x * y,y).
a(C,x * y,y) = a(x,y,C).
a(x,y,C) = a(C,x,y).
a(C,x,y) = a(x,y,C).
a(C,x',y) = a(x',y',C').
x * a(x,y,C)' = R(x,C,y).
R(x,C,y) * a(x,y,C) = x.
R(x,C,y)' * x = a(x,y,C).
a(x,y',C') = a(x,y,C).
a(x,y',C') = a(C,x,y).
a(C,x',y) = a(y',x',C).
a(x',y,C) = a(C,y,x).
a(C,x',y) = a(x,y',C).
a(C,x',y) = a(x',C,y').
a(x,C,C * y) = a(x,C,y).
a(x,C,y) = a(x,C,C' * y).
a(x,C,C' * y) = a(x,C,y).
a(x,y,C') = a(x,C,y).
a(x,C,y') = a(x,y,C).
a(x,C,y') = a(C,x,y).
a(C,x',y) = a(x',C',y).
R(x,y',z)' * x = a(x,z',y).
a(x,C,y') = a(x,C',y).
a(x,C',y) = a(x,C,y').
a(x,C',y) = a(x,y,C).
a(x,C',y) = a(C,x,y).
a(C,x',y) = a(y,x',C').
a(x,y,C') = a(x,y',C).
a(x,y',C) = a(x,y,C').
a(x,y',C) = a(C,y,x).
a(C,x,y) = a(y,x,C').
a(x,y,C') = a(C,y,x).
a(C,x',y) = a(y,C,x').
a(x,y',C) = a(x,C,y).
a(C,x,y) = a(y,C,x).
a(C,x',y) = a(y',C,x).
a(x',C,y) = a(C,y',x).
a(C,x',y) = a(y,C',x).
a(x,C',y) = a(C,y',x).
a(C,x',y) = a(y',x,C').
a(x',y,C') = a(C,y',x).
a(C,x',y) = a(y',C',x').
a(x',C',y) = a(C,y,x).
a(C,x',y) = a(x,C',y').
a(x,C',y') = a(C,x',y).
a(C,x',y) = a(x,y,C').
a(C,x',y) = a(C',x',y').
(x * y) * ((z * x) * y)' = R(z',z * x,y).
R(x',x * y,z) = (y * z) * ((x * y) * z)'.
(C * x) * C' = x.
R(x,y,z)' = (y * z) * ((x * y) * z)'.
(x * y) * ((z * x) * y)' = R(z,x,y)'.
R(x',x * y,z) = R(x,y,z)'.
R(x,x' * y,z) = R(x',y,z)'.
R(x,y,z) = R(x,x' * y,z).
R(x,x' * y,z) = R(x,y,z).
R(x,y,z) = R(x',y,z)'.
R(x',y,z)' = R(x,y,z).
R(x,y,z) * x' = a(x',z',y').
a(x',y',z') = R(x,z,y) * x'.
R(C,x,y)' * C = a(C,y,x).
a(C,x',y) = a(y,x,C).
R(C,x,y)' * C = a(y,x,C).
a(x,y,C)' = a(x,C,y).
a(x,C,y) = a(y,x,C).
a(x,y,C)' = a(y,x,C).
R(C,x,y) * a(y,x,C) = C.
C * a(x,y,C)' = R(C,y,x).
C * a(x,y,C) = R(C,x,y).
R(C,x,y) * C' = a(x,y,C).
a(C',x',y') = a(y,x,C).
a(C',x',y') = a(C,x',y).
a(C,x',y) = a(C',y,x').
R(x,y,z') * x' = a(x',z,y').
a(x,y',C) = a(C',y,x').
a(C',x,y') = a(y,x',C).
a(C',x,y') = a(C,y',x).
a(C,x',y) = a(C',x,y).
R(x,y',z') * x' = a(x',z,y).
a(x',y',C) = a(C',y,x).
a(C',x,y) = a(C,x',y).
a(C,x',y) = a(C',y',x).
a(C,x',y') = a(C,x,y).
a(x',y',C) = a(C,x,y).
a(C',x,y) = a(C,y,x).
a(C',x',y) = a(C,y',x).
R(x * y,z,C) = R(x,z,C) * R(y,z,C).
C * ((x * C) * y) = x * (C * (y * C)).
(C * (x * y)) * (y * C)' = R(x,y,C).
(x * y) * z = y * ((y' * x) * (y * z)).
x * ((x' * y) * (x * z)) = (y * x) * z.
(x * y) * ((z' * x) * y)' = R(z,z' * x,y).
R(x,x' * y,z) = (y * z) * ((x' * y) * z)'.
((x * y') * z) * (z' * y) = R(x,y',z).
C * ((C * x) * y) = x * (C * (y * C)).
R(x,y,C)' = (y * C) * (C * (x * y))'.
(x * C) * (C * (y * x))' = R(y,x,C)'.
R(x * y',y,z) * z = x * (y' * z).
x * (y * (z * x))' = R(y * z,y,x)'.
R(x * y,x,z)' = z * (x * (y * z))'.
(x * C) * (C * (y * (x * (z * x))))' = R((y * x) * z,x,C)'.
R(x * (y * z),x,y) = (x * y) * z.
(x * R(y * x,y,z)')' = R(y,z,x).
(R(x,y,z) * z)' = y * (x * (z * y))'.
R(C * (x * y),C,x) = (x * C) * y.
(x * (y * (z * (x * y))'))' = R(z,y,x).
R((x * C) * y,x,C) = C * (x * y).
R(R(x,C,y * C),y,C) = x.
(x * (y' * z))' = y * ((x * y') * (z * y))'.
x * ((y * x') * (z * x))' = (y * (x' * z))'.
R(x,y,z) = (y * z) * ((x' * y) * z)'.
(x * y) * ((z' * x) * y)' = R(z,x,y).
(C * (x * (y * (x * C))'))' = R(y,x,C).
((x * (y * C)') * C) * y = R(x,(y * C)',C).
R(x * C,y,C)' = y * (x * (y * C))'.
x * (y * (x * C))' = R(y * C,x,C)'.
((x * C) * y)' * x = R(y * C,x,C)'.
R(R(x,(y * C)',C),y,C) = x.
(C * (x * (y * C)')) * y = R(x,(y * C)',C).
((x * (y * (x * C))') * C)' = R(y,x,C).
x * (y * (x * C))' = ((x * C) * y)' * x.
((x * C) * y)' * x = x * (y * (x * C))'.
((((x * C) * y)' * x) * C)' = R(y,x,C).
(x * C) * R(y,x,C) = R((x * C) * y,x,C).
(x * C) * R(y,x,C) = C * (x * y).
(x * C)' * (C * (x * y)) = R(y,x,C).
R((C * (x * (y * C)')) * y,y,C) = x.
R(x,C,y) = (C * (x * (y * C)')) * y.
(C * (x * (y * C)')) * y = R(x,C,y).
(x * C) * ((y * (x * C)') * ((C * (x * z)) * (x * C)))' = (y * R(z,x,C))'.
(x * C) * ((y * (x * C)') * (C * (((x * z) * x) * C)))' = (y * R(z,x,C))'.
(x * C) * ((y * (x * C)') * (C * ((x * (z * x)) * C)))' = (y * R(z,x,C))'.
(x * C) * (C * ((C * (y * (x * C)')) * (x * (z * x))))' = (y * R(z,x,C))'.
(x * R(y,z,C))' = R(((C * (x * (z * C)')) * z) * y,z,C)'.
R(((C * (x * (y * C)')) * y) * z,y,C)' = (x * R(z,y,C))'.
R(R(x,C,y) * z,y,C)' = (x * R(z,y,C))'.
(x * R(y,z,C))'' = R(R(x,C,z) * y,z,C).
R(R(x,C,y) * z,y,C) = (x * R(z,y,C))''.
R(R(x,C,y) * z,y,C) = x * R(z,y,C).
R(x,y,C) * R(z,y,C) = R(x * z,y,C).
R(x * y,C,z) = R(x,C,z) * R(y,C,z).
R(x * R(y,z,C),C,z) = R(x,C,z) * y.
R(x,C,y) * R(z,C,y) = R(x * z,C,y).

end_of_list.
