Theorem PIX-2. A reduction schema for Pixley polynomials.

\{p(p(x, x, y), p(f(z), u, z), z) = y\} ⇔ \{ \begin{matrix}p(x, x, y) = y \\ p(x, y, y) = x \\ p(x, y, x) = x \\ f(x) = x \end{matrix} \} .

The proof of (⇐) is obvious. The proof of (⇒) follows.

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

1 x = x 2 p(A, A, B) = B, p(A, B, B) = A, p(A, B, A) = A, f(A) = A → □ 3 p(p(x, x, y), p(f(z), u, z), z) = y

6,5 p(x, p(f(y), z, y), y) = x  [3 → 3]
8,7 p(x, x, y) = y  [3 :6]
9 p(A, B, B) = A, p(A, B, A) = A, f(A) = A → □ [2 :8 :1]
11,10 p(x, y, y) = x  [7 → 5]
12  p(x, f(y), y) = x  [5 → 5]
14  p(f(x), y, x) = x  [7 → 5, flip]
16  p(A, B, A) = A, f(A) = A → □  [9 :11 :1]
18,17 f(x) = x  [7 → 12, flip]
19  p(A, B, A) = A → □  [16 :18 :1]
20  p(x, y, x) = x  [14 :18]
22  □  [20,19]