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