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