Theorem WAL-1. A relationship between WAL and LT.

{WAL, x ∧ (y ∨ (x ∨ z)) = x} ⇒ {LT}.

It is sufficient to derive the associative laws for ∧ and ∨.

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

1 x = x 2 (A ∧ B) ∧ C = A ∧ (B ∧ C), (A ∨ B) ∨ C = A ∨ (B ∨ C) → □ 3 x ∧ x = x 5 x ∧ y = y ∧ x 6 ((x ∨ y) ∧ (z ∨ y)) ∧ y = y 8 x ∨ x = x 10 x ∨ y = y ∨ x 11 ((x ∧ y) ∨ (z ∧ y)) ∨ y = y 13 x ∧ (y ∨ (x ∨ z)) = x

15  x ∧ (y ∨ (z ∨ x)) = x  [10 → 13]
17  x ∧ (y ∨ x) = x  [8 → 13]
19  x ∧ ((x ∨ y) ∨ z) = x  [10 → 13]
21  x ∧ (x ∨ y) = x  [8 → 13]
31  (x ∨ y) ∧ y = y  [3 → 6]
33  x ∧ ((y ∨ x) ∧ (z ∨ x)) = x  [5 → 6]
35  (x ∨ y) ∧ x = x  [5 → 21]
39  (x ∨ (y ∧ (x ∨ z))) ∨ (x ∨ z) = x ∨ z  [21 → 11]
49  ((x ∧ (y ∨ z)) ∨ z) ∨ (y ∨ z) = y ∨ z  [17 → 11]
53  (x ∧ y) ∨ y = y  [8 → 11]
65  x ∨ (y ∨ (x ∨ z)) = y ∨ (x ∨ z)  [13 → 53]
67  (x ∧ y) ∨ x = x  [5 → 53]
70,69  x ∨ (y ∧ x) = x  [10 → 53]
71  (x ∧ y) ∧ (z ∨ y) = x ∧ y  [53 → 13]
73  x ∧ (y ∧ x) = y ∧ x  [53 → 35]
80,79  x ∨ (x ∧ y) = x  [10 → 67]
85  (x ∧ y) ∧ x = x ∧ y  [67 → 21]
93  ((x ∨ (y ∧ z)) ∧ z) ∧ (y ∧ z) = y ∧ z  [69 → 6]
110,109 x ∨ (y ∨ (z ∨ x)) = y ∨ (z ∨ x)  [15 → 53]
111  (x ∧ y) ∧ (x ∨ z) = x ∧ y  [67 → 19]
153  (x ∧ y) ∧ (x ∧ (z ∨ (x ∧ y))) = x ∧ y  [79 → 33]
157  (x ∧ y) ∧ ((z ∨ (x ∧ y)) ∧ x) = x ∧ y  [79 → 33]
195  (x ∨ y) ∨ (x ∨ (z ∨ y)) = x ∨ (z ∨ y)  [15 → 39]
197  (x ∨ y) ∨ (x ∨ (y ∨ z)) = x ∨ (y ∨ z)  [13 → 39]
231  (x ∨ y) ∨ (z ∧ y) = x ∨ y  [71 → 69]
434,433 ((x ∧ y) ∨ z) ∨ (x ∨ z) = x ∨ z  [111 → 49]
539  x ∨ (y ∧ (x ∧ z)) = x  [79 → 231 :80]
541  x ∨ (y ∧ (z ∧ x)) = x  [69 → 231 :70]
629  x ∨ ((y ∧ x) ∧ z) = x  [85 → 541]
727  x ∨ (y ∨ z) = x ∨ (z ∨ y)  [10 → 65 :110]

1036  (x ∧ y) ∧ ((z ∧ x) ∧ y) = (z ∧ x) ∧ y  [629 → 93]
1421  (x ∨ y) ∨ z = z ∨ (y ∨ x)  [10 → 727]
1423  x ∨ (y ∨ z) = (z ∨ y) ∨ x  [flip 1421]
2968,2967 (x ∧ y) ∧ (x ∧ (z ∨ y)) = x ∧ y  [231 → 153]
3194,3193 (x ∧ (y ∧ z)) ∧ (z ∧ x) = x ∧ (y ∧ z)  [541 → 157]
3196,3195 (x ∧ (y ∧ z)) ∧ (y ∧ x) = x ∧ (y ∧ z)  [539 → 157]
3200,3199 (x ∧ y) ∧ ((z ∨ y) ∧ x) = x ∧ y  [231 → 157]
4876,4875 ((x ∨ y) ∨ z) ∨ (z ∨ y) = z ∨ (x ∨ y)  [1423 → 195]
5085 x ∨ ((x ∧ y) ∨ z) = x ∨ z [433 → 197 :4876,434]
5196,5195 (x ∨ y) ∨ (x ∨ z) = (x ∨ y) ∨ z  [35 → 5085]
5198,5197 (x ∨ y) ∨ (y ∨ z) = (x ∨ y) ∨ z  [31 → 5085]
5282,5281 (x ∨ y) ∨ z = x ∨ (y ∨ z)  [197 :5196,5198]
5737  (A ∧ B) ∧ C = A ∧ (B ∧ C) → □  [2 :5282 :1]
5741  C ∧ (A ∧ B) = A ∧ (B ∧ C) → □  [5 → 5737]
8492  x ∧ ((y ∨ x) ∧ z) = z ∧ x  [3199 → 1036 :3194,3200]
8495,8494 x ∧ (y ∧ (z ∨ x)) = y ∧ x  [2967 → 1036 :3196,2968]
8573  (x ∧ y) ∧ (y ∧ z) = z ∧ (x ∧ y)  [69 → 8492]
8580  (x ∧ (y ∨ z)) ∧ z = x ∧ z  [73 → 8492 :8495, flip]
8607  x ∧ (y ∧ z) = (y ∧ z) ∧ (z ∧ x)  [flip 8573]
8842,8841 (x ∧ y) ∧ (y ∧ z) = x ∧ (y ∧ z)  [79 → 8580]
8853  x ∧ (y ∧ z) = y ∧ (z ∧ x)  [8607 :8842]
8854  □  [8853,5741]