YES We show the termination of the relative TRS R/S: R: minus(x,|0|()) -> x minus(s(x),s(y)) -> minus(x,y) quot(|0|(),s(y)) -> |0|() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) 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))) concat(leaf(),y) -> y concat(cons(u,v),y) -> cons(u,concat(v,y)) less_leaves(x,leaf()) -> false() less_leaves(leaf(),cons(w,z)) -> true() less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z)) S: rand(x) -> x rand(x) -> rand(s(x)) -- SCC decomposition. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: minus#(s(x),s(y)) -> minus#(x,y) p2: quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) p3: quot#(s(x),s(y)) -> minus#(x,y) p4: app#(add(n,x),y) -> app#(x,y) p5: reverse#(add(n,x)) -> app#(reverse(x),add(n,nil())) p6: reverse#(add(n,x)) -> reverse#(x) p7: shuffle#(add(n,x)) -> shuffle#(reverse(x)) p8: shuffle#(add(n,x)) -> reverse#(x) p9: concat#(cons(u,v),y) -> concat#(v,y) p10: less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z)) p11: less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v) p12: less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z) and R consists of: r1: minus(x,|0|()) -> x r2: minus(s(x),s(y)) -> minus(x,y) r3: quot(|0|(),s(y)) -> |0|() r4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) r5: app(nil(),y) -> y r6: app(add(n,x),y) -> add(n,app(x,y)) r7: reverse(nil()) -> nil() r8: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r9: shuffle(nil()) -> nil() r10: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) r11: concat(leaf(),y) -> y r12: concat(cons(u,v),y) -> cons(u,concat(v,y)) r13: less_leaves(x,leaf()) -> false() r14: less_leaves(leaf(),cons(w,z)) -> true() r15: less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z)) r16: rand(x) -> x r17: rand(x) -> rand(s(x)) The estimated dependency graph contains the following SCCs: {p2} {p1} {p7} {p6} {p4} {p10} {p9} -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) and R consists of: r1: minus(x,|0|()) -> x r2: minus(s(x),s(y)) -> minus(x,y) r3: quot(|0|(),s(y)) -> |0|() r4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) r5: app(nil(),y) -> y r6: app(add(n,x),y) -> add(n,app(x,y)) r7: reverse(nil()) -> nil() r8: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r9: shuffle(nil()) -> nil() r10: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) r11: concat(leaf(),y) -> y r12: concat(cons(u,v),y) -> cons(u,concat(v,y)) r13: less_leaves(x,leaf()) -> false() r14: less_leaves(leaf(),cons(w,z)) -> true() r15: less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z)) r16: rand(x) -> x r17: rand(x) -> rand(s(x)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^4 order: lexicographic order interpretations: quot#_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(0,0,1,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x2 s_A(x1) = x1 + (0,0,2,1) minus_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,0,1,1)) x1 + (0,0,0,1) |0|_A() = (1,0,1,3) quot_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,0,1,0)) x1 + ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x2 + (1,1,1,1) app_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,1,0,0)) x2 + (3,2,5,1) nil_A() = (1,1,0,0) add_A(x1,x2) = ((0,0,0,0),(1,0,0,0),(1,1,0,0),(0,0,1,0)) x1 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x2 + (2,1,1,4) reverse_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,1,0,0)) x1 + (4,1,7,1) shuffle_A(x1) = ((1,0,0,0),(0,1,0,0),(1,0,0,0),(1,1,0,0)) x1 + (1,1,0,0) concat_A(x1,x2) = ((1,0,0,0),(1,0,0,0),(0,1,0,0),(1,1,1,0)) x1 + ((1,0,0,0),(1,0,0,0),(1,1,0,0),(1,0,1,0)) x2 + (4,1,1,1) leaf_A() = (1,1,1,1) cons_A(x1,x2) = ((1,0,0,0),(1,0,0,0),(1,0,0,0),(1,0,0,0)) x1 + ((1,0,0,0),(1,0,0,0),(1,0,0,0),(1,1,0,0)) x2 + (6,2,0,5) less_leaves_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,0,0),(1,0,1,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,1,0,0)) x2 + (0,0,1,0) false_A() = (0,2,3,3) true_A() = (0,0,0,0) rand_A(x1) = x1 + (1,1,1,1) 2. lexicographic path order with precedence: precedence: less_leaves > rand > quot# > quot > false > true > s > leaf > shuffle > minus > nil > reverse > |0| > concat > add > app > cons argument filter: pi(quot#) = [2] pi(s) = 1 pi(minus) = 1 pi(|0|) = [] pi(quot) = [] pi(app) = [] pi(nil) = [] pi(add) = [] pi(reverse) = [] pi(shuffle) = [] pi(concat) = [] pi(leaf) = [] pi(cons) = [] pi(less_leaves) = [] pi(false) = [] pi(true) = [] pi(rand) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: minus#(s(x),s(y)) -> minus#(x,y) and R consists of: r1: minus(x,|0|()) -> x r2: minus(s(x),s(y)) -> minus(x,y) r3: quot(|0|(),s(y)) -> |0|() r4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) r5: app(nil(),y) -> y r6: app(add(n,x),y) -> add(n,app(x,y)) r7: reverse(nil()) -> nil() r8: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r9: shuffle(nil()) -> nil() r10: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) r11: concat(leaf(),y) -> y r12: concat(cons(u,v),y) -> cons(u,concat(v,y)) r13: less_leaves(x,leaf()) -> false() r14: less_leaves(leaf(),cons(w,z)) -> true() r15: less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z)) r16: rand(x) -> x r17: rand(x) -> rand(s(x)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^4 order: lexicographic order interpretations: minus#_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,0,0),(0,0,1,0)) x1 + ((0,0,0,0),(1,0,0,0),(0,0,0,0),(0,1,0,0)) x2 s_A(x1) = ((1,0,0,0),(1,1,0,0),(0,0,1,0),(0,0,0,1)) x1 + (0,1,1,1) minus_A(x1,x2) = x1 |0|_A() = (1,1,1,1) quot_A(x1,x2) = x1 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,1,0,0)) x2 + (0,1,1,0) app_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,1,1,0),(0,1,1,1)) x2 + (2,1,1,1) nil_A() = (1,3,1,1) add_A(x1,x2) = ((0,0,0,0),(1,0,0,0),(1,1,0,0),(1,1,1,0)) x1 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x2 + (1,2,1,1) reverse_A(x1) = ((0,0,0,0),(1,0,0,0),(1,1,0,0),(1,1,1,0)) x1 + (4,1,1,11) shuffle_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x1 + (1,0,1,0) concat_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,3,2,1) leaf_A() = (1,1,1,1) cons_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(0,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (2,1,1,1) less_leaves_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,1,1,1)) x2 false_A() = (0,0,0,5) true_A() = (0,0,0,0) rand_A(x1) = x1 + (1,1,1,1) 2. lexicographic path order with precedence: precedence: quot > minus# > s > rand > cons > less_leaves > concat > shuffle > leaf > minus > true > false > add > reverse > nil > app > |0| argument filter: pi(minus#) = [] pi(s) = [1] pi(minus) = [1] pi(|0|) = [] pi(quot) = [1] pi(app) = [] pi(nil) = [] pi(add) = [] pi(reverse) = [] pi(shuffle) = [] pi(concat) = 1 pi(leaf) = [] pi(cons) = [1, 2] pi(less_leaves) = 1 pi(false) = [] pi(true) = [] pi(rand) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: shuffle#(add(n,x)) -> shuffle#(reverse(x)) and R consists of: r1: minus(x,|0|()) -> x r2: minus(s(x),s(y)) -> minus(x,y) r3: quot(|0|(),s(y)) -> |0|() r4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) r5: app(nil(),y) -> y r6: app(add(n,x),y) -> add(n,app(x,y)) r7: reverse(nil()) -> nil() r8: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r9: shuffle(nil()) -> nil() r10: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) r11: concat(leaf(),y) -> y r12: concat(cons(u,v),y) -> cons(u,concat(v,y)) r13: less_leaves(x,leaf()) -> false() r14: less_leaves(leaf(),cons(w,z)) -> true() r15: less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z)) r16: rand(x) -> x r17: rand(x) -> rand(s(x)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^4 order: lexicographic order interpretations: shuffle#_A(x1) = ((0,0,0,0),(1,0,0,0),(0,1,0,0),(0,0,1,0)) x1 add_A(x1,x2) = ((0,0,0,0),(1,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + ((1,0,0,0),(0,1,0,0),(1,1,0,0),(0,0,1,0)) x2 + (1,3,4,1) reverse_A(x1) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(0,0,1,1)) x1 + (0,0,3,5) minus_A(x1,x2) = x1 + (1,1,1,0) |0|_A() = (1,1,1,2) s_A(x1) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + (0,0,3,0) quot_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + ((0,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x2 + (2,2,2,0) app_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(1,1,0,0),(0,0,1,0)) x1 + ((1,0,0,0),(0,1,0,0),(1,1,1,0),(0,0,1,1)) x2 + (0,0,1,0) nil_A() = (0,0,1,1) shuffle_A(x1) = ((1,0,0,0),(1,1,0,0),(0,1,1,0),(1,1,1,0)) x1 + (5,0,1,1) concat_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,5,0,0) leaf_A() = (1,1,1,1) cons_A(x1,x2) = x1 + ((1,0,0,0),(0,0,0,0),(0,0,0,0),(0,1,0,0)) x2 + (10,1,1,1) less_leaves_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(0,0,1,0),(0,0,0,1)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x2 false_A() = (0,2,0,0) true_A() = (0,3,2,4) rand_A(x1) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(0,0,0,0)) x1 + (1,1,1,1) 2. lexicographic path order with precedence: precedence: cons > reverse > concat > nil > shuffle > app > add > |0| > quot > minus > shuffle# > rand > less_leaves > leaf > false > true > s argument filter: pi(shuffle#) = [] pi(add) = [] pi(reverse) = [1] pi(minus) = [] pi(|0|) = [] pi(s) = [] pi(quot) = [] pi(app) = [2] pi(nil) = [] pi(shuffle) = [] pi(concat) = 1 pi(leaf) = [] pi(cons) = [] pi(less_leaves) = 1 pi(false) = [] pi(true) = [] pi(rand) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: reverse#(add(n,x)) -> reverse#(x) and R consists of: r1: minus(x,|0|()) -> x r2: minus(s(x),s(y)) -> minus(x,y) r3: quot(|0|(),s(y)) -> |0|() r4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) r5: app(nil(),y) -> y r6: app(add(n,x),y) -> add(n,app(x,y)) r7: reverse(nil()) -> nil() r8: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r9: shuffle(nil()) -> nil() r10: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) r11: concat(leaf(),y) -> y r12: concat(cons(u,v),y) -> cons(u,concat(v,y)) r13: less_leaves(x,leaf()) -> false() r14: less_leaves(leaf(),cons(w,z)) -> true() r15: less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z)) r16: rand(x) -> x r17: rand(x) -> rand(s(x)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^4 order: lexicographic order interpretations: reverse#_A(x1) = ((1,0,0,0),(1,1,0,0),(1,0,0,0),(1,0,0,0)) x1 add_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x2 + (1,1,1,1) minus_A(x1,x2) = x1 + (1,1,1,1) |0|_A() = (0,1,5,0) s_A(x1) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(1,1,1,0)) x1 + (0,1,1,1) quot_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,0,0,0)) x2 + (1,1,2,10) app_A(x1,x2) = ((1,0,0,0),(1,0,0,0),(0,1,0,0),(0,0,1,0)) x1 + x2 + (0,1,1,1) nil_A() = (0,1,1,1) reverse_A(x1) = ((1,0,0,0),(1,1,0,0),(0,0,0,0),(1,0,1,0)) x1 + (0,1,3,3) shuffle_A(x1) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(1,1,1,1)) x1 + (2,1,0,0) concat_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(1,0,0,0),(0,0,1,0)) x1 + ((1,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x2 + (1,1,0,0) leaf_A() = (1,0,0,0) cons_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(1,0,0,0),(1,1,0,0)) x1 + ((1,0,0,0),(0,1,0,0),(1,0,0,0),(1,1,1,0)) x2 + (3,0,0,0) less_leaves_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,0,0,0)) x1 + ((1,0,0,0),(1,1,0,0),(0,0,1,0),(0,1,0,0)) x2 false_A() = (0,2,1,1) true_A() = (0,0,1,0) rand_A(x1) = x1 + (1,1,1,1) 2. lexicographic path order with precedence: precedence: leaf > concat > app > add > reverse > shuffle > nil > reverse# > quot > s > rand > less_leaves > cons > |0| > true > false > minus argument filter: pi(reverse#) = [] pi(add) = [] pi(minus) = [] pi(|0|) = [] pi(s) = [] pi(quot) = [] pi(app) = [] pi(nil) = [] pi(reverse) = [] pi(shuffle) = [1] pi(concat) = [] pi(leaf) = [] pi(cons) = [] pi(less_leaves) = [] pi(false) = [] pi(true) = [] pi(rand) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: app#(add(n,x),y) -> app#(x,y) and R consists of: r1: minus(x,|0|()) -> x r2: minus(s(x),s(y)) -> minus(x,y) r3: quot(|0|(),s(y)) -> |0|() r4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) r5: app(nil(),y) -> y r6: app(add(n,x),y) -> add(n,app(x,y)) r7: reverse(nil()) -> nil() r8: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r9: shuffle(nil()) -> nil() r10: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) r11: concat(leaf(),y) -> y r12: concat(cons(u,v),y) -> cons(u,concat(v,y)) r13: less_leaves(x,leaf()) -> false() r14: less_leaves(leaf(),cons(w,z)) -> true() r15: less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z)) r16: rand(x) -> x r17: rand(x) -> rand(s(x)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^4 order: lexicographic order interpretations: app#_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(1,0,1,1)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x2 add_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(1,0,0,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,0,1,0)) x2 + (2,0,1,1) minus_A(x1,x2) = x1 + (1,1,1,0) |0|_A() = (1,1,4,3) s_A(x1) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + (0,0,1,1) quot_A(x1,x2) = ((0,0,0,0),(1,0,0,0),(0,0,0,0),(0,1,0,0)) x2 + (2,0,3,2) app_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(1,1,0,0),(1,1,0,0)) x1 + ((1,0,0,0),(0,1,0,0),(1,0,1,0),(1,0,1,1)) x2 + (0,0,1,1) nil_A() = (0,0,0,0) reverse_A(x1) = ((1,0,0,0),(0,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + (0,0,2,2) shuffle_A(x1) = ((1,0,0,0),(1,1,0,0),(0,1,1,0),(0,0,0,0)) x1 + (0,1,1,1) concat_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,0)) x2 + (1,1,1,1) leaf_A() = (1,1,1,1) cons_A(x1,x2) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(1,1,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(1,1,0,0),(0,1,1,0)) x2 + (2,2,1,1) less_leaves_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,0,0),(1,1,1,0)) x2 false_A() = (0,2,1,4) true_A() = (0,2,3,10) rand_A(x1) = x1 + (1,1,1,1) 2. lexicographic path order with precedence: precedence: quot > s > minus > rand > leaf > reverse > true > less_leaves > app > |0| > add > shuffle > false > cons > nil > concat > app# argument filter: pi(app#) = [] pi(add) = [] pi(minus) = [] pi(|0|) = [] pi(s) = [] pi(quot) = [] pi(app) = [2] pi(nil) = [] pi(reverse) = [1] pi(shuffle) = [] pi(concat) = [] pi(leaf) = [] pi(cons) = [] pi(less_leaves) = [1] pi(false) = [] pi(true) = [] pi(rand) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z)) and R consists of: r1: minus(x,|0|()) -> x r2: minus(s(x),s(y)) -> minus(x,y) r3: quot(|0|(),s(y)) -> |0|() r4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) r5: app(nil(),y) -> y r6: app(add(n,x),y) -> add(n,app(x,y)) r7: reverse(nil()) -> nil() r8: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r9: shuffle(nil()) -> nil() r10: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) r11: concat(leaf(),y) -> y r12: concat(cons(u,v),y) -> cons(u,concat(v,y)) r13: less_leaves(x,leaf()) -> false() r14: less_leaves(leaf(),cons(w,z)) -> true() r15: less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z)) r16: rand(x) -> x r17: rand(x) -> rand(s(x)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^4 order: lexicographic order interpretations: less_leaves#_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + ((1,0,0,0),(1,1,0,0),(0,1,1,0),(1,1,0,1)) x2 cons_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(0,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (3,2,1,1) concat_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(0,1,0,0),(1,1,1,0),(1,1,1,1)) x2 + (1,1,3,7) minus_A(x1,x2) = x1 + (1,1,1,1) |0|_A() = (0,0,0,3) s_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (0,1,1,1) quot_A(x1,x2) = x2 + (1,2,1,1) app_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,0,0),(0,0,1,0)) x2 + (0,2,3,1) nil_A() = (1,1,4,12) add_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x1 + ((0,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x2 + (0,1,4,1) reverse_A(x1) = ((1,0,0,0),(1,0,0,0),(1,1,0,0),(1,1,1,0)) x1 + (0,4,1,5) shuffle_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x1 + (0,1,1,0) leaf_A() = (1,1,1,1) less_leaves_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,1,1,1)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(1,1,1,1)) x2 false_A() = (0,0,2,5) true_A() = (0,0,0,0) rand_A(x1) = x1 + (1,1,1,1) 2. lexicographic path order with precedence: precedence: quot > s > true > cons > leaf > reverse > app > add > shuffle > concat > false > minus > nil > |0| > rand > less_leaves# > less_leaves argument filter: pi(less_leaves#) = [] pi(cons) = [1] pi(concat) = 1 pi(minus) = [] pi(|0|) = [] pi(s) = [] pi(quot) = [2] pi(app) = [] pi(nil) = [] pi(add) = [] pi(reverse) = [] pi(shuffle) = [] pi(leaf) = [] pi(less_leaves) = 2 pi(false) = [] pi(true) = [] pi(rand) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: concat#(cons(u,v),y) -> concat#(v,y) and R consists of: r1: minus(x,|0|()) -> x r2: minus(s(x),s(y)) -> minus(x,y) r3: quot(|0|(),s(y)) -> |0|() r4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) r5: app(nil(),y) -> y r6: app(add(n,x),y) -> add(n,app(x,y)) r7: reverse(nil()) -> nil() r8: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) r9: shuffle(nil()) -> nil() r10: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) r11: concat(leaf(),y) -> y r12: concat(cons(u,v),y) -> cons(u,concat(v,y)) r13: less_leaves(x,leaf()) -> false() r14: less_leaves(leaf(),cons(w,z)) -> true() r15: less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z)) r16: rand(x) -> x r17: rand(x) -> rand(s(x)) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17 Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^4 order: lexicographic order interpretations: concat#_A(x1,x2) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(1,1,0,0)) x1 + ((0,0,0,0),(1,0,0,0),(0,1,0,0),(0,1,1,0)) x2 cons_A(x1,x2) = ((1,0,0,0),(1,0,0,0),(0,1,0,0),(1,1,1,0)) x1 + ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x2 + (3,1,2,0) minus_A(x1,x2) = x1 + (1,1,1,1) |0|_A() = (1,1,1,1) s_A(x1) = ((1,0,0,0),(1,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + (0,0,0,1) quot_A(x1,x2) = (2,3,0,2) app_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,0,1,1)) x2 + (1,2,1,2) nil_A() = (1,1,0,1) add_A(x1,x2) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(0,1,0,0),(0,0,0,0)) x2 + (0,1,0,2) reverse_A(x1) = ((1,0,0,0),(1,1,0,0),(0,1,1,0),(1,0,0,0)) x1 + (3,1,0,1) shuffle_A(x1) = ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x1 + (2,2,0,0) concat_A(x1,x2) = ((1,0,0,0),(1,0,0,0),(0,1,0,0),(1,1,1,0)) x1 + ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,1,0,0)) x2 + (1,2,0,0) leaf_A() = (1,0,1,1) less_leaves_A(x1,x2) = ((0,0,0,0),(1,0,0,0),(1,1,0,0),(0,1,0,0)) x1 + ((1,0,0,0),(0,1,0,0),(1,1,1,0),(0,1,0,0)) x2 + (0,1,0,1) false_A() = (0,0,1,0) true_A() = (0,0,8,3) rand_A(x1) = x1 + (1,0,1,1) 2. lexicographic path order with precedence: precedence: rand > less_leaves > concat > cons > true > false > leaf > reverse > quot > s > minus > shuffle > nil > app > add > |0| > concat# argument filter: pi(concat#) = [] pi(cons) = [] pi(minus) = [] pi(|0|) = [] pi(s) = [] pi(quot) = [] pi(app) = [] pi(nil) = [] pi(add) = [] pi(reverse) = [] pi(shuffle) = [] pi(concat) = [] pi(leaf) = [] pi(less_leaves) = [] pi(false) = [] pi(true) = [] pi(rand) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.