Theorem STN-8. An axiom schema for commutative Steiner quasigroups.

\{(g(x) · y) · (z · (y · x)) = z\} ⇔ \{ \begin{matrix}x · y = y · x \\ (x · y) · x = y \\ g(x) = x \end{matrix} \} .

This shows that the equational theory of any finitely based subvariety of Steiner quasigroups is one based. The unary g(x) packs all the remaining equations true in the subvariety in question. For example, we obtain Thm. STN-7 if g(x) = x·x,

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

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

5  (g(x · (y · z)) · (g(z) · y)) · (u · x) = u  [2 → 2]
8,7  (g(x · y) · z) · z = g(y) · x  [2 → 2]
10,9  g(x) · (g(y · z) · x) = g(y) · g(z)  [7 → 7 :8, flip]
13  (g(x) · y) · (g(z) · u) = g(u · z) · (y · x)  [7 → 2]
24  (g(x) · g(y · z)) · (g(y) · g(z)) = g(x)  [9 → 2]
59,58  g(x · y) · x = g(y)  [7 → 5]
69  g(g(x)) · g(y · x) = g(y)  [58 → 58]
77,76  g(x · (y · z)) = g(x) · (g(z) · y)  [2 → 58, flip]
121  g(x) · (y · (z · (z · x))) = y  [58 → 2]
131,130 g(g(x · y)) = g(g(x)) · g(g(y))  [58 → 69, flip]
148  g(x) · (g(x) · g(y)) = g(g(y))  [69 → 24]
155  g(x) · (y · (g(x · z) · g(z))) = y  [69 → 2]
174  (g(x) · y) · y = (g(x) · g(z)) · g(z)  [121 → 7 :77,59]
186  (g(x) · g(y)) · g(y) = (g(x) · z) · z  [flip 174]
197  g(x) · g(y) = g(y) · x  [148 → 7 :10]

233 ((g(g(x)) · g(g(y))) · (g(z) · u)) · (g(z) · u) = g(g(y) · x)

[13 → 58 :77,131]

240 g(g(x) · y) = ((g(g(y)) · g(g(x))) · (g(z) · u)) · (g(z) · u) [flip 233]
245,244 g(x · y) · g(y) = g(x)  [69 → 197, flip]
249 g(x) · (y · g(x)) = y [155 :245]
276,275 g(g(x) · y) = g(x) · g(y)  [58 → 249, flip]

288 ((g(g(x)) · g(g(y))) · (g(z) · u)) · (g(z) · u) = g(y) · g(x)

[240 :276, flip]

335,334 g(g(x)) · (y · g(x)) = y  [249 → 121]
340,339 g(g(x)) · g(g(y)) = g(x) · g(y)  [249 → 9 :59,131]
344,343 g(x · g(y)) = g(x) · g(y)  [249 → 58, flip]
346,345 (g(x) · g(y)) · g(y) = g(x)  [249 → 24 :344,335]
353,352 g(x) · (y · x) = y  [249 → 2 :344,346]
370  ((g(x) · g(y)) · (g(z) · u)) · (g(z) · u) = g(y) · g(x)  [288 :340]
392  (g(x) · y) · y = g(x)  [186 :346, flip]
403,402 g(x · y) = g(x) · g(y)  [9 :353]
418,417 ((g(x) · g(y)) · z) · z = g(y) · x  [7 :403]

472,471 g(x) · g(y) = g(x) · y  [370 :418, flip]
530,529 g(x · y) = g(x) · y  [402 :472]
570 x · (x · y) = g(y) [352 → 392]
585,584 g(x) = x  [570 → 121 :530,353]
591,590 (x · y) · x = y  [570 → 2 :585,585]
594  x · y = y · x  [570 → 2 :585,585]
619  □  [4 :585,591 :594,1,1]

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

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

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