A certified basis of 6 identities
This list of identities is a basis, proved in Lean, of [6, 5597], which generates the variety V[5597]. Removing the identities that follow from the others leaves 3 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-d701ac74093e8221 in the data of the bases-min seal.
Certified for
The identities
- x³y ≈ x²y
- x²y²x ≈ x²y³
- x²yz ≈ xyxz
- x²y²zx ≈ x²y²zy
- x²yz²x ≈ x²yz³
- x²yz²tx ≈ x²yz²tz