Theorem DUAL-BA-5. A self-dual 2-basis for BA (majority reduction).

\{ \begin{matrix}y + (x · (y · z)) = y & (L1), & y · (x + (y + z)) = y & (L2) \\ ((x · y) + (y · z)) + y = y & (L3), & ((x + y) · (y + z)) · y = y & (L4) \\ (x + y) · (x + y′) = x & (B1), & (x · y) + (x · y′) = x & (B2) \end{matrix} \} .

Since we already have a basis for lattice theory, we may include associativity and commutativity of the two operations. We derive half of Padmanabhan’s 6-basis; the other half follows by duality.

(Our first proof, which was found with the standard strategy with max_weight=23, is 119 steps and was found in 80 seconds. While experimenting with the prototype program “eqp”, we stumbled across an 18-step proof of distributivity, and we used that proof to guide Otter with the hints strategy [?] to the following short proof.)

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

19 x = x 20 (A · B) + (A · C) = A · (B + C), (A + B) · B = B,

B + B′ = A + A′ → □

21 x + (y · (x · z)) = x 25 (x + y) · (x + y′) = x 27 x · (y + (x + z)) = x 31 (x · y) + (x · y′) = x 33 x + y = y + x 34 x · y = y · x 35 (x + y) + z = x + (y + z) 38,37 (x · y) · z = x · (y · z)

51  x · (y + x) = x  [21 → 27]
57  x + (y · x) = x  [27 → 21]
64,63  (x + y) · y = y  [34 → 51]

65 (A · B) + (A · C) = A · (B + C), B + B′ = A + A′ → □

[20 :64 :19]

104  (x · y) + (y · x′) = y  [34 → 31]
155  x + ((y · x) + z) = x + z  [57 → 35, flip]
238  (x + y) · ((x + y′) · z) = x · z  [25 → 37, flip]
247  x · (y · z) = y · (z · x)  [34 → 37]
252  x · (y · z) = z · (x · y)  [flip 247]
257  (x · (y · z)) + (x · (y · z′)) = x · y  [37 → 31 :38]
305  (x + y) · (z · y) = z · y  [51 → 252, flip]
362,361 (x · y) + (z · (x · y′)) = (x · y) + (z · x)  [257 → 155, flip]
408,407 (x + y) · (z · y′) = x · (z · y′)  [305 → 238]
409 (x · y) + (z · x) = (z + y) · x [305 → 257 :408,362]
533,532 (x · y) + (y · z) = (x + z) · y  [33 → 409]
554,553 (x + x′) · y = y  [104 :533]
655  x + x′ = y + y′  [553 → 31 :554]
768  □  [34 → 65 :533 :34,655]