Theorem MAJ-2. A majority polynomial reduction schema.

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

(⇒) is trivial by simplification. The proof of (⇐) follows. Proof (found by Otter 3.0.4 on gyro at 0.09 seconds). 1 x = x 2 p(A, A, B) = A, p(A, B, A) = A, p(B, A, A) = A,

f(A) = A → □

3 p(p(x, y, y), z, p(p(x, y, y), f(y), u)) = y

8,7  p(p(x, y, y), z, y) = y  [3 → 3]
10,9  p(x, y, x) = x  [7 → 7]
11  p(x, y, p(p(z, x, x), f(x), u)) = p(p(z, x, x), f(x), u)  [3 → 7]
13  p(A, A, B) = A, p(B, A, A) = A, f(A) = A → □  [2 :10 :1]
15,14  p(x, y, p(x, f(x), z)) = x  [7 → 3 :8]
17,16  p(x, y, y) = y  [9 → 3 :10]
18  p(A, A, B) = A, f(A) = A → □  [13 :17 :1]
19  p(x, f(x), y) = x  [11 :17,15,17, flip]
22,21  f(x) = x  [16 → 19]
24,23  p(x, x, y) = x  [19 :22]
25  □  [18 :24,22 :1,1]