YES We show the termination of the TRS R: app(nil(),y) -> y app(add(n,x),y) -> add(n,app(x,y)) reverse(nil()) -> nil() reverse(add(n,x)) -> app(reverse(x),add(n,nil())) shuffle(nil()) -> nil() shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(add(n,x),y) -> app#(x,y) p2: reverse#(add(n,x)) -> app#(reverse(x),add(n,nil())) p3: reverse#(add(n,x)) -> reverse#(x) p4: shuffle#(add(n,x)) -> shuffle#(reverse(x)) p5: shuffle#(add(n,x)) -> reverse#(x) and R consists of: r1: app(nil(),y) -> y r2: app(add(n,x),y) -> add(n,app(x,y)) r3: reverse(nil()) -> nil() r4: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r5: shuffle(nil()) -> nil() r6: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) The estimated dependency graph contains the following SCCs: {p4} {p3} {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: shuffle#(add(n,x)) -> shuffle#(reverse(x)) and R consists of: r1: app(nil(),y) -> y r2: app(add(n,x),y) -> add(n,app(x,y)) r3: reverse(nil()) -> nil() r4: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r5: shuffle(nil()) -> nil() r6: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) The set of usable rules consists of r1, r2, r3, r4 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: shuffle#_A(x1) = ((1,0),(0,0)) x1 + (1,1) add_A(x1,x2) = ((1,1),(0,0)) x1 + ((1,0),(0,0)) x2 + (3,1) reverse_A(x1) = ((1,0),(1,0)) x1 + (1,2) app_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (0,2) nil_A() = (0,1) precedence: reverse > shuffle# = add = app = nil partial status: pi(shuffle#) = [] pi(add) = [] pi(reverse) = [] pi(app) = [2] pi(nil) = [] The next rules are strictly ordered: p1 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: reverse#(add(n,x)) -> reverse#(x) and R consists of: r1: app(nil(),y) -> y r2: app(add(n,x),y) -> add(n,app(x,y)) r3: reverse(nil()) -> nil() r4: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r5: shuffle(nil()) -> nil() r6: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: reverse#_A(x1) = x1 + (1,1) add_A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (2,1) precedence: add > reverse# partial status: pi(reverse#) = [1] pi(add) = [2] The next rules are strictly ordered: p1 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: app#(add(n,x),y) -> app#(x,y) and R consists of: r1: app(nil(),y) -> y r2: app(add(n,x),y) -> add(n,app(x,y)) r3: reverse(nil()) -> nil() r4: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r5: shuffle(nil()) -> nil() r6: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: standard order interpretations: app#_A(x1,x2) = ((0,1),(0,0)) x1 + x2 + (2,2) add_A(x1,x2) = ((1,1),(1,1)) x1 + ((0,0),(0,1)) x2 + (1,1) precedence: app# = add partial status: pi(app#) = [] pi(add) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.