f(

f(

R

↳Dependency Pair Analysis

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

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

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

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

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

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Semantic Labelling

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

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

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

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

↳DPs

→DP Problem 1

↳SemLab

→DP Problem 2

↳Modular Removal of Rules

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

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

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

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

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

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

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

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

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

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

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

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

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

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_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.

3 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

↳Modular Removal of Rules

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

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

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

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

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

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

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

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

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

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

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})= 1 + 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.

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

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

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

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

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

The result of this processor delivers one new DP problem.

R

↳DPs

→DP Problem 1

↳SemLab

→DP Problem 2

↳MRR

...

→DP Problem 4

↳Modular Removal of Rules

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

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

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

No Dependency Pairs can be deleted.

1 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 5

↳Unlabel

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

none

Removed all semantic labels.

R

↳DPs

→DP Problem 1

↳SemLab

→DP Problem 2

↳MRR

...

→DP Problem 6

↳Non-Overlappingness Check

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

none

R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.

The transformation is resulting in one subcycle:

R

↳DPs

→DP Problem 1

↳SemLab

→DP Problem 2

↳MRR

...

→DP Problem 7

↳Instantiation Transformation

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

none

innermost

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(y, f(x, f(a,x))) -> F(f(f(a,x), f(x, a)), f(a,y))

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

The transformation is resulting in no new DP problems.

Duration:

0:12 minutes