Theorem MAJ-3. A majority schema for two absorption equations.

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

(⇒) is trivial by simplification. The proof of (⇐) follows.

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

1 x = x 2 p(A, A, B) = A, p(A, B, A) = A, p(B, A, A) = A,

f(A) = A, g(A) = A → □

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

5 p(x, p(p(y, x, x), p(p(y, p(x, z, f(x)), g(x)), u, f(p(y, p(x, z, f(x)), g(x)))), g(p(y, p(x, z, f(x)), g(x)))), v) =

p(y, p(x, z, f(x)), g(x))  [3 → 3]

7 p(p(x, p(y, z, z), p(y, z, z)), p(x, z, g(p(y, z, z))), u) = p(y, z, z)

[3 → 3]

12,11 p(p(x, y, y), p(x, p(z, p(y, u, f(y)), g(y)), g(y)), v) = y

[3 → 7 :4,4,4]

25 p(p(p(x, y, y), y, y), y, z) = y [3 → 11]

29 p(p(x, y, y), p(x, p(z, p(u, p(y, v, f(y)), g(y)), g(y)), g(y)), w) = y

[11 → 7 :12,12,12]

42,41 p(x, x, y) = x [25 → 25]

43 p(A, B, A) = A, p(B, A, A) = A, f(A) = A, g(A) = A → □

[2 :42 :1]

64  p(p(x, y, y), p(p(x, y, y), y, g(p(x, y, y))), z) = p(x, y, y)  [41 → 7]
68  p(x, p(x, p(y, p(x, z, f(x)), g(x)), g(x)), u) = x  [41 → 11]

82 p(p(x, p(y, z, f(y)), g(y)), p(y, p(p(p(x, y, y), p(p(x, p(y, z, f(y)), g(y)), u, f(p(x, p(y, z, f(y)), g(y)))), g(p(x, p(y, z, f(y)),

g(y)))), v, f(p(p(x, y, y), p(p(x, p(y, z, f(y)), g(y)), u,
f(p(x, p(y, z, f(y)), g(y)))), g(p(x, p(y, z, f(y)), g(y)))))),
g(p(p(x, y, y), p(p(x, p(y, z, f(y)), g(y)), u, f(p(x, p(y, z,
f(y)), g(y)))), g(p(x, p(y, z, f(y)), g(y)))))), w) =
p(p(x, y, y), p(p(x, p(y, z, f(y)), g(y)), u, f(p(x, p(y, z, f(y)),
g(y)))), g(p(x, p(y, z, f(y)), g(y))))  [3 → 5]
91,90  p(x, p(y, z, f(y)), g(y)) = y  [41 → 5 :4,42, flip]
95,94  p(x, p(y, x, g(x)), z) = p(y, x, g(x))  [41 → 5 :42,42,91,42]
103,102 p(x, p(x, y, f(x)), z) = p(x, y, f(x))  [41 → 5 :42,42,91,42]

107,106 p(x, y, f(x)) = x

[82 :91,91,91,91,91,91,91,91,91,91,91,91,91,103,103,91,91,91,91]

115,114 p(x, y, g(y)) = y  [68 :107,95,95]
117,116 p(p(x, y, y), y, z) = y  [29 :107,115,115,115]
121,120 p(x, y, y) = y  [64 :117,117, flip]

122  p(A, B, A) = A, f(A) = A, g(A) = A → □  [43 :121 :1]^{124,123 f(x) = x  [120 → 106]}^{125  p(A, B, A) = A, g(A) = A → □  [122 :124 :1]}^{127,126 p(x, y, x) = x  [106 :124]}^{128  g(A) = A → □  [125 :127 :1]}^{129  g(x) = x  [114 → 126, flip]}^{131  □  [129,128]}

2