A certified basis of 12 identities
This list of identities is a basis, proved in Lean, of 142 semigroups of order six, all of which generate the variety V[7405]. Removing the identities that follow from the others leaves 6 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-6faa690fab5c0f50 in the data of the bases-min seal.
Certified for
[6, 7405] [6, 7407] [6, 7423] [6, 7425] [6, 7442] [6, 7443] [6, 7488] [6, 7496] [6, 7504] [6, 7801] [6, 7803] [6, 7815] [6, 7817] [6, 7829] [6, 7830] [6, 7839] [6, 7847] [6, 7855] [6, 7958] [6, 7960] [6, 7971] [6, 7989] [6, 7990] [6, 8000] [6, 8002] [6, 8017] [6, 8019] [6, 8023] [6, 8033] [6, 8034] [6, 8043] [6, 8051] [6, 8060] [6, 8205] [6, 8207] [6, 8208] [6, 8209] [6, 8211] [6, 8212] [6, 8265] [6, 8271] [6, 8394] [6, 8395] [6, 8544] [6, 10518] [6, 10519] [6, 10536] [6, 10561] [6, 10562] [6, 10861] [6, 10863] [6, 10869] [6, 10871] [6, 10889] [6, 10891] [6, 10901] [6, 10903] [6, 10930] [6, 10931] [6, 10940] [6, 10941] [6, 11019] [6, 11020] [6, 11032] [6, 11033] [6, 11041] [6, 11044] [6, 11103] [6, 11104] [6, 11105] [6, 11106] [6, 11107] [6, 11351] [6, 11353] [6, 11356] [6, 12567] [6, 12575] [6, 12583] [6, 12630] [6, 12638] [6, 12646] [6, 12712] [6, 12738] [6, 12740] [6, 12749] [6, 12768] [6, 12826] [6, 12828] [6, 12834] [6, 12856] [6, 12918] [6, 12919] [6, 12921] [6, 12922] [6, 12923] [6, 12940] [6, 12942] [6, 12943] [6, 12944] [6, 12946] [6, 12947] [6, 12948] [6, 12968] [6, 12969] [6, 12988] [6, 12992] [6, 12998] [6, 13000] [6, 13003] [6, 13005] [6, 13006] [6, 13020] [6, 13024] [6, 13025] [6, 13026] [6, 13034] [6, 13035] [6, 13036] [6, 13037] [6, 13059] [6, 13060] [6, 13341] [6, 13342] [6, 13343] [6, 13362] [6, 13364] [6, 13365] [6, 13377] [6, 13396] [6, 13399] [6, 13400] [6, 13414] [6, 13431] [6, 13432] [6, 13435] [6, 13618] [6, 13927] [6, 13935] [6, 13943] [6, 14124] [6, 14126] [6, 14242]
The identities
- x² ≈ x³
- x²yx ≈ xyx
- xyx ≈ xyx²
- x²y² ≈ xyxy
- xyxy ≈ xy²x
- xyxzx ≈ xyzx
- x²yzy ≈ xyxzy
- xyxz² ≈ xyzxz
- xyzxy ≈ xyzyx
- xyzxz ≈ xyz²x
- xyxztz ≈ xyzxtz
- xyztxz ≈ xyztzx