YES We show the termination of the TRS R: a(a(y,|0|()),|0|()) -> y c(c(y)) -> y c(a(c(c(y)),x)) -> a(c(c(c(a(x,|0|())))),y) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,|0|())))),y) p2: c#(a(c(c(y)),x)) -> c#(c(c(a(x,|0|())))) p3: c#(a(c(c(y)),x)) -> c#(c(a(x,|0|()))) p4: c#(a(c(c(y)),x)) -> c#(a(x,|0|())) p5: c#(a(c(c(y)),x)) -> a#(x,|0|()) and R consists of: r1: a(a(y,|0|()),|0|()) -> y r2: c(c(y)) -> y r3: c(a(c(c(y)),x)) -> a(c(c(c(a(x,|0|())))),y) The estimated dependency graph contains the following SCCs: {p2, p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: c#(a(c(c(y)),x)) -> c#(c(c(a(x,|0|())))) p2: c#(a(c(c(y)),x)) -> c#(a(x,|0|())) p3: c#(a(c(c(y)),x)) -> c#(c(a(x,|0|()))) and R consists of: r1: a(a(y,|0|()),|0|()) -> y r2: c(c(y)) -> y r3: c(a(c(c(y)),x)) -> a(c(c(c(a(x,|0|())))),y) The set of usable rules consists of r1, r2, r3 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: c#_A(x1) = x1 + 26 a_A(x1,x2) = max{37, x1 + 3, x2 + 17} c_A(x1) = max{42, x1 + 5} |0|_A = 6 precedence: a = c = |0| > c# partial status: pi(c#) = [1] pi(a) = [] pi(c) = [] pi(|0|) = [] 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: c#(a(c(c(y)),x)) -> c#(c(c(a(x,|0|())))) p2: c#(a(c(c(y)),x)) -> c#(a(x,|0|())) and R consists of: r1: a(a(y,|0|()),|0|()) -> y r2: c(c(y)) -> y r3: c(a(c(c(y)),x)) -> a(c(c(c(a(x,|0|())))),y) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: c#(a(c(c(y)),x)) -> c#(c(c(a(x,|0|())))) p2: c#(a(c(c(y)),x)) -> c#(a(x,|0|())) and R consists of: r1: a(a(y,|0|()),|0|()) -> y r2: c(c(y)) -> y r3: c(a(c(c(y)),x)) -> a(c(c(c(a(x,|0|())))),y) The set of usable rules consists of r1, r2, r3 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: c#_A(x1) = max{30, x1 + 18} a_A(x1,x2) = max{x1 + 1, x2 + 14} c_A(x1) = max{21, x1 + 6} |0|_A = 1 precedence: a = c = |0| > c# partial status: pi(c#) = [1] pi(a) = [] pi(c) = [] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: c#(a(c(c(y)),x)) -> c#(a(x,|0|())) and R consists of: r1: a(a(y,|0|()),|0|()) -> y r2: c(c(y)) -> y r3: c(a(c(c(y)),x)) -> a(c(c(c(a(x,|0|())))),y) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: c#(a(c(c(y)),x)) -> c#(a(x,|0|())) and R consists of: r1: a(a(y,|0|()),|0|()) -> y r2: c(c(y)) -> y r3: c(a(c(c(y)),x)) -> a(c(c(c(a(x,|0|())))),y) The set of usable rules consists of r1 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: c#_A(x1) = x1 + 11 a_A(x1,x2) = max{x1, x2 + 7} c_A(x1) = x1 + 5 |0|_A = 2 precedence: c# = a = c = |0| partial status: pi(c#) = [1] pi(a) = [1] pi(c) = [1] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.