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