Theorem DUAL-BA-8. A self-dual 3-basis for BA (majority reduction).

\{ \begin{matrix}(SD-dist) \\ y + (x · (y · z)) = y \\ ((x · y) + (y · z)) + y = y \\ (x + x′) · y = y \\ y · (x + (y + z)) = y \\ ((x + y) · (y + z)) · y = y \\ (x · x′) + y = y \\ x + x′ = 1 \\ x · x′ = 0 \\ (x + y) + z = x + (y + z) \\ (x · y) · z = x · (y · z) \end{matrix} \} ⇒ \{ \begin{matrix}(x · y) + (x · z) = x · (y + z) \\ (x · y) + y = y \end{matrix} \} .

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

1 x = x 2 (A · B) + (A · C) = A · (B + C), (A · B) + B = B → □ 3 (x · y) + ((y · z) + (z · x)) = (x + y) · ((y + z) · (z + x)) 5 x + (y · (x · z)) = x 7 ((x · y) + (y · z)) + y = y 9 (x + x′) · y = y 11 x · (y + (x + z)) = x 15 (x · x′) + y = y 18,17 x + x′ = 1 20,19 x · x′ = 0 22,21 (x + y) + z = x + (y + z) 24,23 (x · y) · z = x · (y · z)

26,25  1 · x = x  [9 :18]
28,27  0 + x = x  [15 :20]
29  (x · y) + ((y · z) + y) = y  [7 :22]
35  (x · 1) + (y + (y · x)) = (x + 1) · ((1 + y) · (y + x))  [25 → 3]
39  0′ = 1  [27 → 17]
41  1 + (x · y) = 1  [25 → 5]
44,43  x + (x · y) = x  [25 → 5]
45  x · (0 · y) = 0  [27 → 5]
47  (x · 1) + y = (x + 1) · ((1 + y) · (y + x))  [35 :44]
49  0 · 1 = 0  [39 → 19]
51  1′ = 0  [25 → 19]
57  (x · y) + (y′ · x) = (x + y) · (y′ + x)  [19 → 3 :28,18,26]
58  (x′ · y) + (y · x) = (x′ + y) · (y + x)  [19 → 3 :28,18,26]
60  (x + y) · (y′ + x) = (x · y) + (y′ · x)  [flip 57]
61  1 + 0 = 1  [51 → 17]
67  (1 + x) · (x + 0) = x  [49 → 3 :26,44,28,28,26, flip]
70,69  x + 1 = 1  [61 → 11 :26]
74,73  x · 1 = x  [17 → 11 :70]

75  x · (y + x) = x  [5 → 11]
80,79  x · (x + y) = x  [27 → 11]
86  x + y = (1 + y) · (y + x)  [47 :74,70,26]
93  x + (y · x) = x  [11 → 5]
96,95  1 + x = 1  [73 → 41]
99  x + y = y + x  [86 :96,26]
101,100 x + 0 = x  [67 :96,26]
106 x + ((y · (x · z)) + u) = x + u [5 → 21, flip]
117,116 x + x = x  [73 → 43]
119,118 0 · x = 0  [27 → 43]
123,122 x · 0 = 0  [45 :119]
125,124 x + ((x · y) + z) = x + z  [43 → 21, flip]
134  x · y = y · x  [118 → 3 :123,28,28,101,28,80]
137  x · (x′ · y) = 0  [19 → 23 :119, flip]
152,151 x · x = x  [116 → 75]
160,159 x · ((y + x) · z) = x · z  [75 → 23, flip]
161 (x · y) + ((y · x) + x) = (x + y) · ((y + x) · x) [151 → 3 :117]
164,163 (x · y) + y = (x + y) · y  [151 → 3 :44,117,80]
165  x · (x · y) = x · y  [151 → 23, flip]
169  (x · y) + ((y + x) · x) = (x + y) · ((y + x) · x)  [161 :164]
171  (A · B) + (A · C) = A · (B + C), (A + B) · B = B → □ [2 :164]
174 x · (y · ((y + z) · (z + x))) = x · y [3 → 79 :24,160]
181,180 x · ((x + y) · z) = x · z  [79 → 23, flip]
183,182 x · (y · (z + x)) = x · y  [174 :181]
185,184 (x · y) + x = x  [118 → 29 :28]
187,186 x + (y + x) = y + x  [75 → 29 :185]
193,192 (x + y) · y = y  [151 → 29 :117,164]
196  (A · B) + (A · C) = A · (B + C) → □  [171 :193 :1]
197  (x + y) · x = x  [169 :193,185,193, flip]
200,199 (x · y) + y = y  [163 :193]
204  x + (y + (z · (x + y))) = x + y  [21 → 93]
206  x + ((y · x) + z) = x + z  [93 → 21, flip]
208  x + (y + z) = z + (x + y)  [21 → 99]
210,209 x′ + x = 1  [17 → 99, flip]
211  (x · (y · z)) + y = y  [5 → 99, flip]
214  x + (y + z) = y + (z + x)  [flip 208]
221  x · (y · z) = z · (x · y)  [23 → 134]
224  (x + (y + z)) · y = y  [11 → 134, flip]
227  (x · y) + ((y · z) + (x · z)) = (x + y) · ((y + z) · (z + x)) [134 → 3]
239  x′′ + x = x′′ · x  [19 → 57 :28,18,26, flip]
243  (x · y) + (x · y′) = (x + y) · (y′ + x)  [134 → 57]
246  ((x + y′) · y) + y′ = x + y′  [75 → 57 :22,210,70,187,26]
249  (x + y) · (y′ + x) = (x · y) + (x · y′)  [flip 243]
281,280 x + (y · (z + x)) = (z + x) · (x + y)  [192 → 3 :125,22,117,183]
287,286 x + ((x + y) · (y + z)) = x + y  [204 :281]

