% --------------------------------------------------------------------------
% Gagola:  Lemma 2-13 => the 35 other distinct lemmas from Lemma List 2
% --------------------------------------------------------------------------

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
% ***********

% define D; A and B are arbitrary constants (for Normality Condition 2)

   R(C,A,B) = D # label("define D").

% commutator (for Normality Conditions 3 and 4)

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

% associator (for Normality Condition 4)

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

% **********
% Lemma 2-13
% **********

   R(u * v,D,y) = R(u,D,y) * R(v,D,y) # label("Lemma 2-13").

end_of_list.

% -------------------------------------------------------------------------
% Lemma List 2: JD supplied lemmas that he believes are true.
% -------------------------------------------------------------------------

formulas(goals).

% D associates with cubes
a(D,x * (x * x),y) = 1 # label("Lemma 2-1").
a(D,x,y * (y * y)) = 1 # label("Lemma 2-2").
a(x,D,y * (y * y)) = 1 # label("Lemma 2-3").
a(x * (x * x),D,y) = 1 # label("Lemma 2-4").
a(x * (x * x),y,D) = 1 # label("Lemma 2-5").
a(x,y * (y * y),D) = 1 # label("Lemma 2-6").

% associators with D in an argument cube to zero
a(D,x,y) * (a(D,x,y) * a(D,x,y)) = 1 # label("Lemma 2-7").
a(x,y,D) * (a(x,y,D) * a(x,y,D)) = 1 # label("Lemma 2-8").
a(x,D,y) * (a(x,D,y) * a(x,D,y)) = 1 # label("Lemma 2-9").

% DR(x,y)^3 = D, xR(D,y)^3 = x, xR(y,D)^3 = x
R(R(R(D,x,y),x,y),x,y) = D # label("Lemma 2-10").
R(R(R(x,D,y),D,y),D,y) = x # label("Lemma 2-11").
R(R(R(x,y,D),y,D),y,D) = x # label("Lemma 2-12").

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

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

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

