Theorem STN-2. (gL)-basis for 4-ary Steiner law.

\{ \begin{matrix}f(v, w, x, y) = f(v, w, y, x) \\ f(e, e, e, e) = e \\ f(e, e, x, f(e, e, x, y)) = y \end{matrix} \} =(gL)⇒ \{f(v, w, x, f(v, w, x, y)) = y\}.

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

1 f(D, A, B, f(D, A, B, C)) ≠ C 3 f(x, y, z, u) = f(x, y, u, z) 4 f(e, e, e, e) = e 6 f(e, e, x, f(e, e, x, y)) = y

11,10  f(e, e, f(e, e, x, y), x) = y  [3 → 6]
12  f(x, y, e, e) = f(x, y, z, f(e, e, z, e))  [6 → 4 :(gL) :(gL)]

17 f(x, y, z, f(u, v, z, w)) = f(x, y, v_{6}, f(u, v, v_{6}, w))

[12 → 12 :(gL) :(gL) :(gL)]

34  f(x, y, f(z, u, v, w), v) = f(x, y, v_{6}, f(z, u, v_{6}, w))  [3 → 17]
120  f(x, y, z, f(u, v, f(u, v, w, v_{6}), v_{6})) = f(x, y, z, w)  [(gL) 34, flip]
134  f(x, y, f(x, y, z, u), u) = z  [120 → 10 :11, flip]
167  f(x, y, z, f(x, y, z, u)) = u  [34 → 134]
169  □  [167,1]