Theorem CS-GL-3. Nearly (1) associative cancellative (gL)-groupoids are commutative.

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

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

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

6  ((x · y) · z) · u = x · (y · (z · u))  [flip 5]
7  ((((x · y) · z) · u) · v) · w = x · ((y · (z · u)) · (v · w))  [6 → 6]
8  ((x · (y · (z · u))) · v) · w = ((x · y) · z) · (u · (v · w))  [6 → 6]
14  ((x · y) · z) · (u · v) = x · (((y · z) · u) · v)  [6 → 6]
38  ((x · y) · z) · (u · v) = x · ((y · (z · u)) · v)  [6 → 7 :(gL)]
42  x · (((y · z) · u) · v) = x · ((y · (z · u)) · v)  [14 → 38]
53  ((x · y) · z) · u = (x · (y · z)) · u  [3,2,42, flip]
63  (x · y) · z = x · (y · z)  [4,2,53, flip]
111  ((x · (y · (z · u))) · v) · w = ((x · y) · v) · (u · (z · w))  [(gL) 8]
125  (x · (y · z)) · u = (x · y) · (z · u)  [63 → 63]
273  (x · y) · (z · (u · v)) = (x · u) · (z · (y · v))  [8 → 111 :(gL)]
453  (x · y) · z = y · (x · z)  [3,273,125, flip]
540  x · y = y · x  [4,63,453]
541  □  [540,1]