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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          sum2#_A(x1,x2) = max{x1 + 22, x2 + 23}
          cons_A(x1,x2) = max{x1 + 16, x2 + 22}
          +_A(x1,x2) = max{21, x2}
          |0|_A = 3
          s_A(x1) = max{18, x1 - 2}
          sum1_A(x1) = max{19, x1 + 4}
          nil_A = 0
          sum2_A(x1,x2) = max{22, x1 + 7, x2 + 8}
          tests_A(x1) = max{19, x1 + 9}
          true_A = 13
          and_A(x1,x2) = max{18, x1, x2 - 2}
          test_A(x1) = max{18, x1}
          rands_A(x1,x2) = x2 + 18
          rand_A(x1) = max{22, x1 + 3}
          done_A(x1) = max{17, x1 + 16}
          eq_A(x1,x2) = x2 + 14
          f_A(x1) = x1 + 17
          g_A(x1) = x1 + 1
          |::|_A(x1,x2) = max{x1 - 22, x2}
    
      precedence:
      
        sum2# > sum1 > g > cons = s = sum2 = tests > |0| = f > + = and > nil > eq > true = test = rands = rand = done = |::|
      
      partial status:
    
        pi(sum2#) = [1, 2]
        pi(cons) = []
        pi(+) = [2]
        pi(|0|) = []
        pi(s) = []
        pi(sum1) = []
        pi(nil) = []
        pi(sum2) = [1]
        pi(tests) = [1]
        pi(true) = []
        pi(and) = [1]
        pi(test) = [1]
        pi(rands) = []
        pi(rand) = []
        pi(done) = [1]
        pi(eq) = [2]
        pi(f) = [1]
        pi(g) = [1]
        pi(|::|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          sum2#_A(x1,x2) = max{x1 - 1, x2 + 1}
          cons_A(x1,x2) = 2
          +_A(x1,x2) = max{30, x2 + 29}
          |0|_A = 12
          s_A(x1) = 30
          sum1_A(x1) = 3
          nil_A = 18
          sum2_A(x1,x2) = 0
          tests_A(x1) = x1 + 4
          true_A = 13
          and_A(x1,x2) = x1 + 40
          test_A(x1) = max{30, x1 + 2}
          rands_A(x1,x2) = 28
          rand_A(x1) = 29
          done_A(x1) = x1 + 27
          eq_A(x1,x2) = max{30, x2 + 14}
          f_A(x1) = max{14, x1 + 13}
          g_A(x1) = max{16, x1 + 15}
          |::|_A(x1,x2) = 14
    
      precedence:
      
        + > sum2# = cons = |0| = s = sum1 = nil > |::| > and > sum2 = tests = true = test = rands = rand = done = eq = f = g
      
      partial status:
    
        pi(sum2#) = [2]
        pi(cons) = []
        pi(+) = []
        pi(|0|) = []
        pi(s) = []
        pi(sum1) = []
        pi(nil) = []
        pi(sum2) = []
        pi(tests) = [1]
        pi(true) = []
        pi(and) = [1]
        pi(test) = [1]
        pi(rands) = []
        pi(rand) = []
        pi(done) = []
        pi(eq) = [2]
        pi(f) = [1]
        pi(g) = [1]
        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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          sum1#_A(x1) = x1 + 4
          cons_A(x1,x2) = max{x1 + 4, x2 + 4}
          +_A(x1,x2) = max{x1 + 8, x2}
          |0|_A = 6
          s_A(x1) = x1
          sum1_A(x1) = x1 + 4
          nil_A = 5
          sum2_A(x1,x2) = max{x1 + 5, x2 + 1}
          tests_A(x1) = x1 + 60
          true_A = 4
          and_A(x1,x2) = max{27, x1 - 9, x2 + 1}
          test_A(x1) = x1 + 6
          rands_A(x1,x2) = max{x1 + 27, x2 + 14}
          rand_A(x1) = x1 + 29
          done_A(x1) = x1 + 4
          eq_A(x1,x2) = max{x1 + 5, x2 + 5}
          f_A(x1) = x1 + 5
          g_A(x1) = x1 + 5
          |::|_A(x1,x2) = max{4, x1 - 22}
    
      precedence:
      
        + = |0| = sum1 > nil > s = sum2 = true = and = test = done = eq = f = |::| > sum1# = g > cons = tests = rands = rand
      
      partial status:
    
        pi(sum1#) = [1]
        pi(cons) = [1, 2]
        pi(+) = [1, 2]
        pi(|0|) = []
        pi(s) = []
        pi(sum1) = [1]
        pi(nil) = []
        pi(sum2) = [1]
        pi(tests) = [1]
        pi(true) = []
        pi(and) = []
        pi(test) = [1]
        pi(rands) = []
        pi(rand) = []
        pi(done) = [1]
        pi(eq) = []
        pi(f) = [1]
        pi(g) = [1]
        pi(|::|) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          sum1#_A(x1) = x1 + 1
          cons_A(x1,x2) = max{x1 - 23, x2}
          +_A(x1,x2) = max{x1 - 9, x2 + 19}
          |0|_A = 43
          s_A(x1) = 28
          sum1_A(x1) = x1 + 13
          nil_A = 31
          sum2_A(x1,x2) = max{0, x1 - 1}
          tests_A(x1) = max{21, x1 + 17}
          true_A = 59
          and_A(x1,x2) = 46
          test_A(x1) = max{46, x1 + 9}
          rands_A(x1,x2) = 22
          rand_A(x1) = 27
          done_A(x1) = x1 + 48
          eq_A(x1,x2) = 58
          f_A(x1) = x1 + 58
          g_A(x1) = x1 + 58
          |::|_A(x1,x2) = 26
    
      precedence:
      
        sum1# = cons = + = |0| = s = sum1 = nil = sum2 = true = and = test = rands = rand > tests = done = eq = f = g = |::|
      
      partial status:
    
        pi(sum1#) = []
        pi(cons) = [2]
        pi(+) = []
        pi(|0|) = []
        pi(s) = []
        pi(sum1) = []
        pi(nil) = []
        pi(sum2) = []
        pi(tests) = [1]
        pi(true) = []
        pi(and) = []
        pi(test) = [1]
        pi(rands) = []
        pi(rand) = []
        pi(done) = [1]
        pi(eq) = []
        pi(f) = [1]
        pi(g) = [1]
        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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          +#_A(x1,x2) = x1 + 1
          s_A(x1) = max{11, x1}
          +_A(x1,x2) = max{2, x1, x2}
          |0|_A = 0
          sum1_A(x1) = max{11, x1 + 6}
          nil_A = 1
          cons_A(x1,x2) = max{x1 + 5, x2 + 6}
          sum2_A(x1,x2) = max{x1, x2 + 4}
          tests_A(x1) = max{42, x1 + 41}
          true_A = 6
          and_A(x1,x2) = max{12, x1 + 2, x2 - 1}
          test_A(x1) = max{4, x1}
          rands_A(x1,x2) = max{x1 + 30, x2 + 9}
          rand_A(x1) = max{19, x1 + 7}
          done_A(x1) = max{8, x1 + 7}
          eq_A(x1,x2) = max{x1 + 5, x2 + 7}
          f_A(x1) = max{3, x1 + 2}
          g_A(x1) = max{1, x1}
          |::|_A(x1,x2) = max{20, x1 + 1, x2}
    
      precedence:
      
        sum2 > and = done > tests > sum1 = cons > +# = true = g = |::| > |0| = eq > test > + > f > s = nil = rands = rand
      
      partial status:
    
        pi(+#) = [1]
        pi(s) = [1]
        pi(+) = [1, 2]
        pi(|0|) = []
        pi(sum1) = []
        pi(nil) = []
        pi(cons) = [1, 2]
        pi(sum2) = [1, 2]
        pi(tests) = [1]
        pi(true) = []
        pi(and) = [1]
        pi(test) = [1]
        pi(rands) = [1, 2]
        pi(rand) = []
        pi(done) = [1]
        pi(eq) = [1, 2]
        pi(f) = [1]
        pi(g) = [1]
        pi(|::|) = [1, 2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          +#_A(x1,x2) = max{62, x1}
          s_A(x1) = max{62, x1 + 2}
          +_A(x1,x2) = max{62, x2}
          |0|_A = 19
          sum1_A(x1) = 2
          nil_A = 1
          cons_A(x1,x2) = max{x1 + 1, x2 + 1}
          sum2_A(x1,x2) = max{x1 + 125, x2 + 64}
          tests_A(x1) = x1 + 30
          true_A = 38
          and_A(x1,x2) = max{63, x1 + 30}
          test_A(x1) = x1 + 40
          rands_A(x1,x2) = max{x1 + 15, x2 + 20}
          rand_A(x1) = 6
          done_A(x1) = x1 + 36
          eq_A(x1,x2) = max{x1 + 39, x2 + 42}
          f_A(x1) = x1 + 37
          g_A(x1) = x1 + 34
          |::|_A(x1,x2) = max{77, x1 - 2, x2 + 20}
    
      precedence:
      
        +# = s = + = |0| = sum1 = nil = cons = sum2 = true = and = test = rands = rand = done > tests = eq = f = g = |::|
      
      partial status:
    
        pi(+#) = [1]
        pi(s) = []
        pi(+) = [2]
        pi(|0|) = []
        pi(sum1) = []
        pi(nil) = []
        pi(cons) = [2]
        pi(sum2) = [1, 2]
        pi(tests) = [1]
        pi(true) = []
        pi(and) = [1]
        pi(test) = [1]
        pi(rands) = [2]
        pi(rand) = []
        pi(done) = []
        pi(eq) = [1, 2]
        pi(f) = [1]
        pi(g) = [1]
        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:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          rands#_A(x1,x2) = max{x1 + 124, x2 + 144}
          s_A(x1) = max{20, x1}
          |::|_A(x1,x2) = 0
          rand_A(x1) = max{49, x1 + 21}
          |0|_A = 42
          +_A(x1,x2) = max{41, x1 + 21, x2}
          sum1_A(x1) = max{41, x1 + 40}
          nil_A = 3
          cons_A(x1,x2) = max{x1 + 41, x2 + 41}
          sum2_A(x1,x2) = max{x1 + 45, x2 + 43}
          tests_A(x1) = x1 + 116
          true_A = 3
          and_A(x1,x2) = max{19, x1 - 12, x2 + 1}
          test_A(x1) = max{137, x1 + 3}
          rands_A(x1,x2) = max{x1 + 49, x2 + 142}
          done_A(x1) = x1 + 141
          eq_A(x1,x2) = max{144, x1 + 4, x2 + 4}
          f_A(x1) = max{138, x1 + 137}
          g_A(x1) = x1 + 140
    
      precedence:
      
        cons > rands > |::| = + = test = eq = f > |0| = sum1 = g > s = nil = tests = true = and = done > rands# > rand = sum2
      
      partial status:
    
        pi(rands#) = [1]
        pi(s) = [1]
        pi(|::|) = []
        pi(rand) = []
        pi(|0|) = []
        pi(+) = [1, 2]
        pi(sum1) = [1]
        pi(nil) = []
        pi(cons) = [2]
        pi(sum2) = []
        pi(tests) = [1]
        pi(true) = []
        pi(and) = []
        pi(test) = [1]
        pi(rands) = [1, 2]
        pi(done) = [1]
        pi(eq) = [1, 2]
        pi(f) = [1]
        pi(g) = [1]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          rands#_A(x1,x2) = x1 + 14
          s_A(x1) = x1 + 78
          |::|_A(x1,x2) = 0
          rand_A(x1) = 45
          |0|_A = 43
          +_A(x1,x2) = max{x1, x2 + 55}
          sum1_A(x1) = max{3, x1 + 1}
          nil_A = 55
          cons_A(x1,x2) = max{2, x2}
          sum2_A(x1,x2) = 0
          tests_A(x1) = max{54, x1 - 74}
          true_A = 80
          and_A(x1,x2) = 79
          test_A(x1) = x1 + 70
          rands_A(x1,x2) = max{x1 - 34, x2 + 22}
          done_A(x1) = x1 + 22
          eq_A(x1,x2) = max{x1 + 85, x2 + 71}
          f_A(x1) = x1 + 7
          g_A(x1) = x1 + 21
    
      precedence:
      
        rands# = s = rand = |0| = + = sum1 = nil = cons = tests = true = and = test = rands = done = eq = f > sum2 = g > |::|
      
      partial status:
    
        pi(rands#) = [1]
        pi(s) = [1]
        pi(|::|) = []
        pi(rand) = []
        pi(|0|) = []
        pi(+) = [1, 2]
        pi(sum1) = []
        pi(nil) = []
        pi(cons) = [2]
        pi(sum2) = []
        pi(tests) = []
        pi(true) = []
        pi(and) = []
        pi(test) = [1]
        pi(rands) = [2]
        pi(done) = []
        pi(eq) = [2]
        pi(f) = [1]
        pi(g) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.