You do need (some subset of) associativity: (y0 * x) * x ?= y0 * (x * x) y1 * x ?= y0 * x y2 ?= y1 y2 is not in general constrained to b

You do need (some subset of) associativity: (y0 * x) * x ?= y0 * (x * x) y1 * x ?= y0 * x y2 ?= y1 y2 is not in general constrained to be the same as y1 otherwise.