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