A certified basis of 4 identities
This list of identities is a basis, proved in Lean, of 31 semigroups of order six, all of which generate the variety V[1000]. Removing the identities that follow from the others leaves 1 identity (Vampire); the variety page shows the shortest known basis.
Identifier sb-da5b25dec9992f31 in the data of the bases-min seal.
Certified for
[6, 1000] [6, 1010] [6, 1055] [6, 1057] [6, 1059] [6, 1061] [6, 1068] [6, 1070] [6, 1077] [6, 1127] [6, 1129] [6, 1131] [6, 1133] [6, 1135] [6, 1137] [6, 1139] [6, 2936] [6, 2963] [6, 2969] [6, 2977] [6, 2983] [6, 2985] [6, 3014] [6, 3018] [6, 3020] [6, 3380] [6, 3624] [6, 5785] [6, 5786] [6, 5795] [6, 6179]
The identities
- x² ≈ x³
- x² ≈ x²y
- x² ≈ xyx
- x² ≈ xyz