Lemma LT-11. Another absorption basis for LT.

\{ \begin{matrix}(x ∧ y) ∨ (x ∧ (x ∨ y)) = x \\ (x ∧ x) ∨ (y ∧ (x ∨ x)) = x \\ (x ∧ y) ∨ (y ∧ (x ∨ y)) = y \\ ((x ∧ y) ∨ (y ∧ z)) ∨ y = y (L3) \\ ((x ∨ (y ∨ z)) ∧ (u ∨ y)) ∧ y = y \end{matrix} \} ⇒

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

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

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

13  ((x ∧ y) ∧ (x ∧ (x ∨ y))) ∨ ((x ∧ y) ∧ x) = x ∧ y  [3 → 3]
26,25 x ∨ x = x  [7 → 9]
31 (x ∧ x) ∨ (y ∧ x) = x [5 :26]
42,41 x ∧ x = x  [25 → 7 :26]
43  x ∨ (y ∧ x) = x  [31 :42]
57  ((x ∨ y) ∧ (z ∨ x)) ∧ x = x  [25 → 11]
59  ((x ∨ (y ∨ z)) ∧ y) ∧ y = y  [25 → 11]
67  (x ∨ (x ∧ y)) ∨ x = x  [11 → 9]
77  (x ∧ y) ∨ y = y  [43 → 9]
80,79 (x ∧ y) ∧ y = x ∧ y  [77 → 3 :26]
82,81 (x ∨ (y ∨ z)) ∧ y = y  [59 :80]
105 (x ∨ (x ∧ y)) ∧ x = x ∨ (x ∧ y) [67 → 3 :26]
122,121 (x ∨ y) ∧ x = x  [77 → 81]
123 x ∨ (x ∧ y) = x [105 :122, flip]

127 (x ∧ ((y ∨ (x ∨ z)) ∧ ((y ∨ (x ∨ z)) ∨ x))) ∨ (x ∧ (y ∨ (x ∨ z))) = x

[81 → 13 :82,82]

169 (x ∨ y) ∨ x = x ∨ y [121 → 123]
174,173 (x ∨ (y ∨ z)) ∨ y = x ∨ (y ∨ z)  [81 → 123]
188,187 x ∧ (y ∨ (x ∨ z)) = x  [127 :174,42,26]
199  ((B ∨ A) ∧ (B ∨ C)) ∧ B = B → □  [2 :188 :1]
414  ((x ∨ y) ∧ (x ∨ z)) ∧ x = x  [169 → 57]
416  □  [414,199]