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