A certified basis of 7 identities
This list of identities is a basis, proved in Lean, of 161 semigroups of order six, all of which generate the variety V[3258]. Removing the identities that follow from the others leaves 3 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-9966fbe26e5d645c in the data of the bases-min seal.
Certified for
[6, 3258] [6, 3259] [6, 3260] [6, 3261] [6, 3278] [6, 3279] [6, 3290] [6, 3298] [6, 3385] [6, 3410] [6, 3411] [6, 3412] [6, 3420] [6, 3421] [6, 3434] [6, 3438] [6, 3465] [6, 3473] [6, 3479] [6, 3480] [6, 3491] [6, 3497] [6, 3501] [6, 3526] [6, 3528] [6, 3529] [6, 3636] [6, 3642] [6, 3646] [6, 3650] [6, 3684] [6, 3692] [6, 3696] [6, 3726] [6, 3730] [6, 3763] [6, 3787] [6, 3804] [6, 3807] [6, 3820] [6, 3847] [6, 6072] [6, 6073] [6, 6074] [6, 6108] [6, 6189] [6, 6190] [6, 6213] [6, 6303] [6, 6317] [6, 6372] [6, 6387] [6, 6454] [6, 6714] [6, 7297] [6, 7298] [6, 7307] [6, 7322] [6, 7323] [6, 7332] [6, 7349] [6, 7352] [6, 7366] [6, 7367] [6, 7374] [6, 7388] [6, 7389] [6, 7408] [6, 7409] [6, 7412] [6, 7458] [6, 7468] [6, 7489] [6, 7573] [6, 7574] [6, 7609] [6, 7736] [6, 7740] [6, 7752] [6, 7756] [6, 7769] [6, 7779] [6, 7782] [6, 7804] [6, 7806] [6, 7840] [6, 7889] [6, 7907] [6, 7930] [6, 7941] [6, 7963] [6, 8003] [6, 8005] [6, 8044] [6, 8095] [6, 8099] [6, 8103] [6, 8105] [6, 8108] [6, 8239] [6, 8604] [6, 8605] [6, 8614] [6, 8641] [6, 8645] [6, 8662] [6, 8675] [6, 9906] [6, 10096] [6, 10097] [6, 10116] [6, 10290] [6, 10689] [6, 10699] [6, 10711] [6, 10712] [6, 10727] [6, 10733] [6, 10761] [6, 10762] [6, 10765] [6, 10780] [6, 10784] [6, 10846] [6, 10847] [6, 10872] [6, 10873] [6, 10875] [6, 10912] [6, 10915] [6, 10942] [6, 11194] [6, 11668] [6, 12531] [6, 12540] [6, 12553] [6, 12568] [6, 12604] [6, 12613] [6, 12619] [6, 12631] [6, 12663] [6, 12669] [6, 12701] [6, 12702] [6, 12713] [6, 12790] [6, 12802] [6, 12807] [6, 12815] [6, 12829] [6, 12971] [6, 12973] [6, 13367] [6, 13891] [6, 13900] [6, 13913] [6, 13928] [6, 14111] [6, 14113] [6, 14237]
The identities
- x² ≈ x³
- xyx ≈ yxy
- x²yx ≈ xyx
- x²y² ≈ xyx
- xyx ≈ xyx²
- xyx ≈ xyxy
- xyx ≈ xy²x