Theorem MCV-2. Mal’cev polynomial under (gL).

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

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

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

19  x · (y · m(x, z, z)) = y  [4 → 2]
34  x · (y · m(z, z, x)) = y  [5 → 2]
36  x · (x · m(y, y, z)) = z  [5 → 3]
48  x · (y · (y · (x · z))) = z  [3 → 3]
69  x · m(y, y, z · m(u, u, x)) = z  [5 → 34]
73  x · m(y, y, x · m(z, z, u)) = u  [5 → 36]
140  x · m(y, y, z) = z · m(u, u, x)  [69 → 73]
173  x · m(y, z, u) = u · m(y, z, x)  [(gL) 140]
222  x · (y · m(x, y, z)) = z  [173 → 19]
239  x · (y · z) = m(y, x, z)  [222 → 48]
241  □  [239,6]