YES We show the termination of the TRS R: f(cons(nil(),y)) -> y f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z) copy(|0|(),y,z) -> f(z) copy(s(x),y,z) -> copy(x,y,cons(f(y),z)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(cons(f(cons(nil(),y)),z)) -> copy#(n(),y,z) p2: copy#(|0|(),y,z) -> f#(z) p3: copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z)) p4: copy#(s(x),y,z) -> f#(y) and R consists of: r1: f(cons(nil(),y)) -> y r2: f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z) r3: copy(|0|(),y,z) -> f(z) r4: copy(s(x),y,z) -> copy(x,y,cons(f(y),z)) The estimated dependency graph contains the following SCCs: {p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z)) and R consists of: r1: f(cons(nil(),y)) -> y r2: f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z) r3: copy(|0|(),y,z) -> f(z) r4: copy(s(x),y,z) -> copy(x,y,cons(f(y),z)) The set of usable rules consists of r1, r2 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: copy#_A(x1,x2,x3) = max{0, x1 - 1} s_A(x1) = x1 + 5 cons_A(x1,x2) = max{x1 + 3, x2 + 9} f_A(x1) = x1 + 6 nil_A = 4 copy_A(x1,x2,x3) = max{x1 + 13, x2 + 24, x3 + 15} n_A = 6 precedence: s = cons = f = nil = copy = n > copy# partial status: pi(copy#) = [] pi(s) = [1] pi(cons) = [1] pi(f) = [1] pi(nil) = [] pi(copy) = [] pi(n) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.