YES

We show the termination of the TRS R:

  f_0(x) -> a()
  f_1(x) -> g_1(x,x)
  g_1(s(x),y) -> b(f_0(y),g_1(x,y))
  f_2(x) -> g_2(x,x)
  g_2(s(x),y) -> b(f_1(y),g_2(x,y))
  f_3(x) -> g_3(x,x)
  g_3(s(x),y) -> b(f_2(y),g_3(x,y))
  f_4(x) -> g_4(x,x)
  g_4(s(x),y) -> b(f_3(y),g_4(x,y))
  f_5(x) -> g_5(x,x)
  g_5(s(x),y) -> b(f_4(y),g_5(x,y))
  f_6(x) -> g_6(x,x)
  g_6(s(x),y) -> b(f_5(y),g_6(x,y))
  f_7(x) -> g_7(x,x)
  g_7(s(x),y) -> b(f_6(y),g_7(x,y))
  f_8(x) -> g_8(x,x)
  g_8(s(x),y) -> b(f_7(y),g_8(x,y))
  f_9(x) -> g_9(x,x)
  g_9(s(x),y) -> b(f_8(y),g_9(x,y))
  f_10(x) -> g_10(x,x)
  g_10(s(x),y) -> b(f_9(y),g_10(x,y))

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: f_1#(x) -> g_1#(x,x)
p2: g_1#(s(x),y) -> f_0#(y)
p3: g_1#(s(x),y) -> g_1#(x,y)
p4: f_2#(x) -> g_2#(x,x)
p5: g_2#(s(x),y) -> f_1#(y)
p6: g_2#(s(x),y) -> g_2#(x,y)
p7: f_3#(x) -> g_3#(x,x)
p8: g_3#(s(x),y) -> f_2#(y)
p9: g_3#(s(x),y) -> g_3#(x,y)
p10: f_4#(x) -> g_4#(x,x)
p11: g_4#(s(x),y) -> f_3#(y)
p12: g_4#(s(x),y) -> g_4#(x,y)
p13: f_5#(x) -> g_5#(x,x)
p14: g_5#(s(x),y) -> f_4#(y)
p15: g_5#(s(x),y) -> g_5#(x,y)
p16: f_6#(x) -> g_6#(x,x)
p17: g_6#(s(x),y) -> f_5#(y)
p18: g_6#(s(x),y) -> g_6#(x,y)
p19: f_7#(x) -> g_7#(x,x)
p20: g_7#(s(x),y) -> f_6#(y)
p21: g_7#(s(x),y) -> g_7#(x,y)
p22: f_8#(x) -> g_8#(x,x)
p23: g_8#(s(x),y) -> f_7#(y)
p24: g_8#(s(x),y) -> g_8#(x,y)
p25: f_9#(x) -> g_9#(x,x)
p26: g_9#(s(x),y) -> f_8#(y)
p27: g_9#(s(x),y) -> g_9#(x,y)
p28: f_10#(x) -> g_10#(x,x)
p29: g_10#(s(x),y) -> f_9#(y)
p30: g_10#(s(x),y) -> g_10#(x,y)

and R consists of:

r1: f_0(x) -> a()
r2: f_1(x) -> g_1(x,x)
r3: g_1(s(x),y) -> b(f_0(y),g_1(x,y))
r4: f_2(x) -> g_2(x,x)
r5: g_2(s(x),y) -> b(f_1(y),g_2(x,y))
r6: f_3(x) -> g_3(x,x)
r7: g_3(s(x),y) -> b(f_2(y),g_3(x,y))
r8: f_4(x) -> g_4(x,x)
r9: g_4(s(x),y) -> b(f_3(y),g_4(x,y))
r10: f_5(x) -> g_5(x,x)
r11: g_5(s(x),y) -> b(f_4(y),g_5(x,y))
r12: f_6(x) -> g_6(x,x)
r13: g_6(s(x),y) -> b(f_5(y),g_6(x,y))
r14: f_7(x) -> g_7(x,x)
r15: g_7(s(x),y) -> b(f_6(y),g_7(x,y))
r16: f_8(x) -> g_8(x,x)
r17: g_8(s(x),y) -> b(f_7(y),g_8(x,y))
r18: f_9(x) -> g_9(x,x)
r19: g_9(s(x),y) -> b(f_8(y),g_9(x,y))
r20: f_10(x) -> g_10(x,x)
r21: g_10(s(x),y) -> b(f_9(y),g_10(x,y))

