YES We show the termination of the TRS R: |sort|(nil()) -> nil() |sort|(cons(x,y)) -> insert(x,|sort|(y)) insert(x,nil()) -> cons(x,nil()) insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v) choose(x,cons(v,w),y,|0|()) -> cons(x,cons(v,w)) choose(x,cons(v,w),|0|(),s(z)) -> cons(v,insert(x,w)) choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: |sort|#(cons(x,y)) -> insert#(x,|sort|(y)) p2: |sort|#(cons(x,y)) -> |sort|#(y) p3: insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v) p4: choose#(x,cons(v,w),|0|(),s(z)) -> insert#(x,w) p5: choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z) and R consists of: r1: |sort|(nil()) -> nil() r2: |sort|(cons(x,y)) -> insert(x,|sort|(y)) r3: insert(x,nil()) -> cons(x,nil()) r4: insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v) r5: choose(x,cons(v,w),y,|0|()) -> cons(x,cons(v,w)) r6: choose(x,cons(v,w),|0|(),s(z)) -> cons(v,insert(x,w)) r7: choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z) The estimated dependency graph contains the following SCCs: {p2} {p3, p4, p5} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: |sort|#(cons(x,y)) -> |sort|#(y) and R consists of: r1: |sort|(nil()) -> nil() r2: |sort|(cons(x,y)) -> insert(x,|sort|(y)) r3: insert(x,nil()) -> cons(x,nil()) r4: insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v) r5: choose(x,cons(v,w),y,|0|()) -> cons(x,cons(v,w)) r6: choose(x,cons(v,w),|0|(),s(z)) -> cons(v,insert(x,w)) r7: choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: |sort|#_A(x1) = x1 + (1,2) cons_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (2,1) precedence: cons > |sort|# partial status: pi(|sort|#) = [1] pi(cons) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: |sort|#_A(x1) = (0,0) cons_A(x1,x2) = (1,1) precedence: |sort|# > cons partial status: pi(|sort|#) = [] pi(cons) = [] 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: insert#(x,cons(v,w)) -> choose#(x,cons(v,w),x,v) p2: choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z) p3: choose#(x,cons(v,w),|0|(),s(z)) -> insert#(x,w) and R consists of: r1: |sort|(nil()) -> nil() r2: |sort|(cons(x,y)) -> insert(x,|sort|(y)) r3: insert(x,nil()) -> cons(x,nil()) r4: insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v) r5: choose(x,cons(v,w),y,|0|()) -> cons(x,cons(v,w)) r6: choose(x,cons(v,w),|0|(),s(z)) -> cons(v,insert(x,w)) r7: choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: insert#_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (2,4) cons_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (3,1) choose#_A(x1,x2,x3,x4) = ((1,0),(0,0)) x2 + (1,3) s_A(x1) = x1 + (5,2) |0|_A() = (1,5) precedence: insert# = cons = choose# = s = |0| partial status: pi(insert#) = [2] pi(cons) = [2] pi(choose#) = [] pi(s) = [1] pi(|0|) = [] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: insert#_A(x1,x2) = ((1,0),(0,0)) x2 + (3,2) cons_A(x1,x2) = ((1,0),(0,0)) x2 + (1,0) choose#_A(x1,x2,x3,x4) = (0,0) s_A(x1) = ((1,0),(0,0)) x1 + (2,1) |0|_A() = (1,1) precedence: insert# = s > |0| > cons = choose# partial status: pi(insert#) = [] pi(cons) = [] pi(choose#) = [] pi(s) = [] pi(|0|) = [] The next rules are strictly ordered: p1, p3 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z) and R consists of: r1: |sort|(nil()) -> nil() r2: |sort|(cons(x,y)) -> insert(x,|sort|(y)) r3: insert(x,nil()) -> cons(x,nil()) r4: insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v) r5: choose(x,cons(v,w),y,|0|()) -> cons(x,cons(v,w)) r6: choose(x,cons(v,w),|0|(),s(z)) -> cons(v,insert(x,w)) r7: choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: choose#(x,cons(v,w),s(y),s(z)) -> choose#(x,cons(v,w),y,z) and R consists of: r1: |sort|(nil()) -> nil() r2: |sort|(cons(x,y)) -> insert(x,|sort|(y)) r3: insert(x,nil()) -> cons(x,nil()) r4: insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v) r5: choose(x,cons(v,w),y,|0|()) -> cons(x,cons(v,w)) r6: choose(x,cons(v,w),|0|(),s(z)) -> cons(v,insert(x,w)) r7: choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: choose#_A(x1,x2,x3,x4) = x4 cons_A(x1,x2) = x1 + (1,1) s_A(x1) = x1 precedence: choose# = cons = s partial status: pi(choose#) = [4] pi(cons) = [1] pi(s) = [1] 2. weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: choose#_A(x1,x2,x3,x4) = x4 + (1,0) cons_A(x1,x2) = x1 + (3,2) s_A(x1) = x1 + (2,1) precedence: cons = s > choose# partial status: pi(choose#) = [4] pi(cons) = [1] pi(s) = [1] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.