YES We show the termination of the TRS R: div(X,e()) -> i(X) i(div(X,Y)) -> div(Y,X) div(div(X,Y),Z) -> div(Y,div(i(X),Z)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: div#(X,e()) -> i#(X) p2: i#(div(X,Y)) -> div#(Y,X) p3: div#(div(X,Y),Z) -> div#(Y,div(i(X),Z)) p4: div#(div(X,Y),Z) -> div#(i(X),Z) p5: div#(div(X,Y),Z) -> i#(X) and R consists of: r1: div(X,e()) -> i(X) r2: i(div(X,Y)) -> div(Y,X) r3: div(div(X,Y),Z) -> div(Y,div(i(X),Z)) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: div#(X,e()) -> i#(X) p2: i#(div(X,Y)) -> div#(Y,X) p3: div#(div(X,Y),Z) -> i#(X) p4: div#(div(X,Y),Z) -> div#(i(X),Z) p5: div#(div(X,Y),Z) -> div#(Y,div(i(X),Z)) and R consists of: r1: div(X,e()) -> i(X) r2: i(div(X,Y)) -> div(Y,X) r3: div(div(X,Y),Z) -> div(Y,div(i(X),Z)) The set of usable rules consists of r1, r2, r3 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: div#_A(x1,x2) = max{x1 + 18, x2 + 8} e_A = 5 i#_A(x1) = x1 + 18 div_A(x1,x2) = max{x1 + 5, x2} i_A(x1) = x1 + 5 precedence: div# = e = i# = div = i partial status: pi(div#) = [] pi(e) = [] pi(i#) = [] pi(div) = [1, 2] pi(i) = [1] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: div#(X,e()) -> i#(X) p2: i#(div(X,Y)) -> div#(Y,X) p3: div#(div(X,Y),Z) -> div#(i(X),Z) p4: div#(div(X,Y),Z) -> div#(Y,div(i(X),Z)) and R consists of: r1: div(X,e()) -> i(X) r2: i(div(X,Y)) -> div(Y,X) r3: div(div(X,Y),Z) -> div(Y,div(i(X),Z)) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: div#(X,e()) -> i#(X) p2: i#(div(X,Y)) -> div#(Y,X) p3: div#(div(X,Y),Z) -> div#(Y,div(i(X),Z)) p4: div#(div(X,Y),Z) -> div#(i(X),Z) and R consists of: r1: div(X,e()) -> i(X) r2: i(div(X,Y)) -> div(Y,X) r3: div(div(X,Y),Z) -> div(Y,div(i(X),Z)) The set of usable rules consists of r1, r2, r3 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: div#_A(x1,x2) = x1 + 2 e_A = 5 i#_A(x1) = x1 + 2 div_A(x1,x2) = max{x1 + 5, x2} i_A(x1) = x1 + 5 precedence: div# = e = i# = div = i partial status: pi(div#) = [1] pi(e) = [] pi(i#) = [1] pi(div) = [1, 2] pi(i) = [1] The next rules are strictly ordered: p4 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: div#(X,e()) -> i#(X) p2: i#(div(X,Y)) -> div#(Y,X) p3: div#(div(X,Y),Z) -> div#(Y,div(i(X),Z)) and R consists of: r1: div(X,e()) -> i(X) r2: i(div(X,Y)) -> div(Y,X) r3: div(div(X,Y),Z) -> div(Y,div(i(X),Z)) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: div#(X,e()) -> i#(X) p2: i#(div(X,Y)) -> div#(Y,X) p3: div#(div(X,Y),Z) -> div#(Y,div(i(X),Z)) and R consists of: r1: div(X,e()) -> i(X) r2: i(div(X,Y)) -> div(Y,X) r3: div(div(X,Y),Z) -> div(Y,div(i(X),Z)) The set of usable rules consists of r1, r2, r3 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: div#_A(x1,x2) = max{x1, x2 - 6} e_A = 7 i#_A(x1) = max{1, x1} div_A(x1,x2) = max{x1 + 3, x2} i_A(x1) = x1 + 3 precedence: e = div = i > div# = i# partial status: pi(div#) = [1] pi(e) = [] pi(i#) = [1] pi(div) = [1, 2] pi(i) = [1] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: div#(X,e()) -> i#(X) p2: div#(div(X,Y),Z) -> div#(Y,div(i(X),Z)) and R consists of: r1: div(X,e()) -> i(X) r2: i(div(X,Y)) -> div(Y,X) r3: div(div(X,Y),Z) -> div(Y,div(i(X),Z)) The estimated dependency graph contains the following SCCs: {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: div#(div(X,Y),Z) -> div#(Y,div(i(X),Z)) and R consists of: r1: div(X,e()) -> i(X) r2: i(div(X,Y)) -> div(Y,X) r3: div(div(X,Y),Z) -> div(Y,div(i(X),Z)) The set of usable rules consists of r1, r2, r3 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: div#_A(x1,x2) = max{x1 + 14, x2 + 7} div_A(x1,x2) = max{6, x1 + 2, x2} i_A(x1) = max{3, x1 + 2} e_A = 0 precedence: div# = div = i = e partial status: pi(div#) = [1] pi(div) = [1, 2] pi(i) = [1] pi(e) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.