Theorem RBA-2. A Robbins algebra with an idempotent element is Boolean.

\{ \begin{matrix}x + y = y + x \\ (x + y) + z = x + (y + z) \\ n(n(x + y) + n(x + n(y))) = x \\ ∃c (c + c = c) \end{matrix} \} ⇒ \{n(x + n(y)) + n(n(x) + n(y)) = y\}.

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

1 x = x 2 x + y = y + x 4,3 (x + y) + z = x + (y + z) 6,5 n(n(x + y) + n(x + n(y))) = x 7 c + c = c 9 n(A + n(B)) + n(n(A) + n(B)) ≠ B

10  c + (c + x) = c + x  [7 → 3, flip]
13  x + (y + z) = y + (z + x)  [2 → 3]
14  x + (y + z) = z + (x + y)  [flip 13]
16,15  c + (x + c) = c + x  [2 → 10]
25  n(n(c) + n(c + n(c))) = c  [7 → 5]
27  n(n(x + (y + z)) + n(x + (y + n(z)))) = x + y  [3 → 5 :4]
29  n(n(x + y) + n(y + n(x))) = y  [2 → 5]
33  n(n(x + (n(y + z) + n(y + n(z)))) + n(x + y)) = x  [5 → 5]
35  n(n(x + y) + n(n(y) + x)) = x  [2 → 5]
39  n(n(x + n(y)) + n(x + y)) = x  [2 → 5]
49  x + (y + z) = z + (y + x)  [2 → 13]
63  n(n(c + n(c)) + n(c)) = c  [2 → 25]
65  n(n(n(c) + (c + n(c))) + c) = n(c)  [25 → 5]
73  n(n(A) + n(B)) + n(A + n(B)) ≠ B  [2 → 9]
98  n(n(x + (n(c + n(c)) + n(c))) + n(x + c)) = x  [63 → 5]
117  n(n(x + (y + z)) + n(y + (x + n(z)))) = y + x  [49 → 29 :4]
147  n(n(x + y) + n(n(x) + y)) = y  [2 → 29]
159  n(n(x + n(y)) + n(y + x)) = x  [2 → 29]
227  n(n(n(x) + y) + n(y + x)) = y  [2 → 35]
289  n(c + n(n(c) + (c + n(c)))) = n(c)  [25 → 39]
303  n(n(x + n(y + z)) + n(z + (x + y))) = x  [14 → 39]
381  n(n(n(x) + y) + n(x + y)) = y  [2 → 147]
459  n(n(c + (x + n(c))) + n(c + x)) = c + x  [10 → 159 :4]
646,645 n(n(c) + n(n(c) + (c + n(c)))) = c  [65 → 381 :4,4,16]
652,651 n(n(c) + (c + n(c))) = n(c + n(c))  [65 → 227 :646, flip]
681 n(c + n(c + n(c))) = n(c) [289 :652]
1451,1450 n(n(c + (n(c + n(c)) + n(c))) + n(c)) = c  [7 → 98]
1583,1582 n(n(x + c) + n(n(c + n(c)) + (x + n(c)))) = x  [25 → 303]
1644  c + n(c + n(c)) = c  [681 → 459 :1451, flip]
1646  n(c + n(c)) + c = c  [2 → 1644]
1719,1718 n(c + n(c)) + x = x  [1646 → 117 :1583, flip]

1725,1724 x + n(c + n(c)) = x  [1646 → 27 :1719,6, flip]^{1770  n(x + n(x)) = n(c + n(c))  [1718 → 33 :6,1719]}^{1957,1956 n(n(n(n(x)) + x)) = n(n(x))  [1770 → 227 :1719]}^{1959,1958 n(n(x)) = x  [1770 → 227 :1725,1957]}^{2091,2090 n(n(x) + y) + n(x + y) = n(y)  [381 → 1958, flip]}^{2177  B ≠ B  [73 :2091,1959]}^{2178  □  [2177,1]}

2