Consider the TRS R consisting of the rewrite rules

1: f(j(x,y),y) -> g(f(x,k(y)))
2: f(x,h1(y,z)) -> h2(0,x,h1(y,z))
3: g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
4: h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
5: i(f(x,h(y))) -> y
6: i(h2(s(x),y,h1(x,z))) -> z
7: k(h(x)) -> h1(0,x)
8: k(h1(x,y)) -> h1(s(x),y)

There are 6 dependency pairs:

9: F(j(x,y),y) -> G(f(x,k(y)))
10: F(j(x,y),y) -> F(x,k(y))
11: F(j(x,y),y) -> K(y)
12: F(x,h1(y,z)) -> H2(0,x,h1(y,z))
13: G(h2(x,y,h1(z,u))) -> H2(s(x),y,h1(z,u))
14: H2(x,j(y,h1(z,u)),h1(z,u)) -> H2(s(x),y,h1(s(z),u))

The approximated dependency graph contains 2 SCCs:
{14}
and {10}.

- Consider the SCC {14}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x,
[h1](x,y) = [j](x,y) = x + y + 1
and [H2](x,y,z) = x + y + z + 1,
rule 14
is strictly decreasing.

- Consider the SCC {10}.
The usable rules are {7,8}.
By taking the polynomial interpretation
[0] = 1,
[F](x,y) = [h](x) = [k](x) = [s](x) = x + 1
and [h1](x,y) = [j](x,y) = x + y + 1,
the rules in {7,8}
are weakly decreasing and
rule 10
is strictly decreasing.

Hence the TRS is terminating.