YES (VAR x0 x1 x2 a b) (RULES divide(inverse(x0),divide(x1,divide(x0,x2))) -> divide(inverse(x2),x1) divide(x2,divide(x0,divide(inverse(x2),x1))) -> divide(inverse(x1),x0) divide(divide(x0,x1),x2) -> divide(x0,divide(x2,inverse(x1))) divide(inverse(x0),divide(x1,x0)) -> inverse(x1) divide(x1,divide(x0,inverse(x1))) -> inverse(x0) inverse(divide(x1,x0)) -> divide(x0,x1) divide(x0,identity()) -> x0 inverse(inverse(x0)) -> x0 multiply(a,b) -> divide(a,inverse(b)) inverse(identity()) -> identity() divide(a,a) -> identity() divide(identity(),a) -> inverse(a) ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers divide_A(x1,x2) = x1 + x2 + 2 identity_A = 1 multiply_A(x1,x2) = x1 + x2 + 3 inverse_A(x1) = x1 identity#_A = 0 weights w0 = 1 w(divide) = 0 w(identity) = 1 w(multiply) = 2 w(inverse) = 0 and precedence: inverse > multiply > divide > identity )