Lemma WAL-3. An absorption basis for WAL.

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

Because the two additional equations are commuted variants of (W3) and (W3′) (p. ??), it is sufficient to derive commutativity and idempotence of the two operations.

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

1 x = x 2 A ∧ A = A, B ∧ A = A ∧ B, A ∨ A = A, B ∨ A = A ∨ 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) ∧ (z ∨ x)) ∧ x = x 11 ((x ∧ y) ∨ (z ∧ x)) ∨ x = x

13  (x ∧ (y ∨ (z ∧ x))) ∧ (z ∧ x) = z ∧ x  [7 → 9]
15  (x ∧ (y ∨ (x ∧ z))) ∧ (x ∧ z) = x ∧ z  [3 → 9]
20,19  x ∨ (x ∧ (((x ∨ y) ∧ (z ∨ x)) ∨ x)) = x  [9 → 7]
23  ((x ∧ y) ∨ x) ∨ x = x  [9 → 11]
26,25  ((x ∨ y) ∧ x) ∧ x = x  [11 → 9]
29  (((x ∧ y) ∨ x) ∧ x) ∨ (x ∧ x) = x  [23 → 7]
33  (x ∧ (y ∧ x)) ∧ (y ∧ x) = y ∧ x  [7 → 25]
44,43  (x ∧ x) ∧ x = x  [25 → 33 :26,26]
46,45  (x ∧ (y ∨ x)) ∧ x = x  [25 → 13 :26,26]
47  (x ∧ x) ∧ (x ∧ x) = x ∧ x  [29 → 13]
62,61  x ∧ (x ∧ (y ∨ x)) = x ∧ (y ∨ x)  [7 → 45 :46]
63  x ∨ (x ∧ ((x ∧ (y ∨ x)) ∨ x)) = x  [45 → 7]
69  ((x ∧ x) ∨ (x ∧ x)) ∨ (x ∧ x) = x ∧ x  [47 → 23]
73  ((x ∧ x) ∧ (y ∨ x)) ∧ x = x  [43 → 15 :44,44]
88,87  x ∧ x = x  [23 → 73 :44]
94,93  (x ∨ x) ∨ x = x  [69 :88,88,88,88]
105  x ∨ (y ∧ (x ∨ x)) = x  [5 :88]
107  B ∧ A = A ∧ B, A ∨ A = A, B ∨ A = A ∨ B → □  [2 :88 :1]
113,112 x ∨ x = x  [87 → 19 :94,88]
114  B ∧ A = A ∧ B, B ∨ A = A ∨ B → □  [107 :113 :1]
115  x ∨ (y ∧ x) = x  [105 :113]
118,117 (x ∧ (((x ∨ y) ∧ (z ∨ x)) ∨ x)) ∨ x = x  [19 → 3 :62,88]
122,121 x ∧ (y ∧ x) = y ∧ x  [115 → 13 :88]
127 (x ∧ y) ∨ y = y [115 → 3 :122,88]
130,129 (x ∧ y) ∧ y = x ∧ y  [127 → 3 :113]
133  (x ∨ y) ∧ x = x  [25 :130]

135  x ∧ (((x ∨ y) ∧ (z ∨ x)) ∨ x) = x  [19 → 63 :46,20,46,118, flip]
140,139 x ∧ ((x ∧ y) ∨ x) = (x ∧ y) ∨ x  [23 → 133]
141  x ∨ ((x ∧ (y ∨ x)) ∨ x) = x  [63 :140]
143  (x ∨ (x ∨ y)) ∨ (x ∨ y) = x ∨ y  [133 → 23]
151  ((x ∧ y) ∨ (z ∧ y)) ∨ y = y  [121 → 11]
171  (x ∧ (y ∨ x)) ∨ x = x  [141 → 135 :140]
178,177 x ∧ (y ∨ x) = x  [171 → 3 :46,46,113, flip]
179 (x ∧ y) ∨ x = x [139 :178, flip]
188,187 (x ∨ y) ∨ y = x ∨ y  [177 → 115]
193  (x ∨ (y ∧ (z ∨ x))) ∨ (z ∨ x) = z ∨ x  [177 → 151]
197  x ∨ (x ∨ y) = x ∨ y  [143 :188]
199  (x ∧ y) ∧ x = x ∧ y  [179 → 3 :113]
211  x ∧ (x ∨ y) = x  [197 → 3 :113]
215  (x ∨ y) ∨ x = x ∨ y  [211 → 115]
235  x ∨ (x ∧ y) = x  [199 → 115]
242,241 (x ∧ y) ∧ (y ∧ x) = y ∧ x  [235 → 13]
285 x ∧ y = y ∧ x [241 → 199 :242,242]
287,286 (x ∨ y) ∨ (y ∨ x) = y ∨ x  [211 → 193]
348  x ∨ y = y ∨ x  [286 → 215 :287,287]
351  □  [114,285,348]