A certified basis of 26 identities
This list of identities is a basis, proved in Lean, of 74 semigroups of order six, all of which generate the variety V[1230]. Removing the identities that follow from the others leaves 4 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-f3af54bce1485c55 in the data of the bases-min seal.
Certified for
[6, 1230] [6, 1232] [6, 1234] [6, 1239] [6, 1243] [6, 1276] [6, 1278] [6, 1280] [6, 1284] [6, 1285] [6, 1312] [6, 1314] [6, 1316] [6, 1320] [6, 1324] [6, 1328] [6, 1332] [6, 1375] [6, 1377] [6, 1379] [6, 1383] [6, 2941] [6, 2945] [6, 2949] [6, 2950] [6, 2971] [6, 2992] [6, 3082] [6, 3083] [6, 3111] [6, 3112] [6, 3144] [6, 3145] [6, 4035] [6, 4038] [6, 4046] [6, 4048] [6, 4057] [6, 4109] [6, 4141] [6, 4144] [6, 4150] [6, 4152] [6, 4156] [6, 4161] [6, 4216] [6, 4250] [6, 4253] [6, 4259] [6, 4261] [6, 4269] [6, 4315] [6, 5802] [6, 5803] [6, 6067] [6, 6070] [6, 6104] [6, 6106] [6, 6219] [6, 6223] [6, 6224] [6, 6268] [6, 6270] [6, 6629] [6, 6744] [6, 6774] [6, 6786] [6, 6853] [6, 6857] [6, 6932] [6, 6996] [6, 7000] [6, 9830] [6, 9864]
The identities
- x² ≈ x⁴
- x³yx ≈ xyx
- x³y² ≈ yxy
- x²yx ≈ xyx²
- x²yx ≈ yxy²
- x²yx² ≈ xyx
- x²yxy ≈ yxy
- x²y² ≈ xyxy
- x²y² ≈ xy²x
- x²y² ≈ yx²y
- x²y²x ≈ yxy
- x²y³ ≈ xyx
- xyx ≈ xyx³
- xyx ≈ xyxy²
- xyx ≈ xy²xy
- xyx ≈ xy³x
- xyx ≈ yx²y²
- xyx ≈ yxyxy
- xyx ≈ yxy²x
- x²yz ≈ xyxz
- xy³z ≈ xyz
- xyzx ≈ xzyx
- xyzy ≈ xzy²
- x²yzx ≈ yxyzy
- x²yzy ≈ xy²zx
- x²yzy ≈ yx²zy