Theorem QLT-4. Bowden’s inequality gives distributivity in QLT. The inequality x ∨ (y ∧ z) ≥ (x ∨ y) ∧ z is written as the following equation.

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

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

3,2 x ∧ x = x 4 x ∧ y = y ∧ x 6,5 (x ∧ y) ∧ z = x ∧ (y ∧ z) 8,7 x ∨ x = x 9 x ∨ y = y ∨ x 11,10 (x ∨ y) ∨ z = x ∨ (y ∨ z) 12 (x ∧ (y ∨ z)) ∨ (x ∧ y) = x ∧ (y ∨ z) 14 (x ∨ (y ∧ z)) ∧ (x ∨ y) = x ∨ (y ∧ z) 16 (x ∨ (y ∧ z)) ∨ ((x ∨ y) ∧ z) = x ∨ (y ∧ z)

17  x ∨ ((y ∧ z) ∨ ((x ∨ y) ∧ z)) = x ∨ (y ∧ z)  [copy,16 :11]

21 A ∨ (B ∧ C) ≠ (A ∨ B) ∧ (A ∨ C)

23  x ∧ (x ∧ y) = x ∧ y  [2 → 5, flip]
25  x ∧ (y ∧ z) = y ∧ (z ∧ x)  [4 → 5]
28  x ∧ (y ∧ z) = z ∧ (x ∧ y)  [flip 25]
29  x ∨ (y ∨ z) = y ∨ (x ∨ z)  [9 → 10 :11]
30  x ∨ (x ∨ y) = x ∨ y  [7 → 10, flip]
32  x ∨ (y ∨ z) = y ∨ (z ∨ x)  [9 → 10]
39,38  x ∧ (y ∧ x) = x ∧ y  [4 → 23]
43,42  x ∨ (y ∨ x) = x ∨ y  [9 → 30]
46  x ∧ (y ∧ (x ∧ z)) = x ∧ (y ∧ z)  [38 → 5 :6,6, flip]
48  x ∨ (y ∨ (z ∨ x)) = x ∨ (y ∨ z)  [10 → 42]
52  (x ∧ (y ∨ z)) ∨ (x ∧ z) = x ∧ (z ∨ y)  [9 → 12]
54  ((x ∨ y) ∧ z) ∨ (z ∧ x) = z ∧ (x ∨ y)  [4 → 12]
56  x ∨ (y ∨ ((x ∨ y) ∧ x)) = x ∨ y  [2 → 12 :11,3]
60  (x ∧ ((x ∧ y) ∨ z)) ∨ (x ∧ y) = x ∧ ((x ∧ y) ∨ z)  [23 → 12]
63,62  (x ∧ (y ∨ z)) ∨ (y ∧ x) = x ∧ (y ∨ z)  [4 → 12]
68  (x ∧ (y ∨ z)) ∨ ((x ∧ y) ∨ u) = (x ∧ (y ∨ z)) ∨ u  [12 → 10, flip]
125  x ∨ (y ∨ z) = z ∨ (y ∨ x)  [9 → 32]
160,159 x ∨ (y ∨ ((x ∨ y) ∧ y)) = x ∨ y  [2 → 17 :3]
161  x ∨ ((y ∧ z) ∨ ((y ∨ x) ∧ z)) = x ∨ (y ∧ z)  [9 → 17]
230  x ∨ (((y ∨ x) ∧ y) ∨ y) = y ∨ x  [32 → 56]
249  (x ∨ y) ∧ (y ∨ x) = x ∨ y  [2 → 52 :11,160, flip]
255  (x ∧ (y ∨ z)) ∨ (z ∧ x) = x ∧ (z ∨ y)  [4 → 52]
290,289 (x ∨ y) ∧ (z ∧ (y ∨ x)) = (x ∨ y) ∧ z  [249 → 46 :39, flip]
293 x ∧ (y ∨ z) = (z ∨ y) ∧ x [249 → 28 :290]
322,321 (x ∨ y) ∧ (y ∨ (x ∧ z)) = y ∨ (x ∧ z)  [14 → 293, flip]
350 (x ∧ y) ∨ (y ∧ x) = y ∧ x [7 → 54 :8]
365,364 ((x ∨ y) ∧ x) ∨ x = x ∧ (x ∨ y)  [2 → 54]

368  x ∨ (y ∧ (y ∨ x)) = y ∨ x  [230 :365]
405,404 (x ∧ y) ∨ (z ∨ (y ∧ x)) = (x ∧ y) ∨ z  [350 → 48 :43, flip]
408  x ∨ (y ∧ z) = (y ∧ z) ∨ ((z ∧ y) ∨ x)  [350 → 125]
411  x ∨ (y ∧ z) = (z ∧ y) ∨ x  [350 → 29 :405]
413,412 (x ∧ y) ∨ ((y ∧ x) ∨ z) = (y ∧ x) ∨ z  [350 → 10, flip]
414  (x ∧ y) ∨ z = z ∨ (y ∧ x)  [flip 408 :413]
430  x ∨ (y ∧ (x ∨ y)) = y ∨ x  [9 → 368]
521,520 (x ∧ y) ∨ ((x ∨ z) ∧ y) = y ∧ (x ∨ z)  [54 → 411, flip]
536  x ∨ (y ∧ (z ∨ x)) = x ∨ (z ∧ y)  [161 :521]
590  (x ∧ (y ∨ x)) ∨ y = x ∨ y  [9 → 430]
675  (x ∧ y) ∨ (((x ∧ y) ∨ z) ∧ x) = x ∧ ((x ∧ y) ∨ z)  [414 → 60]
1481  ((x ∨ y) ∧ (x ∨ z)) ∨ x = (x ∨ y) ∧ (x ∨ z)  [364 → 68 :63, flip]
1510  x ∨ (y ∧ (x ∨ z)) = x ∨ (z ∧ y)  [9 → 536]
1522,1521 x ∨ ((x ∨ y) ∧ z) = x ∨ (y ∧ z)  [293 → 536]
1535,1534 (x ∧ (y ∨ z)) ∨ z = z ∨ (y ∧ x)  [9 → 536]
1550 x ∨ (y ∧ z) = x ∨ (z ∧ (x ∨ y)) [flip 1510]
1559,1558 (x ∧ y) ∨ (z ∧ x) = x ∧ ((x ∧ y) ∨ z)  [675 :1522]
1617,1616 x ∧ (y ∨ (z ∧ x)) = x ∧ (y ∨ z)  [255 :1559,1535]
1634,1633 (x ∧ (y ∨ z)) ∨ y = y ∨ (z ∧ x)  [536 → 590 :6,322,1617,1535]
1645,1644 x ∨ (y ∧ (x ∨ z)) = (x ∨ z) ∧ (x ∨ y)  [1481 :1634]
1653  x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z)  [1550 :1645]
1655  □  [1653,21]