YES We show the termination of the relative TRS R/S: R: +(|0|(),y) -> y +(s(x),y) -> s(+(x,y)) sum1(nil()) -> |0|() sum1(cons(x,y)) -> +(x,sum1(y)) sum2(nil(),z) -> z sum2(cons(x,y),z) -> sum2(y,+(x,z)) tests(|0|()) -> true() tests(s(x)) -> and(test(rands(rand(|0|()),nil())),x) test(done(y)) -> eq(f(y),g(y)) eq(x,x) -> true() rands(|0|(),y) -> done(y) rands(s(x),y) -> rands(x,|::|(rand(|0|()),y)) 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: +#(s(x),y) -> +#(x,y) p2: sum1#(cons(x,y)) -> +#(x,sum1(y)) p3: sum1#(cons(x,y)) -> sum1#(y) p4: sum2#(cons(x,y),z) -> sum2#(y,+(x,z)) p5: sum2#(cons(x,y),z) -> +#(x,z) p6: tests#(s(x)) -> test#(rands(rand(|0|()),nil())) p7: tests#(s(x)) -> rands#(rand(|0|()),nil()) p8: test#(done(y)) -> eq#(f(y),g(y)) p9: rands#(s(x),y) -> rands#(x,|::|(rand(|0|()),y)) and R consists of: r1: +(|0|(),y) -> y r2: +(s(x),y) -> s(+(x,y)) r3: sum1(nil()) -> |0|() r4: sum1(cons(x,y)) -> +(x,sum1(y)) r5: sum2(nil(),z) -> z r6: sum2(cons(x,y),z) -> sum2(y,+(x,z)) r7: tests(|0|()) -> true() r8: tests(s(x)) -> and(test(rands(rand(|0|()),nil())),x) r9: test(done(y)) -> eq(f(y),g(y)) r10: eq(x,x) -> true() r11: rands(|0|(),y) -> done(y) r12: rands(s(x),y) -> rands(x,|::|(rand(|0|()),y)) r13: rand(x) -> x r14: rand(x) -> rand(s(x)) The estimated dependency graph contains the following SCCs: {p4} {p3} {p1} {p9} -- Reduction pair. Consider the non-minimal dependency pair problem (P, R), where P consists of p1: sum2#(cons(x,y),z) -> sum2#(y,+(x,z)) and R consists of: r1: +(|0|(),y) -> y r2: +(s(x),y) -> s(+(x,y)) r3: sum1(nil()) -> |0|() r4: sum1(cons(x,y)) -> +(x,sum1(y)) r5: sum2(nil(),z) -> z r6: sum2(cons(x,y),z) -> sum2(y,+(x,z)) r7: tests(|0|()) -> true() r8: tests(s(x)) -> and(test(rands(rand(|0|()),nil())),x) r9: test(done(y)) -> eq(f(y),g(y)) r10: eq(x,x) -> true() r11: rands(|0|(),y) -> done(y) r12: rands(s(x),y) -> rands(x,|::|(rand(|0|()),y)) r13: rand(x) -> x r14: 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: sum2#_A(x1,x2) = ((1,0),(1,1)) x1 + ((0,0),(1,0)) x2 + (1,1) cons_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (2,1) +_A(x1,x2) = x2 + (1,0) |0|_A() = (4,8) s_A(x1) = (0,2) sum1_A(x1) = x1 + (3,2) nil_A() = (8,7) sum2_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (2,1) tests_A(x1) = x1 + (7,4) true_A() = (1,1) and_A(x1,x2) = (0,1) test_A(x1) = (3,3) rands_A(x1,x2) = (5,7) rand_A(x1) = ((1,0),(1,0)) x1 + (2,1) done_A(x1) = ((0,0),(1,0)) x1 + (3,9) eq_A(x1,x2) = (2,0) f_A(x1) = (1,4) g_A(x1) = (1,4) |::|_A(x1,x2) = (1,3) precedence: + = tests = and = rand = eq > s = sum2 = rands > |0| = test = done = f > sum2# = cons > |::| > sum1 = nil = true = g partial status: pi(sum2#) = [1] pi(cons) = [] pi(+) = [] pi(|0|) = [] pi(s) = [] pi(sum1) = [1] pi(nil) = [] pi(sum2) = [2] pi(tests) = [] pi(true) = [] pi(and) = [] pi(test) = [] pi(rands) = [] pi(rand) = [] pi(done) = [] pi(eq) = [] pi(f) = [] pi(g) = [] pi(|::|) = [] 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: sum1#(cons(x,y)) -> sum1#(y) and R consists of: r1: +(|0|(),y) -> y r2: +(s(x),y) -> s(+(x,y)) r3: sum1(nil()) -> |0|() r4: sum1(cons(x,y)) -> +(x,sum1(y)) r5: sum2(nil(),z) -> z r6: sum2(cons(x,y),z) -> sum2(y,+(x,z)) r7: tests(|0|()) -> true() r8: tests(s(x)) -> and(test(rands(rand(|0|()),nil())),x) r9: test(done(y)) -> eq(f(y),g(y)) r10: eq(x,x) -> true() r11: rands(|0|(),y) -> done(y) r12: rands(s(x),y) -> rands(x,|::|(rand(|0|()),y)) r13: rand(x) -> x r14: 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: sum1#_A(x1) = ((1,0),(0,0)) x1 cons_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (6,2) +_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (4,3) |0|_A() = (4,5) s_A(x1) = ((0,0),(1,0)) x1 sum1_A(x1) = x1 + (1,1) nil_A() = (5,6) sum2_A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (3,1) tests_A(x1) = x1 + (6,3) true_A() = (1,4) and_A(x1,x2) = x1 + (2,2) test_A(x1) = (3,2) rands_A(x1,x2) = (7,6) rand_A(x1) = ((1,0),(1,1)) x1 + (4,1) done_A(x1) = (3,2) eq_A(x1,x2) = (2,3) f_A(x1) = (1,1) g_A(x1) = (1,3) |::|_A(x1,x2) = (1,0) precedence: cons = + = |0| = sum1 = nil = test = rand > s > sum2 > tests = and = |::| > sum1# = true = rands = done = eq = f = g partial status: pi(sum1#) = [] pi(cons) = [] pi(+) = [] pi(|0|) = [] pi(s) = [] pi(sum1) = [] pi(nil) = [] pi(sum2) = [] pi(tests) = [1] pi(true) = [] pi(and) = [] pi(test) = [] pi(rands) = [] pi(rand) = [] pi(done) = [] pi(eq) = [] pi(f) = [] pi(g) = [] pi(|::|) = [] 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: +#(s(x),y) -> +#(x,y) and R consists of: r1: +(|0|(),y) -> y r2: +(s(x),y) -> s(+(x,y)) r3: sum1(nil()) -> |0|() r4: sum1(cons(x,y)) -> +(x,sum1(y)) r5: sum2(nil(),z) -> z r6: sum2(cons(x,y),z) -> sum2(y,+(x,z)) r7: tests(|0|()) -> true() r8: tests(s(x)) -> and(test(rands(rand(|0|()),nil())),x) r9: test(done(y)) -> eq(f(y),g(y)) r10: eq(x,x) -> true() r11: rands(|0|(),y) -> done(y) r12: rands(s(x),y) -> rands(x,|::|(rand(|0|()),y)) r13: rand(x) -> x r14: 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: +#_A(x1,x2) = x1 s_A(x1) = x1 +_A(x1,x2) = x1 + x2 + (1,4) |0|_A() = (4,3) sum1_A(x1) = x1 + (1,1) nil_A() = (5,4) cons_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (3,6) sum2_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (3,3) tests_A(x1) = ((1,0),(0,0)) x1 + (7,1) true_A() = (1,2) and_A(x1,x2) = (0,2) test_A(x1) = x1 + (1,2) rands_A(x1,x2) = ((1,0),(1,1)) x1 + (5,4) rand_A(x1) = ((1,0),(1,1)) x1 + (2,1) done_A(x1) = ((0,0),(1,0)) x1 + (3,12) eq_A(x1,x2) = (2,11) f_A(x1) = (2,11) g_A(x1) = (1,13) |::|_A(x1,x2) = (1,1) precedence: + > s > sum1 > cons > +# > |0| = nil = tests = true = and = rand > sum2 > |::| > rands = done = eq = f > test = g partial status: pi(+#) = [1] pi(s) = [1] pi(+) = [1] pi(|0|) = [] pi(sum1) = [1] pi(nil) = [] pi(cons) = [] pi(sum2) = [2] pi(tests) = [] pi(true) = [] pi(and) = [] pi(test) = [1] pi(rands) = [] pi(rand) = [] pi(done) = [] pi(eq) = [] pi(f) = [] pi(g) = [] pi(|::|) = [] 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: rands#(s(x),y) -> rands#(x,|::|(rand(|0|()),y)) and R consists of: r1: +(|0|(),y) -> y r2: +(s(x),y) -> s(+(x,y)) r3: sum1(nil()) -> |0|() r4: sum1(cons(x,y)) -> +(x,sum1(y)) r5: sum2(nil(),z) -> z r6: sum2(cons(x,y),z) -> sum2(y,+(x,z)) r7: tests(|0|()) -> true() r8: tests(s(x)) -> and(test(rands(rand(|0|()),nil())),x) r9: test(done(y)) -> eq(f(y),g(y)) r10: eq(x,x) -> true() r11: rands(|0|(),y) -> done(y) r12: rands(s(x),y) -> rands(x,|::|(rand(|0|()),y)) r13: rand(x) -> x r14: 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 Take the reduction pair: weighted path order base order: matrix interpretations: carrier: N^2 order: lexicographic order interpretations: rands#_A(x1,x2) = x1 + (8,6) s_A(x1) = x1 + (0,1) |::|_A(x1,x2) = (1,0) rand_A(x1) = ((1,0),(1,0)) x1 + (3,2) |0|_A() = (4,2) +_A(x1,x2) = x1 + x2 + (1,0) sum1_A(x1) = x1 + (5,1) nil_A() = (0,0) cons_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (7,3) sum2_A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (0,1) tests_A(x1) = ((1,0),(1,1)) x1 + (6,2) true_A() = (1,9) and_A(x1,x2) = (0,0) test_A(x1) = (3,4) rands_A(x1,x2) = (5,4) done_A(x1) = (3,5) eq_A(x1,x2) = (2,10) f_A(x1) = (0,0) g_A(x1) = (0,0) precedence: rand > rands# = |::| > + > nil > |0| = sum1 > cons > sum2 = tests = and = rands > true = done = eq = g > s = test = f partial status: pi(rands#) = [1] pi(s) = [] pi(|::|) = [] pi(rand) = [] pi(|0|) = [] pi(+) = [1, 2] pi(sum1) = [1] pi(nil) = [] pi(cons) = [] pi(sum2) = [1, 2] pi(tests) = [] pi(true) = [] pi(and) = [] pi(test) = [] pi(rands) = [] pi(done) = [] pi(eq) = [] pi(f) = [] pi(g) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.