YES We show the termination of the TRS R: g(h(g(x))) -> g(x) g(g(x)) -> g(h(g(x))) h(h(x)) -> h(f(h(x),x)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: g#(g(x)) -> g#(h(g(x))) p2: g#(g(x)) -> h#(g(x)) p3: h#(h(x)) -> h#(f(h(x),x)) and R consists of: r1: g(h(g(x))) -> g(x) r2: g(g(x)) -> g(h(g(x))) r3: h(h(x)) -> h(f(h(x),x)) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: g#(g(x)) -> g#(h(g(x))) and R consists of: r1: g(h(g(x))) -> g(x) r2: g(g(x)) -> g(h(g(x))) r3: h(h(x)) -> h(f(h(x),x)) The set of usable rules consists of r1, r2, r3 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: g#_A(x1) = max{1, x1 - 2} g_A(x1) = x1 + 5 h_A(x1) = max{0, x1 - 5} f_A(x1,x2) = max{x1, x2 - 11} precedence: g# > g > f > h partial status: pi(g#) = [] pi(g) = [] pi(h) = [] pi(f) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: g#_A(x1) = 7 g_A(x1) = 6 h_A(x1) = 8 f_A(x1,x2) = max{8, x1} precedence: g# > g = h > f partial status: pi(g#) = [] pi(g) = [] pi(h) = [] pi(f) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.