Consider the TRS R consisting of the rewrite rules

1: sqr(0) -> 0
2: sqr(s(x)) -> sqr(x) + s(double(x))
3: double(0) -> 0
4: double(s(x)) -> s(s(double(x)))
5: x + 0 -> x
6: x + s(y) -> s(x + y)
7: sqr(s(x)) -> s(sqr(x) + double(x))

There are 6 dependency pairs:

8: SQR(s(x)) -> sqr(x) +# s(double(x))
9: DOUBLE(s(x)) -> DOUBLE(x)
10: x +# s(y) -> x +# y
11: SQR(s(x)) -> sqr(x) +# double(x)
12: SQR(s(x)) -> SQR(x)
13: SQR(s(x)) -> DOUBLE(x)

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

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

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

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

Hence the TRS is terminating.