Consider the TRS R consisting of the rewrite rules

1: double(0) -> 0
2: double(s(x)) -> s(s(double(x)))
3: half(0) -> 0
4: half(s(0)) -> 0
5: half(s(s(x))) -> s(half(x))
6: x - 0 -> x
7: s(x) - s(y) -> x - y
8: if(0,y,z) -> y
9: if(s(x),y,z) -> z
10: half(double(x)) -> x

There are 3 dependency pairs:

11: DOUBLE(s(x)) -> DOUBLE(x)
12: HALF(s(s(x))) -> HALF(x)
13: s(x) -# s(y) -> x -# y

The approximated dependency graph contains 3 SCCs:
{13},
{11}
and {12}.

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

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

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

Hence the TRS is terminating.