A certified basis of 6 identities
This list of identities is a basis, proved in Lean, of 71 semigroups of order six, all of which generate the variety V[852]. Removing the identities that follow from the others leaves 4 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-6d18429a6acd4293 in the data of the bases-min seal.
Certified for
[6, 852] [6, 853] [6, 854] [6, 857] [6, 858] [6, 860] [6, 861] [6, 862] [6, 863] [6, 864] [6, 865] [6, 866] [6, 868] [6, 869] [6, 870] [6, 874] [6, 875] [6, 877] [6, 878] [6, 2224] [6, 2225] [6, 2227] [6, 2228] [6, 2230] [6, 2510] [6, 2511] [6, 2512] [6, 2513] [6, 2516] [6, 2517] [6, 2519] [6, 2520] [6, 2521] [6, 2522] [6, 2524] [6, 2525] [6, 2526] [6, 2528] [6, 2532] [6, 2533] [6, 2537] [6, 2541] [6, 2542] [6, 2543] [6, 2545] [6, 2546] [6, 2548] [6, 2551] [6, 2552] [6, 2554] [6, 2561] [6, 2564] [6, 5083] [6, 5084] [6, 5086] [6, 5087] [6, 5088] [6, 5089] [6, 5090] [6, 5091] [6, 5092] [6, 5093] [6, 5094] [6, 5096] [6, 5097] [6, 5098] [6, 5100] [6, 5101] [6, 5103] [6, 5104] [6, 5110]
The identities
- x²y ≈ xyx
- x²y ≈ xy²
- x²y ≈ yx²
- xyz ≈ xzy
- xyz ≈ yxz
- x⁴ ≈ xyzt