A certified basis of 6 identities
This list of identities is a basis, proved in Lean, of 164 semigroups of order six, all of which generate the variety V[3262]. Removing the identities that follow from the others leaves 3 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-d0224d0f601a3641 in the data of the bases-min seal.
Certified for
[6, 3262] [6, 3263] [6, 3264] [6, 3265] [6, 3280] [6, 3281] [6, 3291] [6, 3299] [6, 3387] [6, 3413] [6, 3414] [6, 3415] [6, 3422] [6, 3423] [6, 3435] [6, 3439] [6, 3468] [6, 3474] [6, 3481] [6, 3482] [6, 3493] [6, 3498] [6, 3502] [6, 3527] [6, 3530] [6, 3531] [6, 3532] [6, 3533] [6, 3534] [6, 3637] [6, 3643] [6, 3647] [6, 3651] [6, 3685] [6, 3686] [6, 3693] [6, 3697] [6, 3698] [6, 3727] [6, 3728] [6, 3729] [6, 3731] [6, 3732] [6, 3733] [6, 3764] [6, 3788] [6, 3789] [6, 3790] [6, 3805] [6, 3808] [6, 3821] [6, 3848] [6, 3849] [6, 6075] [6, 6076] [6, 6077] [6, 6109] [6, 6191] [6, 6214] [6, 6304] [6, 6318] [6, 6373] [6, 6374] [6, 6388] [6, 6455] [6, 6456] [6, 6715] [6, 7299] [6, 7300] [6, 7308] [6, 7324] [6, 7325] [6, 7333] [6, 7350] [6, 7353] [6, 7395] [6, 7396] [6, 7413] [6, 7414] [6, 7417] [6, 7459] [6, 7491] [6, 7581] [6, 7582] [6, 7614] [6, 7737] [6, 7741] [6, 7753] [6, 7757] [6, 7770] [6, 7807] [6, 7809] [6, 7842] [6, 7890] [6, 7908] [6, 7942] [6, 7949] [6, 7964] [6, 7967] [6, 8007] [6, 8009] [6, 8010] [6, 8046] [6, 8096] [6, 8097] [6, 8100] [6, 8101] [6, 8106] [6, 8109] [6, 8111] [6, 8113] [6, 8114] [6, 8240] [6, 8244] [6, 8606] [6, 8607] [6, 8615] [6, 8642] [6, 8646] [6, 8663] [6, 8676] [6, 8677] [6, 9908] [6, 10098] [6, 10099] [6, 10117] [6, 10291] [6, 10690] [6, 10700] [6, 10713] [6, 10714] [6, 10729] [6, 10734] [6, 10781] [6, 10785] [6, 10851] [6, 10852] [6, 10877] [6, 10878] [6, 10880] [6, 10917] [6, 10920] [6, 11202] [6, 11669] [6, 12532] [6, 12541] [6, 12570] [6, 12605] [6, 12614] [6, 12633] [6, 12665] [6, 12670] [6, 12705] [6, 12706] [6, 12792] [6, 12978] [6, 12980] [6, 13378] [6, 13892] [6, 13901] [6, 13930] [6, 14116] [6, 14118] [6, 14239]
The identities
- x² ≈ x³
- xyx ≈ yxy
- x²yx ≈ xyx
- xyx ≈ xyx²
- xyx ≈ xyxy
- xyx ≈ xy²x