YES We show the termination of the TRS R: eq(|0|(),|0|()) -> true() eq(|0|(),s(m)) -> false() eq(s(n),|0|()) -> false() eq(s(n),s(m)) -> eq(n,m) le(|0|(),m) -> true() le(s(n),|0|()) -> false() le(s(n),s(m)) -> le(n,m) min(cons(|0|(),nil())) -> |0|() min(cons(s(n),nil())) -> s(n) min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) replace(n,m,nil()) -> nil() replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) if_replace(true(),n,m,cons(k,x)) -> cons(m,x) if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) |sort|(nil()) -> nil() |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x))) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: eq#(s(n),s(m)) -> eq#(n,m) p2: le#(s(n),s(m)) -> le#(n,m) p3: min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) p4: min#(cons(n,cons(m,x))) -> le#(n,m) p5: if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) p6: if_min#(false(),cons(n,cons(m,x))) -> min#(cons(m,x)) p7: replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) p8: replace#(n,m,cons(k,x)) -> eq#(n,k) p9: if_replace#(false(),n,m,cons(k,x)) -> replace#(n,m,x) p10: |sort|#(cons(n,x)) -> min#(cons(n,x)) p11: |sort|#(cons(n,x)) -> |sort|#(replace(min(cons(n,x)),n,x)) p12: |sort|#(cons(n,x)) -> replace#(min(cons(n,x)),n,x) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(m)) -> false() r3: eq(s(n),|0|()) -> false() r4: eq(s(n),s(m)) -> eq(n,m) r5: le(|0|(),m) -> true() r6: le(s(n),|0|()) -> false() r7: le(s(n),s(m)) -> le(n,m) r8: min(cons(|0|(),nil())) -> |0|() r9: min(cons(s(n),nil())) -> s(n) r10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) r11: if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) r12: if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) r13: replace(n,m,nil()) -> nil() r14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) r15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x) r16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) r17: |sort|(nil()) -> nil() r18: |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x))) The estimated dependency graph contains the following SCCs: {p11} {p7, p9} {p1} {p3, p5, p6} {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: |sort|#(cons(n,x)) -> |sort|#(replace(min(cons(n,x)),n,x)) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(m)) -> false() r3: eq(s(n),|0|()) -> false() r4: eq(s(n),s(m)) -> eq(n,m) r5: le(|0|(),m) -> true() r6: le(s(n),|0|()) -> false() r7: le(s(n),s(m)) -> le(n,m) r8: min(cons(|0|(),nil())) -> |0|() r9: min(cons(s(n),nil())) -> s(n) r10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) r11: if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) r12: if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) r13: replace(n,m,nil()) -> nil() r14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) r15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x) r16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) r17: |sort|(nil()) -> nil() r18: |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x))) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: |sort|#_A(x1) = max{2, x1} cons_A(x1,x2) = max{27, x2 + 25} replace_A(x1,x2,x3) = max{3, x3 + 1} min_A(x1) = 19 eq_A(x1,x2) = 3 |0|_A = 18 true_A = 3 s_A(x1) = 13 false_A = 0 le_A(x1,x2) = 3 if_min_A(x1,x2) = 19 if_replace_A(x1,x2,x3,x4) = max{x1 + 25, x4 + 1} nil_A = 1 precedence: nil > replace = le = if_replace > cons > |sort|# = min = eq = |0| = true = s = false = if_min partial status: pi(|sort|#) = [1] pi(cons) = [] pi(replace) = [] pi(min) = [] pi(eq) = [] pi(|0|) = [] pi(true) = [] pi(s) = [] pi(false) = [] pi(le) = [] pi(if_min) = [] pi(if_replace) = [] 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: if_replace#(false(),n,m,cons(k,x)) -> replace#(n,m,x) p2: replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(m)) -> false() r3: eq(s(n),|0|()) -> false() r4: eq(s(n),s(m)) -> eq(n,m) r5: le(|0|(),m) -> true() r6: le(s(n),|0|()) -> false() r7: le(s(n),s(m)) -> le(n,m) r8: min(cons(|0|(),nil())) -> |0|() r9: min(cons(s(n),nil())) -> s(n) r10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) r11: if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) r12: if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) r13: replace(n,m,nil()) -> nil() r14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) r15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x) r16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) r17: |sort|(nil()) -> nil() r18: |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x))) The set of usable rules consists of r1, r2, r3, r4 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: if_replace#_A(x1,x2,x3,x4) = max{5, x4 - 1} false_A = 10 cons_A(x1,x2) = max{6, x2 + 4} replace#_A(x1,x2,x3) = max{4, x3 + 2} eq_A(x1,x2) = max{9, x1, x2 - 12} |0|_A = 23 true_A = 10 s_A(x1) = max{23, x1 + 11} precedence: if_replace# = false = cons = replace# = eq = |0| = true = s partial status: pi(if_replace#) = [] pi(false) = [] pi(cons) = [2] pi(replace#) = [3] pi(eq) = [1] pi(|0|) = [] pi(true) = [] pi(s) = [1] 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: replace#(n,m,cons(k,x)) -> if_replace#(eq(n,k),n,m,cons(k,x)) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(m)) -> false() r3: eq(s(n),|0|()) -> false() r4: eq(s(n),s(m)) -> eq(n,m) r5: le(|0|(),m) -> true() r6: le(s(n),|0|()) -> false() r7: le(s(n),s(m)) -> le(n,m) r8: min(cons(|0|(),nil())) -> |0|() r9: min(cons(s(n),nil())) -> s(n) r10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) r11: if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) r12: if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) r13: replace(n,m,nil()) -> nil() r14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) r15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x) r16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) r17: |sort|(nil()) -> nil() r18: |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x))) The estimated dependency graph contains the following SCCs: (no SCCs) -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: eq#(s(n),s(m)) -> eq#(n,m) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(m)) -> false() r3: eq(s(n),|0|()) -> false() r4: eq(s(n),s(m)) -> eq(n,m) r5: le(|0|(),m) -> true() r6: le(s(n),|0|()) -> false() r7: le(s(n),s(m)) -> le(n,m) r8: min(cons(|0|(),nil())) -> |0|() r9: min(cons(s(n),nil())) -> s(n) r10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) r11: if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) r12: if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) r13: replace(n,m,nil()) -> nil() r14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) r15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x) r16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) r17: |sort|(nil()) -> nil() r18: |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x))) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: eq#_A(x1,x2) = max{0, x1 - 2, x2 - 2} s_A(x1) = max{3, x1 + 1} precedence: eq# = s partial status: pi(eq#) = [] pi(s) = [] 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: if_min#(false(),cons(n,cons(m,x))) -> min#(cons(m,x)) p2: min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) p3: if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(m)) -> false() r3: eq(s(n),|0|()) -> false() r4: eq(s(n),s(m)) -> eq(n,m) r5: le(|0|(),m) -> true() r6: le(s(n),|0|()) -> false() r7: le(s(n),s(m)) -> le(n,m) r8: min(cons(|0|(),nil())) -> |0|() r9: min(cons(s(n),nil())) -> s(n) r10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) r11: if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) r12: if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) r13: replace(n,m,nil()) -> nil() r14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) r15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x) r16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) r17: |sort|(nil()) -> nil() r18: |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x))) The set of usable rules consists of r5, r6, r7 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: if_min#_A(x1,x2) = max{13, x1 - 2, x2 + 6} false_A = 16 cons_A(x1,x2) = x2 + 4 min#_A(x1) = x1 + 10 le_A(x1,x2) = 19 true_A = 18 |0|_A = 17 s_A(x1) = max{38, x1 + 17} precedence: if_min# = false = cons = min# = le = true = |0| = s partial status: pi(if_min#) = [2] pi(false) = [] pi(cons) = [2] pi(min#) = [] pi(le) = [] pi(true) = [] pi(|0|) = [] pi(s) = [1] 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: min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) p2: if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(m)) -> false() r3: eq(s(n),|0|()) -> false() r4: eq(s(n),s(m)) -> eq(n,m) r5: le(|0|(),m) -> true() r6: le(s(n),|0|()) -> false() r7: le(s(n),s(m)) -> le(n,m) r8: min(cons(|0|(),nil())) -> |0|() r9: min(cons(s(n),nil())) -> s(n) r10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) r11: if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) r12: if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) r13: replace(n,m,nil()) -> nil() r14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) r15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x) r16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) r17: |sort|(nil()) -> nil() r18: |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x))) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) p2: if_min#(true(),cons(n,cons(m,x))) -> min#(cons(n,x)) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(m)) -> false() r3: eq(s(n),|0|()) -> false() r4: eq(s(n),s(m)) -> eq(n,m) r5: le(|0|(),m) -> true() r6: le(s(n),|0|()) -> false() r7: le(s(n),s(m)) -> le(n,m) r8: min(cons(|0|(),nil())) -> |0|() r9: min(cons(s(n),nil())) -> s(n) r10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) r11: if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) r12: if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) r13: replace(n,m,nil()) -> nil() r14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) r15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x) r16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) r17: |sort|(nil()) -> nil() r18: |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x))) The set of usable rules consists of r5, r6, r7 Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: min#_A(x1) = max{2, x1} cons_A(x1,x2) = max{x1 + 3, x2 + 3} if_min#_A(x1,x2) = max{x1 + 1, x2} le_A(x1,x2) = max{x1 + 2, x2 + 5} true_A = 6 |0|_A = 5 s_A(x1) = x1 + 4 false_A = 1 precedence: cons > min# = le = true = |0| = s = false > if_min# partial status: pi(min#) = [1] pi(cons) = [1, 2] pi(if_min#) = [1, 2] pi(le) = [] pi(true) = [] pi(|0|) = [] pi(s) = [1] pi(false) = [] 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: min#(cons(n,cons(m,x))) -> if_min#(le(n,m),cons(n,cons(m,x))) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(m)) -> false() r3: eq(s(n),|0|()) -> false() r4: eq(s(n),s(m)) -> eq(n,m) r5: le(|0|(),m) -> true() r6: le(s(n),|0|()) -> false() r7: le(s(n),s(m)) -> le(n,m) r8: min(cons(|0|(),nil())) -> |0|() r9: min(cons(s(n),nil())) -> s(n) r10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) r11: if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) r12: if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) r13: replace(n,m,nil()) -> nil() r14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) r15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x) r16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) r17: |sort|(nil()) -> nil() r18: |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x))) The estimated dependency graph contains the following SCCs: (no SCCs) -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: le#(s(n),s(m)) -> le#(n,m) and R consists of: r1: eq(|0|(),|0|()) -> true() r2: eq(|0|(),s(m)) -> false() r3: eq(s(n),|0|()) -> false() r4: eq(s(n),s(m)) -> eq(n,m) r5: le(|0|(),m) -> true() r6: le(s(n),|0|()) -> false() r7: le(s(n),s(m)) -> le(n,m) r8: min(cons(|0|(),nil())) -> |0|() r9: min(cons(s(n),nil())) -> s(n) r10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x))) r11: if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x)) r12: if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x)) r13: replace(n,m,nil()) -> nil() r14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x)) r15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x) r16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x)) r17: |sort|(nil()) -> nil() r18: |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x))) The set of usable rules consists of (no rules) Take the reduction pair: weighted path order base order: max/plus interpretations on natural numbers: le#_A(x1,x2) = max{0, x1 - 2, x2 - 2} s_A(x1) = max{3, x1 + 1} precedence: le# = s partial status: pi(le#) = [] pi(s) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.