Theorem LT-10. An absorption 3-basis for LT.

\{ \begin{matrix}y ∧ (x ∨ (y ∨ z)) = y & (L2) \\ ((x ∧ y) ∨ (y ∧ z)) ∨ y = y & (L3) \\ ((y ∨ x) ∧ (y ∨ z)) ∧ y = y & (L4′) \end{matrix} \} .

It is sufficient to prove (L1) and (L4) of the McKenzie basis.

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

1 x = x 2 B ∨ (A ∧ (B ∧ C)) = B, ((A ∨ B) ∧ (B ∨ C)) ∧ B = B → □ 3 x ∧ (y ∨ (x ∨ z)) = x 5 ((x ∧ y) ∨ (y ∧ z)) ∨ y = y 7 ((x ∨ y) ∧ (x ∨ z)) ∧ x = x

11  ((x ∧ y) ∨ y) ∨ y = y  [3 → 5]
14,13  x ∧ (x ∨ y) = x  [5 → 3]
37  (x ∨ y) ∧ x = x  [3 → 7]
41  (x ∨ x) ∨ x = x  [7 → 11]
43  (x ∨ (x ∧ y)) ∨ x = x  [7 → 5]
59  x ∧ ((y ∧ x) ∨ x) = (y ∧ x) ∨ x  [11 → 37]
70,69  x ∨ x = x  [41 → 37 :14, flip]
76,75  x ∧ (y ∨ x) = x  [41 → 3 :70,70]
77  (x ∧ y) ∨ y = y  [59 :76, flip]
91  x ∨ (y ∨ x) = y ∨ x  [75 → 77]
99  x ∧ (y ∧ x) = y ∧ x  [77 → 37]
109  (x ∧ y) ∧ (z ∨ y) = x ∧ y  [77 → 3]
116,115 x ∨ (x ∧ y) = x  [43 → 37 :14, flip]
146,145 ((x ∨ y) ∧ (y ∨ z)) ∧ y = y  [91 → 7]
153  B ∨ (A ∧ (B ∧ C)) = B → □  [2 :146 :1]
202  x ∨ (y ∧ x) = x  [99 → 115]
474  (x ∨ y) ∨ (z ∧ y) = x ∨ y  [109 → 202]
1504  x ∨ (y ∧ (x ∧ z)) = x  [115 → 474 :116]
1506  □  [1504,153]