YES We show the termination of the TRS R: f(f(a(),x),a()) -> f(f(f(a(),a()),f(x,a())),a()) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(f(a(),x),a()) -> f#(f(f(a(),a()),f(x,a())),a()) p2: f#(f(a(),x),a()) -> f#(f(a(),a()),f(x,a())) p3: f#(f(a(),x),a()) -> f#(a(),a()) p4: f#(f(a(),x),a()) -> f#(x,a()) and R consists of: r1: f(f(a(),x),a()) -> f(f(f(a(),a()),f(x,a())),a()) The estimated dependency graph contains the following SCCs: {p1, p2, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: f#(f(a(),x),a()) -> f#(f(f(a(),a()),f(x,a())),a()) p2: f#(f(a(),x),a()) -> f#(x,a()) p3: f#(f(a(),x),a()) -> f#(f(a(),a()),f(x,a())) and R consists of: r1: f(f(a(),x),a()) -> f(f(f(a(),a()),f(x,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: max/plus interpretations on natural numbers: f#_A(x1,x2) = max{16, x2 - 24} f_A(x1,x2) = 27 a_A = 41 precedence: a > f# = f partial status: pi(f#) = [] pi(f) = [] pi(a) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: f#_A(x1,x2) = 11 f_A(x1,x2) = 3 a_A = 4 precedence: f# > a > f partial status: pi(f#) = [] pi(f) = [] pi(a) = [] The next rules are strictly ordered: p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(f(a(),x),a()) -> f#(f(f(a(),a()),f(x,a())),a()) p2: f#(f(a(),x),a()) -> f#(x,a()) and R consists of: r1: f(f(a(),x),a()) -> f(f(f(a(),a()),f(x,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#(f(a(),x),a()) -> f#(f(f(a(),a()),f(x,a())),a()) p2: f#(f(a(),x),a()) -> f#(x,a()) and R consists of: r1: f(f(a(),x),a()) -> f(f(f(a(),a()),f(x,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: standard order interpretations: f#_A(x1,x2) = ((1,0),(0,0)) x1 f_A(x1,x2) = x1 + ((1,0),(0,0)) x2 a_A() = (0,1) precedence: f# = f = a partial status: pi(f#) = [] pi(f) = [] pi(a) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: f#_A(x1,x2) = ((0,1),(0,0)) x1 f_A(x1,x2) = ((0,0),(1,0)) x1 + ((0,0),(1,1)) x2 a_A() = (1,0) precedence: f# = f = a partial status: pi(f#) = [] pi(f) = [] pi(a) = [] 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#(f(a(),x),a()) -> f#(f(f(a(),a()),f(x,a())),a()) and R consists of: r1: f(f(a(),x),a()) -> f(f(f(a(),a()),f(x,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#(f(a(),x),a()) -> f#(f(f(a(),a()),f(x,a())),a()) and R consists of: r1: f(f(a(),x),a()) -> f(f(f(a(),a()),f(x,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: max/plus interpretations on natural numbers: f#_A(x1,x2) = max{x1 + 6, x2 - 9} f_A(x1,x2) = max{0, x1 - 8} a_A = 14 precedence: a > f > f# partial status: pi(f#) = [1] pi(f) = [] pi(a) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: f#_A(x1,x2) = 2 f_A(x1,x2) = 3 a_A = 0 precedence: f > f# > a partial status: pi(f#) = [] pi(f) = [] pi(a) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.