Term Rewriting System R:
[x]
f(x) -> s(x)
f(s(s(x))) -> s(f(f(x)))

Termination of R to be shown.

`   TRS`
`     ↳Dependency Pair Analysis`

R contains the following Dependency Pairs:

F(s(s(x))) -> F(f(x))
F(s(s(x))) -> F(x)

Furthermore, R contains one SCC.

`   TRS`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Modular Removal of Rules`

Dependency Pairs:

F(s(s(x))) -> F(x)
F(s(s(x))) -> F(f(x))

Rules:

f(x) -> s(x)
f(s(s(x))) -> s(f(f(x)))

We have the following set of usable rules:

f(x) -> s(x)
f(s(s(x))) -> s(f(f(x)))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
 POL(s(x1)) =  1 + x1 POL(F(x1)) =  1 + x1 POL(f(x1)) =  1 + x1

We have the following set D of usable symbols: {s, F, f}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

F(s(s(x))) -> F(x)
F(s(s(x))) -> F(f(x))

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

Termination of R successfully shown.
Duration:
0:01 minutes