YES(?,O(n^1))
TRS:
 {
                   f(x, h1(y, z)) -> h2(0(), x, h1(y, z)),
                    f(j(x, y), y) -> g f(x, k y),
             g h2(x, y, h1(z, u)) -> h2(s x, y, h1(z, u)),
                            k h x -> h1(0(), x),
                       k h1(x, y) -> h1(s x, y),
  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
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
                     f(x, h1(y, z)) -> h2(0(), x, h1(y, z)),
                      f(j(x, y), y) -> g f(x, k y),
               g h2(x, y, h1(z, u)) -> h2(s x, y, h1(z, u)),
                              k h x -> h1(0(), x),
                         k h1(x, y) -> h1(s x, y),
    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
   }
  Natural interpretation:
   Strict:
    {
                      f(x, h1(y, z)) -> h2(0(), x, h1(y, z)),
                       f(j(x, y), y) -> g f(x, k y),
                g h2(x, y, h1(z, u)) -> h2(s x, y, h1(z, u)),
                               k h x -> h1(0(), x),
                          k h1(x, y) -> h1(s x, y),
     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
    }
   Weak:
    {}
   Interpretation class: stronglylinear
   [i](X0) = + 1*X0 + 7
   [s](X0) = + 1*X0 + 0
   [h1](X1, X0) = + 1*X0 + 1*X1 + 1
   [0] = + 0
   [h2](X2, X1, X0) = + 1*X0 + 1*X1 + 1*X2 + 0
   [j](X1, X0) = + 1*X0 + 1*X1 + 7
   [k](X0) = + 1*X0 + 1
   [h](X0) = + 1*X0 + 6
   [g](X0) = + 1*X0 + 1
   [f](X1, X0) = + 1*X0 + 1*X1 + 2
   
   Qed