Theorem MCV-1. Associativity of Mal’cev polynomial under (gL).

\{ \begin{matrix}m(x, y, y) = x \\ m(x, x, y) = y \end{matrix} \} =(gL)⇒ \{m(x, y, m(z, u, v)) = m(v, u, m(x, y, z))\}.

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

2 m(x, y, y) = x 3 m(x, x, y) = y 4 m(A, B, m(C, D, E)) ≠ m(E, D, m(A, B, C))

25  m(x, x, y) = m(y, z, z)  [2 → 3]
70  m(x, y, z) = m(z, y, x)  [(gL) 25]
98  m(x, x, m(y, z, u)) = m(u, z, y)  [3 → 70]
99  m(m(x, y, z), u, u) = m(z, y, x)  [2 → 70]
135  m(m(C, D, E), B, A) ≠ m(E, D, m(A, B, C))  [70 → 4]
183  m(x, y, m(z, u, y)) = m(x, u, z)  [(gL) 98]
291  m(m(x, y, z), x, u) = m(z, y, u)  [(gL) 99]
304  m(m(x, y, z), u, v) = m(z, y, m(v, u, x))  [183 → 291]
305  □  [304,135]