f(f(

R

↳Dependency Pair Analysis

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

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

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Semantic Labelling

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

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

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

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

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

R

↳DPs

→DP Problem 1

↳SemLab

→DP Problem 2

↳Modular Removal of Rules

**F _{11}(f_{11}(x, a), a) -> F_{11}(f_{11}(f_{11}(a, f_{11}(a, a)), x), a)**

f_{11}(f_{01}(x, a), a) -> f_{11}(f_{10}(f_{11}(a, f_{11}(a, a)),x), a)

f_{11}(f_{11}(x, a), a) -> f_{11}(f_{11}(f_{11}(a, f_{11}(a, a)),x), a)

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_11(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(a)= 0 _{ }^{ }

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

No Dependency Pairs can be deleted.

2 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

R

↳DPs

→DP Problem 1

↳SemLab

→DP Problem 2

↳MRR

...

→DP Problem 3

↳Unlabel

**F _{11}(f_{11}(x, a), a) -> F_{11}(f_{11}(f_{11}(a, f_{11}(a, a)), x), a)**

none

Removed all semantic labels.

R

↳DPs

→DP Problem 1

↳SemLab

→DP Problem 2

↳MRR

...

→DP Problem 4

↳Instantiation Transformation

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

none

On this DP problem, an Instantiation SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in no new DP problems.

Duration:

0:00 minutes