YES We show the termination of the TRS R: p(a(x0),p(a(a(a(x1))),x2)) -> p(a(x2),p(a(a(b(x0))),x2)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: p#(a(x0),p(a(a(a(x1))),x2)) -> p#(a(x2),p(a(a(b(x0))),x2)) p2: p#(a(x0),p(a(a(a(x1))),x2)) -> p#(a(a(b(x0))),x2) and R consists of: r1: p(a(x0),p(a(a(a(x1))),x2)) -> p(a(x2),p(a(a(b(x0))),x2)) The estimated dependency graph contains the following SCCs: {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: p#(a(x0),p(a(a(a(x1))),x2)) -> p#(a(a(b(x0))),x2) and R consists of: r1: p(a(x0),p(a(a(a(x1))),x2)) -> p(a(x2),p(a(a(b(x0))),x2)) The set of usable rules consists of (no rules) Take the reduction pair: max/plus interpretations on natural numbers: p#_A(x1,x2) = max{x1 - 2, x2 + 1} a_A(x1) = max{1, x1 - 1} p_A(x1,x2) = max{x1 + 3, x2 + 1} b_A(x1) = x1 The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.