Theorem STN-5. A 1-basis for totally symmetric quasigroups (SQUAGS) (1).

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

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

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

9  ((x · x) · (y · z)) · x = (y · y) · z  [2 → 2]
15  (x · x) · (y · (y · y)) = x · (y · y)  [2 → 9, flip]
57,56  (x · (y · y)) · x = (y · y) · (y · y)  [15 → 9]
58  ((x · x) · (x · x)) · (y · (x · x)) = y · y  [15 → 2]
61  x · x = ((y · y) · (y · y)) · (x · (y · y))  [flip 58]
119,118 (x · x) · (x · x) = (x · x) · x  [56 → 9 :57]
138,137 x · x = x  [61 :119,3]
142,141 (x · y) · x = y  [56 :138,138,138,138]
143  □  [4 :138,142 :1,1]

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

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

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