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)
  TDG 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)
   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#(x,h1(y,z)) -> h2#(0(),x,h1(y,z))
    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#(j(x,y),y) -> f#(x,k(y))
    f#(j(x,y),y) -> f#(x,k(y)) -> f#(j(x,y),y) -> k#(y)
    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))
   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)
    Subterm Criterion Processor:
     simple projection:
      pi(f#) = 0
     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)
    Subterm Criterion Processor:
     simple projection:
      pi(h2#) = 1
     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