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))

-- 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)

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))

The estimated dependency graph contains the following SCCs:

  {p15}
  {p12}
  {p9}
  {p6}
  {p3}


-- 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))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      g_5#_A(x1,x2) = x1
      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: 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))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      g_4#_A(x1,x2) = x1
      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: 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))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      g_3#_A(x1,x2) = x1
      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: 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))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      g_2#_A(x1,x2) = x1
      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: 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))

The set of usable rules consists of

  (no rules)

Take the reduction pair:

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

The next rules are strictly ordered:

  p1

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