Wilkie's Identity

Wilkie's identity is an identity which is true over the natural numbers, but not provable using Tarski's high school algebra axioms. The identity takes the following form:

((1+x)y+(1+x+x2)y)z⋅((1+x3)z+(1+x2+x4)z)y=⋅superscriptsuperscript1𝑥𝑦superscript1𝑥superscript𝑥2𝑦𝑧superscriptsuperscript1superscript𝑥3𝑧superscript1superscript𝑥2superscript𝑥4𝑧𝑦absent\displaystyle((1+x)^{y}+(1+x+x^{2})^{y})^{z}\cdot((1+x^{3})^{z}+(1+x^{2}+x^{4}% )^{z})^{y}=
((1+x)z+(1+x+x2)z)y⋅((1+x3)y+(1+x2+x4)y)z⋅superscriptsuperscript1𝑥𝑧superscript1𝑥superscript𝑥2𝑧𝑦superscriptsuperscript1superscript𝑥3𝑦superscript1superscript𝑥2superscript𝑥4𝑦𝑧\displaystyle((1+x)^{z}+(1+x+x^{2})^{z})^{y}\cdot((1+x^{3})^{y}+(1+x^{2}+x^{4}% )^{y})^{z}

The key observation is that we can factor out x 2 − x + 1 superscript 𝑥 2 𝑥 1 x^{2}-x+1 from the second factor to prove the equality, but this is outside of the language of the high-school algebra axioms.