Theorem LT-9. McKenzie’s absorption basis for LT. The four equations (L1, L2, L3, L4) are a basis for lattice theory. It is clear that they are a part of lattice theory, and by duality, it is sufficient to derive the set

\{ \begin{matrix}x ∧ y = y ∧ x \\ (x ∧ y) ∧ z = x ∧ (y ∧ z) \\ x ∧ (x ∨ y) = x \end{matrix} \} .

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

1 x = x 2 B ∧ A = A ∧ B, (A ∧ B) ∧ C = A ∧ (B ∧ C),

A ∧ (A ∨ B) = A → □

4,3 x ∨ (y ∧ (x ∧ z)) = x 5 x ∧ (y ∨ (x ∨ z)) = x 7 ((x ∧ y) ∨ (y ∧ z)) ∨ y = y 9 ((x ∨ y) ∧ (y ∨ z)) ∧ y = y

11  x ∧ (y ∨ x) = x  [3 → 5]
13  x ∨ (y ∧ x) = x  [5 → 3]
15  (x ∧ (y ∧ z)) ∧ y = x ∧ (y ∧ z)  [3 → 11]
18,17  (x ∨ y) ∨ y = x ∨ y  [11 → 13]
19  (x ∨ (y ∨ z)) ∨ y = x ∨ (y ∨ z)  [5 → 13]
22,21  (x ∧ y) ∧ y = x ∧ y  [13 → 11]
28,27  (x ∧ y) ∨ y = y  [11 → 7 :18]
29  x ∨ x = x  [5 → 7 :28]
31  x ∧ x = x  [7 → 11]
34,33  x ∧ (x ∨ y) = x  [7 → 5]
37  B ∧ A = A ∧ B, (A ∧ B) ∧ C = A ∧ (B ∧ C) → □  [2 :34 :1]
41,40  x ∨ (x ∧ y) = x  [31 → 3]
42  x ∨ (y ∨ x) = y ∨ x  [11 → 27]
48  ((x ∧ y) ∨ (y ∧ z)) ∧ y = (x ∧ y) ∨ (y ∧ z)  [7 → 33]
56  (x ∧ ((y ∧ x) ∨ z)) ∧ (y ∧ x) = y ∧ x  [13 → 9]
60  (x ∨ y) ∧ y = y  [29 → 9 :22]
62  ((x ∨ (y ∧ z)) ∧ z) ∧ (y ∧ z) = y ∧ z  [27 → 9]
68  (x ∧ y) ∧ x = x ∧ y  [40 → 11]
70  (x ∧ ((x ∧ y) ∨ z)) ∧ (x ∧ y) = x ∧ y  [40 → 9]
75,74  x ∧ (y ∧ x) = y ∧ x  [13 → 60]
83,82  (x ∧ y) ∨ x = x  [40 → 42 :41]
84  (x ∧ (y ∧ z)) ∨ y = y  [3 → 42 :4]
120  (x ∨ y) ∨ (y ∧ z) = x ∨ y  [82 → 19 :83]
145,144  (x ∧ (y ∧ z)) ∧ z = x ∧ (y ∧ z)  [74 → 15 :75]
152  (x ∧ (y ∧ z)) ∨ z = z  [74 → 84]
158  ((x ∧ y) ∧ z) ∨ x = x  [68 → 84]
280  ((x ∧ y) ∧ z) ∨ y = y  [68 → 152]
298  (x ∧ y) ∨ (z ∨ x) = z ∨ x  [60 → 158]

950  (x ∧ y) ∧ ((z ∧ y) ∧ x) = (z ∧ y) ∧ x  [280 → 56]^{955,954  (x ∧ y) ∧ (y ∧ x) = y ∧ x  [82 → 56]}^{1234  ((x ∨ y) ∧ z) ∧ (y ∧ z) = y ∧ z  [120 → 62]}^{1620  (x ∧ (y ∨ z)) ∧ (z ∧ x) = z ∧ x  [298 → 56]}^{1766  (x ∧ y) ∧ (x ∧ (y ∧ z)) = x ∧ (y ∧ z)  [84 → 70]}^{2857,2856 (x ∧ (y ∧ z)) ∨ (z ∧ y) = z ∧ y  [954 → 84]}^{2860  x ∧ y = y ∧ x  [954 → 48 :2857,955,955,2857]}^{2901  x ∧ (y ∧ z) = x ∧ (z ∧ y)  [2860 → 15 :145]}^{2914  (A ∧ B) ∧ C = A ∧ (B ∧ C) → □  [2860 → 37 :1]}^{3316  (x ∧ y) ∧ z = z ∧ (y ∧ x)  [2860 → 2901]}^{3342  x ∧ (y ∧ z) = (z ∧ y) ∧ x  [flip 3316]}^{10469,10468 (x ∧ y) ∧ ((z ∨ y) ∧ x) = y ∧ x  [3342 → 1234]}^{10470  (x ∧ y) ∧ (y ∧ (z ∨ x)) = x ∧ y  [3316 → 1234]}^{13162,13161 (x ∧ y) ∧ (x ∧ (z ∨ y)) = y ∧ x  [3342 → 1620]}^{19054,19053 ((x ∧ y) ∧ z) ∧ (z ∧ x) = (x ∧ y) ∧ z  [40 → 10470]}^{19056,19055 ((x ∧ y) ∧ z) ∧ (z ∧ y) = (x ∧ y) ∧ z  [13 → 10470]}^{23311  (x ∧ (y ∨ z)) ∧ z = z ∧ x  [13161 → 950 :19054,13162]}^{23318,23317 ((x ∨ y) ∧ z) ∧ y = y ∧ z  [10468 → 950 :19056,10469]}^{23552  x ∧ ((y ∨ x) ∧ z) = x ∧ z  [68 → 23311 :23318, flip]}^{23932,23931 (x ∧ y) ∧ (x ∧ z) = (x ∧ y) ∧ z  [40 → 23552]}^{23934,23933 (x ∧ y) ∧ (y ∧ z) = (x ∧ y) ∧ z  [13 → 23552]}^{24033  (x ∧ y) ∧ z = x ∧ (y ∧ z)  [1766 :23932,23934]}^{24035  □  [24033,2914]}

2