Wilkie's identity

Example

Write $A = 1 + x$, $B = 1 + x + x^2$, $C = 1 + x^3$ and $D = 1 + x^2 + x^4$, where $x^2$ means $x \cdot x$ and so on. Wilkie's identity is $$(A^y + B^y)^x \cdot (C^x + D^x)^y = (A^x + B^x)^y \cdot (C^y + D^y)^x.$$ It is an identity in the signature $1, +, \cdot$, exponentiation.

Check that it holds for all positive integers $x, y$. Let $Q = 1 - x + x^2$, a positive integer for $x \ge 1$. Then $C = A \cdot Q$ and $D = B \cdot Q$. So $C^x + D^x = Q^x (A^x + B^x)$ and $C^y + D^y = Q^y (A^y + B^y)$. Both sides become $(A^y + B^y)^x \cdot (A^x + B^x)^y \cdot Q^{xy}$.

Alex Wilkie showed that this identity cannot be derived from the eleven high school identities, which answers Tarski's high school algebra problem negatively. The check above uses the term $1 - x + x^2$, which needs subtraction and so is not a term of the signature.