YES (VAR x0 x1 x2 a b) (RULES divide(inverse(x0),divide(x1,divide(x0,x2))) -> divide(inverse(x2),x1) divide(x0,divide(x1,divide(inverse(x0),x2))) -> divide(inverse(x2),x1) divide(divide(x0,x1),x2) -> divide(x0,divide(x2,inverse(x1))) divide(x0,divide(x1,inverse(x0))) -> inverse(x1) divide(inverse(x0),divide(x1,x0)) -> inverse(x1) inverse(divide(x1,x0)) -> divide(x0,x1) divide(x0,identity()) -> x0 inverse(inverse(x0)) -> x0 inverse(identity()) -> identity() divide(a,a) -> identity() multiply(a,b) -> divide(a,inverse(b)) divide(identity(),a) -> inverse(a) ) (COMMENT Termination is shown by KBO with weight w0 = 1 w(divide) = 0 w(identity) = 1 w(multiply) = 0 w(inverse) = 0 and precedence: inverse > multiply > divide > identity )