A certified basis of 6 identities
This list of identities is a basis, proved in Lean, of 80 semigroups of order six, all of which generate the variety V[5516]. Removing the identities that follow from the others leaves 2 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-db2f9e5751738f8a in the data of the bases-min seal.
Certified for
[6, 5516] [6, 5518] [6, 5533] [6, 5537] [6, 5539] [6, 5542] [6, 5574] [6, 5582] [6, 5586] [6, 5588] [6, 5590] [6, 5696] [6, 5698] [6, 5702] [6, 5704] [6, 5717] [6, 5719] [6, 5720] [6, 5722] [6, 9409] [6, 9411] [6, 9413] [6, 9417] [6, 9419] [6, 9421] [6, 9428] [6, 9430] [6, 9432] [6, 9474] [6, 9476] [6, 9478] [6, 9485] [6, 9487] [6, 9489] [6, 9516] [6, 9518] [6, 9521] [6, 9524] [6, 9537] [6, 9540] [6, 9550] [6, 9554] [6, 9556] [6, 9558] [6, 9563] [6, 9565] [6, 9568] [6, 9608] [6, 9610] [6, 9615] [6, 9628] [6, 9666] [6, 9668] [6, 9670] [6, 9671] [6, 9673] [6, 9675] [6, 9676] [6, 9680] [6, 9682] [6, 9684] [6, 9692] [6, 9693] [6, 9694] [6, 9695] [6, 9747] [6, 9749] [6, 9751] [6, 9752] [6, 9761] [6, 9764] [6, 9765] [6, 9767] [6, 9774] [6, 9781] [6, 9783] [6, 9785] [6, 9786] [6, 9790] [6, 9793]
The identities
- x³ ≈ x⁴
- x²y ≈ xyx
- x²y ≈ xy²
- x³y ≈ x²y
- xyz ≈ xzy
- x²yz ≈ xyz