Consider the TRS R consisting of the rewrite rules

1: norm(nil) -> 0
2: norm(g(x,y)) -> s(norm(x))
3: f(x,nil) -> g(nil,x)
4: f(x,g(y,z)) -> g(f(x,y),z)
5: rem(nil,y) -> nil
6: rem(g(x,y),0) -> g(x,y)
7: rem(g(x,y),s(z)) -> rem(x,z)

There are 3 dependency pairs:

8: NORM(g(x,y)) -> NORM(x)
9: F(x,g(y,z)) -> F(x,y)
10: REM(g(x,y),s(z)) -> REM(x,z)

The approximated dependency graph contains 3 SCCs:
{9},
{8}
and {10}.

- Consider the SCC {9}.
There are no usable rules.
By taking the polynomial interpretation
[F](x,y) = [g](x,y) = x + y + 1,
rule 9
is strictly decreasing.

- Consider the SCC {8}.
There are no usable rules.
By taking the polynomial interpretation
[NORM](x) = x + 1
and [g](x,y) = x + y + 1,
rule 8
is strictly decreasing.

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

Hence the TRS is terminating.