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:
 Bounds Processor:
  bound: 1
  enrichment: top
  automaton:
   final states: {35,20,19,18,17,11,12,2,10,8,5,1}
   transitions:
    f100() -> 2*
    g0(19) -> 19*
    g0(4) -> 19*,4,8,5,10,1
    f0(2,18) -> 4*
    f0(2,3) -> 4*
    f0(2,17) -> 4*
    f0(2,35) -> 4*
    k0(35) -> 3*
    k0(17) -> 3*
    k0(2) -> 3*
    k0(18) -> 3*
    k0(3) -> 3*
    h20(13,2,11) -> 5*
    h20(36,2,18) -> 19*
    h20(16,2,18) -> 10*
    h20(36,2,6) -> 5*
    h20(36,2,3) -> 19*
    h20(37,2,35) -> 10,19*
    h20(36,2,12) -> 19*
    h20(16,2,12) -> 10*
    h20(7,2,35) -> 19*
    h20(13,2,18) -> 19*
    h20(37,2,17) -> 19*
    h20(7,2,17) -> 19*
    h20(13,2,3) -> 19*,8,5,10,1,4
    h20(9,2,35) -> 10*
    h20(13,2,12) -> 19*,8,5,10,1,4
    h20(37,2,11) -> 20*
    h20(9,2,17) -> 10*
    h20(36,2,35) -> 5,19*
    h20(16,2,35) -> 10,20*
    h20(9,2,11) -> 10*
    h20(37,2,18) -> 10,19*
    h20(36,2,17) -> 5,19*
    h20(37,2,6) -> 5*
    h20(7,2,18) -> 19*
    h20(16,2,17) -> 20*
    h20(7,2,6) -> 5*
    h20(37,2,3) -> 19*
    h20(37,2,12) -> 10,19*
    h20(7,2,3) -> 19*,8,5,10,1,4
    h20(13,2,35) -> 5,19*
    h20(36,2,11) -> 5*
    h20(7,2,12) -> 19*,8,5,10,1,4
    h20(16,2,11) -> 20*,10,8
    h20(13,2,17) -> 5,19*
    h20(9,2,6) -> 20*,10,8
    00() -> 7*
    h10(9,2) -> 17*,3,11
    h10(36,2) -> 3,18*
    h10(16,2) -> 17*,3,11
    h10(13,2) -> 3*
    h10(37,2) -> 35*
    h10(7,2) -> 18*,3,12
    h10(2,2) -> 6*
    s0(37) -> 36*,13,7
    s0(7) -> 13*
    s0(2) -> 9*
    s0(9) -> 16*
    s0(36) -> 36*,13,7
    s0(16) -> 7*
    s0(13) -> 7*
    h11(9,2) -> 11,3,17*
    h11(36,2) -> 18,3,35*
    h11(16,2) -> 11,3,17*
    h11(13,2) -> 3,17*
    h11(37,2) -> 35*
    h11(7,2) -> 17,18,35*,12,3
    s1(37) -> 13,36*,7
    s1(7) -> 36*,13,7
    s1(9) -> 37*,16,7
    s1(36) -> 13,36*,7
    s1(16) -> 7*
    s1(13) -> 7*
    h21(36,2,18) -> 19*
    h21(36,2,3) -> 19*
    h21(37,2,35) -> 10,19*
    h21(7,2,35) -> 4,19*
    h21(37,2,17) -> 19*
    h21(7,2,17) -> 19*,4
    h21(36,2,35) -> 5,19*
    h21(37,2,18) -> 10,19*
    h21(36,2,17) -> 5,19*
    h21(7,2,18) -> 19*
    h21(37,2,3) -> 19*
    h21(7,2,3) -> 1,10,5,8,19*,4
    01() -> 7*
    1 -> 5,8,4
    8 -> 10*
    11 -> 3*
    12 -> 3*
  problem:
   
  Qed