322  (x · y) + (y′ · x) = (y′ + x) · (x + y)  [99 → 58]
338  x · (y · x′) = 0  [134 → 137]
340  x′ · (y · x) = 0  [134 → 137 :24]
376,375 (x · y) + (y′ · x) = (x + y) · (x + y′)  [99 → 60, flip]
386  (x + y) · (x + y′) = (y′ + x) · (x + y)  [322 :376]
388  (x + y) · (x + y′) = (x + y) · (y′ + x)  [57 :376]
491  (x′ + (y · x)) · x = y · x  [340 → 58 :24,152,28,200, flip]

734 (x · y) + ((x · (y · z)) + (z · x)) = x · ((x · y) + z)

[165 → 3 :24,44,183]
812,811 (x + y) · (z · (y · u)) = z · (y · u)  [211 → 224]
824,823 (x + y) · (z · (x · u)) = z · (x · u)  [106 → 224]
828,827 (x + y) · (z · x) = z · x  [3 → 224 :24,24,824,812]
1108,1107 (x · y) + ((x · (y · z)) + u) = (x · y) + u  [23 → 124]
1124,1123 x′ + (y · x) = x′ + y  [58 → 124 :287, flip]
1130,1129 (x · y) + (z · x) = x · ((x · y) + z)  [734 :1108]
1133  (x′ + y) · x = y · x  [491 :1124]
1139  x · ((x · y) + y′) = (x + y) · (x + y′)  [375 :1130]
1796,1795 (x + y′) · y = x · y  [99 → 1133]
1798,1797 x′′ · x = x  [17 → 1133 :26, flip]
1806,1805 (x · y) + y′ = x + y′  [246 :1796]
1808,1807 x′′ + x = x  [239 :1798]
1810,1809 (x + y) · (x + y′) = x  [1139 :1806,80, flip]
1812,1811 (x + y) · (y′ + x) = x  [388 :1810, flip]
1813  (x′ + y) · (y + x) = y  [386 :1810, flip]
1819  (x · y) + (x · y′) = x  [249 :1812, flip]
1973  x′′ = x  [1797 → 43 :1808, flip]
1976,1975 (x + y) · x′ = y · x′  [1973 → 1133]
2749 (x′ + y) · (x + y) = y [99 → 1813]
2879,2878 x + (y · x′) = x + y  [197 → 1819 :1976]
3083  A · ((A · B) + C) = A · (B + C) → □  [134 → 196 :1130]
4371  (x′ + y) · (x + ((z · x′) + y)) = (z · x′) + y  [206 → 2749]
4412,4411 x + (y · (z · x′)) = x + (y · z)  [23 → 2878]
4429,4428 x + ((y · x′) + z) = x + (y + z)  [2878 → 21 :22, flip]
4432,4431 (x · y′) + z = (y′ + z) · (y + (x + z))  [4371 :4429, flip]
4617,4616 (x + y) · (z · (x + (y + u))) = (x + y) · z  [214 → 182]
4739,4738 (x + y) · (z · (y′ + x)) = z · x  [1813 → 221, flip]
4862,4861 (x · y) + (x · z) = x · ((x · y) + z)  [165 → 227 :24,1108,44,183]

4885 x · ((x · y) + (z · y′)) = (y + z) · x

[338 → 227 :28,4862,2879,4432,4617,4739]

4908,4907 x · ((x · y) + z) = (y + (x · z)) · x  [165 → 227 :200,4862,185,828]
4968,4967 (x + (y · z)) · y = (x + z) · y  [4885 :4908,4412]
4971  (B + C) · A = A · (B + C) → □  [3083 :4908,4968]
4972  □  [4971,134]