Theorem LT-3. Sholander’s basis for distributive lattices.

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

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

1 x = x 2 B ∧ A = A ∧ B, (A ∧ B) ∧ C = A ∧ (B ∧ C), A ∧ (A ∨ B) = A,

B ∨ A = A ∨ B, (A ∨ B) ∨ C = A ∨ (B ∨ C),

A ∨ (A ∧ B) = A → □

4,3 x ∧ (x ∨ y) = x 5 x ∧ (y ∨ z) = (z ∧ x) ∨ (y ∧ x)

6 B ∧ A = A ∧ B, (A ∧ B) ∧ C = A ∧ (B ∧ C), B ∨ A = A ∨ B,

(A ∨ B) ∨ C = A ∨ (B ∨ C), A ∨ (A ∧ B) = A → □ [2 :4 :1]
7  (x ∧ y) ∨ (z ∧ y) = y ∧ (z ∨ x)  [flip 5]
8  (x ∧ y) ∨ (y ∧ y) = y  [3 → 5, flip]
19,18  (x ∧ y) ∧ y = x ∧ y  [8 → 3]
20  ((x ∧ y) ∨ (z ∧ y)) ∧ (z ∨ x) = y ∧ (z ∨ x)  [5 → 18]
22  (x ∧ y) ∨ (z ∧ y) = y ∧ (z ∨ (x ∧ y))  [18 → 7]
23  x ∨ (y ∧ (x ∨ z)) = (x ∨ z) ∧ (y ∨ x)  [3 → 7]
26,25  (x ∧ (y ∨ z)) ∨ y = (y ∨ z) ∧ (y ∨ x)  [3 → 7]
33,32  (x ∧ y) ∧ (y ∧ (z ∨ x)) = x ∧ y  [7 → 3]
36  (x ∧ y) ∧ ((y ∧ (z ∨ x)) ∧ (u ∨ (x ∧ y))) = x ∧ y  [32 → 32 :33]
55  x ∧ (y ∨ (z ∧ x)) = x ∧ (y ∨ z)  [7 → 22, flip]
61  x ∧ ((y ∧ x) ∨ x) = x ∧ x  [8 → 55, flip]
67  (x ∧ x) ∨ (y ∧ x) = x ∧ x  [5 → 61 :19]
76,75  x ∧ x = x  [8 → 67, flip]
78,77  x ∧ (y ∨ x) = x  [7 → 67 :76]
81  x ∨ (y ∧ x) = x  [67 :76,76]
95  (x ∧ y) ∨ y = y  [8 :76]
97  x ∨ y = y ∨ x  [5 → 75 :78,4]
108  (x ∧ (y ∨ z)) ∨ z = (y ∨ z) ∧ (z ∨ x)  [77 → 7]
119,118 x ∨ x = x  [75 → 81]
120  (x ∨ (y ∧ z)) ∨ (z ∧ (x ∨ y)) = x ∨ (y ∧ z)  [55 → 81]
132  ((x ∧ y) ∧ z) ∧ (z ∧ y) = (x ∧ y) ∧ z  [81 → 32]
138  x ∧ y = y ∧ x  [7 → 118 :119]
141  (x ∧ y) ∧ x = y ∧ x  [118 → 20 :119,119]
158,157 (x ∨ y) ∧ (y ∨ x) = x ∨ y  [77 → 23, flip]
164 (x ∨ y) ∧ x = x [3 → 23 :119,119, flip]
171,170 (x ∧ y) ∨ (z ∧ y) = y ∧ (x ∨ z)  [7 → 97, flip]
184  x ∧ (y ∨ z) = x ∧ (z ∨ y)  [7 :171]

190  (x ∨ (y ∧ z)) ∧ z = z ∧ (x ∨ y)  [55 → 138, flip]
194  (x ∧ (y ∨ z)) ∧ (z ∧ x) = z ∧ x  [32 → 138, flip]
196  x ∧ (y ∧ x) = y ∧ x  [18 → 138, flip]
206  (x ∧ y) ∨ x = x  [138 → 95]
208  (x ∧ y) ∧ (x ∧ (z ∨ y)) = y ∧ x  [138 → 32]
211,210 x ∨ (x ∧ y) = x  [138 → 81]

214 (A ∧ B) ∧ C = A ∧ (B ∧ C), (A ∨ B) ∨ C = A ∨ (B ∨ C) → □

[6 :211 :138,97,1]

