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

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

Proof (found by Otter 3.0.4 on gyro at 4.67 seconds).

1 B · A · B · A · B · A · B · A = A · B · A · B · A · B · A · B → □ 2 x = x 3 x · y = z, x · u = z → y = u 6,5 (x · y) · z = x · y · z 7 x · y · y · y · y = y · y · y · y · x

10 x · y · z · y · z · y · z · y · z = y · z · y · z · y · z · y · z · x

[5 → 7 :6,6,6,6,6,6]

211  x · y · x · y · x · y · x · y = y · x · y · x · y · x · y · x  [3,2,10]
212  □  [211,1]