YES We show the termination of the TRS R: minus(X,|0|()) -> X minus(s(X),s(Y)) -> p(minus(X,Y)) p(s(X)) -> X div(|0|(),s(Y)) -> |0|() div(s(X),s(Y)) -> s(div(minus(X,Y),s(Y))) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: minus#(s(X),s(Y)) -> p#(minus(X,Y)) p2: minus#(s(X),s(Y)) -> minus#(X,Y) p3: div#(s(X),s(Y)) -> div#(minus(X,Y),s(Y)) p4: div#(s(X),s(Y)) -> minus#(X,Y) and R consists of: r1: minus(X,|0|()) -> X r2: minus(s(X),s(Y)) -> p(minus(X,Y)) r3: p(s(X)) -> X r4: div(|0|(),s(Y)) -> |0|() r5: div(s(X),s(Y)) -> s(div(minus(X,Y),s(Y))) The estimated dependency graph contains the following SCCs: {p3} {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: div#(s(X),s(Y)) -> div#(minus(X,Y),s(Y)) and R consists of: r1: minus(X,|0|()) -> X r2: minus(s(X),s(Y)) -> p(minus(X,Y)) r3: p(s(X)) -> X r4: div(|0|(),s(Y)) -> |0|() r5: div(s(X),s(Y)) -> s(div(minus(X,Y),s(Y))) The set of usable rules consists of r1, r2, r3 Take the reduction pair: lexicographic path order with precedence: precedence: |0| > p > minus > div# > s argument filter: pi(div#) = 1 pi(s) = [1] pi(minus) = 1 pi(p) = 1 pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: minus#(s(X),s(Y)) -> minus#(X,Y) and R consists of: r1: minus(X,|0|()) -> X r2: minus(s(X),s(Y)) -> p(minus(X,Y)) r3: p(s(X)) -> X r4: div(|0|(),s(Y)) -> |0|() r5: div(s(X),s(Y)) -> s(div(minus(X,Y),s(Y))) The set of usable rules consists of (no rules) Take the monotone reduction pair: lexicographic path order with precedence: precedence: s > minus# argument filter: pi(minus#) = [1, 2] pi(s) = [1] The next rules are strictly ordered: p1 r1, r2, r3, r4, r5 We remove them from the problem. Then no dependency pair remains.