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: 2
  enrichment: match
  automaton:
   final states: {24,23,12,11,3,1,2}
   transitions:
    g1(12) -> 1*
    g1(2) -> 1*
    g1(24) -> 1*
    g1(11) -> 1*
    g1(1) -> 1*
    g1(23) -> 1*
    g1(3) -> 1*
    f1(12,12) -> 1*
    f1(2,12) -> 1*
    f1(23,1) -> 1*
    f1(23,3) -> 1*
    f1(3,1) -> 1*
    f1(12,24) -> 1*
    f1(3,3) -> 1*
    f1(2,24) -> 1*
    f1(23,11) -> 1*
    f1(3,11) -> 1*
    f1(24,2) -> 1*
    f1(23,23) -> 1*
    f1(3,23) -> 1*
    f1(24,12) -> 1*
    f1(24,24) -> 1*
    f1(11,2) -> 1*
    f1(1,2) -> 1*
    f1(11,12) -> 1*
    f1(1,12) -> 1*
    f1(12,1) -> 1*
    f1(12,3) -> 1*
    f1(2,1) -> 1*
    f1(11,24) -> 1*
    f1(2,3) -> 1*
    f1(1,24) -> 1*
    f1(12,11) -> 1*
    f1(2,11) -> 1*
    f1(23,2) -> 1*
    f1(12,23) -> 1*
    f1(3,2) -> 1*
    f1(2,23) -> 1*
    f1(23,12) -> 1*
    f1(3,12) -> 1*
    f1(24,1) -> 1*
    f1(24,3) -> 1*
    f1(23,24) -> 1*
    f1(3,24) -> 1*
    f1(24,11) -> 1*
    f1(24,23) -> 1*
    f1(11,1) -> 1*
    f1(11,3) -> 1*
    f1(1,1) -> 1*
    f1(1,3) -> 1*
    f1(11,11) -> 1*
    f1(1,11) -> 1*
    f1(12,2) -> 1*
    f1(11,23) -> 1*
    f1(2,2) -> 1*
    f1(1,23) -> 1*
    k1(12) -> 1*
    k1(2) -> 1*
    k1(24) -> 1*
    k1(11) -> 1*
    k1(1) -> 1*
    k1(23) -> 1*
    k1(3) -> 1*
    h12(12,12) -> 24*,1,13
    h12(2,12) -> 24*,13,1
    h12(23,1) -> 1,24*
    h12(23,3) -> 1*
    h12(3,1) -> 24*,13,1
    h12(12,24) -> 1,24*
    h12(3,3) -> 1*
    h12(2,24) -> 1,24*
    h12(23,11) -> 1,24*
    h12(3,11) -> 24*,13,1
    h12(24,2) -> 1,24*
    h12(23,23) -> 1,24*
    h12(3,23) -> 1,24*
    h12(24,12) -> 24*,1
    h12(14,12) -> 1*
    h12(24,24) -> 1,24*
    h12(14,24) -> 1*
    h12(11,2) -> 24*,13,1
    h12(1,2) -> 24*,13,1
    h12(11,12) -> 24*,13,1
    h12(1,12) -> 24*,13,1
    h12(12,1) -> 24*,13,1
    h12(2,1) -> 24*,13,1
    h12(12,3) -> 1*
    h12(11,24) -> 1,24*
    h12(2,3) -> 1*
    h12(1,24) -> 1,24*
    h12(12,11) -> 24*,13,1
    h12(2,11) -> 24*,13,1
    h12(23,2) -> 1,24*
    h12(12,23) -> 1,24*
    h12(3,2) -> 1*
    h12(2,23) -> 1,24*
    h12(23,12) -> 24*,1
    h12(3,12) -> 24*,1
    h12(24,1) -> 1,24*
    h12(24,3) -> 1*
    h12(14,1) -> 1*
    h12(23,24) -> 1,24*
    h12(3,24) -> 1,24*
    h12(24,11) -> 1,24*
    h12(14,11) -> 1*
    h12(24,23) -> 1,24*
    h12(14,23) -> 1*
    h12(11,1) -> 24*,13,1
    h12(1,1) -> 24*,13,1
    h12(11,3) -> 1*
    h12(1,3) -> 1*
    h12(11,11) -> 24*,13,1
    h12(1,11) -> 24*,13,1
    h12(12,2) -> 24*,1
    h12(11,23) -> 1,24*
    h12(2,2) -> 1*
    h12(1,23) -> 1,24*
    s2(12) -> 23*,1,14
    s2(2) -> 1*
    s2(24) -> 1,23*
    s2(14) -> 1*
    s2(11) -> 23*,14,1
    s2(1) -> 23*,14,1
    s2(23) -> 1,23*
    s2(3) -> 1*
    h22(24,23,1) -> 1*
    h22(11,2,24) -> 1*
    h22(12,23,23) -> 1*
    h22(3,2,23) -> 1*
    h22(1,2,24) -> 1*
    h22(12,23,2) -> 1*
    h22(3,2,2) -> 1*
    h22(2,23,23) -> 1*
    h22(23,2,11) -> 1*
    h22(3,23,12) -> 1*
    h22(24,12,3) -> 1*
    h22(2,23,2) -> 1*
    h22(12,23,11) -> 1*
    h22(3,2,11) -> 1*
    h22(23,12,23) -> 1*
    h22(24,12,12) -> 1*
    h22(2,23,11) -> 1*
    h22(23,12,2) -> 1*
    h22(11,12,24) -> 1*
    h22(3,12,23) -> 1*
    h22(1,12,24) -> 1*
    h22(3,12,2) -> 1*
    h22(23,12,11) -> 1*
    h22(24,24,3) -> 1*
    h22(24,1,23) -> 1*
    h22(23,1,13) -> 1*
    h22(3,12,11) -> 1*
    h22(24,1,2) -> 1*
    h22(24,3,23) -> 1*
    h22(12,1,24) -> 1*
    h22(24,3,2) -> 1*
    h22(23,24,23) -> 1*
    h22(24,24,12) -> 1*
    h22(11,1,1) -> 1*
    h22(2,1,24) -> 1*
    h22(12,3,24) -> 1*
    h22(11,24,24) -> 1*
    h22(24,1,11) -> 1*
    h22(1,1,1) -> 1*
    h22(11,3,1) -> 1*
    h22(2,3,24) -> 1*
    h22(3,24,23) -> 1*
    h22(1,24,24) -> 1*
    h22(24,3,11) -> 1*
    h22(1,3,1) -> 1*
    h22(3,24,2) -> 1*
    h22(23,24,11) -> 1*
    h22(24,11,23) -> 1*
    h22(23,11,13) -> 1*
    h22(24,11,2) -> 1*
    h22(12,11,24) -> 1*
    h22(3,24,11) -> 1*
    h22(11,11,1) -> 1*
    h22(2,11,24) -> 1*
    h22(24,11,11) -> 1*
    h22(1,11,1) -> 1*
    h22(11,2,3) -> 1*
    h22(23,2,24) -> 1*
    h22(1,2,3) -> 1*
    h22(24,23,23) -> 1*
    h22(23,23,13) -> 1*
    h22(24,23,2) -> 1*
    h22(12,23,24) -> 1*
    h22(11,2,12) -> 1*
    h22(12,2,1) -> 1*
    h22(3,2,24) -> 1*
    h22(11,23,1) -> 1*
    h22(2,23,24) -> 1*
    h22(1,2,12) -> 1*
    h22(2,2,1) -> 1*
    h22(24,23,11) -> 1*
    h22(1,23,1) -> 1*
    h22(11,12,3) -> 1*
    h22(23,12,24) -> 1*
    h22(1,12,3) -> 1*
    h22(14,12,13) -> 1*
    h22(11,12,12) -> 1*
    h22(12,12,1) -> 1*
    h22(3,12,24) -> 1*
    h22(1,12,12) -> 1*
    h22(2,12,1) -> 1*
    h22(12,1,3) -> 1*
    h22(23,24,2) -> 1*
    h22(24,1,24) -> 1*
    h22(2,1,3) -> 1*
    h22(12,3,3) -> 1*
    h22(23,1,1) -> 1*
    h22(11,24,3) -> 1*
    h22(24,3,24) -> 1*
    h22(14,1,24) -> 1*
    h22(2,3,3) -> 1*
    h22(11,1,23) -> 1*
    h22(23,24,24) -> 1*
    h22(12,1,12) -> 1*
    h22(23,3,1) -> 1*
    h22(1,24,3) -> 1*
    h22(11,1,2) -> 1*
    h22(1,1,23) -> 1*
    h22(11,3,23) -> 1*
    h22(12,3,12) -> 1*
    h22(2,1,12) -> 1*
    h22(14,24,13) -> 1*
    h22(3,1,1) -> 1*
    h22(1,1,2) -> 1*
    h22(11,3,2) -> 1*
    h22(11,24,12) -> 1*
    h22(1,3,23) -> 1*
    h22(12,24,1) -> 1*
    h22(3,24,24) -> 1*
    h22(2,3,12) -> 1*
    h22(3,3,1) -> 1*
    h22(1,3,2) -> 1*
    h22(1,24,12) -> 1*
    h22(11,1,11) -> 1*
    h22(12,11,3) -> 1*
    h22(2,24,1) -> 1*
    h22(24,11,24) -> 1*
    h22(11,3,11) -> 1*
    h22(1,1,11) -> 1*
    h22(2,11,3) -> 1*
    h22(23,11,1) -> 1*
    h22(14,11,24) -> 1*
    h22(1,3,11) -> 1*
    h22(11,11,23) -> 1*
    h22(12,11,12) -> 1*
    h22(11,11,2) -> 1*
    h22(1,11,23) -> 1*
    h22(2,11,12) -> 1*
    h22(3,11,1) -> 1*
    h22(1,11,2) -> 1*
    h22(23,2,3) -> 1*
    h22(11,11,11) -> 1*
    h22(1,11,11) -> 1*
    h22(12,23,3) -> 1*
    h22(3,2,3) -> 1*
    h22(24,23,24) -> 1*
    h22(23,2,12) -> 1*
    h22(24,2,1) -> 1*
    h22(2,23,3) -> 1*
    h22(23,23,1) -> 1*
    h22(12,2,23) -> 1*
    h22(14,23,24) -> 1*
    h22(12,2,2) -> 1*
    h22(11,23,23) -> 1*
    h22(12,23,12) -> 1*
    h22(2,2,23) -> 1*
    h22(11,23,2) -> 1*
    h22(3,2,12) -> 1*
    h22(2,2,2) -> 1*
    h22(1,23,23) -> 1*
    h22(2,23,12) -> 1*
    h22(23,12,3) -> 1*
    h22(3,23,1) -> 1*
    h22(1,23,2) -> 1*
    h22(12,2,11) -> 1*
    h22(11,23,11) -> 1*
    h22(2,2,11) -> 1*
    h22(3,12,3) -> 1*
    h22(23,12,12) -> 1*
    h22(1,23,11) -> 1*
    h22(24,12,1) -> 1*
    h22(12,12,23) -> 1*
    h22(12,12,2) -> 1*
    h22(2,12,23) -> 1*
    h22(3,12,12) -> 1*
    h22(24,1,3) -> 1*
    h22(2,12,2) -> 1*
    h22(24,3,3) -> 1*
    h22(12,12,11) -> 1*
    h22(23,24,3) -> 1*
    h22(23,1,23) -> 1*
    h22(24,1,12) -> 1*
    h22(2,12,11) -> 1*
    h22(23,1,2) -> 1*
    h22(23,3,23) -> 1*
    h22(11,1,24) -> 1*
    h22(24,3,12) -> 1*
    h22(23,3,2) -> 1*
    h22(3,24,3) -> 1*
    h22(23,24,12) -> 1*
    h22(24,24,1) -> 1*
    h22(3,1,23) -> 1*
    h22(1,1,24) -> 1*
    h22(11,3,24) -> 1*
    h22(3,1,2) -> 1*
    h22(12,24,23) -> 1*
    h22(23,1,11) -> 1*
    h22(24,11,3) -> 1*
    h22(3,3,23) -> 1*
    h22(1,3,24) -> 1*
    h22(12,24,2) -> 1*
    h22(3,3,2) -> 1*
    h22(2,24,23) -> 1*
    h22(23,3,11) -> 1*
    h22(3,24,12) -> 1*
    h22(2,24,2) -> 1*
    h22(3,1,11) -> 1*
    h22(23,11,23) -> 1*
    h22(24,11,12) -> 1*
    h22(12,24,11) -> 1*
    h22(23,11,2) -> 1*
    h22(3,3,11) -> 1*
    h22(11,11,24) -> 1*
    h22(2,24,11) -> 1*
    h22(3,11,23) -> 1*
    h22(1,11,24) -> 1*
    h22(3,11,2) -> 1*
    h22(23,11,11) -> 1*
    h22(24,23,3) -> 1*
    h22(3,11,11) -> 1*
    h22(24,2,23) -> 1*
    h22(24,2,2) -> 1*
    h22(23,23,23) -> 1*
    h22(24,23,12) -> 1*
    h22(23,23,2) -> 1*
    h22(12,2,24) -> 1*
    h22(11,23,24) -> 1*
    h22(11,2,1) -> 1*
    h22(2,2,24) -> 1*
    h22(3,23,23) -> 1*
    h22(1,23,24) -> 1*
    h22(24,2,11) -> 1*
    h22(1,2,1) -> 1*
    h22(3,23,2) -> 1*
    h22(23,23,11) -> 1*
    h22(24,12,23) -> 1*
    h22(23,12,13) -> 1*
    h22(3,23,11) -> 1*
    h22(24,12,2) -> 1*
    h22(12,12,24) -> 1*
    h22(11,12,1) -> 1*
    h22(2,12,24) -> 1*
    h22(24,12,11) -> 1*
    h22(1,12,1) -> 1*
    h22(11,1,3) -> 1*
    h22(23,1,24) -> 1*
    h22(1,1,3) -> 1*
    h22(11,3,3) -> 1*
    h22(23,3,24) -> 1*
    h22(14,1,13) -> 1*
    h22(1,3,3) -> 1*
    h22(24,24,23) -> 1*
    h22(11,1,12) -> 1*
    h22(23,24,13) -> 1*
    h22(12,1,1) -> 1*
    h22(3,1,24) -> 1*
    h22(12,24,24) -> 1*
    h22(11,3,12) -> 1*
    h22(1,1,12) -> 1*
    h22(2,1,1) -> 1*
    h22(12,3,1) -> 1*
    h22(3,3,24) -> 1*
    h22(11,24,1) -> 1*
    h22(2,24,24) -> 1*
    h22(1,3,12) -> 1*
    h22(2,3,1) -> 1*
    h22(24,24,11) -> 1*
    h22(11,11,3) -> 1*
    h22(1,24,1) -> 1*
    h22(23,11,24) -> 1*
    h22(1,11,3) -> 1*
    h22(14,11,13) -> 1*
    h22(11,11,12) -> 1*
    h22(12,11,1) -> 1*
    h22(3,11,24) -> 1*
    h22(1,11,12) -> 1*
    h22(2,11,1) -> 1*
    h22(12,2,3) -> 1*
    h22(11,23,3) -> 1*
    h22(24,2,24) -> 1*
    h22(2,2,3) -> 1*
    h22(23,23,24) -> 1*
    h22(23,2,1) -> 1*
    h22(1,23,3) -> 1*
    h22(11,2,23) -> 1*
    h22(12,2,12) -> 1*
    h22(14,23,13) -> 1*
    h22(11,2,2) -> 1*
    h22(11,23,12) -> 1*
    h22(1,2,23) -> 1*
    h22(12,23,1) -> 1*
    h22(3,23,24) -> 1*
    h22(2,2,12) -> 1*
    h22(3,2,1) -> 1*
    h22(1,2,2) -> 1*
    h22(1,23,12) -> 1*
    h22(2,23,1) -> 1*
    h22(11,2,11) -> 1*
    h22(12,12,3) -> 1*
    h22(24,12,24) -> 1*
    h22(1,2,11) -> 1*
    h22(2,12,3) -> 1*
    h22(23,12,1) -> 1*
    h22(14,12,24) -> 1*
    h22(11,12,23) -> 1*
    h22(12,12,12) -> 1*
    h22(11,12,2) -> 1*
    h22(1,12,23) -> 1*
    h22(2,12,12) -> 1*
    h22(23,1,3) -> 1*
    h22(3,12,1) -> 1*
    h22(1,12,2) -> 1*
    h22(23,3,3) -> 1*
    h22(24,24,2) -> 1*
    h22(11,12,11) -> 1*
    h22(3,1,3) -> 1*
    h22(23,1,12) -> 1*
    h22(24,1,1) -> 1*
    h22(1,12,11) -> 1*
    h22(12,24,3) -> 1*
    h22(3,3,3) -> 1*
    h22(12,1,23) -> 1*
    h22(24,24,24) -> 1*
    h22(23,3,12) -> 1*
    h22(24,3,1) -> 1*
    h22(2,24,3) -> 1*
    h22(12,1,2) -> 1*
    h22(23,24,1) -> 1*
    h22(2,1,23) -> 1*
    h22(12,3,23) -> 1*
    h22(14,24,24) -> 1*
    h22(3,1,12) -> 1*
    h22(2,1,2) -> 1*
    h22(12,3,2) -> 1*
    h22(11,24,23) -> 1*
    h22(12,24,12) -> 1*
    h22(23,11,3) -> 1*
    h22(2,3,23) -> 1*
    h22(11,24,2) -> 1*
    h22(3,3,12) -> 1*
    h22(2,3,2) -> 1*
    h22(1,24,23) -> 1*
    h22(2,24,12) -> 1*
    h22(12,1,11) -> 1*
    h22(3,24,1) -> 1*
    h22(1,24,2) -> 1*
    h22(2,1,11) -> 1*
    h22(12,3,11) -> 1*
    h22(3,11,3) -> 1*
    h22(23,11,12) -> 1*
    h22(24,11,1) -> 1*
    h22(11,24,11) -> 1*
    h22(2,3,11) -> 1*
    h22(12,11,23) -> 1*
    h22(1,24,11) -> 1*
    h22(12,11,2) -> 1*
    h22(2,11,23) -> 1*
    h22(3,11,12) -> 1*
    h22(2,11,2) -> 1*
    h22(24,2,3) -> 1*
    h22(12,11,11) -> 1*
    h22(23,23,3) -> 1*
    h22(2,11,11) -> 1*
    h22(23,2,23) -> 1*
    h22(24,2,12) -> 1*
    h22(23,2,2) -> 1*
    h22(3,23,3) -> 1*
    h22(23,23,12) -> 1*
    02() -> 23*,1,14
    j0(2,12) -> 1,11*
    j0(23,1) -> 1,11*
    j0(23,3) -> 1,11*
    j0(3,1) -> 11*,1,2
    j0(12,24) -> 1,11*
    j0(3,3) -> 11*,1,2
    j0(2,24) -> 1,11*
    j0(23,11) -> 1,11*
    j0(3,11) -> 1,11*
    j0(24,2) -> 1,11*
    j0(23,23) -> 1,11*
    j0(3,23) -> 1,11*
    j0(24,12) -> 1,11*
    j0(24,24) -> 1,11*
    j0(11,2) -> 1,11*
    j0(1,2) -> 11*,1,2
    j0(11,12) -> 1,11*
    j0(1,12) -> 1,11*
    j0(12,1) -> 1,11*
    j0(12,3) -> 1,11*
    j0(2,1) -> 11*,1,2
    j0(11,24) -> 1,11*
    j0(2,3) -> 11*,1,2
    j0(1,24) -> 1,11*
    j0(12,11) -> 1,11*
    j0(2,11) -> 1,11*
    j0(23,2) -> 1,11*
    j0(12,23) -> 1,11*
    j0(3,2) -> 11*,1,2
    j0(2,23) -> 1,11*
    j0(23,12) -> 1,11*
    j0(3,12) -> 1,11*
    j0(24,1) -> 1,11*
    j0(24,3) -> 1,11*
    j0(23,24) -> 1,11*
    j0(3,24) -> 1,11*
    j0(24,11) -> 1,11*
    j0(24,23) -> 1,11*
    j0(11,1) -> 1,11*
    j0(11,3) -> 1,11*
    j0(1,1) -> 11*,1,2
    j0(1,3) -> 11*,1,2
    j0(11,11) -> 1,11*
    j0(1,11) -> 1,11*
    j0(12,2) -> 1,11*
    j0(11,23) -> 1,11*
    j0(2,2) -> 11*,1,2
    j0(1,23) -> 1,11*
    j0(12,12) -> 1,11*
    i0(12) -> 1*
    i0(2) -> 1*
    i0(24) -> 1*
    i0(11) -> 1*
    i0(1) -> 1*
    i0(23) -> 1*
    i0(3) -> 1*
    h0(12) -> 1,12*
    h0(2) -> 12*,1,3
    h0(24) -> 1,12*
    h0(11) -> 1,12*
    h0(1) -> 12*,1,3
    h0(23) -> 1,12*
    h0(3) -> 12*,1,3
    2 -> 1*
    3 -> 1*
    11 -> 1*
    12 -> 1*
    23 -> 1*
    24 -> 1*
  problem:
   
  Qed