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: {12,11,3,1,2}
   transitions:
    f0(2,12) -> 1*
    f0(3,1) -> 1*
    f0(3,3) -> 1*
    f0(3,11) -> 1*
    f0(11,2) -> 1*
    f0(1,2) -> 1*
    f0(11,12) -> 1*
    f0(1,12) -> 1*
    f0(12,1) -> 1*
    f0(2,1) -> 1*
    f0(12,3) -> 1*
    f0(2,3) -> 1*
    f0(12,11) -> 1*
    f0(2,11) -> 1*
    f0(3,2) -> 1*
    f0(3,12) -> 1*
    f0(11,1) -> 1*
    f0(1,1) -> 1*
    f0(11,3) -> 1*
    f0(1,3) -> 1*
    f0(11,11) -> 1*
    f0(1,11) -> 1*
    f0(12,2) -> 1*
    f0(2,2) -> 1*
    f0(12,12) -> 1*
    j0(2,12) -> 1,11*
    j0(3,1) -> 11*,1,2
    j0(3,3) -> 11*,1,2
    j0(3,11) -> 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(2,1) -> 11*,1,2
    j0(12,3) -> 1,11*
    j0(2,3) -> 11*,1,2
    j0(12,11) -> 1,11*
    j0(2,11) -> 1,11*
    j0(3,2) -> 11*,1,2
    j0(3,12) -> 1,11*
    j0(11,1) -> 1,11*
    j0(1,1) -> 11*,1,2
    j0(11,3) -> 1,11*
    j0(1,3) -> 11*,1,2
    j0(11,11) -> 1,11*
    j0(1,11) -> 1,11*
    j0(12,2) -> 1,11*
    j0(2,2) -> 11*,1,2
    j0(12,12) -> 1,11*
    g0(12) -> 1*
    g0(2) -> 1*
    g0(11) -> 1*
    g0(1) -> 1*
    g0(3) -> 1*
    k0(12) -> 1*
    k0(2) -> 1*
    k0(11) -> 1*
    k0(1) -> 1*
    k0(3) -> 1*
    h10(2,12) -> 1*
    h10(3,1) -> 1*
    h10(3,3) -> 1*
    h10(3,11) -> 1*
    h10(11,2) -> 1*
    h10(1,2) -> 1*
    h10(11,12) -> 1*
    h10(1,12) -> 1*
    h10(12,1) -> 1*
    h10(2,1) -> 1*
    h10(12,3) -> 1*
    h10(2,3) -> 1*
    h10(12,11) -> 1*
    h10(2,11) -> 1*
    h10(3,2) -> 1*
    h10(3,12) -> 1*
    h10(11,1) -> 1*
    h10(1,1) -> 1*
    h10(11,3) -> 1*
    h10(1,3) -> 1*
    h10(11,11) -> 1*
    h10(1,11) -> 1*
    h10(12,2) -> 1*
    h10(2,2) -> 1*
    h10(12,12) -> 1*
    h20(3,2,2) -> 1*
    h20(3,2,11) -> 1*
    h20(3,12,2) -> 1*
    h20(3,12,11) -> 1*
    h20(11,1,1) -> 1*
    h20(1,1,1) -> 1*
    h20(11,3,1) -> 1*
    h20(1,3,1) -> 1*
    h20(11,11,1) -> 1*
    h20(1,11,1) -> 1*
    h20(11,2,3) -> 1*
    h20(1,2,3) -> 1*
    h20(11,2,12) -> 1*
    h20(12,2,1) -> 1*
    h20(1,2,12) -> 1*
    h20(2,2,1) -> 1*
    h20(11,12,3) -> 1*
    h20(1,12,3) -> 1*
    h20(11,12,12) -> 1*
    h20(12,12,1) -> 1*
    h20(1,12,12) -> 1*
    h20(2,12,1) -> 1*
    h20(12,1,3) -> 1*
    h20(2,1,3) -> 1*
    h20(12,3,3) -> 1*
    h20(2,3,3) -> 1*
    h20(12,1,12) -> 1*
    h20(11,1,2) -> 1*
    h20(12,3,12) -> 1*
    h20(2,1,12) -> 1*
    h20(3,1,1) -> 1*
    h20(1,1,2) -> 1*
    h20(11,3,2) -> 1*
    h20(2,3,12) -> 1*
    h20(3,3,1) -> 1*
    h20(1,3,2) -> 1*
    h20(11,1,11) -> 1*
    h20(12,11,3) -> 1*
    h20(11,3,11) -> 1*
    h20(1,1,11) -> 1*
    h20(2,11,3) -> 1*
    h20(1,3,11) -> 1*
    h20(12,11,12) -> 1*
    h20(11,11,2) -> 1*
    h20(2,11,12) -> 1*
    h20(3,11,1) -> 1*
    h20(1,11,2) -> 1*
    h20(11,11,11) -> 1*
    h20(1,11,11) -> 1*
    h20(3,2,3) -> 1*
    h20(12,2,2) -> 1*
    h20(3,2,12) -> 1*
    h20(2,2,2) -> 1*
    h20(12,2,11) -> 1*
    h20(2,2,11) -> 1*
    h20(3,12,3) -> 1*
    h20(12,12,2) -> 1*
    h20(3,12,12) -> 1*
    h20(2,12,2) -> 1*
    h20(12,12,11) -> 1*
    h20(2,12,11) -> 1*
    h20(3,1,2) -> 1*
    h20(3,3,2) -> 1*
    h20(3,1,11) -> 1*
    h20(3,3,11) -> 1*
    h20(3,11,2) -> 1*
    h20(3,11,11) -> 1*
    h20(11,2,1) -> 1*
    h20(1,2,1) -> 1*
    h20(11,12,1) -> 1*
    h20(1,12,1) -> 1*
    h20(11,1,3) -> 1*
    h20(1,1,3) -> 1*
    h20(11,3,3) -> 1*
    h20(1,3,3) -> 1*
    h20(11,1,12) -> 1*
    h20(12,1,1) -> 1*
    h20(11,3,12) -> 1*
    h20(1,1,12) -> 1*
    h20(2,1,1) -> 1*
    h20(12,3,1) -> 1*
    h20(1,3,12) -> 1*
    h20(2,3,1) -> 1*
    h20(11,11,3) -> 1*
    h20(1,11,3) -> 1*
    h20(11,11,12) -> 1*
    h20(12,11,1) -> 1*
    h20(1,11,12) -> 1*
    h20(2,11,1) -> 1*
    h20(12,2,3) -> 1*
    h20(2,2,3) -> 1*
    h20(12,2,12) -> 1*
    h20(11,2,2) -> 1*
    h20(2,2,12) -> 1*
    h20(3,2,1) -> 1*
    h20(1,2,2) -> 1*
    h20(11,2,11) -> 1*
    h20(12,12,3) -> 1*
    h20(1,2,11) -> 1*
    h20(2,12,3) -> 1*
    h20(12,12,12) -> 1*
    h20(11,12,2) -> 1*
    h20(2,12,12) -> 1*
    h20(3,12,1) -> 1*
    h20(1,12,2) -> 1*
    h20(11,12,11) -> 1*
    h20(3,1,3) -> 1*
    h20(1,12,11) -> 1*
    h20(3,3,3) -> 1*
    h20(12,1,2) -> 1*
    h20(3,1,12) -> 1*
    h20(2,1,2) -> 1*
    h20(12,3,2) -> 1*
    h20(3,3,12) -> 1*
    h20(2,3,2) -> 1*
    h20(12,1,11) -> 1*
    h20(2,1,11) -> 1*
    h20(12,3,11) -> 1*
    h20(3,11,3) -> 1*
    h20(2,3,11) -> 1*
    h20(12,11,2) -> 1*
    h20(3,11,12) -> 1*
    h20(2,11,2) -> 1*
    h20(12,11,11) -> 1*
    h20(2,11,11) -> 1*
    00() -> 1*
    s0(12) -> 1*
    s0(2) -> 1*
    s0(11) -> 1*
    s0(1) -> 1*
    s0(3) -> 1*
    i0(12) -> 1*
    i0(2) -> 1*
    i0(11) -> 1*
    i0(1) -> 1*
    i0(3) -> 1*
    h0(12) -> 1,12*
    h0(2) -> 12*,1,3
    h0(11) -> 1,12*
    h0(1) -> 12*,1,3
    h0(3) -> 12*,1,3
    h11(12,12) -> 1*
    h11(2,12) -> 1*
    h11(3,1) -> 1*
    h11(3,3) -> 1*
    h11(3,11) -> 1*
    h11(11,2) -> 1*
    h11(1,2) -> 1*
    h11(11,12) -> 1*
    h11(1,12) -> 1*
    h11(12,1) -> 1*
    h11(2,1) -> 1*
    h11(12,3) -> 1*
    h11(2,3) -> 1*
    h11(12,11) -> 1*
    h11(2,11) -> 1*
    h11(3,2) -> 1*
    h11(3,12) -> 1*
    h11(11,1) -> 1*
    h11(1,1) -> 1*
    h11(11,3) -> 1*
    h11(1,3) -> 1*
    h11(11,11) -> 1*
    h11(1,11) -> 1*
    h11(12,2) -> 1*
    h11(2,2) -> 1*
    s1(12) -> 1*
    s1(2) -> 1*
    s1(11) -> 1*
    s1(1) -> 1*
    s1(3) -> 1*
    01() -> 1*
    h21(11,1,1) -> 1*
    h21(1,1,1) -> 1*
    h21(11,3,1) -> 1*
    h21(1,3,1) -> 1*
    h21(11,11,1) -> 1*
    h21(1,11,1) -> 1*
    h21(11,2,12) -> 1*
    h21(12,2,1) -> 1*
    h21(1,2,12) -> 1*
    h21(11,12,12) -> 1*
    h21(12,12,1) -> 1*
    h21(1,12,12) -> 1*
    h21(12,1,12) -> 1*
    h21(12,3,12) -> 1*
    h21(11,1,11) -> 1*
    h21(11,3,11) -> 1*
    h21(1,1,11) -> 1*
    h21(1,3,11) -> 1*
    h21(12,11,12) -> 1*
    h21(11,11,11) -> 1*
    h21(1,11,11) -> 1*
    h21(12,2,11) -> 1*
    h21(12,12,11) -> 1*
    h21(11,2,1) -> 1*
    h21(1,2,1) -> 1*
    h21(11,12,1) -> 1*
    h21(1,12,1) -> 1*
    h21(11,1,12) -> 1*
    h21(12,1,1) -> 1*
    h21(11,3,12) -> 1*
    h21(1,1,12) -> 1*
    h21(12,3,1) -> 1*
    h21(1,3,12) -> 1*
    h21(11,11,12) -> 1*
    h21(12,11,1) -> 1*
    h21(1,11,12) -> 1*
    h21(12,2,12) -> 1*
    h21(11,2,11) -> 1*
    h21(1,2,11) -> 1*
    h21(12,12,12) -> 1*
    h21(11,12,11) -> 1*
    h21(1,12,11) -> 1*
    h21(12,1,11) -> 1*
    h21(12,3,11) -> 1*
    h21(12,11,11) -> 1*
    g1(12) -> 1*
    g1(11) -> 1*
    g1(1) -> 1*
    f1(12,12) -> 1*
    f1(2,12) -> 1*
    f1(3,1) -> 1*
    f1(3,11) -> 1*
    f1(11,12) -> 1*
    f1(1,12) -> 1*
    f1(12,1) -> 1*
    f1(2,1) -> 1*
    f1(12,11) -> 1*
    f1(2,11) -> 1*
    f1(3,12) -> 1*
    f1(11,1) -> 1*
    f1(1,1) -> 1*
    f1(11,11) -> 1*
    f1(1,11) -> 1*
    k1(12) -> 1*
    k1(2) -> 1*
    k1(11) -> 1*
    k1(1) -> 1*
    k1(3) -> 1*
    h12(12,12) -> 1*
    h12(11,2) -> 1*
    h12(11,12) -> 1*
    h12(1,12) -> 1*
    h12(12,1) -> 1*
    h12(12,3) -> 1*
    h12(12,11) -> 1*
    h12(2,11) -> 1*
    h12(3,12) -> 1*
    h12(11,1) -> 1*
    h12(1,1) -> 1*
    h12(11,3) -> 1*
    h12(1,3) -> 1*
    h12(11,11) -> 1*
    h12(1,11) -> 1*
    h12(12,2) -> 1*
    h12(2,2) -> 1*
    s2(12) -> 1*
    s2(11) -> 1*
    s2(1) -> 1*
    h22(11,1,1) -> 1*
    h22(1,1,1) -> 1*
    h22(11,11,1) -> 1*
    h22(1,11,1) -> 1*
    h22(11,12,12) -> 1*
    h22(12,12,1) -> 1*
    h22(1,12,12) -> 1*
    h22(12,1,12) -> 1*
    h22(11,1,11) -> 1*
    h22(1,1,11) -> 1*
    h22(12,11,12) -> 1*
    h22(11,11,11) -> 1*
    h22(1,11,11) -> 1*
    h22(12,12,11) -> 1*
    h22(11,12,1) -> 1*
    h22(1,12,1) -> 1*
    h22(11,1,12) -> 1*
    h22(12,1,1) -> 1*
    h22(1,1,12) -> 1*
    h22(11,11,12) -> 1*
    h22(12,11,1) -> 1*
    h22(1,11,12) -> 1*
    h22(12,12,12) -> 1*
    h22(11,12,11) -> 1*
    h22(1,12,11) -> 1*
    h22(12,1,11) -> 1*
    h22(12,11,11) -> 1*
    02() -> 1*
    2 -> 1*
    3 -> 1*
    11 -> 1*
    12 -> 1*
  problem:
   
  Qed