A certified basis of 5 identities
This list of identities is a basis, proved in Lean, of 115 semigroups of order six, all of which generate the variety V[2585]. Removing the identities that follow from the others leaves 2 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-81f56eb60084a795 in the data of the bases-min seal.
Certified for
[6, 2585] [6, 2621] [6, 2643] [6, 2689] [6, 2709] [6, 2716] [6, 2724] [6, 2816] [6, 2820] [6, 2824] [6, 2832] [6, 2836] [6, 2839] [6, 2842] [6, 5120] [6, 5137] [6, 5148] [6, 5167] [6, 5174] [6, 5200] [6, 5204] [6, 5271] [6, 5276] [6, 5280] [6, 5284] [6, 5286] [6, 5295] [6, 5297] [6, 5332] [6, 5337] [6, 5360] [6, 5362] [6, 5372] [6, 5384] [6, 5392] [6, 5405] [6, 5408] [6, 5430] [6, 5436] [6, 5443] [6, 5446] [6, 5472] [6, 5477] [6, 5513] [6, 5517] [6, 5585] [6, 5587] [6, 5693] [6, 5703] [6, 5716] [6, 5721] [6, 5725] [6, 5730] [6, 5845] [6, 5853] [6, 5863] [6, 5866] [6, 5869] [6, 9267] [6, 9273] [6, 9285] [6, 9294] [6, 9322] [6, 9325] [6, 9330] [6, 9334] [6, 9339] [6, 9344] [6, 9358] [6, 9365] [6, 9370] [6, 9374] [6, 9388] [6, 9392] [6, 9408] [6, 9410] [6, 9427] [6, 9429] [6, 9473] [6, 9477] [6, 9484] [6, 9488] [6, 9490] [6, 9494] [6, 9508] [6, 9512] [6, 9515] [6, 9519] [6, 9525] [6, 9555] [6, 9557] [6, 9560] [6, 9605] [6, 9609] [6, 9613] [6, 9625] [6, 9635] [6, 9641] [6, 9663] [6, 9665] [6, 9667] [6, 9672] [6, 9679] [6, 9681] [6, 9746] [6, 9748] [6, 9760] [6, 9762] [6, 9772] [6, 9780] [6, 9782] [6, 9788] [6, 9792] [6, 9794] [6, 9796]
The identities
- x³ ≈ x⁴
- xy ≈ yx
- x²y ≈ xy²
- x³y ≈ x²y
- x²yz ≈ xyz