f(f(a,

R

↳Overlay and local confluence Check

The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.

R

↳OC

→TRS2

↳Dependency Pair Analysis

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

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

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

Furthermore,

R

↳OC

→TRS2

↳DPs

→DP Problem 1

↳Semantic Labelling

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

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

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})= 0 a= 1

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

R

↳OC

→TRS2

↳DPs

→DP Problem 1

↳SemLab

...

→DP Problem 2

↳Modular Removal of Rules

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

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

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

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

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

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})= 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

No Dependency Pairs can be deleted.

4 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

R

↳OC

→TRS2

↳DPs

→DP Problem 1

↳SemLab

...

→DP Problem 3

↳Unlabel

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

none

innermost

Removed all semantic labels.

R

↳OC

→TRS2

↳DPs

→DP Problem 1

↳SemLab

...

→DP Problem 4

↳Remaining Obligation(s)

The following remains to be proven:

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

none

innermost

Duration:

0:02 minutes