YES We show the termination of the TRS R: f(a(),h(x)) -> f(g(x),h(x)) h(g(x)) -> h(a()) g(h(x)) -> g(x) h(h(x)) -> x -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(a(),h(x)) -> f#(g(x),h(x)) p2: f#(a(),h(x)) -> g#(x) p3: h#(g(x)) -> h#(a()) p4: g#(h(x)) -> g#(x) and R consists of: r1: f(a(),h(x)) -> f(g(x),h(x)) r2: h(g(x)) -> h(a()) r3: g(h(x)) -> g(x) r4: h(h(x)) -> x The estimated dependency graph contains the following SCCs: {p1} {p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: f#(a(),h(x)) -> f#(g(x),h(x)) and R consists of: r1: f(a(),h(x)) -> f(g(x),h(x)) r2: h(g(x)) -> h(a()) r3: g(h(x)) -> g(x) r4: h(h(x)) -> x The set of usable rules consists of r2, r3 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: f#_A(x1,x2) = x1 a_A() = 3 h_A(x1) = 2 g_A(x1) = 1 base order 2: precedence: a > h = g > f# partial status: pi(f#) = [1] pi(a) = [] pi(h) = [] pi(g) = [] The following rules are removed: p1 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: g#(h(x)) -> g#(x) and R consists of: r1: f(a(),h(x)) -> f(g(x),h(x)) r2: h(g(x)) -> h(a()) r3: g(h(x)) -> g(x) r4: h(h(x)) -> x The set of usable rules consists of r1, r4 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: g#_A(x1) = x1 h_A(x1) = x1 + 2 f_A(x1,x2) = 0 a_A() = 4 g_A(x1) = x1 + 3 base order 2: precedence: g# > h > a > g > f partial status: pi(g#) = [1] pi(h) = [] pi(f) = [] pi(a) = [] pi(g) = [1] The following rules are removed: p1 Then no dependency pair remains.