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: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: g#_A(x1) = ((1,0),(1,0)) x1 g_A(x1) = (3,5) h_A(x1) = (2,4) f_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,0)) x2 + (1,1) precedence: g# = g > h = f partial status: pi(g#) = [] pi(g) = [] pi(h) = [] pi(f) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: g#_A(x1) = (0,0) g_A(x1) = (0,0) h_A(x1) = (2,1) f_A(x1,x2) = (1,2) precedence: h > g = f > g# 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.