Theorem UAL-4. Uniqueness of binary Steiner law under (gL). The type of theory is ⟨2, 2, 0⟩ with corresponding operations f, g, and e.

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

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

2 f(x, y) = f(y, x) 3 f(x, f(y, x)) = y 4 f(e, e) = e 5 g(x, y) = g(y, x) 6 g(x, g(y, x)) = y 7 g(e, e) = e 8 g(A, B) ≠ f(A, B) 9 f(e, e) = e 10 f(x, f(y, x)) = y

11  f(x, g(e, e)) = f(e, x)  [7 → 2]
15  f(x, f(x, y)) = y  [2 → 3]
22  g(x, g(x, y)) = y  [5 → 6]
48  g(x, y) = f(z, f(z, g(y, x)))  [15 → 5]
106  f(x, g(e, e)) = f(e, g(y, g(y, x)))  [22 → 11]
493  f(e, g(x, g(e, y))) = f(y, g(x, e))  [4 → 106 :(gL) :9, flip]
500  f(x, g(x, e)) = e  [6 → 493 :9, flip]
536  f(x, g(x, y)) = f(z, g(z, y))  [500 → 500 :(gL)]
551  g(e, x) = f(x, e)  [500 → 48]
860  f(x, g(x, y)) = y  [551 → 536 :10]
983  g(x, y) = f(x, y)  [22 → 860, flip]
984  □  [983,8]