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: max/plus interpretations on natural numbers: |sort|#_A(x1) = max{0, x1 - 3} cons_A(x1,x2) = x2 + 13 replace_A(x1,x2,x3) = x3 min_A(x1) = max{0, x1 - 11} eq_A(x1,x2) = 0 |0|_A = 1 true_A = 0 s_A(x1) = 1 false_A = 0 le_A(x1,x2) = 16 if_min_A(x1,x2) = max{1, x2 - 18} if_replace_A(x1,x2,x3,x4) = max{x1 + 12, x4} nil_A = 1 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: max/plus interpretations on natural numbers: if_replace#_A(x1,x2,x3,x4) = max{x1 + 1, x4 - 2} false_A = 0 cons_A(x1,x2) = max{x1 + 3, x2 + 3} replace#_A(x1,x2,x3) = max{1, x3} eq_A(x1,x2) = 1 |0|_A = 0 true_A = 0 s_A(x1) = max{0, x1 - 1} 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: if_replace#(false(),n,m,cons(k,x)) -> replace#(n,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: 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: max/plus interpretations on natural numbers: eq#_A(x1,x2) = max{x1 + 1, x2 + 1} s_A(x1) = x1 + 1 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: max/plus interpretations on natural numbers: if_min#_A(x1,x2) = max{x1 + 3, x2} false_A = 0 cons_A(x1,x2) = max{x1 + 5, x2 + 1} min#_A(x1) = max{1, x1} le_A(x1,x2) = 0 true_A = 0 |0|_A = 0 s_A(x1) = max{0, x1 - 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: max/plus interpretations on natural numbers: min#_A(x1) = x1 + 1 cons_A(x1,x2) = x2 + 1 if_min#_A(x1,x2) = max{x1 + 1, x2 + 1} le_A(x1,x2) = 0 true_A = 0 |0|_A = 0 s_A(x1) = max{0, x1 - 1} false_A = 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: 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: max/plus interpretations on natural numbers: le#_A(x1,x2) = max{x1 + 1, x2 + 1} s_A(x1) = x1 + 1 The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.