The estimated dependency graph contains the following SCCs:

  {p30}
  {p27}
  {p24}
  {p21}
  {p18}
  {p15}
  {p12}
  {p9}
  {p6}
  {p3}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: g_10#(s(x),y) -> g_10#(x,y)

and R consists of:

r1: f_0(x) -> a()
r2: f_1(x) -> g_1(x,x)
r3: g_1(s(x),y) -> b(f_0(y),g_1(x,y))
r4: f_2(x) -> g_2(x,x)
r5: g_2(s(x),y) -> b(f_1(y),g_2(x,y))
r6: f_3(x) -> g_3(x,x)
r7: g_3(s(x),y) -> b(f_2(y),g_3(x,y))
r8: f_4(x) -> g_4(x,x)
r9: g_4(s(x),y) -> b(f_3(y),g_4(x,y))
r10: f_5(x) -> g_5(x,x)
r11: g_5(s(x),y) -> b(f_4(y),g_5(x,y))
r12: f_6(x) -> g_6(x,x)
r13: g_6(s(x),y) -> b(f_5(y),g_6(x,y))
r14: f_7(x) -> g_7(x,x)
r15: g_7(s(x),y) -> b(f_6(y),g_7(x,y))
r16: f_8(x) -> g_8(x,x)
r17: g_8(s(x),y) -> b(f_7(y),g_8(x,y))
r18: f_9(x) -> g_9(x,x)
r19: g_9(s(x),y) -> b(f_8(y),g_9(x,y))
r20: f_10(x) -> g_10(x,x)
r21: g_10(s(x),y) -> b(f_9(y),g_10(x,y))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      g_10#_A(x1,x2) = x1
      s_A(x1) = ((1,0),(1,1)) x1 + (1,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: g_9#(s(x),y) -> g_9#(x,y)

and R consists of:

r1: f_0(x) -> a()
r2: f_1(x) -> g_1(x,x)
r3: g_1(s(x),y) -> b(f_0(y),g_1(x,y))
r4: f_2(x) -> g_2(x,x)
r5: g_2(s(x),y) -> b(f_1(y),g_2(x,y))
r6: f_3(x) -> g_3(x,x)
r7: g_3(s(x),y) -> b(f_2(y),g_3(x,y))
r8: f_4(x) -> g_4(x,x)
r9: g_4(s(x),y) -> b(f_3(y),g_4(x,y))
r10: f_5(x) -> g_5(x,x)
r11: g_5(s(x),y) -> b(f_4(y),g_5(x,y))
r12: f_6(x) -> g_6(x,x)
r13: g_6(s(x),y) -> b(f_5(y),g_6(x,y))
r14: f_7(x) -> g_7(x,x)
r15: g_7(s(x),y) -> b(f_6(y),g_7(x,y))
r16: f_8(x) -> g_8(x,x)
r17: g_8(s(x),y) -> b(f_7(y),g_8(x,y))
r18: f_9(x) -> g_9(x,x)
r19: g_9(s(x),y) -> b(f_8(y),g_9(x,y))
r20: f_10(x) -> g_10(x,x)
r21: g_10(s(x),y) -> b(f_9(y),g_10(x,y))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      g_9#_A(x1,x2) = x1
      s_A(x1) = ((1,0),(1,1)) x1 + (1,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: g_8#(s(x),y) -> g_8#(x,y)

and R consists of:

r1: f_0(x) -> a()
r2: f_1(x) -> g_1(x,x)
r3: g_1(s(x),y) -> b(f_0(y),g_1(x,y))
r4: f_2(x) -> g_2(x,x)
r5: g_2(s(x),y) -> b(f_1(y),g_2(x,y))
r6: f_3(x) -> g_3(x,x)
r7: g_3(s(x),y) -> b(f_2(y),g_3(x,y))
r8: f_4(x) -> g_4(x,x)
r9: g_4(s(x),y) -> b(f_3(y),g_4(x,y))
r10: f_5(x) -> g_5(x,x)
r11: g_5(s(x),y) -> b(f_4(y),g_5(x,y))
r12: f_6(x) -> g_6(x,x)
r13: g_6(s(x),y) -> b(f_5(y),g_6(x,y))
r14: f_7(x) -> g_7(x,x)
r15: g_7(s(x),y) -> b(f_6(y),g_7(x,y))
r16: f_8(x) -> g_8(x,x)
r17: g_8(s(x),y) -> b(f_7(y),g_8(x,y))
r18: f_9(x) -> g_9(x,x)
r19: g_9(s(x),y) -> b(f_8(y),g_9(x,y))
r20: f_10(x) -> g_10(x,x)
r21: g_10(s(x),y) -> b(f_9(y),g_10(x,y))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      g_8#_A(x1,x2) = x1
      s_A(x1) = ((1,0),(1,1)) x1 + (1,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: g_7#(s(x),y) -> g_7#(x,y)

and R consists of:

r1: f_0(x) -> a()
r2: f_1(x) -> g_1(x,x)
r3: g_1(s(x),y) -> b(f_0(y),g_1(x,y))
r4: f_2(x) -> g_2(x,x)
r5: g_2(s(x),y) -> b(f_1(y),g_2(x,y))
r6: f_3(x) -> g_3(x,x)
r7: g_3(s(x),y) -> b(f_2(y),g_3(x,y))
r8: f_4(x) -> g_4(x,x)
r9: g_4(s(x),y) -> b(f_3(y),g_4(x,y))
r10: f_5(x) -> g_5(x,x)
r11: g_5(s(x),y) -> b(f_4(y),g_5(x,y))
r12: f_6(x) -> g_6(x,x)
r13: g_6(s(x),y) -> b(f_5(y),g_6(x,y))
r14: f_7(x) -> g_7(x,x)
r15: g_7(s(x),y) -> b(f_6(y),g_7(x,y))
r16: f_8(x) -> g_8(x,x)
r17: g_8(s(x),y) -> b(f_7(y),g_8(x,y))
r18: f_9(x) -> g_9(x,x)
r19: g_9(s(x),y) -> b(f_8(y),g_9(x,y))
r20: f_10(x) -> g_10(x,x)
r21: g_10(s(x),y) -> b(f_9(y),g_10(x,y))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      g_7#_A(x1,x2) = ((1,0),(1,0)) x1
      s_A(x1) = ((1,0),(1,1)) x1 + (1,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: g_6#(s(x),y) -> g_6#(x,y)

and R consists of:

r1: f_0(x) -> a()
r2: f_1(x) -> g_1(x,x)
r3: g_1(s(x),y) -> b(f_0(y),g_1(x,y))
r4: f_2(x) -> g_2(x,x)
r5: g_2(s(x),y) -> b(f_1(y),g_2(x,y))
r6: f_3(x) -> g_3(x,x)
r7: g_3(s(x),y) -> b(f_2(y),g_3(x,y))
r8: f_4(x) -> g_4(x,x)
r9: g_4(s(x),y) -> b(f_3(y),g_4(x,y))
r10: f_5(x) -> g_5(x,x)
r11: g_5(s(x),y) -> b(f_4(y),g_5(x,y))
r12: f_6(x) -> g_6(x,x)
r13: g_6(s(x),y) -> b(f_5(y),g_6(x,y))
r14: f_7(x) -> g_7(x,x)
r15: g_7(s(x),y) -> b(f_6(y),g_7(x,y))
r16: f_8(x) -> g_8(x,x)
r17: g_8(s(x),y) -> b(f_7(y),g_8(x,y))
r18: f_9(x) -> g_9(x,x)
r19: g_9(s(x),y) -> b(f_8(y),g_9(x,y))
r20: f_10(x) -> g_10(x,x)
r21: g_10(s(x),y) -> b(f_9(y),g_10(x,y))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      g_6#_A(x1,x2) = x1
      s_A(x1) = ((1,0),(1,1)) x1 + (1,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: g_5#(s(x),y) -> g_5#(x,y)

and R consists of:

r1: f_0(x) -> a()
r2: f_1(x) -> g_1(x,x)
r3: g_1(s(x),y) -> b(f_0(y),g_1(x,y))
r4: f_2(x) -> g_2(x,x)
r5: g_2(s(x),y) -> b(f_1(y),g_2(x,y))
r6: f_3(x) -> g_3(x,x)
r7: g_3(s(x),y) -> b(f_2(y),g_3(x,y))
r8: f_4(x) -> g_4(x,x)
r9: g_4(s(x),y) -> b(f_3(y),g_4(x,y))
r10: f_5(x) -> g_5(x,x)
r11: g_5(s(x),y) -> b(f_4(y),g_5(x,y))
r12: f_6(x) -> g_6(x,x)
r13: g_6(s(x),y) -> b(f_5(y),g_6(x,y))
r14: f_7(x) -> g_7(x,x)
r15: g_7(s(x),y) -> b(f_6(y),g_7(x,y))
r16: f_8(x) -> g_8(x,x)
r17: g_8(s(x),y) -> b(f_7(y),g_8(x,y))
r18: f_9(x) -> g_9(x,x)
r19: g_9(s(x),y) -> b(f_8(y),g_9(x,y))
r20: f_10(x) -> g_10(x,x)
r21: g_10(s(x),y) -> b(f_9(y),g_10(x,y))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      g_5#_A(x1,x2) = ((1,0),(1,0)) x1
      s_A(x1) = ((1,0),(1,1)) x1 + (1,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: g_4#(s(x),y) -> g_4#(x,y)

and R consists of:

r1: f_0(x) -> a()
r2: f_1(x) -> g_1(x,x)
r3: g_1(s(x),y) -> b(f_0(y),g_1(x,y))
r4: f_2(x) -> g_2(x,x)
r5: g_2(s(x),y) -> b(f_1(y),g_2(x,y))
r6: f_3(x) -> g_3(x,x)
r7: g_3(s(x),y) -> b(f_2(y),g_3(x,y))
r8: f_4(x) -> g_4(x,x)
r9: g_4(s(x),y) -> b(f_3(y),g_4(x,y))
r10: f_5(x) -> g_5(x,x)
r11: g_5(s(x),y) -> b(f_4(y),g_5(x,y))
r12: f_6(x) -> g_6(x,x)
r13: g_6(s(x),y) -> b(f_5(y),g_6(x,y))
r14: f_7(x) -> g_7(x,x)
r15: g_7(s(x),y) -> b(f_6(y),g_7(x,y))
r16: f_8(x) -> g_8(x,x)
r17: g_8(s(x),y) -> b(f_7(y),g_8(x,y))
r18: f_9(x) -> g_9(x,x)
r19: g_9(s(x),y) -> b(f_8(y),g_9(x,y))
r20: f_10(x) -> g_10(x,x)
r21: g_10(s(x),y) -> b(f_9(y),g_10(x,y))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      g_4#_A(x1,x2) = x1
      s_A(x1) = ((1,0),(1,1)) x1 + (1,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: g_3#(s(x),y) -> g_3#(x,y)

and R consists of:

r1: f_0(x) -> a()
r2: f_1(x) -> g_1(x,x)
r3: g_1(s(x),y) -> b(f_0(y),g_1(x,y))
r4: f_2(x) -> g_2(x,x)
r5: g_2(s(x),y) -> b(f_1(y),g_2(x,y))
r6: f_3(x) -> g_3(x,x)
r7: g_3(s(x),y) -> b(f_2(y),g_3(x,y))
r8: f_4(x) -> g_4(x,x)
r9: g_4(s(x),y) -> b(f_3(y),g_4(x,y))
r10: f_5(x) -> g_5(x,x)
r11: g_5(s(x),y) -> b(f_4(y),g_5(x,y))
r12: f_6(x) -> g_6(x,x)
r13: g_6(s(x),y) -> b(f_5(y),g_6(x,y))
r14: f_7(x) -> g_7(x,x)
r15: g_7(s(x),y) -> b(f_6(y),g_7(x,y))
r16: f_8(x) -> g_8(x,x)
r17: g_8(s(x),y) -> b(f_7(y),g_8(x,y))
r18: f_9(x) -> g_9(x,x)
r19: g_9(s(x),y) -> b(f_8(y),g_9(x,y))
r20: f_10(x) -> g_10(x,x)
r21: g_10(s(x),y) -> b(f_9(y),g_10(x,y))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      g_3#_A(x1,x2) = ((1,0),(1,0)) x1
      s_A(x1) = ((1,0),(1,1)) x1 + (1,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: g_2#(s(x),y) -> g_2#(x,y)

and R consists of:

r1: f_0(x) -> a()
r2: f_1(x) -> g_1(x,x)
r3: g_1(s(x),y) -> b(f_0(y),g_1(x,y))
r4: f_2(x) -> g_2(x,x)
r5: g_2(s(x),y) -> b(f_1(y),g_2(x,y))
r6: f_3(x) -> g_3(x,x)
r7: g_3(s(x),y) -> b(f_2(y),g_3(x,y))
r8: f_4(x) -> g_4(x,x)
r9: g_4(s(x),y) -> b(f_3(y),g_4(x,y))
r10: f_5(x) -> g_5(x,x)
r11: g_5(s(x),y) -> b(f_4(y),g_5(x,y))
r12: f_6(x) -> g_6(x,x)
r13: g_6(s(x),y) -> b(f_5(y),g_6(x,y))
r14: f_7(x) -> g_7(x,x)
r15: g_7(s(x),y) -> b(f_6(y),g_7(x,y))
r16: f_8(x) -> g_8(x,x)
r17: g_8(s(x),y) -> b(f_7(y),g_8(x,y))
r18: f_9(x) -> g_9(x,x)
r19: g_9(s(x),y) -> b(f_8(y),g_9(x,y))
r20: f_10(x) -> g_10(x,x)
r21: g_10(s(x),y) -> b(f_9(y),g_10(x,y))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      g_2#_A(x1,x2) = x1
      s_A(x1) = ((1,0),(1,1)) x1 + (1,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: g_1#(s(x),y) -> g_1#(x,y)

and R consists of:

r1: f_0(x) -> a()
r2: f_1(x) -> g_1(x,x)
r3: g_1(s(x),y) -> b(f_0(y),g_1(x,y))
r4: f_2(x) -> g_2(x,x)
r5: g_2(s(x),y) -> b(f_1(y),g_2(x,y))
r6: f_3(x) -> g_3(x,x)
r7: g_3(s(x),y) -> b(f_2(y),g_3(x,y))
r8: f_4(x) -> g_4(x,x)
r9: g_4(s(x),y) -> b(f_3(y),g_4(x,y))
r10: f_5(x) -> g_5(x,x)
r11: g_5(s(x),y) -> b(f_4(y),g_5(x,y))
r12: f_6(x) -> g_6(x,x)
r13: g_6(s(x),y) -> b(f_5(y),g_6(x,y))
r14: f_7(x) -> g_7(x,x)
r15: g_7(s(x),y) -> b(f_6(y),g_7(x,y))
r16: f_8(x) -> g_8(x,x)
r17: g_8(s(x),y) -> b(f_7(y),g_8(x,y))
r18: f_9(x) -> g_9(x,x)
r19: g_9(s(x),y) -> b(f_8(y),g_9(x,y))
r20: f_10(x) -> g_10(x,x)
r21: g_10(s(x),y) -> b(f_9(y),g_10(x,y))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      g_1#_A(x1,x2) = ((1,0),(1,0)) x1
      s_A(x1) = ((1,0),(1,1)) x1 + (1,1)

The next rules are strictly ordered:

  p1

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