YES
(VAR b a c)
(RULES
double_divide(b,a) -> multiply(inverse(b),inverse(a))
multiply(multiply(b,a),c) -> multiply(b,multiply(a,c))
inverse(multiply(b,a)) -> multiply(inverse(a),inverse(b))
multiply(b,multiply(inverse(b),a)) -> a
multiply(inverse(b),b) -> identity()
multiply(inverse(b),multiply(b,a)) -> a
inverse(identity()) -> identity()
multiply(b,inverse(b)) -> identity()
multiply(identity(),b) -> b
multiply(b,identity()) -> b
inverse(inverse(b)) -> b
)