Consider the TRS R consisting of the rewrite rules

1: x - 0 -> x
2: s(x) - s(y) -> x - y
3: x * 0 -> 0
4: x * s(y) -> (x * y) + x
5: if(true,x,y) -> x
6: if(false,x,y) -> y
7: odd(0) -> false
8: odd(s(0)) -> true
9: odd(s(s(x))) -> odd(x)
10: half(0) -> 0
11: half(s(0)) -> 0
12: half(s(s(x))) -> s(half(x))
13: if(true,x,y) -> true
14: if(false,x,y) -> false
15: pow(x,y) -> f(x,y,s(0))
16: f(x,0,z) -> z
17: f(x,s(y),z) -> if(odd(s(y)),f(x,y,x * z),f(x * x,half(s(y)),z))

There are 12 dependency pairs:

18: s(x) -# s(y) -> x -# y
19: x *# s(y) -> x *# y
20: ODD(s(s(x))) -> ODD(x)
21: HALF(s(s(x))) -> HALF(x)
22: POW(x,y) -> F(x,y,s(0))
23: F(x,s(y),z) -> IF(odd(s(y)),f(x,y,x * z),f(x * x,half(s(y)),z))
24: F(x,s(y),z) -> ODD(s(y))
25: F(x,s(y),z) -> F(x,y,x * z)
26: F(x,s(y),z) -> x *# z
27: F(x,s(y),z) -> F(x * x,half(s(y)),z)
28: F(x,s(y),z) -> x *# x
29: F(x,s(y),z) -> HALF(s(y))

The approximated dependency graph contains 5 SCCs:
{19},
{18},
{21},
{20}
and {25,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 {18}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [-#](x,y) = x + y + 1,
rule 18
is strictly decreasing.

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

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

- Consider the SCC {25,27}.
The usable rules are {3,4,10-12}.
By taking the polynomial interpretation
[0] = 1,
[half](x) = x,
[+](x,y) = [s](x) = x + 1,
[*](x,y) = x + y + 1
and [F](x,y,z) = y + 1,
the rules in {4,10,27}
are weakly decreasing and
the rules in {3,11,12,25}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {27}.
By taking the polynomial interpretation
[*](x,y) = [+](x,y) = [0] = 0,
[s](x) = x + 1,
[half](x) = x - 1
and [F](x,y,z) = y,
we obtain a quasi-model of the usable rules.
Furthermore, dependency pair 27
is strictly decreasing.


Hence the TRS is terminating.