Consider the TRS R consisting of the rewrite rules

1: even(0) -> true
2: even(s(0)) -> false
3: even(s(s(x))) -> even(x)
4: half(0) -> 0
5: half(s(s(x))) -> s(half(x))
6: plus(0,y) -> y
7: plus(s(x),y) -> s(plus(x,y))
8: times(0,y) -> 0
9: times(s(x),y) -> if_times(even(s(x)),s(x),y)
10: if_times(true,s(x),y) -> plus(times(half(s(x)),y),times(half(s(x)),y))
11: if_times(false,s(x),y) -> plus(y,times(x,y))

There are 10 dependency pairs:

12: EVEN(s(s(x))) -> EVEN(x)
13: HALF(s(s(x))) -> HALF(x)
14: PLUS(s(x),y) -> PLUS(x,y)
15: TIMES(s(x),y) -> IF_TIMES(even(s(x)),s(x),y)
16: TIMES(s(x),y) -> EVEN(s(x))
17: IF_TIMES(true,s(x),y) -> PLUS(times(half(s(x)),y),times(half(s(x)),y))
18: IF_TIMES(true,s(x),y) -> TIMES(half(s(x)),y)
19: IF_TIMES(true,s(x),y) -> HALF(s(x))
20: IF_TIMES(false,s(x),y) -> PLUS(y,times(x,y))
21: IF_TIMES(false,s(x),y) -> TIMES(x,y)

The approximated dependency graph contains 4 SCCs:
{12},
{13},
{14}
and {15,18,21}.

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

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

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

- Consider the SCC {15,18,21}.
The usable rules are {1-5}.
By taking the polynomial interpretation
[0] = [false] = [true] = 1,
[half](x) = x,
[even](x) = [s](x) = x + 1,
[TIMES](x,y) = x + y + 1
and [IF_TIMES](x,y,z) = y + z + 1,
the rules in {4,15,18}
are weakly decreasing and
the rules in {1-3,5,21}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {15,18}.
By taking the polynomial interpretation
[0] = [even](x) = [false] = [true] = 0,
[TIMES](x,y) = x,
[s](x) = x + 1,
[half](x) = x - 1
and [IF_TIMES](x,y,z) = y,
we obtain a quasi-model of the usable rules.
Furthermore, dependency pair 15
is weakly decreasing and
dependency pair 18
is strictly decreasing.


Hence the TRS is terminating.