Theorem CS-GL-4. Nearly (2) associative cancellative (gL)-groupoids are commutative.

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

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

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

6  (((x · y) · z) · u) · v = x · (y · (z · (u · v)))  [flip 5]

7 ((x · (y · (z · (u · v)))) · w) · v_{6} = ((x · y) · z) · (u · (v · (w · v_{6})))

[6 → 6]

8 (x · (y · (z · (u · v)))) · w = (x · y) · (z · (u · (v · w))) [6 → 6]

25 ((x · (y · (z · (u · v)))) · w) · v_{6} = ((x · y) · w) · (u · (v · (z · v_{6})))

[(gL) 7]

32  (x · (y · (z · (u · v)))) · w = (x · y) · (w · (u · (v · z)))  [4,8,25, flip]
33  (x · (y · (z · u))) · v = (x · (y · (v · u))) · z  [4,7,25 :(gL)]
37  (x · y) · (z · (u · (v · w))) = (x · v) · (z · (u · (y · w))) [7 → 25 :(gL)]
56  x · (y · (z · (u · v))) = x · (v · (z · (u · y)))  [8 → 32 :(gL)]
61  x · (y · (z · u)) = u · (y · (z · x))  [3,33,56]
208  x · y = y · x  [4,61,37]
209  □  [208,1]