f(

f(s(s(

TRS

↳Dependency Pair Analysis

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

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

Furthermore,

TRS

↳DPs

→DP Problem 1

↳Modular Removal of Rules

**F(s(s( x))) -> F(x)**

f(x) -> s(x)

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

We have the following set of usable rules:

To remove rules and DPs from this DP problem we used the following monotonic and C

f(x) -> s(x)

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

Polynomial interpretation:

_{ }^{ }POL(s(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(F(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(f(x)_{1})= 1 + x _{1}_{ }^{ }

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