YES
Time: 0.000613
TRS:
 {           g h2(x, y, h1(z, u)) -> h2(s x, y, h1(z, u)),
                   f(x, h1(y, z)) -> h2(0(), x, h1(y, z)),
                    f(j(x, y), y) -> g f(x, k y),
                       k h1(x, y) -> h1(s x, y),
                            k h x -> h1(0(), x),
  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}
 RUF:
  Strict:
   {g h2(x, y, h1(z, u)) -> h2(s x, y, h1(z, u)),
          f(x, h1(y, z)) -> h2(0(), x, h1(y, z)),
              k h1(x, y) -> h1(s x, y)}
  Weak:
   {}
  RUF:
   Strict:
    {}
   Weak:
    {}
   Qed