Theorem LT-5. A new self-dual form of distributivity for lattice theory.

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

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

Proof (found by Otter 3.0.4 on gyro at 11.74 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 ∧ (x ∨ y) = x 15,14 x ∨ (x ∧ y) = x 16 (((x ∧ y) ∨ z) ∧ y) ∨ (z ∧ x) = (((x ∨ y) ∧ z) ∨ y) ∧ (z ∨ x) 20 A ∨ (B ∧ C) ≠ (A ∨ B) ∧ (A ∨ C)

21  x ∧ (y ∧ z) = y ∧ (x ∧ z)  [4 → 5 :6]
22  x ∧ (x ∧ y) = x ∧ y  [2 → 5, flip]
29,28  x ∧ (y ∨ x) = x  [9 → 12]
33,32  (x ∨ y) ∧ x = x  [4 → 12]
36  x ∨ (y ∨ z) = y ∨ (x ∨ z)  [9 → 10 :11]
38,37  x ∨ (x ∨ y) = x ∨ y  [7 → 10, flip]
47  x ∨ (y ∧ x) = x  [4 → 14]
51  (x ∧ y) ∨ x = x  [9 → 14]
53  x ∨ ((x ∧ y) ∨ z) = x ∨ z  [14 → 10, flip]
56,55  x ∧ (y ∧ x) = x ∧ y  [14 → 28 :6]
57  x ∧ (y ∨ (z ∨ x)) = x  [10 → 28]
61  (x ∨ y) ∧ y = y  [4 → 28]

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

[4 → 16]

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

[12 → 16 :11,33,38]

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

[32 → 16 :33,11, flip]

92,91  x ∨ (y ∨ x) = x ∨ y  [32 → 14 :11]
94,93  (x ∨ y) ∧ (x ∧ z) = x ∧ z  [32 → 5, flip]
95  (((x ∨ y) ∧ z) ∨ x) ∧ (z ∨ (x ∨ y)) = x ∨ (z ∧ (x ∨ y))  [89 :92]
110,109 x ∨ ((y ∧ x) ∨ z) = x ∨ z  [47 → 10, flip]
118 (((x ∨ y) ∧ z) ∨ y) ∧ (z ∧ x) = z ∧ x [16 → 61 :6,94]

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

[61 → 16 :33,11,8, flip]

127 (B ∧ C) ∨ A ≠ (A ∨ B) ∧ (A ∨ C) [9 → 20]
141,140 (x ∨ y) ∧ (z ∧ y) = z ∧ y  [61 → 21, flip]

142  (x ∨ y) ∧ (z ∧ x) = z ∧ x  [32 → 21, flip]
207,206 (x ∨ y) ∧ (z ∨ (y ∨ x)) = x ∨ y  [91 → 57]
559,558 ((x ∧ y) ∨ z) ∧ (u ∨ (y ∨ z)) = (x ∧ y) ∨ z  [109 → 57]
696,695 (x ∨ (y ∧ z)) ∧ (z ∧ y) = z ∧ y  [55 → 140 :56]
747,746 ((x ∧ y) ∨ z) ∧ (y ∧ x) = y ∧ x  [55 → 142 :56]

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

[67 → 53 :11,11,15]

1222,1221 (x ∧ (y ∨ z)) ∨ y = (y ∨ (x ∧ (y ∨ z))) ∧ (y ∨ z)  [55 → 76 :747]
1224,1223 ((x ∨ y) ∧ z) ∨ x = (x ∨ ((x ∨ y) ∧ z)) ∧ (x ∨ y)  [22 → 76 :33]

1226,1225 (x ∨ ((x ∨ y) ∧ z)) ∧ (x ∨ y) = (x ∨ z) ∧ (x ∨ y)

[4 → 76 :1222,6,696,1224]

1234,1233 x ∨ ((x ∨ y) ∧ z) = (x ∨ z) ∧ (x ∨ y)  [9 → 76 :1224,1226,6,141]
1246,1245 x ∨ (y ∧ (x ∨ z)) = (x ∨ y) ∧ (x ∨ z)  [95 :1224,1234,6,3,6,29, flip]
1248,1247 ((x ∨ y) ∧ z) ∨ x = (x ∨ z) ∧ (x ∨ y)  [1223 :1234,6,3]
1254,1253 (x ∧ y) ∨ ((z ∨ x) ∧ (z ∨ y)) = (x ∧ y) ∨ z  [936 :1246,110]
2199 (x ∧ y) ∨ (((y ∨ z) ∧ x) ∨ z) = ((y ∨ z) ∧ x) ∨ z [118 → 51]
2238,2237 x ∨ (y ∧ (z ∨ x)) = (x ∨ y) ∧ (x ∨ z)  [9 → 122 :1248,6,207, flip]
2265,2264 ((x ∨ y) ∧ z) ∨ y = (y ∨ z) ∧ (y ∨ x)  [36 → 122 :559,2238]
2280  (x ∧ y) ∨ z = (z ∨ x) ∧ (z ∨ y)  [2199 :2265,1254,2265]
2281  □  [2280,127]