x * 1 = x.
x' * x = 1.
x' * (x * y) = y.
(x * y) * y' = x.
(x * y)' = y' * x'.
x * (y * x) = (x * y) * x.
(x * y) * x = x * (y * x).
((x * y) * z) * y = x * (y * (z * y)).
R(x,y,z) = ((x * y) * z) * (y * z)'.
R(x * y,D,z) = R(x,D,z) * R(y,D,z).
R(x,D,y) * R(z,D,y) = R(x * z,D,y).
x'' * 1 = x.
x * (y * x)' = y'.
(x * (y * (z * y))) * y' = (x * y) * z.
R(x,y,z) = ((x * y) * z) * (z' * y').
R(x,y,x) = (x * (y * x)) * (y * x)'.
(x * (y * x)) * (y * x)' = R(x,y,x).
x = x''.
x'' = x.
x * (x' * y) = y.
x * y = y * ((y' * x) * y).
x * ((x' * y) * x) = y * x.
R(x,y,y' * z) = ((x * y) * (y' * z)) * z'.
((x * y) * (y' * z)) * z' = R(x,y,y' * z).
(x * (y * x)')' = y.
R(x,y,(z * y)') = ((x * y) * (z * y)') * z.
((x * y) * (z * y)') * z = R(x,y,(z * y)').
R(x,y,x) = x.
R(x,D,y) * y = R(x * y,D,y).
R(x * y,D,y) = R(x,D,y) * y.
R(x,D,y') = R(x * y,D,y') * y'.
R(x * y,D,y') * y' = R(x,D,y').
(x * (y * z)) * z' = (x * z) * (z' * y).
R(x,y,z) = ((x * y) * (y' * z)) * z'.
R(x,y,z) * y = R(x * y,z,(y * z)').
R(x * y,z,(y * z)') = R(x,y,z) * y.
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,y') = R(x,y,z) * y.
(R(x,y,D) * y) * y' = R(x,D,y').
R(x,D,y') = R(x,y,D).
R(x,y,D) * R(z,D,y') = R(x * z,D,y').
R(x,y,D) * R(z,D,y') = R(x * z,y,D).
R(x,y,D) * R(z,y,D) = R(x * z,y,D).
a(D,x',y) = a(D,x,y').
(x * x) * y = x * (x * y).
((x * y) * x) * z = x * (y * (x * z)).
(x * y) * (z * x) = x * ((y * z) * x).
(x * y) * z = (x * (y * z)) * a(x,y,z).
(x * (y * z)) * a(x,y,z) = (x * y) * z.
(x * y)' * x = y'.
(x * (y * x)) * z = x * (y * (x * z)).
R(x,y * z,z') = ((x * (y * z)) * z') * y'.
((x * (y * z)) * z') * y' = R(x,y * z,z').
R(x,x,y) = (x * (x * y)) * (x * y)'.
(x * (x * y)) * (x * y)' = R(x,x,y).
R(x * y,z,y) = (x * (y * (z * y))) * (z * y)'.
(x * (y * (z * y))) * (z * y)' = R(x * y,z,y).
(x * (y * z))' * ((x * y) * z) = a(x,y,z).
(x * y') * y = x.
(x * y')' = y * x'.
(x' * y)' = y' * x.
((x * y) * x) * (x' * z) = x * (y * z).
(x' * y) * z = (z * x)' * (z * (y * z)).
(x * y)' * (x * (z * x)) = (y' * z) * x.
(x * (y * z'))' = (z * y') * x'.
x' * ((x * (y * x)) * z) = y * (x * z).
R(x,x,y) = x.
D * R(x,D,y) = R(D * x,D,y).
R(D * x,D,y) = D * R(x,D,y).
x' * ((x * y') * z) = (x * y)' * (x * z).
(x * y)' * (x * z) = x' * ((x * y') * z).
(x * (y * (z * x)))' * (x * ((y * z) * x)) = a(x,y,z * x).
R(x,y,z) * z = (x * y) * (y' * z).
R(x * y,x,z) = (x * (y * z)) * z'.
R(x * y,x,z) * z = x * (y * z).
R(x,y,z) * z = y * ((y' * x) * z).
x * (y * (z * x))' = R(y * z,y,x)'.
R(x * y,x,z)' = z * (x * (y * z))'.
R(x * y,x,z) = (x * z) * (z' * y).
R(x,y,z) = R(x * z,x,y) * z'.
R(x * y,x,z) * y' = R(x,z,y).
R(x,y,z) * z = R(x * z,x,y).
R(x * y,x,z) = R(x,z,y) * y.
x * R(y * x,y,z)' = R(y,z,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).
x * (y * (z * (x * y))') = R(z,y,x)'.
x' * ((x * y') * (y * z)) = R(z,y',x').
(x * y)' * (x * (y * z)) = R(z,y',x').
R(x,y',z')' = (z * (y * x))' * (z * y).
(x * (y * z))' * (x * y) = R(z,y',x')'.
(x * (y * (z * (x * y))'))' = R(z,x * y,y').
R(x * y,x,z * y) = R(x * y,z,y).
R(x * y,z,y) * y' = R(x,z * y,y).
R(x,y,z) = R(x,y,y * z).
R(x,y,y * z) = R(x,y,z).
R(x * y,x,z) * y' = R(x,x * z,y).
R(x,D,y) = R(x,y',D).
R(x,y',D) = R(x,D,y).
R(x,x * y,z) = R(x,y,z).
R(x,y',z) = R(x,(y * x)',z).
R(x,(y * x)',z) = R(x,y',z).
R(x,y',D) = R(x,D,y * x).
R(x,D,y * x) = R(x,y',D).
R(x,D,y * x) = R(x,D,y).
R(D * x,D,y * x) = D * R(x,D,y).
D * R(x,D,y) = R(D * x,y,x).
R(D * x,y,x) = D * R(x,D,y).
R(D * x,D,y) = R(D * x,y,x).
R(D * x,y,x) * x' = R(D,y,x).
R(D,x,y) = R(D,x * y,y).
R(D,x * y,y) = R(D,x,y).
R(D,x,y) = R(D,x * y',y).
R(D,x * y',y) = R(D,x,y).
R(x,y,z)'' = R(x,z * y,y').
R(x,y * z,z') = R(x,z,y)''.
R(x,y * z,z') = R(x,z,y).
R(x,y * z',z) = R(x,z',y).
R(D,x',y) = R(D,y,x).
R(D,x',y') = R(D,x,y).
a(x,y,z * x) = ((y * (z * x))' * (y * z)) * x.
((x * (y * z))' * (x * y)) * z = a(z,x,y * z).
R(x,y',z')' * x = a(x,z,y * x).
a(x,y,z * x) = R(x,z',y')' * x.
a(x,y,z' * x) = R(x,z,y')' * x.
a(x,y',z' * x) = R(x,z,y)' * x.
a(x,y',z') = R(x,x * z,y)' * x.
R(x,x * y,z)' * x = a(x,z',y').
R(x,y,z)' * x = a(x,z',y').
R(x,y,z')' * x = a(x,z,y').
R(x,y',z')' * x = a(x,z,y).
R(D,x,y)' * D = a(D,y,x).
a(D,x',y) = a(D,y',x').
R(D,x,y) = R(D,y,x').
R(D,x,y') = R(D,y,x).
R(D,x,y')' * D = a(D,x,y).
a(D,x',y) = a(D,y,x).
a(D,x',y) = a(x',y,D).
(x * (y' * z')) * (z * y) = x.
R(x,y,z) * (y * z) = (x * y) * z.
((x * y) * z)' * (x * (y * z)) = a(x,y,z)'.
((x * y') * z') * (z * y) = R(x,y',z').
(x * (y * (x * z))) * z' = x * (y * x).
(x * y') * z' = x * (((x * z) * y)' * x).
x * (((x * y) * z)' * x) = (x * z') * y'.
((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).
((x * y') * (y * z))' * (x * z) = a(x * y',y,z).
(R(x,y,z) * z) * y = x * (z * y).
((R(x,y,z) * z) * y) * (z * y)' = x.
R(R(x,y,z),z,y) = x.
((x * y') * (y * z))' * (x * z) = a(x,y',y * z)'.
(x * (((x * y) * z)' * x)) * (y * z) = x * a(x,y,z)'.
(x * (y * z'))' * (x * y) = R(z,y',x').
(x * (y * z'))' = z * (((z * x) * y)' * z).
x * (((x * y) * z)' * x) = (y * (z * x'))'.
R(x,y * z,z') = R(x,y * z,y).
R(x,y',z') = R(x,z,(z * y)').
R(x,y,(y * z)') = R(x,z',y').
R(x,y,z) = R(x,z * y,z).
R(x,y * z,y) = R(x,z,y).
R(x,D,(D * y)') = R(x,y,D).
R(x,y',D') = R(x,y,D).
R(R(x,y',D'),D,y) = x.
R(x,D,y) = R(x,D',y').
R(x,D',y') = R(x,D,y).
a(x,y',y * z)' = a(x * y',y,z).
(x * (y * z'))' * (x * y) = z * a(z,x,y)'.
x * a(x,y,z)' = R(x,z',y').
x * a(x,D,y)' = R(x,y,D).
x * a(x,y,D)' = R(x,D,y).
R(x,y,D) * a(x,D,y) = x.
R(x,y,D)' * x = a(x,D,y).
R(x,D,y) * a(x,y,D) = x.
R(x,D,y)' * x = a(x,y,D).
R(x,D,y)' * x = a(x,D,y').
a(x,D,y') = a(x,y,D).
a(x,D,y) = a(x,y',D).
a(x,y',D) = a(x,D,y).
a(x * y,x,z) = a(x,y,x * z)'.
a(x,y,x * z)' = a(x * y,x,z).
a(x',y,z)' = a(x' * y,x',x * z).
a(x' * y,x',x * z) = a(x',y,z)'.
a(x * y,x,z)' = a(x,y,x * z).
a(x,y,z)' = a(x * y,x,x' * z).
a(x * y,x,x' * z) = a(x,y,z)'.
a(x,y,z)' = a(y,y' * x,y * z).
a(x,x' * y,x * z) = a(y,x,z)'.
a(x,y',y * z) = a(y',y * x,z)'.
a(x',x * y,z)' = a(y,x',x * z).
a(x,y',y * z)' = a(y',y * x,z).
a(x',x * y,z) = a(y * x',x,z).
a(x * y',y,z) = a(y',y * x,z).
a(x,y,z) = a(y',y * (x * y),z).
a(x',x * (y * x),z) = a(y,x,z).
a(x * y,z,y) = a(x,y,z * y)'.
a(x,y,z * y)' = a(x * y,z,y).
a(x * y',y,z * y)' = a(x,z,y).
a(x',x * y,z * x)' = a(y,z,x).
a(x,D',y') = a(x,D,y).
a(x,y',D') = a(x,y,D).
a(x,D',y) = a(x,D,y').
a(x,y,D') = a(x,y',D).
a(x,y',D) = a(x,y,D').
a(x,D',y) = a(x,y,D).
a(x,y,D') = a(x,D,y).
a(x,D,y) = a(x,y,D').
a(x,y,z * x) = a(x,y,z'').
a(x,y,z * x) = a(x,y,z).
a(x',y,z) = a(x',y,z * x).
a(x',y,z * x) = a(x',y,z).
a(x,y,z') = a(x,y,(x * z)').
a(x,y,(x * z)') = a(x,y,z').
a(x',x * y,z)' = a(y,z,x).
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,y' * z) = a(x,z,y').
a(x,y,D')' = a(x * y,y,D).
a(x * y,y,D) = a(x,y,D')'.
a(x * y,z,x') = a(x,y,z)'.
a(D * x,D,y) = a(D,x,y)'.
a(D,x,y)'' = a(D,x,D * y).
a(D,x,D * y) = a(D,x,y)''.
a(D,x,D * y) = a(D,x,y).
a(D,x,y) = a(D,y,x').
a(D,x,y') = a(D,y,x).
a(D,D * x,y) = a(D,y,x').
a(D,D * x,y) = a(D,x,y).
a(D,x,y) = a(D,D' * x,y).
a(D,D' * x,y) = a(D,x,y).
a(D,x,D * y) = a(x,D,y)'.
a(x,D,y)' = a(D,x,y).
a(D,x,y)' = a(x,D,y).
a(x,y,D)' = a(D,x,y').
a(x,y,D)' = a(D,y,x).
a(D,x,y)' = a(y,x,D).
a(x,y,D) = a(y,D,x).
a(x,D,y) = a(y,x,D).
a(x * y,y,D) = a(y,D,x).
a(x * y,y,D) = a(x,y,D).
a(x,y,D) = a(x,y,D')'.
a(x,y,D')' = a(x,y,D).
a(x,D,y)' = a(x,y,D).
a(x,y,D) = a(D,x,y).
a(D,x,y) = a(x,y,D).
a(D,x',y) = a(x',D,y').
a(x,D,y') = a(D,x,y).
a(D,x,y) = a(x,D,y').
a(D,x',y) = a(x',y',D').
a(x,y',D') = a(D,x,y).
a(D,x,y) = a(x,y',D').
a(D,x',y) = a(x',D',y).
a(x,D',y) = a(D,x,y).
a(D,x,y) = a(x,D',y).
a(D,x',y) = a(x,y',D).
a(D,x',y) = a(y',x',D).
a(x',y,D) = a(D,y,x).
a(D,x',y) = a(y,D,x').
a(x,D,y) = a(D,y,x).
a(D,x,y) = a(y,D,x).
a(D,x',y) = a(y,x',D').
a(x,y,D) = a(y,x,D').
a(x,y,D') = a(y,x,D).
a(x,y,D') = a(D,y,x).
a(D,x,y) = a(y,x,D').
a(D,x',y) = a(y',D,x).
a(x',y,D) = a(y,x,D).
a(x',y,D) = a(y',D,x).
a(x',D,y) = a(y',x,D).
a(x',D,y) = a(D,y',x).
a(D,x',y) = a(y',D',x').
a(x',D',y) = a(y,x,D).
a(x',D',y) = a(D,y,x).
a(D,x',y) = a(y,D',x).
a(x,D',y) = a(D,y',x).
a(D,x',y) = a(x,y,D').
a(D,x',y) = a(y,D,x)'.
a(x,D,y)' = a(D,y',x).
a(x,y,D) = a(D,y',x).
a(D,x',y) = a(y,x,D).
a(x,y,D') = a(D,x',y).
a(D,x',y) = a(x,D',y').
a(x,D',y') = a(y,x,D).
a(x,D',y') = a(D,x',y).
a(D,x',y) = a(y',x,D').
a(x',y,D') = a(D,y',x).
a(D,x',y) = a(D',y,x').
a(x',y * x,z) = a(x' * y,x,z).
a(x' * y,x,z) = a(x',y * x,z).
a(x,y,z) = a(x,y,z * x').
a(x,y,z * x') = a(x,y,z).
a(D,x,y)' = a(D' * x,D,y).
a(D' * x,D,y) = a(D,x,y)'.
a(D,x,y)' = a(D,y,x).
a(D,x * D',y)' = a(D,y,x).
a(D,x,y)' = a(D',x * D,y).
a(D',x * D,y) = a(D,x,y)'.
a(D',x,y) = a(D,x * D',y)'.
a(D,x * D',y)' = a(D',x,y).
a(D',x,y) = a(D,y,x).
a(D,x',y) = a(D',x',y').
a(D,x * D,y) = a(D,y',x).
a(D,x * D,y) = a(D,x,y).
a(D,x,y) = a(D,x * D',y).
a(D,x * D',y) = a(D,x,y).
a(D,x,y')' = a(x,y,D).
a(D,x,y')' = a(D,x,y).
a(D,x * D',y')' = a(D,x,y).
a(D',x,y') = a(D,x,y).
a(D,x',y) = a(D',x,y).
a(D,x,y)' = a(D,x',y).
a(D,x * D',y)' = a(D,x',y).
a(D',x,y) = a(D,x',y).
a(D,x',y) = a(D',y',x).
a(D,x * D',y)' = a(x,D,y).
a(D',x,y) = a(x,D,y).
a(D',x',y) = a(D,y',x).
R(R(R(x,D,y),D,y),D,y) = x.
1 * x = x.
x * x' = 1.
(x * y) * y = x * (y * y).
C * x = x * C.
R(C,A,B) = D.
D = R(C,A,B).
x * y = (y * x) * K(x,y).
(x * y) * K(y,x) = y * x.
1 = 1'.
1' = 1.
(x' * y') * ((y * x) * z) = z.
(x' * x') * (x * y) = x' * y.
(x * (x * y)) * y' = x * x.
(x * y)' * (x * (y * y)) = y.
(x * (y * y)) * y' = x * y.
x' * ((x * y) * x) = y * x.
x * y' = y' * ((y * x) * y').
x' * ((x * y) * x') = y * x'.
x' * (((x * y) * x) * z) = y * (x * z).
(x * y) * (z * x) = z' * ((z * x) * (y * (z * x))).
x' * ((x * y) * (z * (x * y))) = (y * z) * (x * y).
(((x * x) * y) * z) * y = x * (x * (y * (z * y))).
((x * (y * y)) * z) * y = (x * y) * (y * (z * y)).
x' * ((x * y) * (z * x)) = (y * z) * x.
x * (y * z') = z' * (((z * x) * y) * z').
x' * (((x * y) * z) * x') = y * (z * x').
R(x',x * y,z) = (y * z) * ((x * y) * z)'.
R(x * x,y,z) = ((x * (x * y)) * z) * (y * z)'.
((x * (x * y)) * z) * (y * z)' = R(x * x,y,z).
R(x,y * z,z) = ((x * (y * z)) * z) * (y * (z * z))'.
((x * (y * z)) * z) * (y * (z * z))' = R(x,y * z,z).
C' * (x * C) = x.
x' * (C * x) = C.
(C * x) * C' = x.
C * (x * x) = x * (x * C).
(C * x) * C = x * (C * C).
C * (x * C) = x * (C * C).
(C * (C * x)) * y = C * (x * (C * y)).
((x * C) * y) * x = C * (x * (y * x)).
((C * x) * y) * C = x * (C * (y * C)).
C * ((x * C) * y) = x * (C * (y * C)).
(x * C) * (y * C) = C * ((x * y) * C).
(x * y) * (x * C) = x * ((y * C) * x).
(C * x) * (y * C) = C * (C * (x * y)).
R(C,x,y) = ((x * C) * y) * (x * y)'.
((x * C) * y) * (x * y)' = R(C,x,y).
(x * y)' * (y * x) = K(y,x).
((x * y) * z) * a(x,y,z)' = x * (y * z).
(((x * y) * z) * u) * a(x,y,z) = (x * (y * z)) * (a(x,y,z) * (u * a(x,y,z))).
(x * (y * z)) * (a(x,y,z) * (u * a(x,y,z))) = (((x * y) * z) * u) * a(x,y,z).
x * (C * x') = C.
x * x = C * (x * (C' * x)).
C * (x * (C' * x)) = x * x.
(x * (C * y)) * (C' * x) = x * (y * x).
(x * y) * z = y * ((y' * x) * (y * z)).
x * ((x' * y) * (x * z)) = (y * x) * z.
x * (y * z) = z * (((z' * x) * y) * z).
x * (((x' * y) * z) * x) = y * (z * x).
x * C' = C' * x.
C' * x = x * C'.
x * (y * (y' * (x' * z))) = z.
(x * (x * y')) * y = x * x.
x * y = (x * y') * (y * y).
(x * y') * (y * y) = x * y.
(x * y) * z = (x * z') * (z * (y * z)).
(x * y') * (y * (z * y)) = (x * z) * y.
(x * y) * z = x * ((y * (z * x')) * x).
x * ((y * (z * x')) * x) = (x * y) * z.
R(x * y',y,z) = (x * z) * (y * z)'.
C * (x * C') = x.
C * (x * (C' * (y * C'))) = (x * C') * y.
x' * y = (y * x)' * (y * y).
(x * y)' * (x * x) = y' * x.
(x * y)' * (y * x) = K(x,y)'.
x * (y * (y * x))' = (y * y)'.
x * (y * (x * x))' = (y * x)'.
x * (x * (y * x))' = (x * y)'.
C' * (x * C') = x * (C' * C').
(x * C') * (y * C') = C' * ((x * y) * C').
(x * y') * ((y * x') * z) = z.
(x * (x * y'))' = y * (x * x)'.
R(x,y,z)' = (y * z) * ((x * y) * z)'.
(x * y) * ((z * x) * y)' = R(z,x,y)'.
(x' * y) * (C * (y' * x)) = C.
C * (x * x) = x * (C * x).
(x * (C * C)) * y = C * (x * (C * y)).
(x * x) * y' = (x * (x * y)) * (y' * y').
(x * (x * y)) * (y' * y') = (x * x) * y'.
(x' * y') * (x * y) = K(x,y).
((x' * y') * z') * ((z * (y * x)) * u) = u.
(C' * x') * ((C * x) * y) = y.
x * (y * (y' * z)) = x * z.
x * (C * y) = x * (y * C).
x * (C * (C * y)) = x * (y * (C * C)).
x * a(x * (y' * z'),z,y) = ((x * (y' * z')) * z) * y.
K(x,y)' = K(y,x).
x * (x * y)' = (x * (y * x'))'.
(x * (y * x'))' = x * (x * y)'.
(x' * (y * (C * (y' * x)))) * a(x',y,C * (y' * x)) = C.
(C' * x')' * y = (C * x) * y.
(x * x)' * (x * y) = x' * y.
(C * C)' * x = C' * (x * C').
x * (y * x') = (x * y) * x'.
(x * y) * x' = x * (y * x').
(R(x,y,z) * ((x * y) * z)) * (y * z)' = R(x,y,z) * R(x,y,z).
((x * y) * y) * z = (x * y) * (x' * ((x * y) * z)).
(x * y) * (x' * ((x * y) * z)) = ((x * y) * y) * z.
(x * (x * (y * x))) * z = x * ((x * y) * (x * z)).
C * (x * (y * x)) = x * (y * (x * C)).
(x * (y * x)) * (x' * z) = x * (y * z).
((C * C)' * x) * y = C' * (x * (C' * y)).
(C * (C * x)) * y = C * (x * (y * C)).
C * ((C * x) * y) = x * (C * (y * C)).
C * ((x * C) * y) = x * (C * (C * y)).
C * ((x * C) * y) = x * (y * (C * C)).
(x * C) * (y * C) = C * (C * (x * y)).
x * (y * C) = y * (((y' * x) * C) * y).
x * (((x' * y) * C) * x) = y * (x * C).
(C * x) * (C * y) = C * (C * (x * y)).
x * (y * C) = C * (C * ((x * C') * y)).
C * (C * ((x * C') * y)) = x * (y * C).
C' * (C' * x) = x * (C' * C').
(C * C)' * x = x * (C' * C').
(C * C)' * x = x * (C * C)'.
x' * ((C * (x * (y * x))) * x) = (y * (x * C)) * x.
C * ((C * x) * y) = x * (C * (C * y)).
C * (x * y) = (x * C') * (C * (C * y)).
(x * C') * (C * (C * y)) = C * (x * y).
(x * (y * (C * C)))' * C = ((x * C) * y)'.
(x * C) * y = C * (C * (x * (y * C'))).
C * (C * (x * (y * C'))) = (x * C) * y.
x' * ((y * x) * z) = (x' * y) * (x * z).
(x' * y) * (x * z) = x' * ((y * x) * z).
(x * (y * z)) * y' = (x * y) * (z * y').
(x * (y * (x * C))) * x' = (C * x) * y.
x' * ((x * y) * z) = (y * (z * x')) * x.
(x * (y * z')) * z = z' * ((z * x) * y).
R(x,y,C) = (C * (x * y)) * (C' * y').
(C * (x * y)) * (C' * y') = R(x,y,C).
x * ((x' * y) * C) = (y * x) * (C * x').
(x * y) * (C * y') = y * ((y' * x) * C).
x * K(x,y) = (y' * x) * y.
(x' * y) * x = y * K(y,x).
x * ((y * K(y,x)) * x) = y * (x * x).
(x * y') * (y * z) = (x * (z * y')) * y.
(x * (y * z')) * z = (x * z') * (z * y).
(x * y') * (z * y) = (x * (y' * z)) * y.
(x * (y' * z)) * y = (x * y') * (z * y).
(C * (x * y)) * (C * ((z * x) * y)') = C * (C * R(z,x,y)').
x' * ((x * y) * z) = (y * x') * (x * z).
(x * y') * (y * z) = y' * ((y * x) * z).
x' * (((x * y) * z) * u) = (y * (z * x')) * (x * u).
(x * (y * z')) * (z * u) = z' * (((z * x) * y) * u).
((x * y) * z) * (x' * u) = x * ((y * (z * x')) * u).
x * ((C * (x' * y)) * x) = y * (x * C).
(x * C') * y = C * (x * (C' * (C' * y))).
C * (x * (C' * (C' * y))) = (x * C') * y.
(C * x) * y = x * ((y * (x * C)) * x').
x * ((y * (x * C)) * x') = (C * x) * y.
x * ((y * (x * C)) * x') = (x * C) * y.
x * (y * x') = (x * C) * (y * (C' * x')).
(x * C) * (y * (C' * x')) = x * (y * x').
x' * (((x * (y' * z')) * z) * y) = a(x * (y' * z'),z,y).
((C * C)' * (x * y))' * ((x * (C * C)') * y) = a((C * C)',x,y).
C * (((x * (y * (C * C)))' * C) * (x * y)) = a(x,y,C * C).
C * (C * (x * (y * C'))) = (x * y) * (a(x,y,C')' * C).
(x * y) * (a(x,y,C')' * C) = C * (C * (x * (y * C'))).
x * ((y * x) * (C * x')) = (x * C) * y.
x' * ((x * C) * y) = (y * x) * (C * x').
(x * y) * (C * y') = y' * ((y * C) * x).
R(x * C,C,y) * y = C * (x * y).
(C * (x * y)) * y' = R(x * C,C,y).
R(x * (y * C),x,C) = (x * C) * y.
R(x * C,C,y) = y * ((y' * C) * x).
x * ((x' * C) * y) = R(y * C,C,x).
x * ((C * x') * y) = R(y * C,C,x).
(x * y) * (C * y') = y * (C * (y' * x)).
x * ((C * x') * (y * x)) = y * (x * C).
x * (y * C) = R((x * y) * C,C,y).
R((x * y) * C,C,y) = x * (y * C).
R(C * (x * y),C,y) = x * (y * C).
R(C * x',C,y) = (y * x)' * (y * C).
(x * y)' * (x * C) = R(C * y',C,x).
R(x * (y * C),y,C) = C * (x * y).
x * ((y * x)' * (y * z)) = R(z,y',x).
x * R(C * x',C,y) = R(C,y',x).
x * (C * (x' * y)) = x' * ((x * C) * y).
x' * ((x * C) * y) = x * (C * (x' * y)).
x * (C * (x' * (y * x))) = (C * y) * x.
(x * y') * (C * ((y * x') * (z * (x * y')))) = (C * z) * (x * y').
x * (C * (y * x)) = (C * (x * y)) * x.
(C * (x * y)) * x = x * (C * (y * x)).
x * (C * (y * (x * x))) = (C * (x * (y * x))) * x.
(C * (x * (y * x))) * x = x * (C * (y * (x * x))).
(x * (C * (y * x))) * x' = C * (x * y).
C * (x * y) = x * ((C * (y * x)) * x').
x * ((C * (y * x)) * x') = C * (x * y).
x * R(y * C,C,x) = C * (x * y).
x' * (C * (x * y)) = R(y * C,C,x).
x * (x * ((C * x') * y)) = C * (x * y).
x * (x * y) = C * (x * ((x * C') * y)).
C * (x * ((x * C') * y)) = x * (x * y).
x * (y * (z * x')) = ((x * y) * z) * x'.
((x * y) * z) * x' = x * (y * (z * x')).
R(x',x * y,z) = R(x,y,z)'.
R(x,x' * y,z) = R(x',y,z)'.
(x * (x * y)) * (y' * y') = x * (x * y').
((x' * y') * z') * ((z * y) * x) = a(z,y,x).
((C * C)' * x) * y = C' * (x * (y * C')).
(x * (x * y)) * (y * y)' = x * (x * y').
R(x,y',z')' = (z * y)' * (z * (y * x')).
(x * y)' * (x * (y * z')) = R(z,y',x')'.
C * (((C * C)' * x) * y) = x * (y * C').
C * ((x * (C * C)') * y) = x * (y * C').
((x * (x * y)) * z) * y = x * (x * (y * (z * y))).
R(x,C,y) = R(x,C,y * C).
R(x,C,y * C) = R(x,C,y).
R(x * x,x * (x * y),z) = R(x * 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) * ((x * y) * z) = (x * (x * y)) * z.
R(x,y,z) = R(x',y,z)'.
R(x',y,z)' = R(x,y,z).
R(D * x,y,x) = R(D,y,x) * x.
R(R(D,x,y) * z',z,y) = R(D * y,x,y) * (z * y)'.
C * (x * ((y * C') * (z * C'))) = (x * C') * (y * z).
((x' * y') * (z' * u')) * (((u * z) * y) * x) = a(u * z,y,x).
((C'' * x') * y') * (C' * (y * x)) = a(y,x,C').
(((C * C)' * x') * y') * (C * ((y * x) * C)) = a(y,x,C * C).
(((x * (x * x)) * y) * x) * (y * x)' = x * (x * x).
x * ((y * z) * (x * y)) = (x * y) * (z * (x * y)).
(x * y) * (z * (x * y)) = x * ((y * z) * (x * y)).
(C' * x') * R(y,x,C) = C' * ((x' * (C * (y * x))) * (C' * x')).
C' * ((x' * (C * (y * x))) * (C' * x')) = (C' * x') * R(y,x,C).
(x * y) * (x' * ((x * y) * z)) = (x * (y * y)) * z.
x' * (x * (C * (y * (x * x)))) = (y * (x * C)) * x.
R(x * (x * x),y,x) = x * (x * x).
(x * y)' * ((x * (y * y)) * z) = x' * ((x * y) * z).
(x * (y * C)) * y = C * (x * (y * y)).
((x * ((y * z) * x)) * x) * (z * (x * x))' = R(x * y,z * x,x).
(C * (x * ((y * x) * x))) * (y * (x * x))' = R(x * C,y * x,x).
R(C * ((x * y)' * (x * (y * y))),C,x * (y * y)) = x' * ((x * y) * C).
x' * R(x,y',z') = a(x,z,y)'.
x * a(x,y,z')' = R(x,z,y').
R(x,y,D) * x' = a(x',D,y).
x' * (((x * y') * z') * (z * y)) = a(x,z,y)'.
D' * R(D,x,y) = a(D,y,x)'.
x' * (((x * y') * (y * z')) * z) = a(x,z,y)'.
(x' * ((x * y') * z')) * (z * y) = a(z,y,x)'.
(x * C') * (x * y) = x * (x * (y * C')).
(x * C') * y = x * (x * ((x' * y) * C')).
x * (x * ((x' * y) * C')) = (x * C') * y.
x * (x * (C' * (x' * y))) = (x * C') * y.
x' * ((x * C') * y) = x * (C' * (x' * y)).
x' * ((C' * x) * y) = x * (C' * (x' * y)).
(C' * (x * y')) * y = y * (C' * (y' * x)).
(x' * C') * (x * y) = x * (C' * (x' * y)).
((C * x') * y') * (C' * (y * x)) = a(y,x,C').
a(x,y,C') = C * ((y' * (x' * C')) * (x * y)).
C * ((x' * (y' * C')) * (y * x)) = a(y,x,C').
a(C,x,y * C)' = a(C * x,C,y).
a(C,x * C',C * y)' = a(x,C,y).
a(C,x * C',y * C)' = a(x,C,y).
a(x,y,y * C)' = a(x * y,C,y).
a(x * y,z,y)' = a(x,y,z * y).
a(x * (y * C),y,y * C)' = a(x,y * C,C * (y * y)).
a(x,y * C,C * (y * y)) = a((x * (y * C)) * y,C,y).
a((x * (y * C)) * y,C,y) = a(x,y * C,C * (y * y)).
a(C * (x * (y * y)),C,y) = a(x,y * C,C * (y * y)).
a(C * (x * (y * y)),C,y) = a(x,y * C,y * (y * C)).
R(x,y,z) * x' = a(x',z',y').
a(x,y,x * C) = a(x,y,C).
a(C,x,y)' = a(C * x,C,y).
a(C * x,C,y) = a(C,x,y)'.
a(C,x * C',y)' = a(x,C,y).
a(x,x' * y,C) = a(y,x,C)'.
(x * (y * (z * x'))) * a(x,y,z) = (x * y) * (z * x').
a(C,x * (y * y),y)' = a(x,y * C,y * (y * C)).
a(x,y * C,y * (y * C)) = a(C,x * (y * y),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,z)' = a(z',z * x,y).
a(x',x * y,z) = a(y,z,x)'.
a(C',x,y)' = a(x * C',y,C).
a(x * C',y,C) = a(C',x,y)'.
a(x,y * z,z) = a(x,y,z).
a(x,y * (z * z),z) = a(x,y * z,z).
a(x,y * C,y) = a(x,C,y).
a(x,C',y * C) = a(x,y,C).
a(x,y,D) = a(x,D * y,D).
a(x,D * y,D) = a(x,y,D).
a(x * y,z,y)' = 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) = a(x,y',z * y).
a(x,y',z * y) = 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,y' * C) = a(x,y,C).
a(x,x' * y,z) = a(y,z,x')'.
a(x',C * (x * C),y) = a(C * C,y,x)'.
a(x,y,C') = a(x,C,y).
a(x,C,y) = a(x,y,C').
a(x,C,y') = a(x,y,C).
a(x,C,y * C) = a(x,y,C').
a(x,C,y' * z') = a(x,z * y,C).
a(x,y * z,C) = a(x,C,z' * y').
a(x,C,y) = a(x,y',C).
a(x,y',C) = a(x,C,y).
C * ((x' * (y' * C')) * (y * x)) = a(y,C,x * C).
a(x,C',y) = a(x,y,C).
a(D,x,y) = a(D,x',y').
a(D,x',y') = a(D,x,y).
x * a(D,y,x) = R(x,D,y).
D' * R(D,x,y) = a(x,y,D).
a(x,y',D) = a(y,x,D).
a(x,D * y,D) = a(y,D,x).
a(x',D,y) = a(x,y,D).
R(x,y,D) * x' = a(x,y,D).
a(x,y,D)' = a(y,x,D).
a(x,y,D)' = a(x,D,y).
(x * a(y,z,D))' = a(y,D,z) * x'.
x * a(x,y,D) = R(x,y,D).
a(x,D,y) = a(y,D,x)'.
a(x,D,y)' = a(y,D,x).
a(D,x',y') = a(y,D,x).
x * a(x,D,y) = R(x,D,y).
D * a(x,y,D) = R(D,x,y).
(a(x,y,D) * D)' * R(D,x,y) = K(D,a(x,y,D)).
D * a(x,D,y) = R(D,y,x).
a(x,y,D) * x = R(x,y,D).
a(x,y,D)' * R(x,y,D) = x.
a(x,y,D) * y = R(y,x',D).
a(x,D,y) * R(x,y,D) = x.
x * R(x,y,D)' = a(x,D,y).
a(x,y,D) * y = R(y,D,x).
R(x * x,D,y) * x' = a(y,x * x,D) * x.
a(x,y * y,D) * y = R(y * y,D,x) * y'.
a(x,D,y) * x = R(x,D,y).
a(x,D,y)' * R(x,D,y) = x.
R(x,D,y) * x' = a(x,D,y).
a(x,y,D) * R(x,D,y) = x.
a(x,D,y) * R(y,D,x) = y.
x * R(x,D,y)' = a(x,y,D).
R(x,D,y) * (a(x,y,D) * x)' = (a(x,y,D) * a(x,y,D))'.
(a(x,D,y) * a(x,D,y))' * y = a(x,D,y)' * R(y,D,x).
x * R(x,y,D)' = a(R(x,y,D),D,y).
a(R(x,y,D),D,y) = x * R(x,y,D)'.
R(D * x,y,x) * (D * x)' = a(D * x,D,y).
(x * a(x,y,D))' = R(x,D,y) * (x * x)'.
R(x,D,y) * (x * x)' = (x * a(x,y,D))'.
a(C,x * C',y) = a(x,y,C')'.
a(D',x',y') = a(x,D,y).
R(D,x,y) * D' = a(y,D,x).
a(x,D,y) * D = R(D,y,x).
a(x,D,y) * (D * D) = R(D,y,x) * D.
(D * a(x,D,y))' = D * (D * R(D,y,x))'.
D * (D * R(D,x,y))' = (D * a(y,D,x))'.
a(x,y,D) * D = R(D,x,y).
a(x,y,D)' * D = R(D,y,x).
a(x,y,D) * R(D,y,x) = D.
D * R(D,x,y)' = a(y,x,D).
R(D,x,y) * (a(y,x,D) * D)' = (a(y,x,D) * a(y,x,D))'.
a(x,D,y) = D * R(D,x,y)'.
D * R(D,x,y)' = a(x,D,y).
a(x,y * (z * z),z) = a(x,y,z).
a(x,C,y' * x'') = a(y,x,C)'.
(a(x,y,D) * a(z,u,D))' = a(z,D,u) * a(x,D,y).
a(R(x,y,D),D,y) = a(x,D,y).
a(x,D,y) = a(y,R(x,y,D),D).
a(x,R(y,x,D),D) = a(y,D,x).
a(x,R(y,x,D),D) = a(x,y,D).
a(x,y,D)' = a(x,D,R(y,x,D)).
a(x,D,R(y,x,D)) = a(x,y,D)'.
a(x,D,R(y,x,D)) = a(y,x,D).
a(x,y,D) = a(R(x,y,D),y,D).
a(R(x,y,D),y,D) = a(x,y,D).
a(x,y,D) = a(R(x,D,y),y,D).
a(R(x,D,y),y,D) = a(x,y,D).
R(x,D,y) * a(x,y,D)' = R(R(x,D,y),D,y).
a(x,C,y' * x) = a(y,x,C)'.
a(x,y,C)' = a(y,C,x').
a(x,y,C)' = a(y,x,C).
(x' * ((x * y') * (C * C)')) * ((C * C) * y) = a(x',C * (x * C),y).
R(x,D,y) * (x * x)' = R(x,y,D)'.
D * (D * R(D,x,y))' = R(D,x,y)'.
R(R(D,x,y) * D',D,y) = a(D * y,D,x).
R(R(D,x,y) * D',D,y) = a(x,D * y,D).
R(R(D,x,y) * D',D,y) = a(y,D,x).
R(a(x,D,y),D,x) = a(x,D,y).
R(a(x,D,y'),D,x) = a(x,y,D).
R(a(x,y,D),D,x) = a(x,y,D).
a(x,y,D) * R(z,D,x) = R(a(x,y,D) * z,D,x).
R(a(x,y,D) * z,D,x) = a(x,y,D) * R(z,D,x).
R(x,D,y) * a(x,D,y) = R(R(x,D,y),D,y).
R(D,x,y)' * R(D,x,y) = K(D,a(x,y,D)).
K(D,a(x,y,D)) = 1.
1' = K(a(x,y,D),D).
K(a(x,y,D),D) = 1'.
K(a(x,y,D),D) = 1.
K(a(x,D,y),D) = 1.
D * ((a(x,D,y) * 1) * D) = a(x,D,y) * (D * D).
D * (a(x,D,y) * D) = a(x,D,y) * (D * D).
a(x,D,y) * (D * D) = D * (a(x,D,y) * D).
a(x,D,y) * (D * D) = D * R(D,y,x).
D * R(D,x,y) = R(D,x,y) * D.
R(D,x,y) * D = D * R(D,x,y).
(D * (D * R(D,x,y))) * z = D * (R(D,x,y) * (D * z)).
a(x,y * C,y * (y * C)) = a(C,x,y)'.
a(C,x,y)' = a(x,y * C,y).
a(x,y * C,y) = a(C,x,y)'.
a(C,x,y)' = a(x,C,y).
a(x,C,y)' = a(C,x,y).
C * a(x,C,y) = R(C,y',x').
C * a(x,C,y') = R(C,y,x').
a(x,y,C')' = a(C,x,y).
a(C,x * C',y) = a(x,C',y).
C * a(x,y,C) = R(C,y,x').
a(C,x * C',y) = a(x,y,C).
a(x,y,C)' = a(x,C,y).
a(x,y,C) = a(x,y,C')'.
a(x,y,C')' = a(x,y,C).
a(x,y,C) * a(x,C,y) = 1.
a(x,C,y)' = a(x,y,C).
(x * a(y,C,z)) * a(y,z,C) = x.
a(x,y,C)' = a(x,y,C').
a(x,C,y) = a(y,C,x').
a(x,C,y') = a(y,C,x).
a(x,C,y) = a(y,x,C).
a(x,y,C) = a(y,x,C').
a(x,y,C') = a(y,x,C).
a(x,C,y)' = a(y,C,x).
a(x,y,C) = a(C,x,y).
a(C,x,y) = a(x,y,C).
a(x,C,y') = a(C,x,y).
a(C,x,y) = a(x,C,y').
a(x * C',y,C) = a(x,y,C).
a(x,C,y) = a(C,y,x).
a(C,x,y) = a(y,C,x).
a(C,x',y) = a(y,x,C).
a(x,y',C) = a(C,y,x).
a(C,x,y) = a(y,x',C).
a(x,y,C') = a(C,x',y).
a(C,x',y) = a(x,y,C').
a(x,y,C) * a(C,y,x) = 1.
a(C,x,y) * a(C,x',y) = 1.
a(x,y,C) = a(C',x,y)'.
a(C',x,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) * (C * (a(C,x',y) * C')) = 1.
a(C,x,y) * (C * (a(x,y,C') * C')) = 1.
C * ((x * (x' * (y' * (z' * C')))) * (z * y)) = a(z,C,y * C).
(((x * y) * z) * x') * a(x,y,z) = (x * y) * (z * x').
C * (((x * C) * y)' * (x * y)) = a(x,y,C * C).
(x * y) * (a(x,y,C')' * C) = (x * C) * y.
(x * y) * (C * a(x,y,C')') = (x * C) * y.
(x * y) * (C * a(x,y,C)) = (x * C) * y.
R(x,D,y) * R(x,y,D)' = (a(x,y,D) * a(x,y,D))'.
(a(x,y,D) * a(x,y,D))' = R(x,D,y) * R(x,y,D)'.
R(x,D,y) * R(x,y,D)' = a(x,D,y) * a(x,D,y).
a(x,D,y) * a(x,D,y) = R(x,D,y) * R(x,y,D)'.
R(D,x,y) * R(D,y,x)' = (a(y,x,D) * a(y,x,D))'.
(a(x,y,D) * a(x,y,D))' = R(D,y,x) * R(D,x,y)'.
(a(x,D,y) * a(y,x,D))' = R(D,x,y) * R(D,y,x)'.
(a(x,D,y) * a(x,D,y))' = R(D,x,y) * R(D,y,x)'.
((x * (x * y)) * z) * (y * z)' = R(x,y,z) * R(x,y,z).
R(x,y,z) * R(x,y,z) = R(x * x,y,z).
R(x * x,y,z) * u = R(x,y,z) * (R(x,y,z) * u).
R(x,y,z) * (R(x,y,z) * u) = R(x * x,y,z) * u.
D * R(C,A,B) = R(C * C,A,B).
R(C * C,A,B) = D * R(C,A,B).
(x * (x * R(y,z,u))) * R(y * y,z,u)' = x * (x * R(y,z,u)').
R(C * C,A,B) = D * D.
R(x,D,y) * (R(x,D,y) * (x * x)') = a(x * x,D,y).
R(x,D,y) * a(x,D,y) = R(x * x,D,y) * x'.
R(x * x,D,y) * x' = R(x,D,y) * a(x,D,y).
a(x,y * y,D) * y = R(y,D,x) * a(y,D,x).
(R(x,D,y) * a(x,D,y)) * x' = a(y,x * x,D).
R(R(x,D,y),D,y) * x' = a(y,x * x,D).
R(x,D,y) * R(x,y,D)' = a(x * x,D,y).
a(x,D,y) * a(x,D,y) = a(x * x,D,y).
(a(x,D,y) * a(x,D,y))' = a(y,D,x * x).
a(x,D,y * y) * x = a(y,D,x)' * R(x,D,y).
a(x,D,y)' * R(y,D,x) = a(y,D,x * x) * y.
a(x,D,y * y) = R(D,y,x) * R(D,x,y)'.
R(D,x,y) * R(D,y,x)' = a(y,D,x * x).
a(x,D,y)' * R(y,D,x) = R(y,D,x * x).
a(x,y,D) * R(y,D,x) = R(y,D,x * x).
R(a(x,y,D) * y,D,x) = R(y,D,x * x).
R(R(x,D,y),D,y) = R(x,D,y * y).
R(x,D,y * y) * x' = a(y,x * x,D).
a(x,y * y,D) = a(y,D,x * x).
D * a(x,D,y * y) = R(D,y,x * x).
R(D,x,y * y) = D * a(y,D,x * x).
x' * (((x * y') * (y * z')) * z) = a(x * (z' * y'),y,z).
(C' * (x' * (y' * C'))) * (C * ((y * x) * C)) = a(y,x,C * C).
R(x * y,z * x,x) = x * (((y * z) * x) * (x * (z * (x * x))')).
x * (((y * z) * x) * (x * (z * (x * x))')) = R(x * y,z * x,x).
(C * (x * (y * (x * x)))) * (y * (x * x))' = R(x * C,y * x,x).
a(x * (y' * z'),z,y) = a(x,y,z)'.
x * a(x,y,z)' = ((x * (y' * z')) * z) * y.
((x * (y' * z')) * z) * y = x * a(x,y,z)'.
(x * (C' * (x' * y'))) * y = C' * a(C',y,x)'.
x * (((y * z) * x) * (z * x)') = R(x * y,z * x,x).
x * R(y,z,x) = R(x * y,z * x,x).
R(x * y,z * x,x) = x * R(y,z,x).
R(x * C,y * x,x) = R(x * C,C,y * (x * x)).
R(x * C,C,y * (x * x)) = R(x * C,y * x,x).
((x * y)' * (C * C)) * ((x * (C * C)') * y) = a((C * C)',x,y).
a((C * C)',x,y) = C * ((x * y)' * (C * ((x * (C * C)') * y))).
C * ((x * y)' * (C * ((x * (C * C)') * y))) = a((C * C)',x,y).
C * ((x * y)' * (x * (y * C'))) = a((C * C)',x,y).
C * R(C,x',y')' = a((C * C)',y,x).
a((C * C)',x,y) = C * R(C,y',x')'.
a(x * x,y,z) * x' = ((z' * y') * x') * (x' * ((((x * x) * y) * z) * x')).
((x' * y') * z') * (z' * ((((z * z) * y) * x) * z')) = a(z * z,y,x) * z'.
D * (D * R(D,x,y)') = D * (R(D,x,y) * (D * R(D * D,x,y)')).
D * (R(D,x,y) * (D * R(D * D,x,y)')) = D * (D * R(D,x,y)').
C * ((C * (C' * (x' * (y' * C')))) * (y * x)) = a(y,x,C * C).
D * (R(D,x,y) * (D * R(D * D,x,y)')) = D * a(x,D,y).
D * (R(D,x,y) * (D * R(D * D,x,y)')) = R(D,y,x).
a(x,y,C * C) = a(x,C,y * C).
a(x,C,y * C) = a(x,y,C * C).
a(x,y,C * C) = a(x,y,C').
a(x,y,C * C) = a(y,x,C).
(x' * y') * (C * ((y * x) * (z * (x' * y')))) = (C * z) * (x' * y').
C' * (x' * ((y * x) * x')) = (C' * x') * R(y,x,C).
C' * (x' * y) = (C' * x') * R(y,x,C).
(C' * x') * R(y,x,C) = C' * (x' * y).
(C' * x') * ((C * (y * x)) * (C' * x')) = C' * (x' * y).
R(C * x,C,y * (x * x)) = y' * ((y * x) * C).
R(x * C,C,y * (x * x)) = y' * ((y * x) * C).
R(x * C,C,y * (x * x)) = y' * (C * (y * x)).
R(x * C,C,y * (x * x)) = R(x * C,C,y).
R(x * C,C,y) = R(x * C,y * x,x).
R(x * C,y * x,x) = R(x * C,C,y).
R(x * C,C,y) = x * R(C,y,x).
x * R(x' * C,C,y) = R(C,y,x').
x * R(C * x',C,y) = R(C,y,x').
R(C,x,y') = R(C,x',y).
R(C,x',y) = R(C,x,y').
R(C,x,y) = R(C,x',y').
R(C,x',y') = R(C,x,y).
C * a(x,C,y) = R(C,y,x).
a((C * C)',x,y) = C * R(C,y,x)'.
C * a(x,y,C) = R(C,x,y).
R(C,x,y) * a(y,x,C) = C.
R(x,C,R(C,y,z)) = R(x,C,a(y,z,C)).
R(x,C,a(y,z,C)) = R(x,C,R(C,y,z)).
R(C,x,y) = R(C,y,x').
R(C,x,y') = R(C,y,x).
(x * y) * R(C,x,y) = (x * C) * y.
R(C,x,y) = R(C,y',x).
R(C,x',y) = R(C,y,x).
((x * C) * y') * (x * y')' = R(C,y,x).
R(C,x,y * C) = R(C,y',x).
C' * (R(C,x,y) * R(C,x,y)) = a(y,x,C)' * R(C,x,y).
R(C,x,y * C) = R(C,x,y).
R(C,x,C * y) = R(C,x,y).
R(C,x,C * y') = R(C,y,x).
((x * C) * y)' * (x * y) = R(C,x,y)'.
C * R(C,x,y)' = a(x,y,C * C).
a(x,y,C * C) = C * R(C,x,y)'.
C * R(C,x,y)' = a(y,x,C).
a((C * C)',x,y) = a(y,x,C * C).
C * (C * R(C,x,y)') = R(C,y,x).
R(C,x,y) * R(C,y,x) = C * C.
D * R(C,B,A) = C * C.
R(D * (R(C,B,A) * C),R(C,B,A),C) = C * (C * C).
((x * C) * y') * (y * x') = R(C,y,x).
R(C,x,C * y') = ((x * C) * y') * (y * x').
((x * C) * y') * (y * x') = R(C,x,C * y').
R(C,x,C * y') = y' * ((y * (x * C)) * x').
x' * ((x * (y * C)) * y') = R(C,y,C * x').
R(D * (C * R(C,B,A)),R(C,B,A),C) = C * (C * C).
C' * R(C * C,x,y) = a(y,x,C)' * R(C,x,y).
a(x,y,C)' * R(C,y,x) = C' * R(C * C,y,x).
(x' * ((x * y') * (C' * C'))) * ((C * C) * y) = a(x',C * (x * C),y).
(C' * x') * (C * (x * (y * x'))) = (C * y) * (C' * x').
(C' * x') * (C * (x * y)) = (C * (y * x)) * (C' * x').
(C * (x * y)) * (C' * y') = (C' * y') * (C * (y * x)).
(C * ((x * y) * z)) * (C' * z') = (C' * z') * (C * ((z * (x * z)) * (z' * y))).
(C' * x') * (C * ((x * (y * x)) * (x' * z))) = (C * ((y * z) * x)) * (C' * x').
(x' * (C' * (C' * (x * y')))) * ((C * C) * y) = a(x',C * (x * C),y).
(x' * (C' * (C' * (x * y')))) * (C * (C * y)) = a(x',C * (x * C),y).
C * ((C * (x' * (C' * (C' * (x * y'))))) * y) = a(x',C * (x * C),y).
C * (((x' * C') * (x * y')) * y) = a(x',C * (x * C),y).
C * ((x * (C' * (x' * y'))) * y) = a(x',C * (x * C),y).
C * ((x * (C' * (x' * y'))) * y) = a(C * C,y,x)'.
C * (C' * a(C',x,y)') = a(C * C,x,y)'.
a(C * C,x,y)' = a(C',x,y)'.
a(C',x,y)'' = a(C * C,x,y).
a(C * C,x,y) = a(C',x,y)''.
a(C * C,x,y) = a(C',x,y).
a(C * C,x,y) = a(x,y,C').
a(C,x,y) * (C * (a(C * C,x,y) * C')) = 1.
((x' * y') * z') * ((((z * y) * x) * u) * a(z,y,x)) = a(z,y,x) * (u * a(z,y,x)).
((x' * y') * z') * (z' * (((z * (z * y)) * x) * z')) = a(z * z,y,x) * z'.
(C' * x') * (C * ((x * (y * x)) * (z * (z' * (x' * u))))) = (C * ((y * u) * x)) * (C' * x').
((x' * y') * z') * ((z * y) * (x * z')) = a(z * z,y,x) * z'.
((x' * y') * z') * ((z * y) * (x * z')) = a(z,y,x) * (z' * a(z,y,x)).
a(x,y,z) * (x' * a(x,y,z)) = a(x * x,y,z) * x'.
a(C,x,y) * (C * (a(C,x,y) * (C' * a(C,x,y)))) = 1.
a(C,x,y) * (a(C,x,y) * a(C,x,y)) = 1.
a(x,C,y') * (a(C,x,y) * a(C,x,y)) = 1.
a(x,C,y') * (a(C,x,y) * a(x,y,C)) = 1.
a(x,C,y') * (a(x,y,C) * a(x,y,C)) = 1.
a(x,C,y) * (a(y,x,C) * a(y,x,C)) = 1.
a(x,C,y) * (a(x,C,y) * a(y,x,C)) = 1.
a(x,C,y) * (a(x,C,y) * a(x,C,y)) = 1.
a(x,C,y)' * 1 = a(x,C,y) * a(x,C,y).
a(x,C,y) * a(x,C,y) = a(x,C,y)' * 1.
a(x,C,y) * a(x,C,y) = a(x,C,y)'.
C * a(x,C,y)' = a(x,C,y) * (C * a(x,C,y)).
a(x,C,y) * (C * a(x,C,y)) = C * a(x,C,y)'.
a(x,C,y) * R(C,y,x) = C * a(x,C,y)'.
a(x,C,y) * R(C,y,x) = C * a(y,C,x).
a(x,C,y) * R(C,y,x) = R(C,x,y).
a(x,y,C)' * R(C,y,x) = R(C,x,y).
R(C,x,y) = C' * R(C * C,y,x).
C' * R(C * C,x,y) = R(C,y,x).
C * R(C,x,y) = R(C * C,y,x).
R(C * C,x,y) = C * R(C,y,x).
R(D * R(C * C,A,B),R(C,B,A),C) = C * (C * C).
R(D * (D * D),R(C,B,A),C) = C * (C * C).
(C' * x') * ((C * (C * (x * (y * x)))) * (C' * (x' * z))) = (C * ((y * z) * x)) * (C' * x').
(C' * x') * ((C * (C * (x * (y * x)))) * ((C' * x') * ((C * (z * x)) * (C' * x')))) = (C * ((y * z) * x)) * (C' * x').
(C' * x') * (((C * x) * (C * (y * x))) * ((C' * x') * ((C * (z * x)) * (C' * x')))) = (C * ((y * z) * x)) * (C' * x').
(C' * x') * (((C' * x')' * (C * (y * x))) * ((C' * x') * ((C * (z * x)) * (C' * x')))) = (C * ((y * z) * x)) * (C' * x').
(C * ((x * y) * z)) * (C' * z') = ((C * (x * z)) * (C' * z')) * ((C * (y * z)) * (C' * z')).
((C * (x * y)) * (C' * y')) * ((C * (z * y)) * (C' * y')) = (C * ((x * z) * y)) * (C' * y').
((C * (x * y)) * (C' * y')) * R(z,y,C) = (C * ((x * z) * y)) * (C' * y').
R(x,y,C) * R(z,y,C) = (C * ((x * z) * y)) * (C' * y').
(C * ((x * y) * z)) * (C' * z') = R(x,z,C) * R(y,z,C).
R(x,y,C) * R(z,y,C) = R(x * z,y,C).
x * R(y,x,C) = R(x * y,x,C).
R(x * y,x,C) = x * R(y,x,C).
x * R(y * C,x,C) = (x * C) * y.
x' * ((x * C) * y) = R(y * C,x,C).
x * ((x' * C) * y) = R(y * C,x',C).
(x * y) * (C * y') = R(x * C,y,C).
R(x * C,y,C) = y * (C * (y' * x)).
x * (C * (x' * y)) = R(y * C,x,C).
(x * (y * C)) * y' = R(x * C,y,C).
(x' * R(x * C,y,C)) * a(x',y,C * (y' * x)) = C.
x' * R(x * C,y,C) = R(C,y,C * x').
R(x * C,y',C) = R(x * C,C,y).
R(x,y',C) = R((x * C') * C,C,y).
R((x * C') * C,C,y) = R(x,y',C).
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).
x' * R(x * C,y,C) = R(C,x,y).
R(C,x,y) * a(x',y,C * (y' * x)) = C.
R(C,x,y)' * C = a(x',y,C * (y' * x)).
a(x',y,C * (y' * x)) = R(C,x,y)' * C.
C * R(C,x,y)' = a(x',y,C * (y' * x)).
a(x',y,C * (y' * x)) = C * R(C,x,y)'.
R(x,C,a(y',z,C * (z' * y))) = R(x,C,R(C,y,z)').
a((C * C)',x,y) = a(y',x,C * (x' * y)).
a(x',y,C * (y' * x)) = a((C * C)',y,x).
R(x,C,a(y',z,C * (z' * y))) = R(x,R(C,y,z),C).
R(x,C,a((C * C)',y,z)) = R(x,R(C,z,y),C).
R(x,C,a(y,z,C * C)) = R(x,R(C,y,z),C).
R(x,C,a(y,z,C)) = R(x,R(C,z,y),C).
R(x,R(C,y,z),C) = R(x,C,a(z,y,C)).
R(x,R(C,y,z),C) = R(x,C,R(C,z,y)).
R(D * (D * D),C,R(C,A,B)) = C * (C * C).
R(D * (D * D),C,D) = C * (C * C).
C * (C * C) = D * (D * D).
(C * (C * C)) * x = D * (D * (D * x)).
D * (D * (D * x)) = C * (C * (C * x)).
C * (C * (C * x)) = D * (D * (D * x)).
D * (D * (D * x)) = C * (x * (C * C)).
C * (x * (C * C)) = D * (D * (D * x)).
((C * (C * (C * x))) * y) * ((D * x) * y)' = R(D * D,D * x,y).
C * (R(D,x,y)' * (C * C)) = D * (D * a(y,x,D)).
C * (R(D,x,y)' * (C * C)) = D * R(D,y,x).
C * (C * (C * R(D,x,y)')) = D * R(D,y,x).
(C * ((C * x) * (y * C))) * ((D * x) * y)' = R(D * D,D * x,y).
(C * (C * ((x * y) * C))) * ((D * x) * y)' = R(D * D,D * x,y).
R(D * D,D * x,y) = C * ((C * (x * y)) * (C * ((D * x) * y)')).
C * ((C * (x * y)) * (C * ((D * x) * y)')) = R(D * D,D * x,y).
C * (C * (C * R(D,x,y)')) = R(D * D,D * x,y).
C * (C * (C * R(D,D * x,y)')) = R(D * D,x,y).
C * (C * (C * R(D,x,y)')) = R(D * D,x,y).
R(D * D,x,y) = D * R(D,y,x).
D * R(D * D,x,y)' = R(D,y,x)'.
D * (R(D,x,y) * R(D,y,x)') = R(D,y,x).
D * a(x,D,y * y) = R(D,x,y).
R(D,x,y * y) = R(D,y,x).
D * R(D,x,y)' = a(y,D,x * x).
a(x,D,y * y) = D * R(D,y,x)'.
a(x,D,y * y) = a(x,y,D).
x * a(x,y,D) = R(x,D,y * y).
R(x,D,y * y) = x * a(x,y,D).
R(x,D,y * y) = R(x,y,D).
R(R(x,D,y * y),D,y) = x.
R(R(R(x,y,D),y,D),y,D) = x.
R(R(R(R(x,y,z),u,w),w,u),z,y) = x.
R(R(x,D,y),D,y) = R(x,y,D).
a(x,D,y) * (a(x,D,y) * a(x,D,y)) = 1.
a(x,D,y) * a(x,y,D) = 1.
a(x,D,y) * a(x,D,y) = a(y,x * x,D).
a(x,D,y * y) = a(y,D,x).
a(x,D,y) * a(y,x * x,D) = 1.
a(x,y,D) * (a(x,y,D) * a(x,y,D)) = 1.
a(x,y,D) * a(x,D,y) = 1.
(x * a(y,D,z))' = a(y,z,D) * x'.
(a(x,D,y) * a(z,D,u))' = a(z,u,D) * a(x,y,D).
a(x,D,y * y) = a(y,x,D) * a(y,x,D).
a(x,y,D) * a(x,y,D) = a(y,D,x * x).
a(x,y,D) * a(x,y,D) = a(x,D,y).
a(D,x,y) * (a(D,x,y) * a(D,x,y)) = 1.
a(D,x,y) * (a(y,D,x) * a(y,D,x)) = 1.
a(D,x,y) * (a(D,x,y) * a(y,D,x)) = 1.
R(R(R(D,x,y),x,y),x,y) = D.
((x * y') * z)' = z' * (y * x').
(x * (y' * z))' = (z' * y) * x'.
R(x,y',z) = ((x * y') * z) * (z' * y).
((x * y') * z) * (z' * y) = R(x,y',z).
x * ((x' * y) * z) = (y * x) * (x' * z).
(x * y) * (y' * z) = y * ((y' * x) * z).
x * ((x' * y) * z') = (y * x) * (z * x)'.
(x * y) * (z * y)' = y * ((y' * x) * z').
R(x * (y * z),x,y) = (x * y) * z.
R(x * (y * ((x * y)' * z)),x,y) = z.
R(x,y,z) = z * ((z' * y) * (y' * x)).
R(x,y,z) = z * (y * ((z * y)' * x)).
R(x,y,z) = z * (R(z',y,x) * x).
x * (R(x',y,z) * z) = R(z,y,x).
x * ((x' * (y * z')) * z) = R(y,z',x).
x * (((y * z') * x)' * y) = R(z,y',x).
x * (((y * z) * x)' * y) = R(z',y',x).
(x * y) * (z * y)' = y * (z * (x' * y))'.
R(x,y,z)' = R(x',y,z).
x * (R(x,y,z)' * z) = R(z,y,x).
x * (((y * z) * x)' * y) = R(z,y',x)'.
x * R(y,z,x') = R(x',z,y)' * y.
R(x',y,z)' * z = x * R(z,y,x').
R(x,y,z) * z = x * R(z,y,x').
R(x,y * x,z) * z = x * R(z,x,y).
R(R(D,x,y),x,y') = D.
R(D,x,D * y) = R(D,y,x').
R(D,x,y) * (D' * y') = R(y',x,R(D,x,y)).
R(x',y,R(D,y,x)) = R(D,y,x) * (D' * x').
R(D,x,D * y) = R(D,x,y).
R(D,x,y) = (D * y) * (x * (((D * y) * x)' * D)).
(D * x) * (y * (((D * x) * y)' * D)) = R(D,y,x).
R(x,y * x,D) = R(x,y',D').
R(x,D',y) = R(x,D,y').
R(x,D',y) = R(x,y,D).
R(x,y * x,D) = R(x,y,D).
x * (y * R(x,y,z))' = R(y,z * y,x)'.
R(x',y,R(D,y,x)) = R(D,y,x) * (x * D)'.
(D * x) * R(x,D',y)' = R(D,y,x).
(D * x) * R(x,y,D)' = R(D,y,x).
(x * y) * (z * (x * y)) = x * (y * ((z * x) * y)).
(x * R(x,y,D)') * (D * (x * R(x,y,D)')) = x * (R(x,y,D)' * R(D,y,x)).
R(D,x,y) * a(y,D,x) = D * (a(y,D,x) * a(y,D,x)).
D * (a(x,D,y) * a(x,D,y)) = R(D,y,x) * a(x,D,y).
(a(x,D,y) * D) * a(x,D,y) = a(x,D,y) * R(D,y,x).
R(D,x,y) * (z * D)' = D * (z * (a(y,D,x)' * D))'.
D * (x * (a(y,D,z)' * D))' = R(D,z,y) * (x * D)'.
a(x,D,y)' * D = R(D,x,y).
R(D,x,y) * a(y,D,x) = a(y,D,x) * R(D,x,y).
a(x,D,y) * R(D,y,x) = R(D,y,x) * a(x,D,y).
D * (x * R(D,y,z))' = R(D,z,y) * (x * D)'.
R(D,x,y) * (z * D)' = D * (z * R(D,y,x))'.
R(x',y,R(D,y,x)) = D * (x * R(D,x,y))'.
R(x',y,R(D,y,x)) = R(x,y * x,D)'.
R(x',y,R(D,y,x)) = R(x,y,D)'.
x * (R(x,y,D)' * R(D,y,x)) = R(R(D,y,x),y,x).
D * a(x,y * y,D) = R(D,x,y) * a(y,D,x).
R(D,x,y) * a(y,D,x) = D * a(x,y * y,D).
R(D,x,y) * a(y,D,x) = R(D,x,y * y).
a(x,D,y) * R(D,y,x) = R(D,y,x * x).
a(x,D,y) * (D * (x * R(x,y,D)')) = x * (R(x,y,D)' * R(D,y,x)).
a(x,D,y) * (D * a(x,D,y)) = x * (R(x,y,D)' * R(D,y,x)).
a(x,D,y) * R(D,y,x) = x * (R(x,y,D)' * R(D,y,x)).
x * (R(x,y,D)' * R(D,y,x)) = a(x,D,y) * R(D,y,x).
a(x,D,y) * R(D,y,x) = R(D,x,y).
x * (R(x,y,D)' * R(D,y,x)) = R(D,x,y).
R(D,x,y) = R(R(D,y,x),y,x).
R(R(D,x,y),x,y) = R(D,y,x).
a(x * (x * x),y,D) = 1.
x * (y * x) = y' * ((y * x) * (y * x)).
x' * ((x * y) * (x * y)) = y * (x * y).
(x * y) * ((x * z) * (x * y)) = x * (y * (x * (z * (x * y)))).
x * (y * (x * y)) = (x * y) * (x * y).
(x * y) * (x * y) = x * (y * (x * y)).
x * (R(x,y,D) * a(x,D,y)) = R(x,y,D) * (a(x,D,y) * (R(x,y,D) * a(x,D,y))).
R(x,y,D) * (a(x,D,y) * (R(x,y,D) * a(x,D,y))) = x * (R(x,y,D) * a(x,D,y)).
R(x,y',D)' * x = a(x,y,D).
(x * y) * (x * (y * (x * y))) = x * (y * (x * (y * (x * y)))).
a(x,D,y) * y = R(y,x,D).
x * (R(x,y,D) * (a(x,D,y) * (R(x,y,D) * a(x,D,y)))) = R(x,y,D) * (a(x,D,y) * (R(x,y,D) * (a(x,D,y) * (R(x,y,D) * a(x,D,y))))).
R(x,y,D) * (a(x,D,y) * (R(x,y,D) * (a(x,D,y) * (R(x,y,D) * a(x,D,y))))) = x * (R(x,y,D) * (a(x,D,y) * (R(x,y,D) * a(x,D,y)))).
R(x,y,D) * (a(x,D,y) * (R(x,y,D) * a(x,D,y))) = x * x.
a(x,D,y) * (x * x) = R(x * x,y,D).
R(x,y,D) * (a(x,D,y) * (R(x,y,D) * (a(x,D,y) * (R(x,y,D) * a(x,D,y))))) = x * (x * x).
R(x,y,D) * (a(x,D,y) * (x * x)) = x * (x * x).
R(x,y,D) * R(x * x,y,D) = x * (x * x).
x * (x * x) = R(x * (x * x),y,D).
R(x * (x * x),y,D) = x * (x * x).
(x * (x * x))' * (x * (x * x)) = a(x * (x * x),y,D).
a(x * (x * x),y,D) = (x * (x * x))' * (x * (x * x)).
a(x * (x * x),D,y) = 1.
1 = a(x * (x * x),D,y).
a(x,D,y * (y * y)) = 1.
a(x,y * (y * y),D) = 1.
1 = a(x,y * (y * y),D).
a(D,x * (x * x),y) = 1.
a(D,x,y * (y * y)) = 1.
a(x,D,y')' = a(D,y,x).
a(x,y',D) = a(D,y,x).
a(D,x,y) = a(y,x',D).

end_of_list.
