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