SemiBase

A certified basis of 23 identities

This list of identities is a basis, proved in Lean, of 2 semigroups of order six, all of which generate the variety V[6543]. Removing the identities that follow from the others leaves 4 identities (Vampire); the variety page shows the shortest known basis.

Identifier sb-9c5ed0b88c00c88c in the data of the bases-min seal.

Certified for

The identities

  1. x² ≈ x⁴
  2. x³y ≈ xyx²
  3. x³yx ≈ xyx
  4. x²y ≈ x²yx²
  5. x²y² ≈ xyxy
  6. x²y² ≈ xy²x
  7. xyx ≈ xyx³
  8. x³y² ≈ x²y²x
  9. x³y² ≈ xyx²y
  10. x²y³ ≈ xy²xy
  11. x²y³ ≈ xy³x
  12. x³yz ≈ xyx²z
  13. x³yz ≈ xyzx²
  14. x²y²z ≈ xy²xz
  15. x²yzy ≈ xyxzy
  16. xyxz² ≈ xyzxz
  17. xyxz² ≈ xyz²x
  18. xy³z ≈ xyzy²
  19. xy²z² ≈ xyz²y
  20. xyzxy ≈ xyzyx
  21. xyxztz ≈ xyzxtz
  22. xyxztz ≈ xyzxtz
  23. xyztxz ≈ xyztzx