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