Theorem TC-7. Associativity of Mal’cev polynomial under TC.

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

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

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

1 x = x 2 x · y = z, u · v = z, x · w = v_{6}, v_{7} · v = v_{6} → u · w = v_{7} · y 4,3 m(x, y, z) = ((y · y) · x) · (z · y) 5 x · (y · x) = y 7 m(A, B, m(C, D, E)) = m(m(A, B, C), D, E) → □

8 ((B · B) · A) · ((((D · D) · C) · (E · D)) · B) =

((D · D) · (((B · B) · A) · (C · B))) · (E · D) → □

[copy,7 :4,4,4,4]

14  (x · y) · x = y  [5 → 5]
17  (x · ((y · z) · u)) · y = (x · z) · u  [2,14,14,1,14, flip]
19  x · (y · (z · u)) = ((u · x) · y) · z  [2,14,5,5,14]
784  x · (((y · z) · u) · v) = (y · ((((v · w) · x) · z) · u)) · w  [2,1,5,5,17]
1734,1733 (x · ((((y · z) · u) · v) · w)) · z = (x · (u · (v · y))) · w  [19 → 17]
1752  x · (((y · z) · u) · v) = (y · (x · (z · v))) · u  [784 :1734]
1753  □  [1752,8]