Consider the TRS R consisting of the rewrite rules

1: perfectp(0) -> false
2: perfectp(s(x)) -> f(x,s(0),s(x),s(x))
3: f(0,y,0,u) -> true
4: f(0,y,s(z),u) -> false
5: f(s(x),0,z,u) -> f(x,u,minus(z,s(x)),u)
6: f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))

There are 4 dependency pairs:

7: PERFECTP(s(x)) -> F(x,s(0),s(x),s(x))
8: F(s(x),0,z,u) -> F(x,u,minus(z,s(x)),u)
9: F(s(x),s(y),z,u) -> F(s(x),minus(y,x),z,u)
10: F(s(x),s(y),z,u) -> F(x,u,z,u)

The approximated dependency graph contains one SCC:
{8,10}.

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

- Consider the SCC {8}.
By taking the polynomial interpretation
[0] = 1,
[minus](x,y) = x,
[s](x) = x + 1
and [F](x,y,z,w) = x + z + w + 1,
rule 8
is strictly decreasing.


Hence the TRS is terminating.