Consider the TRS R consisting of the rewrite rules

1: f(0) -> 0
2: f(s(0)) -> s(0)
3: f(s(s(x))) -> p(h(g(x)))
4: g(0) -> pair(s(0),s(0))
5: g(s(x)) -> h(g(x))
6: h(x) -> pair(p(x) + q(x),p(x))
7: p(pair(x,y)) -> x
8: q(pair(x,y)) -> y
9: x + 0 -> x
10: x + s(y) -> s(x + y)
11: f(s(s(x))) -> p(g(x)) + q(g(x))
12: g(s(x)) -> pair(p(g(x)) + q(g(x)),p(g(x)))

There are 15 dependency pairs:

13: F(s(s(x))) -> P(h(g(x)))
14: F(s(s(x))) -> H(g(x))
15: G(s(x)) -> H(g(x))
16: H(x) -> p(x) +# q(x)
17: H(x) -> Q(x)
18: H(x) -> P(x)
19: x +# s(y) -> x +# y
20: F(s(s(x))) -> p(g(x)) +# q(g(x))
21: F(s(s(x))) -> P(g(x))
22: F(s(s(x))) -> Q(g(x))
23: F(s(s(x))) -> G(x)
24: G(s(x)) -> p(g(x)) +# q(g(x))
25: G(s(x)) -> Q(g(x))
26: G(s(x)) -> P(g(x))
27: G(s(x)) -> G(x)

The approximated dependency graph contains 2 SCCs:
{19}
and {27}.

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

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

Hence the TRS is terminating.