A certified basis of 16 identities
This list of identities is a basis, proved in Lean, of [6, 2979], which generates the variety V[2979]. Removing the identities that follow from the others leaves 5 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-28b9f18f74bcdde2 in the data of the bases-min seal.
Certified for
The identities
- x² ≈ x³
- x²yx ≈ xyx
- x²y² ≈ xyx²
- x²y² ≈ xyxy
- x²y² ≈ yx²y
- xyxz ≈ yxyz
- xyz² ≈ xzy²
- x²yzy ≈ yxzy
- xyxzx ≈ xyzx
- xy²zx ≈ xyzx
- x²yz² ≈ xyxz²
- x²yz² ≈ xyzxy
- x²yz² ≈ xyzxz
- x²yz² ≈ xyzyx
- x²yz² ≈ xyz²x
- xy²zt ≈ xyzt