Theorem CS-9. Support (9) for the CS conjecture.

{CS, xy^{n} = y^{n}x} ⇒ {(xy)^{n} = (yx)^{n}}.

Otter easily proves the statement for n = 2, 3, 4, 5, and it is easy to construct by hand a proof of the general theorem by looking at the Otter proofs.

Proof .

xy^{n} = y^{n}x  [hypothesis]
x(xw)^{n} = (xw)^{n}x [set y = xw]
= x(wx)^{n} [change power notation]
(xw)^{n} = (wx)^{n} [cancel x]