Theorem CS-GL-1. Cancellative (gL)-semigroups are commutative.

\{ \begin{matrix}(xy)z = x(yz) \\ cancellation \end{matrix} \} =(gL)⇒ \{xy = yx\}.

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

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

6  (((x · y) · z) · u) · v = (x · (y · z)) · (u · v)  [4 → 4]
11  (x · (y · z)) · u = (x · y) · (z · u)  [4 → 4]
432  (((x · y) · z) · u) · v = (x · u) · ((y · z) · v)  [(gL) 6]
433  ((x · y) · z) · u = x · (u · (y · z))  [3,11,432, flip]
1205  x · y = y · x  [2,432,433]
1206  □  [1205,5]