YES (VAR x0 x1 x2 a b) (RULES divide(x0,divide(x1,x2)) -> divide(divide(x0,inverse(x2)),x1) inverse(divide(x1,x0)) -> divide(x0,x1) divide(divide(x0,x2),inverse(x2)) -> x0 divide(divide(x0,inverse(x1)),x1) -> x0 inverse(inverse(x1)) -> x1 divide(x0,identity()) -> 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 EKBO with interpretations on natural numbers divide_A(x1,x2) = x1 + x2 + 1 identity_A = 0 multiply_A(x1,x2) = x1 + x2 + 1 inverse_A(x1) = x1 divide#_A(x1,x2) = x2 identity#_A = 0 multiply#_A(x1,x2) = x1 + x2 weights w0 = 2 w(divide) = 0 w(identity) = 2 w(multiply) = 0 w(inverse) = 0 and precedence: inverse > multiply > divide > identity )