YES We show the termination of the TRS R: f(a(),y) -> f(y,g(y)) g(a()) -> b() g(b()) -> b() -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(a(),y) -> f#(y,g(y)) p2: f#(a(),y) -> g#(y) and R consists of: r1: f(a(),y) -> f(y,g(y)) r2: g(a()) -> b() r3: g(b()) -> b() The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: f#(a(),y) -> f#(y,g(y)) and R consists of: r1: f(a(),y) -> f(y,g(y)) r2: g(a()) -> b() r3: g(b()) -> b() The set of usable rules consists of r2, r3 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: f#_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(0,0)) x2 + (2,1) a_A() = (3,2) g_A(x1) = (2,3) b_A() = (1,1) precedence: f# = g > a = b partial status: pi(f#) = [] pi(a) = [] pi(g) = [] pi(b) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.