YES (VAR x y z) (RULES multiply(inverse(x),x) -> identity() multiply(x,inverse(x)) -> identity() inverse(multiply(x,y)) -> multiply(inverse(y),inverse(x)) b() -> d() inverse(identity()) -> identity() inverse(inverse(x)) -> x multiply(x,identity()) -> x multiply(x,multiply(inverse(x),y)) -> y multiply(inverse(x),multiply(x,y)) -> y multiply(multiply(x,y),z) -> multiply(x,multiply(y,z)) multiply(identity(),x) -> x )