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:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        s > g_5#
      
      argument filter:
    
        pi(g_5#) = 1
        pi(s) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        s > g_5#
      
      argument filter:
    
        pi(g_5#) = [1]
        pi(s) = [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:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        s > g_4#
      
      argument filter:
    
        pi(g_4#) = 1
        pi(s) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        s > g_4#
      
      argument filter:
    
        pi(g_4#) = [1]
        pi(s) = [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:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        s > g_3#
      
      argument filter:
    
        pi(g_3#) = 1
        pi(s) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        s > g_3#
      
      argument filter:
    
        pi(g_3#) = [1]
        pi(s) = [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:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        s > g_2#
      
      argument filter:
    
        pi(g_2#) = 1
        pi(s) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        s > g_2#
      
      argument filter:
    
        pi(g_2#) = [1]
        pi(s) = [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:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        s > g_1#
      
      argument filter:
    
        pi(g_1#) = 1
        pi(s) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        s > g_1#
      
      argument filter:
    
        pi(g_1#) = [1]
        pi(s) = [1]
    

The next rules are strictly ordered:

  p1

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