219  x ∧ (y ∨ (x ∨ z)) = x  [164 → 55 :78, flip]
224  (x ∨ (y ∧ z)) ∧ (x ∨ z) = (x ∨ y) ∧ (x ∨ z)  [55 → 25 :26, flip]
249,248 x ∧ (x ∧ y) = x ∧ y  [206 → 164]
269 (x ∧ y) ∧ ((y ∧ (z ∨ x)) ∧ x) = x ∧ y [210 → 36]
282,281 (x ∧ y) ∨ (y ∧ x) = x ∧ y  [141 → 210]
315  (x ∧ y) ∧ (z ∨ x) = x ∧ y  [206 → 219]
525  (x ∨ y) ∧ z = z ∧ (y ∨ x)  [138 → 184]
526  x ∧ (y ∨ z) = (z ∨ y) ∧ x  [flip 525]
671  ((x ∨ y) ∧ z) ∨ y = (x ∨ y) ∧ (y ∨ z)  [138 → 108]
713  (x ∧ y) ∨ z = (z ∨ x) ∧ (z ∨ (x ∧ y))  [315 → 25]
724  (x ∨ y) ∧ (x ∨ (y ∧ z)) = (y ∧ z) ∨ x  [flip 713]
798,797 (x ∨ (y ∧ z)) ∨ (y ∧ (x ∨ z)) = x ∨ (z ∧ y)  [138 → 120]
1260  (x ∧ y) ∧ ((z ∧ y) ∧ x) = (z ∧ y) ∧ x  [138 → 132]
1284  (x ∧ y) ∧ z = z ∧ (y ∧ x)  [281 → 525 :282]
2656,2655 (x ∧ y) ∧ ((y ∧ z) ∧ x) = (y ∧ z) ∧ x  [210 → 194]
2710,2709 (x ∧ (y ∨ z)) ∧ z = z ∧ x  [269 :2656]
3035 x ∧ (y ∧ (z ∨ x)) = x ∧ y [18 → 208 :2710,33, flip]

3069 x ∧ (y ∨ (z ∧ (u ∨ x))) = ((u ∨ x) ∧ (y ∨ z)) ∧ x

[190 → 2709, flip]
3076,3075 ((x ∨ y) ∧ z) ∧ y = y ∧ z  [138 → 2709]
3098,3097 x ∧ (y ∨ (z ∧ (u ∨ x))) = x ∧ (y ∨ z)  [3069 :3076]
3101 x ∨ (y ∧ z) = x ∨ (z ∧ y) [2709 → 120 :3098,798,2710]
3127,3126 (x ∧ y) ∧ (z ∧ x) = (x ∧ y) ∧ z  [210 → 3035]
3135,3134 (x ∧ y) ∧ (z ∧ y) = (x ∧ y) ∧ z  [81 → 3035]
3144  (x ∧ y) ∧ z = (z ∧ y) ∧ x  [1260 :3127,3135]
3369  x ∨ (y ∨ z) = x ∨ (z ∨ y)  [157 → 3101 :158]
3452,3451 (x ∧ y) ∧ z = x ∧ (y ∧ z)  [1284 → 3144, flip]
3685  (A ∨ B) ∨ C = A ∨ (B ∨ C) → □  [214 :3452 :1]
3692  (B ∨ A) ∨ C = A ∨ (B ∨ C) → □  [97 → 3685]
3730,3729 (x ∨ y) ∧ (x ∨ (z ∧ y)) = x ∨ (z ∧ y)  [196 → 224 :76, flip]
3733 (x ∨ (y ∨ z)) ∧ (x ∨ y) = x ∨ y [164 → 224 :76, flip]
3746,3745 x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z)  [138 → 224 :3730]
3747  (x ∨ y) ∧ (x ∨ z) = (y ∧ z) ∨ x  [724 :3746,249]
3801  (x ∨ y) ∨ z = z ∨ (y ∨ x)  [97 → 3369]
5932,5931 (x ∨ y) ∧ (y ∨ (x ∨ z)) = y ∨ x  [526 → 3733]
5957  (x ∨ y) ∨ (y ∨ z) = (y ∨ z) ∨ x  [3733 → 671 :5932]
6203  ((x ∧ y) ∨ z) ∨ x = x ∨ z  [3747 → 671 :5932]

6252  (x ∨ y) ∨ (x ∨ z) = (x ∨ z) ∨ y  [164 → 6203]^{6290  (x ∨ y) ∨ z = (x ∨ z) ∨ (x ∨ y)  [flip 6252]}^{6533,6532 (x ∨ y) ∨ (x ∨ z) = (x ∨ y) ∨ z  [3801 → 5957]}^{6552  (x ∨ y) ∨ z = (x ∨ z) ∨ y  [6290 :6533]}^{6570  (x ∨ y) ∨ z = y ∨ (x ∨ z)  [97 → 6552, flip]}^{6572  □  [6570,3692]}

3