Theorem STN-7. A 1-basis for commutative SQUAGS.

\{((xx)y)(z(yx)) = z\} ⇔ \{ \begin{matrix}xy = yx \\ xx = x \\ (xy)x = y \end{matrix} \} .

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

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

5  x · (y · ((x · ((z · z) · z)) · (z · z))) = y  [2 → 2]
9  (((x · y) · (x · y)) · z) · z = (y · y) · x  [2 → 2]
15  x · (x · ((y · y) · y)) = (y · y) · y  [2 → 5]
26,25  (x · x) · (x · x) = (x · x) · x  [2 → 15]
29  ((((x · x) · x) · ((x · x) · x)) · y) · ((x · x) · x) = y  [15 → 2]
36,35  ((x · x) · x) · ((x · x) · x) = ((x · x) · x) · (x · x)  [25 → 25 :26,26]
37  ((((x · x) · x) · (x · x)) · y) · ((x · x) · x) = y  [29 :36]
41  x · (x · (((y · y) · y) · (y · y))) = ((y · y) · y) · (y · y)  [25 → 15 :26]
46,45  ((x · x) · x) · (x · x) = x · x  [25 → 2 :36]
55  x · (x · (y · y)) = y · y  [41 :46,46]
58,57  ((x · x) · y) · ((x · x) · x) = y  [37 :46]
60,59  x · x = x  [35 :58,46, flip]
62,61  (x · y) · x = y  [57 :60,60,60]
63  x · (x · y) = y  [55 :60,60]
75  ((x · y) · z) · z = y · x  [9 :60,60]
79  B · A = A · B → □  [4 :60,62 :1,1]
81,80  (x · y) · y = x  [61 → 63]
82  x · y = y · x  [75 :81]
83  □  [82,79]

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

1 x = x 3,2 x · x = x 4 (x · y) · x = y 6 x · y = y · x 7 ((A · A) · B) · (C · (B · A)) ≠ C

8  (A · B) · (C · (B · A)) ≠ C  [copy,7 :3]
10,9  x · (y · x) = y  [4 → 4]
15  C ≠ C  [6 → 8 :10]
16  □  [15,1]