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