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