f(a, f(f(a,

R

↳Dependency Pair Analysis

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Semantic Labelling

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

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

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

f(x_{0}, x_{1})= 0 a= 1 F(x_{0}, x_{1})= 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 _{10}(a, f_{01}(f_{10}(a, x), a)) -> F_{10}(a, f_{10}(a, x))**

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

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

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_{10}(a, f_{01}(f_{10}(a,x), a)) -> f_{01}(f_{10}(a, f_{10}(a,x)), a)

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

Polynomial interpretation:

_{ }^{ }POL(f_11(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})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(F_10(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 the lhs is strictly greater than the corresponding rhs:

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

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

Duration:

0:00 minutes