Theorem QUART-1. Mazur lemma.

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

{m(x, y, m(x, z, u)) = m(u, y, m(u, z, u))}.

Our first version of this problem had a different conclusion:

m(x, y, m(x, z, w)) = m(u, y, m(u, z, w)).

After Otter failed to prove the first version, we found the following counterexample. Define m(x, y, z) as ax + by + cz in an Abelian group. Such an algebra is always a (gL)-algebra. The first equation m(x, y, m(x, y, z)) = z demands that a + ac = 0, b + bc = 0, and c^{2} = 1. Thus c = −1 would satisfy all the conditions without the number a being 0. Now the second equation m(x, y, z) = m(x, z, y) demands that b = c. Hence choose b = c = −1 and a = 2, say. Now, m(x, y, m(z, x, w)) = 2x − y − (2z − x − w) = x − y − 2z − w, which is not independent of x in the Abelian group of integers! Thus our original goal is not a consequence of the assumptions. However, the following equation is true in this model: m(x, y, m(x, z, w)) = m(u, y, m(u, z, w) because the left-hand side reduces to 2x − y − (2x − z − w) = z − y + w, which is independent of x. Thus, the corrected formulation of Thm. QUART-1 is given above.

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

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

10  m(x, y, m(x, y, z)) = m(u, v, m(u, v, z))  [2 → 2]
163  m(x, y, m(x, z, u)) = m(v, y, m(v, z, u))  [(gL) 10]
164  □  [163,4]