YES

Problem:
 f(j(x,y),y) -> g(f(x,k(y)))
 f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
 g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
 h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
 i(f(x,h(y))) -> y
 i(h2(s(x),y,h1(x,z))) -> z
 k(h(x)) -> h1(0(),x)
 k(h1(x,y)) -> h1(s(x),y)

Proof:
 DP Processor:
  DPs:
   f#(j(x,y),y) -> k#(y)
   f#(j(x,y),y) -> f#(x,k(y))
   f#(j(x,y),y) -> g#(f(x,k(y)))
   f#(x,h1(y,z)) -> h2#(0(),x,h1(y,z))
   g#(h2(x,y,h1(z,u))) -> h2#(s(x),y,h1(z,u))
   h2#(x,j(y,h1(z,u)),h1(z,u)) -> h2#(s(x),y,h1(s(z),u))
  TRS:
   f(j(x,y),y) -> g(f(x,k(y)))
   f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
   g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
   h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
   i(f(x,h(y))) -> y
   i(h2(s(x),y,h1(x,z))) -> z
   k(h(x)) -> h1(0(),x)
   k(h1(x,y)) -> h1(s(x),y)
  Usable Rule Processor:
   DPs:
    f#(j(x,y),y) -> k#(y)
    f#(j(x,y),y) -> f#(x,k(y))
    f#(j(x,y),y) -> g#(f(x,k(y)))
    f#(x,h1(y,z)) -> h2#(0(),x,h1(y,z))
    g#(h2(x,y,h1(z,u))) -> h2#(s(x),y,h1(z,u))
    h2#(x,j(y,h1(z,u)),h1(z,u)) -> h2#(s(x),y,h1(s(z),u))
   TRS:
    k(h(x)) -> h1(0(),x)
    k(h1(x,y)) -> h1(s(x),y)
    f(j(x,y),y) -> g(f(x,k(y)))
    f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
    g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
    h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
   EDG Processor:
    DPs:
     f#(j(x,y),y) -> k#(y)
     f#(j(x,y),y) -> f#(x,k(y))
     f#(j(x,y),y) -> g#(f(x,k(y)))
     f#(x,h1(y,z)) -> h2#(0(),x,h1(y,z))
     g#(h2(x,y,h1(z,u))) -> h2#(s(x),y,h1(z,u))
     h2#(x,j(y,h1(z,u)),h1(z,u)) -> h2#(s(x),y,h1(s(z),u))
    TRS:
     k(h(x)) -> h1(0(),x)
     k(h1(x,y)) -> h1(s(x),y)
     f(j(x,y),y) -> g(f(x,k(y)))
     f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
     g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
     h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
    graph:
     h2#(x,j(y,h1(z,u)),h1(z,u)) -> h2#(s(x),y,h1(s(z),u)) ->
     h2#(x,j(y,h1(z,u)),h1(z,u)) -> h2#(s(x),y,h1(s(z),u))
     g#(h2(x,y,h1(z,u))) -> h2#(s(x),y,h1(z,u)) ->
     h2#(x,j(y,h1(z,u)),h1(z,u)) -> h2#(s(x),y,h1(s(z),u))
     f#(j(x,y),y) -> g#(f(x,k(y))) ->
     g#(h2(x,y,h1(z,u))) -> h2#(s(x),y,h1(z,u))
     f#(j(x,y),y) -> f#(x,k(y)) -> f#(j(x,y),y) -> k#(y)
     f#(j(x,y),y) -> f#(x,k(y)) -> f#(j(x,y),y) -> f#(x,k(y))
     f#(j(x,y),y) -> f#(x,k(y)) -> f#(j(x,y),y) -> g#(f(x,k(y)))
     f#(j(x,y),y) -> f#(x,k(y)) ->
     f#(x,h1(y,z)) -> h2#(0(),x,h1(y,z))
     f#(x,h1(y,z)) -> h2#(0(),x,h1(y,z)) -> h2#(x,j(y,h1(z,u)),h1(z,u)) -> h2#(s(x),y,h1(s(z),u))
    Restore Modifier:
     DPs:
      f#(j(x,y),y) -> k#(y)
      f#(j(x,y),y) -> f#(x,k(y))
      f#(j(x,y),y) -> g#(f(x,k(y)))
      f#(x,h1(y,z)) -> h2#(0(),x,h1(y,z))
      g#(h2(x,y,h1(z,u))) -> h2#(s(x),y,h1(z,u))
      h2#(x,j(y,h1(z,u)),h1(z,u)) -> h2#(s(x),y,h1(s(z),u))
     TRS:
      f(j(x,y),y) -> g(f(x,k(y)))
      f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
      g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
      h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
      i(f(x,h(y))) -> y
      i(h2(s(x),y,h1(x,z))) -> z
      k(h(x)) -> h1(0(),x)
      k(h1(x,y)) -> h1(s(x),y)
     SCC Processor:
      #sccs: 2
      #rules: 2
      #arcs: 8/36
      DPs:
       f#(j(x,y),y) -> f#(x,k(y))
      TRS:
       f(j(x,y),y) -> g(f(x,k(y)))
       f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
       g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
       h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
       i(f(x,h(y))) -> y
       i(h2(s(x),y,h1(x,z))) -> z
       k(h(x)) -> h1(0(),x)
       k(h1(x,y)) -> h1(s(x),y)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0, x1) = x0,
        
        [i](x0) = x0,
        
        [h](x0) = x0,
        
        [s](x0) = 0,
        
        [h2](x0, x1, x2) = x2,
        
        [0] = 0,
        
        [h1](x0, x1) = x1,
        
        [g](x0) = x0,
        
        [k](x0) = x0,
        
        [f](x0, x1) = x1,
        
        [j](x0, x1) = x0 + x1 + 1
       orientation:
        f#(j(x,y),y) = x + y + 1 >= x = f#(x,k(y))
        
        f(j(x,y),y) = y >= y = g(f(x,k(y)))
        
        f(x,h1(y,z)) = z >= z = h2(0(),x,h1(y,z))
        
        g(h2(x,y,h1(z,u))) = u >= u = h2(s(x),y,h1(z,u))
        
        h2(x,j(y,h1(z,u)),h1(z,u)) = u >= u = h2(s(x),y,h1(s(z),u))
        
        i(f(x,h(y))) = y >= y = y
        
        i(h2(s(x),y,h1(x,z))) = z >= z = z
        
        k(h(x)) = x >= x = h1(0(),x)
        
        k(h1(x,y)) = y >= y = h1(s(x),y)
       problem:
        DPs:
         
        TRS:
         f(j(x,y),y) -> g(f(x,k(y)))
         f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
         g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
         h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
         i(f(x,h(y))) -> y
         i(h2(s(x),y,h1(x,z))) -> z
         k(h(x)) -> h1(0(),x)
         k(h1(x,y)) -> h1(s(x),y)
       Qed
      
      DPs:
       h2#(x,j(y,h1(z,u)),h1(z,u)) -> h2#(s(x),y,h1(s(z),u))
      TRS:
       f(j(x,y),y) -> g(f(x,k(y)))
       f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
       g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
       h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
       i(f(x,h(y))) -> y
       i(h2(s(x),y,h1(x,z))) -> z
       k(h(x)) -> h1(0(),x)
       k(h1(x,y)) -> h1(s(x),y)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [h2#](x0, x1, x2) = x1,
        
        [i](x0) = x0,
        
        [h](x0) = x0,
        
        [s](x0) = 0,
        
        [h2](x0, x1, x2) = x2,
        
        [0] = 0,
        
        [h1](x0, x1) = x1,
        
        [g](x0) = x0,
        
        [k](x0) = x0,
        
        [f](x0, x1) = x1,
        
        [j](x0, x1) = x0 + 1
       orientation:
        h2#(x,j(y,h1(z,u)),h1(z,u)) = y + 1 >= y = h2#(s(x),y,h1(s(z),u))
        
        f(j(x,y),y) = y >= y = g(f(x,k(y)))
        
        f(x,h1(y,z)) = z >= z = h2(0(),x,h1(y,z))
        
        g(h2(x,y,h1(z,u))) = u >= u = h2(s(x),y,h1(z,u))
        
        h2(x,j(y,h1(z,u)),h1(z,u)) = u >= u = h2(s(x),y,h1(s(z),u))
        
        i(f(x,h(y))) = y >= y = y
        
        i(h2(s(x),y,h1(x,z))) = z >= z = z
        
        k(h(x)) = x >= x = h1(0(),x)
        
        k(h1(x,y)) = y >= y = h1(s(x),y)
       problem:
        DPs:
         
        TRS:
         f(j(x,y),y) -> g(f(x,k(y)))
         f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
         g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
         h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
         i(f(x,h(y))) -> y
         i(h2(s(x),y,h1(x,z))) -> z
         k(h(x)) -> h1(0(),x)
         k(h1(x,y)) -> h1(s(x),y)
       Qed