% -----------------------------------------------------------
% Gagola:  Moufang + Normal 1 => {Normal 2, Normal 3, Drapal}
% -----------------------------------------------------------

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.

% *********************
% Normality Condition 1
% *********************

% condition from J.D.'s talk at ADAM 2013

  (((C * x) * y) * (y' * x')) * z = z * (((C * x) * y) * (y' * x'))
     # label("Normal 1").

% *********************
% Normality Condition 2
% *********************

% condition used by J.D.

% define D; A and B are arbitrary constants

  R(C,A,B) = D.

% D is in the commutant

% D * x = x * D # label("Normal 2").

% *********************
% Normality Condition 3
% *********************

% condition used by MK (uses commutator K)

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

% K(R(C,x,y),z) = 1 # label("Normal 3").

% ****************************************
% Normality Condition 4 (Drapal Condition)
% ****************************************

% uses associator (a) and commutator (K)

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

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

% a(x,C,K(y,z)) = 1 # label("Drapal Condition").

end_of_list.

formulas(goals).

% (((C * x) * y) * (y' * x')) * z = z * (((C * x) * y) * (y' * x'))
%    # label("Normal 1").

  D * x = x * D # label("Normal 2").

  K(R(C,x,y),z) = 1 # label("Normal 3").

  a(x,C,K(y,z)) = 1 # label("Drapal Condition").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

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

end_of_list.
