A certified basis of 23 identities
This list of identities is a basis, proved in Lean, of 59 semigroups of order six, all of which generate the variety V[4022]. Removing the identities that follow from the others leaves 3 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-be4758ea2bdf05e9 in the data of the bases-min seal.
Certified for
[6, 4022] [6, 4027] [6, 4029] [6, 4032] [6, 4130] [6, 4134] [6, 4138] [6, 4237] [6, 4242] [6, 4244] [6, 4247] [6, 5954] [6, 5978] [6, 5998] [6, 6000] [6, 6785] [6, 6836] [6, 6931] [6, 6979] [6, 8805] [6, 8810] [6, 8821] [6, 8824] [6, 8829] [6, 8831] [6, 8834] [6, 8891] [6, 8905] [6, 8955] [6, 8960] [6, 8971] [6, 8974] [6, 8979] [6, 8981] [6, 8984] [6, 9033] [6, 9046] [6, 9872] [6, 9874] [6, 9877] [6, 10179] [6, 10181] [6, 10194] [6, 10211] [6, 10360] [6, 10362] [6, 10365] [6, 10366] [6, 10369] [6, 10374] [6, 10375] [6, 10379] [6, 10385] [6, 10387] [6, 10680] [6, 11637] [6, 11721] [6, 11765] [6, 11767]
The identities
- x² ≈ x⁴
- x³y ≈ xy
- x²yx ≈ xyx²
- x²yx ≈ xy³
- x²yx² ≈ xyx
- x²yxy ≈ xy²
- x²y² ≈ xyxy
- x²y² ≈ xy²x
- x²y²x ≈ xy²
- x²y³ ≈ xyx
- xyx ≈ xyx³
- xyx ≈ xyxy²
- xyx ≈ xy²xy
- xyx²y ≈ xy²
- xyxyx ≈ xy²
- xy² ≈ xy²x²
- x²yxz ≈ xyz
- x²yz ≈ xyxz
- xyx²z ≈ xyz
- xyzx ≈ xzyx
- xyzy ≈ xzy²
- x²yzx ≈ xy²zy
- x²yzy ≈ xy²zx