Consider the TRS R consisting of the rewrite rules

1: minus(0,y) -> 0
2: minus(s(x),0) -> s(x)
3: minus(s(x),s(y)) -> minus(x,y)
4: le(0,y) -> true
5: le(s(x),0) -> false
6: le(s(x),s(y)) -> le(x,y)
7: if(true,x,y) -> x
8: if(false,x,y) -> y
9: perfectp(0) -> false
10: perfectp(s(x)) -> f(x,s(0),s(x),s(x))
11: f(0,y,0,u) -> true
12: f(0,y,s(z),u) -> false
13: f(s(x),0,z,u) -> f(x,u,minus(z,s(x)),u)
14: 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 10 dependency pairs:

15: MINUS(s(x),s(y)) -> MINUS(x,y)
16: LE(s(x),s(y)) -> LE(x,y)
17: PERFECTP(s(x)) -> F(x,s(0),s(x),s(x))
18: F(s(x),0,z,u) -> F(x,u,minus(z,s(x)),u)
19: F(s(x),0,z,u) -> MINUS(z,s(x))
20: F(s(x),s(y),z,u) -> IF(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
21: F(s(x),s(y),z,u) -> LE(x,y)
22: F(s(x),s(y),z,u) -> F(s(x),minus(y,x),z,u)
23: F(s(x),s(y),z,u) -> MINUS(y,x)
24: F(s(x),s(y),z,u) -> F(x,u,z,u)

The approximated dependency graph contains 3 SCCs:
{16},
{15}
and {18,22,24}.

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

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

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

- Consider the SCC {18,22}.
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,
the rules in {1,2,22}
are weakly decreasing and
the rules in {3,18}
are strictly decreasing.
There is one new SCC.

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



Hence the TRS is terminating.