Consider the TRS R consisting of the rewrite rules

1: x - 0 -> x
2: s(x) - s(y) -> x - y
3: 0 <= y -> true
4: s(x) <= 0 -> false
5: s(x) <= s(y) -> x <= y
6: if(true,x,y) -> x
7: if(false,x,y) -> y
8: perfectp(0) -> false
9: perfectp(s(x)) -> f(x,s(0),s(x),s(x))
10: f(0,y,0,u) -> true
11: f(0,y,s(z),u) -> false
12: f(s(x),0,z,u) -> f(x,u,z - s(x),u)
13: f(s(x),s(y),z,u) -> if(x <= y,f(s(x),y - x,z,u),f(x,u,z,u))

There are 10 dependency pairs:

14: s(x) -# s(y) -> x -# y
15: s(x) <=# s(y) -> x <=# y
16: PERFECTP(s(x)) -> F(x,s(0),s(x),s(x))
17: F(s(x),0,z,u) -> F(x,u,z - s(x),u)
18: F(s(x),0,z,u) -> z -# s(x)
19: F(s(x),s(y),z,u) -> IF(x <= y,f(s(x),y - x,z,u),f(x,u,z,u))
20: F(s(x),s(y),z,u) -> x <=# y
21: F(s(x),s(y),z,u) -> F(s(x),y - x,z,u)
22: F(s(x),s(y),z,u) -> y -# x
23: F(s(x),s(y),z,u) -> F(x,u,z,u)

The approximated dependency graph contains 3 SCCs:
{14},
{15}
and {17,21,23}.

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

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

- Consider the SCC {17,21,23}.
The usable rules are {1,2}.
By taking the polynomial interpretation
[0] = 1,
[-](x,y) = [s](x) = x + 1
and [F](x,y,z,w) = x + z + w + 1,
the rules in {17,21}
are weakly decreasing and
the rules in {1,2,23}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {17,21}.
By taking the polynomial interpretation
[0] = 1,
[s](x) = x + 1,
[F](x,y,z,w) = x + w + 1
and [-](x,y) = x + y + 1,
rule 21
is weakly decreasing and
the rules in {1,2,17}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {21}.
By taking the polynomial interpretation
[0] = 1,
[-](x,y) = x,
[s](x) = x + 1
and [F](x,y,z,w) = x + y + z + w + 1,
rule 1
is weakly decreasing and
the rules in {2,21}
are strictly decreasing.



Hence the TRS is terminating.