YES We show the termination of the TRS R: f(g(X)) -> g(f(f(X))) f(h(X)) -> h(g(X)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(g(X)) -> f#(f(X)) p2: f#(g(X)) -> f#(X) and R consists of: r1: f(g(X)) -> g(f(f(X))) r2: f(h(X)) -> h(g(X)) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: f#(g(X)) -> f#(f(X)) p2: f#(g(X)) -> f#(X) and R consists of: r1: f(g(X)) -> g(f(f(X))) r2: f(h(X)) -> h(g(X)) The set of usable rules consists of r1, r2 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^4 order: lexicographic order interpretations: f#_A(x1) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,1,0,0)) x1 g_A(x1) = ((1,0,0,0),(1,1,0,0),(0,0,1,0),(0,1,0,0)) x1 + (0,1,1,0) f_A(x1) = ((1,0,0,0),(0,1,0,0),(0,1,0,0),(0,1,0,0)) x1 + (0,0,1,0) h_A(x1) = ((0,0,0,0),(1,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + (1,1,1,0) 2. lexicographic path order with precedence: precedence: f > g > h > f# argument filter: pi(f#) = [] pi(g) = [] pi(f) = [] pi(h) = [] The next rules are strictly ordered: p1, p2 We remove them from the problem. Then no dependency pair remains.