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