f(

R

↳Dependency Pair Analysis

F(x, f(a,y)) -> F(f(y, f(f(a, a), a)),x)

F(x, f(a,y)) -> F(y, f(f(a, a), a))

F(x, f(a,y)) -> F(f(a, a), a)

F(x, f(a,y)) -> F(a, a)

Furthermore,

R

↳DPs

→DP Problem 1

↳Usable Rules (Innermost)

**F( x, f(a, y)) -> F(f(y, f(f(a, a), a)), x)**

f(x, f(a,y)) -> f(f(y, f(f(a, a), a)),x)

innermost

As we are in the innermost case, we can delete all 1 non-usable-rules.

R

↳DPs

→DP Problem 1

↳UsableRules

→DP Problem 2

↳Semantic Labelling

**F( x, f(a, y)) -> F(f(y, f(f(a, a), a)), x)**

none

innermost

Using Semantic Labelling, the DP problem could be transformed. The following model was found:

F(x_{0}, x_{1})= 1 f(x_{0}, x_{1})= 1 + x _{1}a= 0

From the dependency graph we obtain 1 (labeled) SCCs which each result in correspondingDP problem.

R

↳DPs

→DP Problem 1

↳UsableRules

→DP Problem 2

↳SemLab

...

→DP Problem 3

↳Modular Removal of Rules

**F _{00}(x, f_{01}(a, y)) -> F_{00}(f_{11}(y, f_{10}(f_{00}(a, a), a)), x)**

none

innermost

We have the following set of usable rules: none

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

Polynomial interpretation:

_{ }^{ }POL(f_11(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(F_00(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f_00(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f_10(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f_01(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(a)= 0 _{ }^{ }

We have the following set D of usable symbols: {f

The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F_{00}(x, f_{01}(a,y)) -> F_{00}(f_{11}(y, f_{10}(f_{00}(a, a), a)),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.

**Innermost Termination** of *R* successfully shown.

Duration:

0:00 minutes